Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → 𝐹 : ℕ0 ⟶ ℕ0 )
nn0seqcvgd.2 ⊢ ( 𝜑 → 𝑁 = ( 𝐹 ‘ 0 ) )
nn0seqcvgd.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≠ 0 → ( 𝐹 ‘ ( 𝑘 + 1 ) ) < ( 𝐹 ‘ 𝑘 ) ) )
Assertion nn0seqcvgd ( 𝜑 → ( 𝐹 ‘ 𝑁 ) = 0 )

Proof

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