This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem algfx

Description: If F reaches a fixed point when the countdown function C reaches 0 , F remains fixed after N steps. (Contributed by Paul Chapman, 22-Jun-2011)

Ref Expression
Hypotheses algcvga.1 ⊢ 𝐹 : 𝑆 ⟶ 𝑆
algcvga.2 ⊢ 𝑅 = seq 0 ( ( 𝐹 ∘ 1st ) , ( ℕ0 × { 𝐴 } ) )
algcvga.3 ⊢ 𝐶 : 𝑆 ⟶ ℕ0
algcvga.4 ⊢ ( 𝑧 ∈ 𝑆 → ( ( 𝐶 ‘ ( 𝐹 ‘ 𝑧 ) ) ≠ 0 → ( 𝐶 ‘ ( 𝐹 ‘ 𝑧 ) ) < ( 𝐶 ‘ 𝑧 ) ) )
algcvga.5 ⊢ 𝑁 = ( 𝐶 ‘ 𝐴 )
algfx.6 ⊢ ( 𝑧 ∈ 𝑆 → ( ( 𝐶 ‘ 𝑧 ) = 0 → ( 𝐹 ‘ 𝑧 ) = 𝑧 ) )
Assertion algfx ( 𝐴 ∈ 𝑆 → ( 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝑅 ‘ 𝐾 ) = ( 𝑅 ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 algcvga.1 ⊢ 𝐹 : 𝑆 ⟶ 𝑆
2 algcvga.2 ⊢ 𝑅 = seq 0 ( ( 𝐹 ∘ 1st ) , ( ℕ0 × { 𝐴 } ) )
3 algcvga.3 ⊢ 𝐶 : 𝑆 ⟶ ℕ0
4 algcvga.4 ⊢ ( 𝑧 ∈ 𝑆 → ( ( 𝐶 ‘ ( 𝐹 ‘ 𝑧 ) ) ≠ 0 → ( 𝐶 ‘ ( 𝐹 ‘ 𝑧 ) ) < ( 𝐶 ‘ 𝑧 ) ) )
5 algcvga.5 ⊢ 𝑁 = ( 𝐶 ‘ 𝐴 )
6 algfx.6 ⊢ ( 𝑧 ∈ 𝑆 → ( ( 𝐶 ‘ 𝑧 ) = 0 → ( 𝐹 ‘ 𝑧 ) = 𝑧 ) )
7 3 ffvelcdmi ⊢ ( 𝐴 ∈ 𝑆 → ( 𝐶 ‘ 𝐴 ) ∈ ℕ0 )
8 5 7 eqeltrid ⊢ ( 𝐴 ∈ 𝑆 → 𝑁 ∈ ℕ0 )
9 8 nn0zd ⊢ ( 𝐴 ∈ 𝑆 → 𝑁 ∈ ℤ )
10 uzval ⊢ ( 𝑁 ∈ ℤ → ( ℤ≥ ‘ 𝑁 ) = { 𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧 } )
11 10 eleq2d ⊢ ( 𝑁 ∈ ℤ → ( 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ↔ 𝐾 ∈ { 𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧 } ) )
12 11 pm5.32i ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) ↔ ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ { 𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧 } ) )
13 fveqeq2 ⊢ ( 𝑚 = 𝑁 → ( ( 𝑅 ‘ 𝑚 ) = ( 𝑅 ‘ 𝑁 ) ↔ ( 𝑅 ‘ 𝑁 ) = ( 𝑅 ‘ 𝑁 ) ) )
14 13 imbi2d ⊢ ( 𝑚 = 𝑁 → ( ( 𝐴 ∈ 𝑆 → ( 𝑅 ‘ 𝑚 ) = ( 𝑅 ‘ 𝑁 ) ) ↔ ( 𝐴 ∈ 𝑆 → ( 𝑅 ‘ 𝑁 ) = ( 𝑅 ‘ 𝑁 ) ) ) )
15 fveqeq2 ⊢ ( 𝑚 = 𝑘 → ( ( 𝑅 ‘ 𝑚 ) = ( 𝑅 ‘ 𝑁 ) ↔ ( 𝑅 ‘ 𝑘 ) = ( 𝑅 ‘ 𝑁 ) ) )
16 15 imbi2d ⊢ ( 𝑚 = 𝑘 → ( ( 𝐴 ∈ 𝑆 → ( 𝑅 ‘ 𝑚 ) = ( 𝑅 ‘ 𝑁 ) ) ↔ ( 𝐴 ∈ 𝑆 → ( 𝑅 ‘ 𝑘 ) = ( 𝑅 ‘ 𝑁 ) ) ) )
17 fveqeq2 ⊢ ( 𝑚 = ( 𝑘 + 1 ) → ( ( 𝑅 ‘ 𝑚 ) = ( 𝑅 ‘ 𝑁 ) ↔ ( 𝑅 ‘ ( 𝑘 + 1 ) ) = ( 𝑅 ‘ 𝑁 ) ) )
18 17 imbi2d ⊢ ( 𝑚 = ( 𝑘 + 1 ) → ( ( 𝐴 ∈ 𝑆 → ( 𝑅 ‘ 𝑚 ) = ( 𝑅 ‘ 𝑁 ) ) ↔ ( 𝐴 ∈ 𝑆 → ( 𝑅 ‘ ( 𝑘 + 1 ) ) = ( 𝑅 ‘ 𝑁 ) ) ) )
19 fveqeq2 ⊢ ( 𝑚 = 𝐾 → ( ( 𝑅 ‘ 𝑚 ) = ( 𝑅 ‘ 𝑁 ) ↔ ( 𝑅 ‘ 𝐾 ) = ( 𝑅 ‘ 𝑁 ) ) )
20 19 imbi2d ⊢ ( 𝑚 = 𝐾 → ( ( 𝐴 ∈ 𝑆 → ( 𝑅 ‘ 𝑚 ) = ( 𝑅 ‘ 𝑁 ) ) ↔ ( 𝐴 ∈ 𝑆 → ( 𝑅 ‘ 𝐾 ) = ( 𝑅 ‘ 𝑁 ) ) ) )
21 eqidd ⊢ ( 𝐴 ∈ 𝑆 → ( 𝑅 ‘ 𝑁 ) = ( 𝑅 ‘ 𝑁 ) )
22 21 a1i ⊢ ( 𝑁 ∈ ℤ → ( 𝐴 ∈ 𝑆 → ( 𝑅 ‘ 𝑁 ) = ( 𝑅 ‘ 𝑁 ) ) )
23 10 eleq2d ⊢ ( 𝑁 ∈ ℤ → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ↔ 𝑘 ∈ { 𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧 } ) )
24 23 pm5.32i ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) ↔ ( 𝑁 ∈ ℤ ∧ 𝑘 ∈ { 𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧 } ) )
25 eluznn0 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑘 ∈ ℕ0 )
26 8 25 sylan ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑘 ∈ ℕ0 )
27 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
28 0zd ⊢ ( 𝐴 ∈ 𝑆 → 0 ∈ ℤ )
29 id ⊢ ( 𝐴 ∈ 𝑆 → 𝐴 ∈ 𝑆 )
30 1 a1i ⊢ ( 𝐴 ∈ 𝑆 → 𝐹 : 𝑆 ⟶ 𝑆 )
31 27 2 28 29 30 algrp1 ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑅 ‘ ( 𝑘 + 1 ) ) = ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) )
32 26 31 syldan ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑅 ‘ ( 𝑘 + 1 ) ) = ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) )
33 27 2 28 29 30 algrf ⊢ ( 𝐴 ∈ 𝑆 → 𝑅 : ℕ0 ⟶ 𝑆 )
34 33 ffvelcdmda ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑅 ‘ 𝑘 ) ∈ 𝑆 )
35 26 34 syldan ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑅 ‘ 𝑘 ) ∈ 𝑆 )
36 1 2 3 4 5 algcvga ⊢ ( 𝐴 ∈ 𝑆 → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝐶 ‘ ( 𝑅 ‘ 𝑘 ) ) = 0 ) )
37 36 imp ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐶 ‘ ( 𝑅 ‘ 𝑘 ) ) = 0 )
38 fveqeq2 ⊢ ( 𝑧 = ( 𝑅 ‘ 𝑘 ) → ( ( 𝐶 ‘ 𝑧 ) = 0 ↔ ( 𝐶 ‘ ( 𝑅 ‘ 𝑘 ) ) = 0 ) )
39 fveq2 ⊢ ( 𝑧 = ( 𝑅 ‘ 𝑘 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) )
40 id ⊢ ( 𝑧 = ( 𝑅 ‘ 𝑘 ) → 𝑧 = ( 𝑅 ‘ 𝑘 ) )
41 39 40 eqeq12d ⊢ ( 𝑧 = ( 𝑅 ‘ 𝑘 ) → ( ( 𝐹 ‘ 𝑧 ) = 𝑧 ↔ ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) = ( 𝑅 ‘ 𝑘 ) ) )
42 38 41 imbi12d ⊢ ( 𝑧 = ( 𝑅 ‘ 𝑘 ) → ( ( ( 𝐶 ‘ 𝑧 ) = 0 → ( 𝐹 ‘ 𝑧 ) = 𝑧 ) ↔ ( ( 𝐶 ‘ ( 𝑅 ‘ 𝑘 ) ) = 0 → ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) = ( 𝑅 ‘ 𝑘 ) ) ) )
43 42 6 vtoclga ⊢ ( ( 𝑅 ‘ 𝑘 ) ∈ 𝑆 → ( ( 𝐶 ‘ ( 𝑅 ‘ 𝑘 ) ) = 0 → ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) = ( 𝑅 ‘ 𝑘 ) ) )
44 35 37 43 sylc ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) = ( 𝑅 ‘ 𝑘 ) )
45 32 44 eqtrd ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑅 ‘ ( 𝑘 + 1 ) ) = ( 𝑅 ‘ 𝑘 ) )
46 45 eqeq1d ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑅 ‘ ( 𝑘 + 1 ) ) = ( 𝑅 ‘ 𝑁 ) ↔ ( 𝑅 ‘ 𝑘 ) = ( 𝑅 ‘ 𝑁 ) ) )
47 46 biimprd ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑅 ‘ 𝑘 ) = ( 𝑅 ‘ 𝑁 ) → ( 𝑅 ‘ ( 𝑘 + 1 ) ) = ( 𝑅 ‘ 𝑁 ) ) )
48 47 expcom ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝐴 ∈ 𝑆 → ( ( 𝑅 ‘ 𝑘 ) = ( 𝑅 ‘ 𝑁 ) → ( 𝑅 ‘ ( 𝑘 + 1 ) ) = ( 𝑅 ‘ 𝑁 ) ) ) )
49 48 adantl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐴 ∈ 𝑆 → ( ( 𝑅 ‘ 𝑘 ) = ( 𝑅 ‘ 𝑁 ) → ( 𝑅 ‘ ( 𝑘 + 1 ) ) = ( 𝑅 ‘ 𝑁 ) ) ) )
50 24 49 sylbir ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑘 ∈ { 𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧 } ) → ( 𝐴 ∈ 𝑆 → ( ( 𝑅 ‘ 𝑘 ) = ( 𝑅 ‘ 𝑁 ) → ( 𝑅 ‘ ( 𝑘 + 1 ) ) = ( 𝑅 ‘ 𝑁 ) ) ) )
51 50 a2d ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑘 ∈ { 𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧 } ) → ( ( 𝐴 ∈ 𝑆 → ( 𝑅 ‘ 𝑘 ) = ( 𝑅 ‘ 𝑁 ) ) → ( 𝐴 ∈ 𝑆 → ( 𝑅 ‘ ( 𝑘 + 1 ) ) = ( 𝑅 ‘ 𝑁 ) ) ) )
52 14 16 18 20 22 51 uzind3 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ { 𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧 } ) → ( 𝐴 ∈ 𝑆 → ( 𝑅 ‘ 𝐾 ) = ( 𝑅 ‘ 𝑁 ) ) )
53 12 52 sylbi ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝐴 ∈ 𝑆 → ( 𝑅 ‘ 𝐾 ) = ( 𝑅 ‘ 𝑁 ) ) )
54 53 ex ⊢ ( 𝑁 ∈ ℤ → ( 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝐴 ∈ 𝑆 → ( 𝑅 ‘ 𝐾 ) = ( 𝑅 ‘ 𝑁 ) ) ) )
55 54 com3r ⊢ ( 𝐴 ∈ 𝑆 → ( 𝑁 ∈ ℤ → ( 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝑅 ‘ 𝐾 ) = ( 𝑅 ‘ 𝑁 ) ) ) )
56 9 55 mpd ⊢ ( 𝐴 ∈ 𝑆 → ( 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝑅 ‘ 𝐾 ) = ( 𝑅 ‘ 𝑁 ) ) )