Metamath Proof Explorer

Theorem algcvga

Description: The countdown function C remains 0 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 ⊢ 𝑁 = ( 𝐶 ‘ 𝐴 )
Assertion algcvga ( 𝐴 ∈ 𝑆 → ( 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝐶 ‘ ( 𝑅 ‘ 𝐾 ) ) = 0 ) )

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 3 ffvelrni ⊢ ( 𝐴 ∈ 𝑆 → ( 𝐶 ‘ 𝐴 ) ∈ ℕ0 )
7 5 6 eqeltrid ⊢ ( 𝐴 ∈ 𝑆 → 𝑁 ∈ ℕ0 )
8 nn0z ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
9 eluz1 ⊢ ( 𝑁 ∈ ℤ → ( 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ↔ ( 𝐾 ∈ ℤ ∧ 𝑁 ≤ 𝐾 ) ) )
10 2fveq3 ⊢ ( 𝑚 = 𝑁 → ( 𝐶 ‘ ( 𝑅 ‘ 𝑚 ) ) = ( 𝐶 ‘ ( 𝑅 ‘ 𝑁 ) ) )
11 10 eqeq1d ⊢ ( 𝑚 = 𝑁 → ( ( 𝐶 ‘ ( 𝑅 ‘ 𝑚 ) ) = 0 ↔ ( 𝐶 ‘ ( 𝑅 ‘ 𝑁 ) ) = 0 ) )
12 11 imbi2d ⊢ ( 𝑚 = 𝑁 → ( ( 𝐴 ∈ 𝑆 → ( 𝐶 ‘ ( 𝑅 ‘ 𝑚 ) ) = 0 ) ↔ ( 𝐴 ∈ 𝑆 → ( 𝐶 ‘ ( 𝑅 ‘ 𝑁 ) ) = 0 ) ) )
13 2fveq3 ⊢ ( 𝑚 = 𝑘 → ( 𝐶 ‘ ( 𝑅 ‘ 𝑚 ) ) = ( 𝐶 ‘ ( 𝑅 ‘ 𝑘 ) ) )
14 13 eqeq1d ⊢ ( 𝑚 = 𝑘 → ( ( 𝐶 ‘ ( 𝑅 ‘ 𝑚 ) ) = 0 ↔ ( 𝐶 ‘ ( 𝑅 ‘ 𝑘 ) ) = 0 ) )
15 14 imbi2d ⊢ ( 𝑚 = 𝑘 → ( ( 𝐴 ∈ 𝑆 → ( 𝐶 ‘ ( 𝑅 ‘ 𝑚 ) ) = 0 ) ↔ ( 𝐴 ∈ 𝑆 → ( 𝐶 ‘ ( 𝑅 ‘ 𝑘 ) ) = 0 ) ) )
16 2fveq3 ⊢ ( 𝑚 = ( 𝑘 + 1 ) → ( 𝐶 ‘ ( 𝑅 ‘ 𝑚 ) ) = ( 𝐶 ‘ ( 𝑅 ‘ ( 𝑘 + 1 ) ) ) )
17 16 eqeq1d ⊢ ( 𝑚 = ( 𝑘 + 1 ) → ( ( 𝐶 ‘ ( 𝑅 ‘ 𝑚 ) ) = 0 ↔ ( 𝐶 ‘ ( 𝑅 ‘ ( 𝑘 + 1 ) ) ) = 0 ) )
18 17 imbi2d ⊢ ( 𝑚 = ( 𝑘 + 1 ) → ( ( 𝐴 ∈ 𝑆 → ( 𝐶 ‘ ( 𝑅 ‘ 𝑚 ) ) = 0 ) ↔ ( 𝐴 ∈ 𝑆 → ( 𝐶 ‘ ( 𝑅 ‘ ( 𝑘 + 1 ) ) ) = 0 ) ) )
19 2fveq3 ⊢ ( 𝑚 = 𝐾 → ( 𝐶 ‘ ( 𝑅 ‘ 𝑚 ) ) = ( 𝐶 ‘ ( 𝑅 ‘ 𝐾 ) ) )
20 19 eqeq1d ⊢ ( 𝑚 = 𝐾 → ( ( 𝐶 ‘ ( 𝑅 ‘ 𝑚 ) ) = 0 ↔ ( 𝐶 ‘ ( 𝑅 ‘ 𝐾 ) ) = 0 ) )
21 20 imbi2d ⊢ ( 𝑚 = 𝐾 → ( ( 𝐴 ∈ 𝑆 → ( 𝐶 ‘ ( 𝑅 ‘ 𝑚 ) ) = 0 ) ↔ ( 𝐴 ∈ 𝑆 → ( 𝐶 ‘ ( 𝑅 ‘ 𝐾 ) ) = 0 ) ) )
22 1 2 3 4 5 algcvg ⊢ ( 𝐴 ∈ 𝑆 → ( 𝐶 ‘ ( 𝑅 ‘ 𝑁 ) ) = 0 )
23 22 a1i ⊢ ( 𝑁 ∈ ℤ → ( 𝐴 ∈ 𝑆 → ( 𝐶 ‘ ( 𝑅 ‘ 𝑁 ) ) = 0 ) )
24 nn0ge0 ⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ 𝑁 )
25 24 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℤ ) → 0 ≤ 𝑁 )
26 0re ⊢ 0 ∈ ℝ
27 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
28 zre ⊢ ( 𝑘 ∈ ℤ → 𝑘 ∈ ℝ )
29 letr ⊢ ( ( 0 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( ( 0 ≤ 𝑁 ∧ 𝑁 ≤ 𝑘 ) → 0 ≤ 𝑘 ) )
30 26 27 28 29 mp3an3an ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℤ ) → ( ( 0 ≤ 𝑁 ∧ 𝑁 ≤ 𝑘 ) → 0 ≤ 𝑘 ) )
31 25 30 mpand ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℤ ) → ( 𝑁 ≤ 𝑘 → 0 ≤ 𝑘 ) )
32 elnn0z ⊢ ( 𝑘 ∈ ℕ0 ↔ ( 𝑘 ∈ ℤ ∧ 0 ≤ 𝑘 ) )
33 32 simplbi2 ⊢ ( 𝑘 ∈ ℤ → ( 0 ≤ 𝑘 → 𝑘 ∈ ℕ0 ) )
34 33 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℤ ) → ( 0 ≤ 𝑘 → 𝑘 ∈ ℕ0 ) )
35 31 34 syld ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℤ ) → ( 𝑁 ≤ 𝑘 → 𝑘 ∈ ℕ0 ) )
36 7 35 sylan ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℤ ) → ( 𝑁 ≤ 𝑘 → 𝑘 ∈ ℕ0 ) )
37 36 impr ⊢ ( ( 𝐴 ∈ 𝑆 ∧ ( 𝑘 ∈ ℤ ∧ 𝑁 ≤ 𝑘 ) ) → 𝑘 ∈ ℕ0 )
38 37 expcom ⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑁 ≤ 𝑘 ) → ( 𝐴 ∈ 𝑆 → 𝑘 ∈ ℕ0 ) )
39 38 3adant1 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑁 ≤ 𝑘 ) → ( 𝐴 ∈ 𝑆 → 𝑘 ∈ ℕ0 ) )
40 39 ancld ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑁 ≤ 𝑘 ) → ( 𝐴 ∈ 𝑆 → ( 𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0 ) ) )
41 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
42 0zd ⊢ ( 𝐴 ∈ 𝑆 → 0 ∈ ℤ )
43 id ⊢ ( 𝐴 ∈ 𝑆 → 𝐴 ∈ 𝑆 )
44 1 a1i ⊢ ( 𝐴 ∈ 𝑆 → 𝐹 : 𝑆 ⟶ 𝑆 )
45 41 2 42 43 44 algrf ⊢ ( 𝐴 ∈ 𝑆 → 𝑅 : ℕ0 ⟶ 𝑆 )
46 45 ffvelrnda ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑅 ‘ 𝑘 ) ∈ 𝑆 )
47 2fveq3 ⊢ ( 𝑧 = ( 𝑅 ‘ 𝑘 ) → ( 𝐶 ‘ ( 𝐹 ‘ 𝑧 ) ) = ( 𝐶 ‘ ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) ) )
48 47 neeq1d ⊢ ( 𝑧 = ( 𝑅 ‘ 𝑘 ) → ( ( 𝐶 ‘ ( 𝐹 ‘ 𝑧 ) ) ≠ 0 ↔ ( 𝐶 ‘ ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) ) ≠ 0 ) )
49 fveq2 ⊢ ( 𝑧 = ( 𝑅 ‘ 𝑘 ) → ( 𝐶 ‘ 𝑧 ) = ( 𝐶 ‘ ( 𝑅 ‘ 𝑘 ) ) )
50 47 49 breq12d ⊢ ( 𝑧 = ( 𝑅 ‘ 𝑘 ) → ( ( 𝐶 ‘ ( 𝐹 ‘ 𝑧 ) ) < ( 𝐶 ‘ 𝑧 ) ↔ ( 𝐶 ‘ ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝐶 ‘ ( 𝑅 ‘ 𝑘 ) ) ) )
51 48 50 imbi12d ⊢ ( 𝑧 = ( 𝑅 ‘ 𝑘 ) → ( ( ( 𝐶 ‘ ( 𝐹 ‘ 𝑧 ) ) ≠ 0 → ( 𝐶 ‘ ( 𝐹 ‘ 𝑧 ) ) < ( 𝐶 ‘ 𝑧 ) ) ↔ ( ( 𝐶 ‘ ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) ) ≠ 0 → ( 𝐶 ‘ ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝐶 ‘ ( 𝑅 ‘ 𝑘 ) ) ) ) )
52 51 4 vtoclga ⊢ ( ( 𝑅 ‘ 𝑘 ) ∈ 𝑆 → ( ( 𝐶 ‘ ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) ) ≠ 0 → ( 𝐶 ‘ ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝐶 ‘ ( 𝑅 ‘ 𝑘 ) ) ) )
53 1 3 algcvgb ⊢ ( ( 𝑅 ‘ 𝑘 ) ∈ 𝑆 → ( ( ( 𝐶 ‘ ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) ) ≠ 0 → ( 𝐶 ‘ ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝐶 ‘ ( 𝑅 ‘ 𝑘 ) ) ) ↔ ( ( ( 𝐶 ‘ ( 𝑅 ‘ 𝑘 ) ) ≠ 0 → ( 𝐶 ‘ ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝐶 ‘ ( 𝑅 ‘ 𝑘 ) ) ) ∧ ( ( 𝐶 ‘ ( 𝑅 ‘ 𝑘 ) ) = 0 → ( 𝐶 ‘ ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) ) = 0 ) ) ) )
54 simpr ⊢ ( ( ( ( 𝐶 ‘ ( 𝑅 ‘ 𝑘 ) ) ≠ 0 → ( 𝐶 ‘ ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝐶 ‘ ( 𝑅 ‘ 𝑘 ) ) ) ∧ ( ( 𝐶 ‘ ( 𝑅 ‘ 𝑘 ) ) = 0 → ( 𝐶 ‘ ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) ) = 0 ) ) → ( ( 𝐶 ‘ ( 𝑅 ‘ 𝑘 ) ) = 0 → ( 𝐶 ‘ ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) ) = 0 ) )
55 53 54 syl6bi ⊢ ( ( 𝑅 ‘ 𝑘 ) ∈ 𝑆 → ( ( ( 𝐶 ‘ ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) ) ≠ 0 → ( 𝐶 ‘ ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) ) < ( 𝐶 ‘ ( 𝑅 ‘ 𝑘 ) ) ) → ( ( 𝐶 ‘ ( 𝑅 ‘ 𝑘 ) ) = 0 → ( 𝐶 ‘ ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) ) = 0 ) ) )
56 52 55 mpd ⊢ ( ( 𝑅 ‘ 𝑘 ) ∈ 𝑆 → ( ( 𝐶 ‘ ( 𝑅 ‘ 𝑘 ) ) = 0 → ( 𝐶 ‘ ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) ) = 0 ) )
57 46 56 syl ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐶 ‘ ( 𝑅 ‘ 𝑘 ) ) = 0 → ( 𝐶 ‘ ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) ) = 0 ) )
58 41 2 42 43 44 algrp1 ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑅 ‘ ( 𝑘 + 1 ) ) = ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) )
59 58 fveqeq2d ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐶 ‘ ( 𝑅 ‘ ( 𝑘 + 1 ) ) ) = 0 ↔ ( 𝐶 ‘ ( 𝐹 ‘ ( 𝑅 ‘ 𝑘 ) ) ) = 0 ) )
60 57 59 sylibrd ⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐶 ‘ ( 𝑅 ‘ 𝑘 ) ) = 0 → ( 𝐶 ‘ ( 𝑅 ‘ ( 𝑘 + 1 ) ) ) = 0 ) )
61 40 60 syl6 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑁 ≤ 𝑘 ) → ( 𝐴 ∈ 𝑆 → ( ( 𝐶 ‘ ( 𝑅 ‘ 𝑘 ) ) = 0 → ( 𝐶 ‘ ( 𝑅 ‘ ( 𝑘 + 1 ) ) ) = 0 ) ) )
62 61 a2d ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑁 ≤ 𝑘 ) → ( ( 𝐴 ∈ 𝑆 → ( 𝐶 ‘ ( 𝑅 ‘ 𝑘 ) ) = 0 ) → ( 𝐴 ∈ 𝑆 → ( 𝐶 ‘ ( 𝑅 ‘ ( 𝑘 + 1 ) ) ) = 0 ) ) )
63 12 15 18 21 23 62 uzind ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ≤ 𝐾 ) → ( 𝐴 ∈ 𝑆 → ( 𝐶 ‘ ( 𝑅 ‘ 𝐾 ) ) = 0 ) )
64 63 3expib ⊢ ( 𝑁 ∈ ℤ → ( ( 𝐾 ∈ ℤ ∧ 𝑁 ≤ 𝐾 ) → ( 𝐴 ∈ 𝑆 → ( 𝐶 ‘ ( 𝑅 ‘ 𝐾 ) ) = 0 ) ) )
65 9 64 sylbid ⊢ ( 𝑁 ∈ ℤ → ( 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝐴 ∈ 𝑆 → ( 𝐶 ‘ ( 𝑅 ‘ 𝐾 ) ) = 0 ) ) )
66 8 65 syl ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝐴 ∈ 𝑆 → ( 𝐶 ‘ ( 𝑅 ‘ 𝐾 ) ) = 0 ) ) )
67 66 com3r ⊢ ( 𝐴 ∈ 𝑆 → ( 𝑁 ∈ ℕ0 → ( 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝐶 ‘ ( 𝑅 ‘ 𝐾 ) ) = 0 ) ) )
68 7 67 mpd ⊢ ( 𝐴 ∈ 𝑆 → ( 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝐶 ‘ ( 𝑅 ‘ 𝐾 ) ) = 0 ) )