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	ffvelrni	⊢ ( 𝐴 ∈ 𝑆 → ( 𝐶 ‘ 𝐴 ) ∈ ℕ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	ffvelrnda	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝑘 ∈ ℕ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	⊢ ( 𝐴 ∈ 𝑆 → ( 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝑅 ‘ 𝐾 ) = ( 𝑅 ‘ 𝑁 ) ) )