nn0seqcvgd

Description: A strictly-decreasing nonnegative integer sequence with initial term N reaches zero by the N th term. Deduction version. (Contributed by Paul Chapman, 31-Mar-2011)

	Ref	Expression
Hypotheses	nn0seqcvgd.1	$⊢ φ \to F : ℕ_{0} ⟶ ℕ_{0}$
	nn0seqcvgd.2	$⊢ φ \to N = F (0)$
	nn0seqcvgd.3	$⊢ (φ \land k \in ℕ_{0}) \to (F (k + 1) \neq 0 \to F (k + 1) < F (k))$
Assertion	nn0seqcvgd	$⊢ φ \to F (N) = 0$

Proof

Step	Hyp	Ref	Expression
1		nn0seqcvgd.1	$⊢ φ \to F : ℕ_{0} ⟶ ℕ_{0}$
2		nn0seqcvgd.2	$⊢ φ \to N = F (0)$
3		nn0seqcvgd.3	$⊢ (φ \land k \in ℕ_{0}) \to (F (k + 1) \neq 0 \to F (k + 1) < F (k))$
4		0nn0	$⊢ 0 \in ℕ_{0}$
5		ffvelrn	$⊢ (F : ℕ_{0} ⟶ ℕ_{0} \land 0 \in ℕ_{0}) \to F (0) \in ℕ_{0}$
6	1 4 5	sylancl	$⊢ φ \to F (0) \in ℕ_{0}$
7	2 6	eqeltrd	$⊢ φ \to N \in ℕ_{0}$
8	7	nn0red	$⊢ φ \to N \in ℝ$
9	8	leidd	$⊢ φ \to N \leq N$
10		fveq2	$⊢ m = 0 \to F (m) = F (0)$
11		oveq2	$⊢ m = 0 \to N - m = N - 0$
12	10 11	breq12d	$⊢ m = 0 \to (F (m) \leq N - m \leftrightarrow F (0) \leq N - 0)$
13	12	imbi2d	$⊢ m = 0 \to ((φ \to F (m) \leq N - m) \leftrightarrow (φ \to F (0) \leq N - 0))$
14		fveq2	$⊢ m = k \to F (m) = F (k)$
15		oveq2	$⊢ m = k \to N - m = N - k$
16	14 15	breq12d	$⊢ m = k \to (F (m) \leq N - m \leftrightarrow F (k) \leq N - k)$
17	16	imbi2d	$⊢ m = k \to ((φ \to F (m) \leq N - m) \leftrightarrow (φ \to F (k) \leq N - k))$
18		fveq2	$⊢ m = k + 1 \to F (m) = F (k + 1)$
19		oveq2	$⊢ m = k + 1 \to N - m = N - (k + 1)$
20	18 19	breq12d	$⊢ m = k + 1 \to (F (m) \leq N - m \leftrightarrow F (k + 1) \leq N - (k + 1))$
21	20	imbi2d	$⊢ m = k + 1 \to ((φ \to F (m) \leq N - m) \leftrightarrow (φ \to F (k + 1) \leq N - (k + 1)))$
22		fveq2	$⊢ m = N \to F (m) = F (N)$
23		oveq2	$⊢ m = N \to N - m = N - N$
24	22 23	breq12d	$⊢ m = N \to (F (m) \leq N - m \leftrightarrow F (N) \leq N - N)$
25	24	imbi2d	$⊢ m = N \to ((φ \to F (m) \leq N - m) \leftrightarrow (φ \to F (N) \leq N - N))$
26	2 9	eqbrtrrd	$⊢ φ \to F (0) \leq N$
27	8	recnd	$⊢ φ \to N \in ℂ$
28	27	subid1d	$⊢ φ \to N - 0 = N$
29	26 28	breqtrrd	$⊢ φ \to F (0) \leq N - 0$
30	29	a1i	$⊢ N \in ℕ_{0} \to (φ \to F (0) \leq N - 0)$
31		nn0re	$⊢ k \in ℕ_{0} \to k \in ℝ$
32		posdif	$⊢ (k \in ℝ \land N \in ℝ) \to (k < N \leftrightarrow 0 < N - k)$
33	31 8 32	syl2anr	$⊢ (φ \land k \in ℕ_{0}) \to (k < N \leftrightarrow 0 < N - k)$
34	33	adantr	$⊢ ((φ \land k \in ℕ_{0}) \land F (k + 1) = 0) \to (k < N \leftrightarrow 0 < N - k)$
35		breq1	$⊢ F (k + 1) = 0 \to (F (k + 1) < N - k \leftrightarrow 0 < N - k)$
36	35	adantl	$⊢ ((φ \land k \in ℕ_{0}) \land F (k + 1) = 0) \to (F (k + 1) < N - k \leftrightarrow 0 < N - k)$
37		peano2nn0	$⊢ k \in ℕ_{0} \to k + 1 \in ℕ_{0}$
38		ffvelrn	$⊢ (F : ℕ_{0} ⟶ ℕ_{0} \land k + 1 \in ℕ_{0}) \to F (k + 1) \in ℕ_{0}$
39	1 37 38	syl2an	$⊢ (φ \land k \in ℕ_{0}) \to F (k + 1) \in ℕ_{0}$
40	39	nn0zd	$⊢ (φ \land k \in ℕ_{0}) \to F (k + 1) \in ℤ$
41	7	nn0zd	$⊢ φ \to N \in ℤ$
42		nn0z	$⊢ k \in ℕ_{0} \to k \in ℤ$
43		zsubcl	$⊢ (N \in ℤ \land k \in ℤ) \to N - k \in ℤ$
44	41 42 43	syl2an	$⊢ (φ \land k \in ℕ_{0}) \to N - k \in ℤ$
45		zltlem1	$⊢ (F (k + 1) \in ℤ \land N - k \in ℤ) \to (F (k + 1) < N - k \leftrightarrow F (k + 1) \leq N - k - 1)$
46	40 44 45	syl2anc	$⊢ (φ \land k \in ℕ_{0}) \to (F (k + 1) < N - k \leftrightarrow F (k + 1) \leq N - k - 1)$
47		nn0cn	$⊢ k \in ℕ_{0} \to k \in ℂ$
48		ax-1cn	$⊢ 1 \in ℂ$
49		subsub4	$⊢ (N \in ℂ \land k \in ℂ \land 1 \in ℂ) \to N - k - 1 = N - (k + 1)$
50	48 49	mp3an3	$⊢ (N \in ℂ \land k \in ℂ) \to N - k - 1 = N - (k + 1)$
51	27 47 50	syl2an	$⊢ (φ \land k \in ℕ_{0}) \to N - k - 1 = N - (k + 1)$
52	51	breq2d	$⊢ (φ \land k \in ℕ_{0}) \to (F (k + 1) \leq N - k - 1 \leftrightarrow F (k + 1) \leq N - (k + 1))$
53	46 52	bitrd	$⊢ (φ \land k \in ℕ_{0}) \to (F (k + 1) < N - k \leftrightarrow F (k + 1) \leq N - (k + 1))$
54	53	adantr	$⊢ ((φ \land k \in ℕ_{0}) \land F (k + 1) = 0) \to (F (k + 1) < N - k \leftrightarrow F (k + 1) \leq N - (k + 1))$
55	34 36 54	3bitr2d	$⊢ ((φ \land k \in ℕ_{0}) \land F (k + 1) = 0) \to (k < N \leftrightarrow F (k + 1) \leq N - (k + 1))$
56	55	biimpa	$⊢ (((φ \land k \in ℕ_{0}) \land F (k + 1) = 0) \land k < N) \to F (k + 1) \leq N - (k + 1)$
57	56	an32s	$⊢ (((φ \land k \in ℕ_{0}) \land k < N) \land F (k + 1) = 0) \to F (k + 1) \leq N - (k + 1)$
58	57	a1d	$⊢ (((φ \land k \in ℕ_{0}) \land k < N) \land F (k + 1) = 0) \to (F (k) \leq N - k \to F (k + 1) \leq N - (k + 1))$
59	39	nn0red	$⊢ (φ \land k \in ℕ_{0}) \to F (k + 1) \in ℝ$
60	1	ffvelrnda	$⊢ (φ \land k \in ℕ_{0}) \to F (k) \in ℕ_{0}$
61	60	nn0red	$⊢ (φ \land k \in ℕ_{0}) \to F (k) \in ℝ$
62	44	zred	$⊢ (φ \land k \in ℕ_{0}) \to N - k \in ℝ$
63		ltletr	$⊢ (F (k + 1) \in ℝ \land F (k) \in ℝ \land N - k \in ℝ) \to ((F (k + 1) < F (k) \land F (k) \leq N - k) \to F (k + 1) < N - k)$
64	59 61 62 63	syl3anc	$⊢ (φ \land k \in ℕ_{0}) \to ((F (k + 1) < F (k) \land F (k) \leq N - k) \to F (k + 1) < N - k)$
65	64 53	sylibd	$⊢ (φ \land k \in ℕ_{0}) \to ((F (k + 1) < F (k) \land F (k) \leq N - k) \to F (k + 1) \leq N - (k + 1))$
66	3 65	syland	$⊢ (φ \land k \in ℕ_{0}) \to ((F (k + 1) \neq 0 \land F (k) \leq N - k) \to F (k + 1) \leq N - (k + 1))$
67	66	adantr	$⊢ ((φ \land k \in ℕ_{0}) \land k < N) \to ((F (k + 1) \neq 0 \land F (k) \leq N - k) \to F (k + 1) \leq N - (k + 1))$
68	67	expdimp	$⊢ (((φ \land k \in ℕ_{0}) \land k < N) \land F (k + 1) \neq 0) \to (F (k) \leq N - k \to F (k + 1) \leq N - (k + 1))$
69	58 68	pm2.61dane	$⊢ ((φ \land k \in ℕ_{0}) \land k < N) \to (F (k) \leq N - k \to F (k + 1) \leq N - (k + 1))$
70	69	anasss	$⊢ (φ \land (k \in ℕ_{0} \land k < N)) \to (F (k) \leq N - k \to F (k + 1) \leq N - (k + 1))$
71	70	expcom	$⊢ (k \in ℕ_{0} \land k < N) \to (φ \to (F (k) \leq N - k \to F (k + 1) \leq N - (k + 1)))$
72	71	a2d	$⊢ (k \in ℕ_{0} \land k < N) \to ((φ \to F (k) \leq N - k) \to (φ \to F (k + 1) \leq N - (k + 1)))$
73	72	3adant1	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0} \land k < N) \to ((φ \to F (k) \leq N - k) \to (φ \to F (k + 1) \leq N - (k + 1)))$
74	13 17 21 25 30 73	fnn0ind	$⊢ (N \in ℕ_{0} \land N \in ℕ_{0} \land N \leq N) \to (φ \to F (N) \leq N - N)$
75	7 7 9 74	syl3anc	$⊢ φ \to (φ \to F (N) \leq N - N)$
76	75	pm2.43i	$⊢ φ \to F (N) \leq N - N$
77	27	subidd	$⊢ φ \to N - N = 0$
78	76 77	breqtrd	$⊢ φ \to F (N) \leq 0$
79	1 7	ffvelrnd	$⊢ φ \to F (N) \in ℕ_{0}$
80	79	nn0ge0d	$⊢ φ \to 0 \leq F (N)$
81	79	nn0red	$⊢ φ \to F (N) \in ℝ$
82		0re	$⊢ 0 \in ℝ$
83		letri3	$⊢ (F (N) \in ℝ \land 0 \in ℝ) \to (F (N) = 0 \leftrightarrow (F (N) \leq 0 \land 0 \leq F (N)))$
84	81 82 83	sylancl	$⊢ φ \to (F (N) = 0 \leftrightarrow (F (N) \leq 0 \land 0 \leq F (N)))$
85	78 80 84	mpbir2and	$⊢ φ \to F (N) = 0$

Metamath Proof Explorer

Theorem nn0seqcvgd

Proof