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	$⊢ F : S ⟶ S$
	algcvga.2	$⊢ R = seq 0 ((F \circ 1^{st}), (ℕ_{0} \times \{A\}))$
	algcvga.3	$⊢ C : S ⟶ ℕ_{0}$
	algcvga.4	$⊢ z \in S \to (C (F (z)) \neq 0 \to C (F (z)) < C (z))$
	algcvga.5	$⊢ N = C (A)$
	algfx.6	$⊢ z \in S \to (C (z) = 0 \to F (z) = z)$
Assertion	algfx	$⊢ A \in S \to (K \in ℤ_{\geq N} \to R (K) = R (N))$

Proof

Step	Hyp	Ref	Expression
1		algcvga.1	$⊢ F : S ⟶ S$
2		algcvga.2	$⊢ R = seq 0 ((F \circ 1^{st}), (ℕ_{0} \times \{A\}))$
3		algcvga.3	$⊢ C : S ⟶ ℕ_{0}$
4		algcvga.4	$⊢ z \in S \to (C (F (z)) \neq 0 \to C (F (z)) < C (z))$
5		algcvga.5	$⊢ N = C (A)$
6		algfx.6	$⊢ z \in S \to (C (z) = 0 \to F (z) = z)$
7	3	ffvelcdmi	$⊢ A \in S \to C (A) \in ℕ_{0}$
8	5 7	eqeltrid	$⊢ A \in S \to N \in ℕ_{0}$
9	8	nn0zd	$⊢ A \in S \to N \in ℤ$
10		uzval	$⊢ N \in ℤ \to ℤ_{\geq N} = \{z \in ℤ \| N \leq z\}$
11	10	eleq2d	$⊢ N \in ℤ \to (K \in ℤ_{\geq N} \leftrightarrow K \in \{z \in ℤ \| N \leq z\})$
12	11	pm5.32i	$⊢ (N \in ℤ \land K \in ℤ_{\geq N}) \leftrightarrow (N \in ℤ \land K \in \{z \in ℤ \| N \leq z\})$
13		fveqeq2	$⊢ m = N \to (R (m) = R (N) \leftrightarrow R (N) = R (N))$
14	13	imbi2d	$⊢ m = N \to ((A \in S \to R (m) = R (N)) \leftrightarrow (A \in S \to R (N) = R (N)))$
15		fveqeq2	$⊢ m = k \to (R (m) = R (N) \leftrightarrow R (k) = R (N))$
16	15	imbi2d	$⊢ m = k \to ((A \in S \to R (m) = R (N)) \leftrightarrow (A \in S \to R (k) = R (N)))$
17		fveqeq2	$⊢ m = k + 1 \to (R (m) = R (N) \leftrightarrow R (k + 1) = R (N))$
18	17	imbi2d	$⊢ m = k + 1 \to ((A \in S \to R (m) = R (N)) \leftrightarrow (A \in S \to R (k + 1) = R (N)))$
19		fveqeq2	$⊢ m = K \to (R (m) = R (N) \leftrightarrow R (K) = R (N))$
20	19	imbi2d	$⊢ m = K \to ((A \in S \to R (m) = R (N)) \leftrightarrow (A \in S \to R (K) = R (N)))$
21		eqidd	$⊢ A \in S \to R (N) = R (N)$
22	21	a1i	$⊢ N \in ℤ \to (A \in S \to R (N) = R (N))$
23	10	eleq2d	$⊢ N \in ℤ \to (k \in ℤ_{\geq N} \leftrightarrow k \in \{z \in ℤ \| N \leq z\})$
24	23	pm5.32i	$⊢ (N \in ℤ \land k \in ℤ_{\geq N}) \leftrightarrow (N \in ℤ \land k \in \{z \in ℤ \| N \leq z\})$
25		eluznn0	$⊢ (N \in ℕ_{0} \land k \in ℤ_{\geq N}) \to k \in ℕ_{0}$
26	8 25	sylan	$⊢ (A \in S \land k \in ℤ_{\geq N}) \to k \in ℕ_{0}$
27		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
28		0zd	$⊢ A \in S \to 0 \in ℤ$
29		id	$⊢ A \in S \to A \in S$
30	1	a1i	$⊢ A \in S \to F : S ⟶ S$
31	27 2 28 29 30	algrp1	$⊢ (A \in S \land k \in ℕ_{0}) \to R (k + 1) = F (R (k))$
32	26 31	syldan	$⊢ (A \in S \land k \in ℤ_{\geq N}) \to R (k + 1) = F (R (k))$
33	27 2 28 29 30	algrf	$⊢ A \in S \to R : ℕ_{0} ⟶ S$
34	33	ffvelcdmda	$⊢ (A \in S \land k \in ℕ_{0}) \to R (k) \in S$
35	26 34	syldan	$⊢ (A \in S \land k \in ℤ_{\geq N}) \to R (k) \in S$
36	1 2 3 4 5	algcvga	$⊢ A \in S \to (k \in ℤ_{\geq N} \to C (R (k)) = 0)$
37	36	imp	$⊢ (A \in S \land k \in ℤ_{\geq N}) \to C (R (k)) = 0$
38		fveqeq2	$⊢ z = R (k) \to (C (z) = 0 \leftrightarrow C (R (k)) = 0)$
39		fveq2	$⊢ z = R (k) \to F (z) = F (R (k))$
40		id	$⊢ z = R (k) \to z = R (k)$
41	39 40	eqeq12d	$⊢ z = R (k) \to (F (z) = z \leftrightarrow F (R (k)) = R (k))$
42	38 41	imbi12d	$⊢ z = R (k) \to ((C (z) = 0 \to F (z) = z) \leftrightarrow (C (R (k)) = 0 \to F (R (k)) = R (k)))$
43	42 6	vtoclga	$⊢ R (k) \in S \to (C (R (k)) = 0 \to F (R (k)) = R (k))$
44	35 37 43	sylc	$⊢ (A \in S \land k \in ℤ_{\geq N}) \to F (R (k)) = R (k)$
45	32 44	eqtrd	$⊢ (A \in S \land k \in ℤ_{\geq N}) \to R (k + 1) = R (k)$
46	45	eqeq1d	$⊢ (A \in S \land k \in ℤ_{\geq N}) \to (R (k + 1) = R (N) \leftrightarrow R (k) = R (N))$
47	46	biimprd	$⊢ (A \in S \land k \in ℤ_{\geq N}) \to (R (k) = R (N) \to R (k + 1) = R (N))$
48	47	expcom	$⊢ k \in ℤ_{\geq N} \to (A \in S \to (R (k) = R (N) \to R (k + 1) = R (N)))$
49	48	adantl	$⊢ (N \in ℤ \land k \in ℤ_{\geq N}) \to (A \in S \to (R (k) = R (N) \to R (k + 1) = R (N)))$
50	24 49	sylbir	$⊢ (N \in ℤ \land k \in \{z \in ℤ \| N \leq z\}) \to (A \in S \to (R (k) = R (N) \to R (k + 1) = R (N)))$
51	50	a2d	$⊢ (N \in ℤ \land k \in \{z \in ℤ \| N \leq z\}) \to ((A \in S \to R (k) = R (N)) \to (A \in S \to R (k + 1) = R (N)))$
52	14 16 18 20 22 51	uzind3	$⊢ (N \in ℤ \land K \in \{z \in ℤ \| N \leq z\}) \to (A \in S \to R (K) = R (N))$
53	12 52	sylbi	$⊢ (N \in ℤ \land K \in ℤ_{\geq N}) \to (A \in S \to R (K) = R (N))$
54	53	ex	$⊢ N \in ℤ \to (K \in ℤ_{\geq N} \to (A \in S \to R (K) = R (N)))$
55	54	com3r	$⊢ A \in S \to (N \in ℤ \to (K \in ℤ_{\geq N} \to R (K) = R (N)))$
56	9 55	mpd	$⊢ A \in S \to (K \in ℤ_{\geq N} \to R (K) = R (N))$

Metamath Proof Explorer

Theorem algfx

Proof