algcvga

Description: The countdown function C remains 0 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)$
Assertion	algcvga	$⊢ A \in S \to (K \in ℤ_{\geq N} \to C (R (K)) = 0)$

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	3	ffvelrni	$⊢ A \in S \to C (A) \in ℕ_{0}$
7	5 6	eqeltrid	$⊢ A \in S \to N \in ℕ_{0}$
8		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
9		eluz1	$⊢ N \in ℤ \to (K \in ℤ_{\geq N} \leftrightarrow (K \in ℤ \land N \leq K))$
10		2fveq3	$⊢ m = N \to C (R (m)) = C (R (N))$
11	10	eqeq1d	$⊢ m = N \to (C (R (m)) = 0 \leftrightarrow C (R (N)) = 0)$
12	11	imbi2d	$⊢ m = N \to ((A \in S \to C (R (m)) = 0) \leftrightarrow (A \in S \to C (R (N)) = 0))$
13		2fveq3	$⊢ m = k \to C (R (m)) = C (R (k))$
14	13	eqeq1d	$⊢ m = k \to (C (R (m)) = 0 \leftrightarrow C (R (k)) = 0)$
15	14	imbi2d	$⊢ m = k \to ((A \in S \to C (R (m)) = 0) \leftrightarrow (A \in S \to C (R (k)) = 0))$
16		2fveq3	$⊢ m = k + 1 \to C (R (m)) = C (R (k + 1))$
17	16	eqeq1d	$⊢ m = k + 1 \to (C (R (m)) = 0 \leftrightarrow C (R (k + 1)) = 0)$
18	17	imbi2d	$⊢ m = k + 1 \to ((A \in S \to C (R (m)) = 0) \leftrightarrow (A \in S \to C (R (k + 1)) = 0))$
19		2fveq3	$⊢ m = K \to C (R (m)) = C (R (K))$
20	19	eqeq1d	$⊢ m = K \to (C (R (m)) = 0 \leftrightarrow C (R (K)) = 0)$
21	20	imbi2d	$⊢ m = K \to ((A \in S \to C (R (m)) = 0) \leftrightarrow (A \in S \to C (R (K)) = 0))$
22	1 2 3 4 5	algcvg	$⊢ A \in S \to C (R (N)) = 0$
23	22	a1i	$⊢ N \in ℤ \to (A \in S \to C (R (N)) = 0)$
24		nn0ge0	$⊢ N \in ℕ_{0} \to 0 \leq N$
25	24	adantr	$⊢ (N \in ℕ_{0} \land k \in ℤ) \to 0 \leq N$
26		0re	$⊢ 0 \in ℝ$
27		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
28		zre	$⊢ k \in ℤ \to k \in ℝ$
29		letr	$⊢ (0 \in ℝ \land N \in ℝ \land k \in ℝ) \to ((0 \leq N \land N \leq k) \to 0 \leq k)$
30	26 27 28 29	mp3an3an	$⊢ (N \in ℕ_{0} \land k \in ℤ) \to ((0 \leq N \land N \leq k) \to 0 \leq k)$
31	25 30	mpand	$⊢ (N \in ℕ_{0} \land k \in ℤ) \to (N \leq k \to 0 \leq k)$
32		elnn0z	$⊢ k \in ℕ_{0} \leftrightarrow (k \in ℤ \land 0 \leq k)$
33	32	simplbi2	$⊢ k \in ℤ \to (0 \leq k \to k \in ℕ_{0})$
34	33	adantl	$⊢ (N \in ℕ_{0} \land k \in ℤ) \to (0 \leq k \to k \in ℕ_{0})$
35	31 34	syld	$⊢ (N \in ℕ_{0} \land k \in ℤ) \to (N \leq k \to k \in ℕ_{0})$
36	7 35	sylan	$⊢ (A \in S \land k \in ℤ) \to (N \leq k \to k \in ℕ_{0})$
37	36	impr	$⊢ (A \in S \land (k \in ℤ \land N \leq k)) \to k \in ℕ_{0}$
38	37	expcom	$⊢ (k \in ℤ \land N \leq k) \to (A \in S \to k \in ℕ_{0})$
39	38	3adant1	$⊢ (N \in ℤ \land k \in ℤ \land N \leq k) \to (A \in S \to k \in ℕ_{0})$
40	39	ancld	$⊢ (N \in ℤ \land k \in ℤ \land N \leq k) \to (A \in S \to (A \in S \land k \in ℕ_{0}))$
41		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
42		0zd	$⊢ A \in S \to 0 \in ℤ$
43		id	$⊢ A \in S \to A \in S$
44	1	a1i	$⊢ A \in S \to F : S ⟶ S$
45	41 2 42 43 44	algrf	$⊢ A \in S \to R : ℕ_{0} ⟶ S$
46	45	ffvelrnda	$⊢ (A \in S \land k \in ℕ_{0}) \to R (k) \in S$
47		2fveq3	$⊢ z = R (k) \to C (F (z)) = C (F (R (k)))$
48	47	neeq1d	$⊢ z = R (k) \to (C (F (z)) \neq 0 \leftrightarrow C (F (R (k))) \neq 0)$
49		fveq2	$⊢ z = R (k) \to C (z) = C (R (k))$
50	47 49	breq12d	$⊢ z = R (k) \to (C (F (z)) < C (z) \leftrightarrow C (F (R (k))) < C (R (k)))$
51	48 50	imbi12d	$⊢ z = R (k) \to ((C (F (z)) \neq 0 \to C (F (z)) < C (z)) \leftrightarrow (C (F (R (k))) \neq 0 \to C (F (R (k))) < C (R (k))))$
52	51 4	vtoclga	$⊢ R (k) \in S \to (C (F (R (k))) \neq 0 \to C (F (R (k))) < C (R (k)))$
53	1 3	algcvgb	$⊢ R (k) \in S \to ((C (F (R (k))) \neq 0 \to C (F (R (k))) < C (R (k))) \leftrightarrow ((C (R (k)) \neq 0 \to C (F (R (k))) < C (R (k))) \land (C (R (k)) = 0 \to C (F (R (k))) = 0)))$
54		simpr	$⊢ ((C (R (k)) \neq 0 \to C (F (R (k))) < C (R (k))) \land (C (R (k)) = 0 \to C (F (R (k))) = 0)) \to (C (R (k)) = 0 \to C (F (R (k))) = 0)$
55	53 54	syl6bi	$⊢ R (k) \in S \to ((C (F (R (k))) \neq 0 \to C (F (R (k))) < C (R (k))) \to (C (R (k)) = 0 \to C (F (R (k))) = 0))$
56	52 55	mpd	$⊢ R (k) \in S \to (C (R (k)) = 0 \to C (F (R (k))) = 0)$
57	46 56	syl	$⊢ (A \in S \land k \in ℕ_{0}) \to (C (R (k)) = 0 \to C (F (R (k))) = 0)$
58	41 2 42 43 44	algrp1	$⊢ (A \in S \land k \in ℕ_{0}) \to R (k + 1) = F (R (k))$
59	58	fveqeq2d	$⊢ (A \in S \land k \in ℕ_{0}) \to (C (R (k + 1)) = 0 \leftrightarrow C (F (R (k))) = 0)$
60	57 59	sylibrd	$⊢ (A \in S \land k \in ℕ_{0}) \to (C (R (k)) = 0 \to C (R (k + 1)) = 0)$
61	40 60	syl6	$⊢ (N \in ℤ \land k \in ℤ \land N \leq k) \to (A \in S \to (C (R (k)) = 0 \to C (R (k + 1)) = 0))$
62	61	a2d	$⊢ (N \in ℤ \land k \in ℤ \land N \leq k) \to ((A \in S \to C (R (k)) = 0) \to (A \in S \to C (R (k + 1)) = 0))$
63	12 15 18 21 23 62	uzind	$⊢ (N \in ℤ \land K \in ℤ \land N \leq K) \to (A \in S \to C (R (K)) = 0)$
64	63	3expib	$⊢ N \in ℤ \to ((K \in ℤ \land N \leq K) \to (A \in S \to C (R (K)) = 0))$
65	9 64	sylbid	$⊢ N \in ℤ \to (K \in ℤ_{\geq N} \to (A \in S \to C (R (K)) = 0))$
66	8 65	syl	$⊢ N \in ℕ_{0} \to (K \in ℤ_{\geq N} \to (A \in S \to C (R (K)) = 0))$
67	66	com3r	$⊢ A \in S \to (N \in ℕ_{0} \to (K \in ℤ_{\geq N} \to C (R (K)) = 0))$
68	7 67	mpd	$⊢ A \in S \to (K \in ℤ_{\geq N} \to C (R (K)) = 0)$

Metamath Proof Explorer

Theorem algcvga

Proof