Step | Hyp | Ref
| Expression |
1 | | nn0seqcvgd.2 |
. . . . . 6
β’ (π β π = (πΉβ0)) |
2 | | nn0seqcvgd.1 |
. . . . . . 7
β’ (π β πΉ:β0βΆβ0) |
3 | | 0nn0 12491 |
. . . . . . 7
β’ 0 β
β0 |
4 | | ffvelcdm 7077 |
. . . . . . 7
β’ ((πΉ:β0βΆβ0
β§ 0 β β0) β (πΉβ0) β
β0) |
5 | 2, 3, 4 | sylancl 585 |
. . . . . 6
β’ (π β (πΉβ0) β
β0) |
6 | 1, 5 | eqeltrd 2827 |
. . . . 5
β’ (π β π β
β0) |
7 | 6 | nn0red 12537 |
. . . . . 6
β’ (π β π β β) |
8 | 7 | leidd 11784 |
. . . . 5
β’ (π β π β€ π) |
9 | | fveq2 6885 |
. . . . . . . 8
β’ (π = 0 β (πΉβπ) = (πΉβ0)) |
10 | | oveq2 7413 |
. . . . . . . 8
β’ (π = 0 β (π β π) = (π β 0)) |
11 | 9, 10 | breq12d 5154 |
. . . . . . 7
β’ (π = 0 β ((πΉβπ) β€ (π β π) β (πΉβ0) β€ (π β 0))) |
12 | 11 | imbi2d 340 |
. . . . . 6
β’ (π = 0 β ((π β (πΉβπ) β€ (π β π)) β (π β (πΉβ0) β€ (π β 0)))) |
13 | | fveq2 6885 |
. . . . . . . 8
β’ (π = π β (πΉβπ) = (πΉβπ)) |
14 | | oveq2 7413 |
. . . . . . . 8
β’ (π = π β (π β π) = (π β π)) |
15 | 13, 14 | breq12d 5154 |
. . . . . . 7
β’ (π = π β ((πΉβπ) β€ (π β π) β (πΉβπ) β€ (π β π))) |
16 | 15 | imbi2d 340 |
. . . . . 6
β’ (π = π β ((π β (πΉβπ) β€ (π β π)) β (π β (πΉβπ) β€ (π β π)))) |
17 | | fveq2 6885 |
. . . . . . . 8
β’ (π = (π + 1) β (πΉβπ) = (πΉβ(π + 1))) |
18 | | oveq2 7413 |
. . . . . . . 8
β’ (π = (π + 1) β (π β π) = (π β (π + 1))) |
19 | 17, 18 | breq12d 5154 |
. . . . . . 7
β’ (π = (π + 1) β ((πΉβπ) β€ (π β π) β (πΉβ(π + 1)) β€ (π β (π + 1)))) |
20 | 19 | imbi2d 340 |
. . . . . 6
β’ (π = (π + 1) β ((π β (πΉβπ) β€ (π β π)) β (π β (πΉβ(π + 1)) β€ (π β (π + 1))))) |
21 | | fveq2 6885 |
. . . . . . . 8
β’ (π = π β (πΉβπ) = (πΉβπ)) |
22 | | oveq2 7413 |
. . . . . . . 8
β’ (π = π β (π β π) = (π β π)) |
23 | 21, 22 | breq12d 5154 |
. . . . . . 7
β’ (π = π β ((πΉβπ) β€ (π β π) β (πΉβπ) β€ (π β π))) |
24 | 23 | imbi2d 340 |
. . . . . 6
β’ (π = π β ((π β (πΉβπ) β€ (π β π)) β (π β (πΉβπ) β€ (π β π)))) |
25 | 1, 8 | eqbrtrrd 5165 |
. . . . . . . 8
β’ (π β (πΉβ0) β€ π) |
26 | 7 | recnd 11246 |
. . . . . . . . 9
β’ (π β π β β) |
27 | 26 | subid1d 11564 |
. . . . . . . 8
β’ (π β (π β 0) = π) |
28 | 25, 27 | breqtrrd 5169 |
. . . . . . 7
β’ (π β (πΉβ0) β€ (π β 0)) |
29 | 28 | a1i 11 |
. . . . . 6
β’ (π β β0
β (π β (πΉβ0) β€ (π β 0))) |
30 | | nn0re 12485 |
. . . . . . . . . . . . . . . . 17
β’ (π β β0
β π β
β) |
31 | | posdif 11711 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ π β β) β (π < π β 0 < (π β π))) |
32 | 30, 7, 31 | syl2anr 596 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β0) β (π < π β 0 < (π β π))) |
33 | 32 | adantr 480 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β0) β§ (πΉβ(π + 1)) = 0) β (π < π β 0 < (π β π))) |
34 | | breq1 5144 |
. . . . . . . . . . . . . . . 16
β’ ((πΉβ(π + 1)) = 0 β ((πΉβ(π + 1)) < (π β π) β 0 < (π β π))) |
35 | 34 | adantl 481 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β0) β§ (πΉβ(π + 1)) = 0) β ((πΉβ(π + 1)) < (π β π) β 0 < (π β π))) |
36 | | peano2nn0 12516 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β0
β (π + 1) β
β0) |
37 | | ffvelcdm 7077 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΉ:β0βΆβ0
β§ (π + 1) β
β0) β (πΉβ(π + 1)) β
β0) |
38 | 2, 36, 37 | syl2an 595 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β0) β (πΉβ(π + 1)) β
β0) |
39 | 38 | nn0zd 12588 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β0) β (πΉβ(π + 1)) β β€) |
40 | 6 | nn0zd 12588 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β β€) |
41 | | nn0z 12587 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β0
β π β
β€) |
42 | | zsubcl 12608 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β€ β§ π β β€) β (π β π) β β€) |
43 | 40, 41, 42 | syl2an 595 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β0) β (π β π) β β€) |
44 | | zltlem1 12619 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΉβ(π + 1)) β β€ β§ (π β π) β β€) β ((πΉβ(π + 1)) < (π β π) β (πΉβ(π + 1)) β€ ((π β π) β 1))) |
45 | 39, 43, 44 | syl2anc 583 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β0) β ((πΉβ(π + 1)) < (π β π) β (πΉβ(π + 1)) β€ ((π β π) β 1))) |
46 | | nn0cn 12486 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β0
β π β
β) |
47 | | ax-1cn 11170 |
. . . . . . . . . . . . . . . . . . . 20
β’ 1 β
β |
48 | | subsub4 11497 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§ π β β β§ 1 β
β) β ((π β
π) β 1) = (π β (π + 1))) |
49 | 47, 48 | mp3an3 1446 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ π β β) β ((π β π) β 1) = (π β (π + 1))) |
50 | 26, 46, 49 | syl2an 595 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β0) β ((π β π) β 1) = (π β (π + 1))) |
51 | 50 | breq2d 5153 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β0) β ((πΉβ(π + 1)) β€ ((π β π) β 1) β (πΉβ(π + 1)) β€ (π β (π + 1)))) |
52 | 45, 51 | bitrd 279 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β0) β ((πΉβ(π + 1)) < (π β π) β (πΉβ(π + 1)) β€ (π β (π + 1)))) |
53 | 52 | adantr 480 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β0) β§ (πΉβ(π + 1)) = 0) β ((πΉβ(π + 1)) < (π β π) β (πΉβ(π + 1)) β€ (π β (π + 1)))) |
54 | 33, 35, 53 | 3bitr2d 307 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β0) β§ (πΉβ(π + 1)) = 0) β (π < π β (πΉβ(π + 1)) β€ (π β (π + 1)))) |
55 | 54 | biimpa 476 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β0) β§ (πΉβ(π + 1)) = 0) β§ π < π) β (πΉβ(π + 1)) β€ (π β (π + 1))) |
56 | 55 | an32s 649 |
. . . . . . . . . . . 12
β’ ((((π β§ π β β0) β§ π < π) β§ (πΉβ(π + 1)) = 0) β (πΉβ(π + 1)) β€ (π β (π + 1))) |
57 | 56 | a1d 25 |
. . . . . . . . . . 11
β’ ((((π β§ π β β0) β§ π < π) β§ (πΉβ(π + 1)) = 0) β ((πΉβπ) β€ (π β π) β (πΉβ(π + 1)) β€ (π β (π + 1)))) |
58 | | nn0seqcvgd.3 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β0) β ((πΉβ(π + 1)) β 0 β (πΉβ(π + 1)) < (πΉβπ))) |
59 | 38 | nn0red 12537 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β0) β (πΉβ(π + 1)) β β) |
60 | 2 | ffvelcdmda 7080 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β0) β (πΉβπ) β
β0) |
61 | 60 | nn0red 12537 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β0) β (πΉβπ) β β) |
62 | 43 | zred 12670 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β0) β (π β π) β β) |
63 | | ltletr 11310 |
. . . . . . . . . . . . . . . 16
β’ (((πΉβ(π + 1)) β β β§ (πΉβπ) β β β§ (π β π) β β) β (((πΉβ(π + 1)) < (πΉβπ) β§ (πΉβπ) β€ (π β π)) β (πΉβ(π + 1)) < (π β π))) |
64 | 59, 61, 62, 63 | syl3anc 1368 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β0) β (((πΉβ(π + 1)) < (πΉβπ) β§ (πΉβπ) β€ (π β π)) β (πΉβ(π + 1)) < (π β π))) |
65 | 64, 52 | sylibd 238 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β0) β (((πΉβ(π + 1)) < (πΉβπ) β§ (πΉβπ) β€ (π β π)) β (πΉβ(π + 1)) β€ (π β (π + 1)))) |
66 | 58, 65 | syland 602 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β0) β (((πΉβ(π + 1)) β 0 β§ (πΉβπ) β€ (π β π)) β (πΉβ(π + 1)) β€ (π β (π + 1)))) |
67 | 66 | adantr 480 |
. . . . . . . . . . . 12
β’ (((π β§ π β β0) β§ π < π) β (((πΉβ(π + 1)) β 0 β§ (πΉβπ) β€ (π β π)) β (πΉβ(π + 1)) β€ (π β (π + 1)))) |
68 | 67 | expdimp 452 |
. . . . . . . . . . 11
β’ ((((π β§ π β β0) β§ π < π) β§ (πΉβ(π + 1)) β 0) β ((πΉβπ) β€ (π β π) β (πΉβ(π + 1)) β€ (π β (π + 1)))) |
69 | 57, 68 | pm2.61dane 3023 |
. . . . . . . . . 10
β’ (((π β§ π β β0) β§ π < π) β ((πΉβπ) β€ (π β π) β (πΉβ(π + 1)) β€ (π β (π + 1)))) |
70 | 69 | anasss 466 |
. . . . . . . . 9
β’ ((π β§ (π β β0 β§ π < π)) β ((πΉβπ) β€ (π β π) β (πΉβ(π + 1)) β€ (π β (π + 1)))) |
71 | 70 | expcom 413 |
. . . . . . . 8
β’ ((π β β0
β§ π < π) β (π β ((πΉβπ) β€ (π β π) β (πΉβ(π + 1)) β€ (π β (π + 1))))) |
72 | 71 | a2d 29 |
. . . . . . 7
β’ ((π β β0
β§ π < π) β ((π β (πΉβπ) β€ (π β π)) β (π β (πΉβ(π + 1)) β€ (π β (π + 1))))) |
73 | 72 | 3adant1 1127 |
. . . . . 6
β’ ((π β β0
β§ π β
β0 β§ π
< π) β ((π β (πΉβπ) β€ (π β π)) β (π β (πΉβ(π + 1)) β€ (π β (π + 1))))) |
74 | 12, 16, 20, 24, 29, 73 | fnn0ind 12665 |
. . . . 5
β’ ((π β β0
β§ π β
β0 β§ π
β€ π) β (π β (πΉβπ) β€ (π β π))) |
75 | 6, 6, 8, 74 | syl3anc 1368 |
. . . 4
β’ (π β (π β (πΉβπ) β€ (π β π))) |
76 | 75 | pm2.43i 52 |
. . 3
β’ (π β (πΉβπ) β€ (π β π)) |
77 | 26 | subidd 11563 |
. . 3
β’ (π β (π β π) = 0) |
78 | 76, 77 | breqtrd 5167 |
. 2
β’ (π β (πΉβπ) β€ 0) |
79 | 2, 6 | ffvelcdmd 7081 |
. . 3
β’ (π β (πΉβπ) β
β0) |
80 | 79 | nn0ge0d 12539 |
. 2
β’ (π β 0 β€ (πΉβπ)) |
81 | 79 | nn0red 12537 |
. . 3
β’ (π β (πΉβπ) β β) |
82 | | 0re 11220 |
. . 3
β’ 0 β
β |
83 | | letri3 11303 |
. . 3
β’ (((πΉβπ) β β β§ 0 β β)
β ((πΉβπ) = 0 β ((πΉβπ) β€ 0 β§ 0 β€ (πΉβπ)))) |
84 | 81, 82, 83 | sylancl 585 |
. 2
β’ (π β ((πΉβπ) = 0 β ((πΉβπ) β€ 0 β§ 0 β€ (πΉβπ)))) |
85 | 78, 80, 84 | mpbir2and 710 |
1
β’ (π β (πΉβπ) = 0) |