Step | Hyp | Ref
| Expression |
1 | | fveq2 6846 |
. . . . . . 7
β’ (π = 1 β
(β€β₯βπ) =
(β€β₯β1)) |
2 | 1 | eleq2d 2820 |
. . . . . 6
β’ (π = 1 β ((πΉβπ) β (β€β₯βπ) β (πΉβπ) β
(β€β₯β1))) |
3 | 2 | rexbidv 3172 |
. . . . 5
β’ (π = 1 β (βπ β β (πΉβπ) β (β€β₯βπ) β βπ β β (πΉβπ) β
(β€β₯β1))) |
4 | 3 | imbi2d 341 |
. . . 4
β’ (π = 1 β (((πΉ:ββΆβ β§ βπ β β (πΉβπ) < (πΉβ(π + 1))) β βπ β β (πΉβπ) β (β€β₯βπ)) β ((πΉ:ββΆβ β§ βπ β β (πΉβπ) < (πΉβ(π + 1))) β βπ β β (πΉβπ) β
(β€β₯β1)))) |
5 | | fveq2 6846 |
. . . . . . 7
β’ (π = π β (β€β₯βπ) =
(β€β₯βπ)) |
6 | 5 | eleq2d 2820 |
. . . . . 6
β’ (π = π β ((πΉβπ) β (β€β₯βπ) β (πΉβπ) β (β€β₯βπ))) |
7 | 6 | rexbidv 3172 |
. . . . 5
β’ (π = π β (βπ β β (πΉβπ) β (β€β₯βπ) β βπ β β (πΉβπ) β (β€β₯βπ))) |
8 | 7 | imbi2d 341 |
. . . 4
β’ (π = π β (((πΉ:ββΆβ β§ βπ β β (πΉβπ) < (πΉβ(π + 1))) β βπ β β (πΉβπ) β (β€β₯βπ)) β ((πΉ:ββΆβ β§ βπ β β (πΉβπ) < (πΉβ(π + 1))) β βπ β β (πΉβπ) β (β€β₯βπ)))) |
9 | | fveq2 6846 |
. . . . . . 7
β’ (π = (π + 1) β
(β€β₯βπ) = (β€β₯β(π + 1))) |
10 | 9 | eleq2d 2820 |
. . . . . 6
β’ (π = (π + 1) β ((πΉβπ) β (β€β₯βπ) β (πΉβπ) β (β€β₯β(π + 1)))) |
11 | 10 | rexbidv 3172 |
. . . . 5
β’ (π = (π + 1) β (βπ β β (πΉβπ) β (β€β₯βπ) β βπ β β (πΉβπ) β (β€β₯β(π + 1)))) |
12 | 11 | imbi2d 341 |
. . . 4
β’ (π = (π + 1) β (((πΉ:ββΆβ β§ βπ β β (πΉβπ) < (πΉβ(π + 1))) β βπ β β (πΉβπ) β (β€β₯βπ)) β ((πΉ:ββΆβ β§ βπ β β (πΉβπ) < (πΉβ(π + 1))) β βπ β β (πΉβπ) β (β€β₯β(π + 1))))) |
13 | | fveq2 6846 |
. . . . . . 7
β’ (π = π΄ β (β€β₯βπ) =
(β€β₯βπ΄)) |
14 | 13 | eleq2d 2820 |
. . . . . 6
β’ (π = π΄ β ((πΉβπ) β (β€β₯βπ) β (πΉβπ) β (β€β₯βπ΄))) |
15 | 14 | rexbidv 3172 |
. . . . 5
β’ (π = π΄ β (βπ β β (πΉβπ) β (β€β₯βπ) β βπ β β (πΉβπ) β (β€β₯βπ΄))) |
16 | 15 | imbi2d 341 |
. . . 4
β’ (π = π΄ β (((πΉ:ββΆβ β§ βπ β β (πΉβπ) < (πΉβ(π + 1))) β βπ β β (πΉβπ) β (β€β₯βπ)) β ((πΉ:ββΆβ β§ βπ β β (πΉβπ) < (πΉβ(π + 1))) β βπ β β (πΉβπ) β (β€β₯βπ΄)))) |
17 | | 1nn 12172 |
. . . . . . 7
β’ 1 β
β |
18 | 17 | ne0ii 4301 |
. . . . . 6
β’ β
β β
|
19 | | ffvelcdm 7036 |
. . . . . . . 8
β’ ((πΉ:ββΆβ β§
π β β) β
(πΉβπ) β β) |
20 | | elnnuz 12815 |
. . . . . . . 8
β’ ((πΉβπ) β β β (πΉβπ) β
(β€β₯β1)) |
21 | 19, 20 | sylib 217 |
. . . . . . 7
β’ ((πΉ:ββΆβ β§
π β β) β
(πΉβπ) β
(β€β₯β1)) |
22 | 21 | ralrimiva 3140 |
. . . . . 6
β’ (πΉ:ββΆβ β
βπ β β
(πΉβπ) β
(β€β₯β1)) |
23 | | r19.2z 4456 |
. . . . . 6
β’ ((β
β β
β§ βπ β β (πΉβπ) β (β€β₯β1))
β βπ β
β (πΉβπ) β
(β€β₯β1)) |
24 | 18, 22, 23 | sylancr 588 |
. . . . 5
β’ (πΉ:ββΆβ β
βπ β β
(πΉβπ) β
(β€β₯β1)) |
25 | 24 | adantr 482 |
. . . 4
β’ ((πΉ:ββΆβ β§
βπ β β
(πΉβπ) < (πΉβ(π + 1))) β βπ β β (πΉβπ) β
(β€β₯β1)) |
26 | | peano2nn 12173 |
. . . . . . . . . 10
β’ (π β β β (π + 1) β
β) |
27 | 26 | adantl 483 |
. . . . . . . . 9
β’ (((π β β β§ (πΉ:ββΆβ β§
βπ β β
(πΉβπ) < (πΉβ(π + 1)))) β§ π β β) β (π + 1) β β) |
28 | | nnre 12168 |
. . . . . . . . . . . . 13
β’ (π β β β π β
β) |
29 | 28 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β β β§ (πΉ:ββΆβ β§
βπ β β
(πΉβπ) < (πΉβ(π + 1)))) β§ π β β) β π β β) |
30 | 19 | nnred 12176 |
. . . . . . . . . . . . . 14
β’ ((πΉ:ββΆβ β§
π β β) β
(πΉβπ) β β) |
31 | 30 | adantlr 714 |
. . . . . . . . . . . . 13
β’ (((πΉ:ββΆβ β§
βπ β β
(πΉβπ) < (πΉβ(π + 1))) β§ π β β) β (πΉβπ) β β) |
32 | 31 | adantll 713 |
. . . . . . . . . . . 12
β’ (((π β β β§ (πΉ:ββΆβ β§
βπ β β
(πΉβπ) < (πΉβ(π + 1)))) β§ π β β) β (πΉβπ) β β) |
33 | | 1red 11164 |
. . . . . . . . . . . 12
β’ (((π β β β§ (πΉ:ββΆβ β§
βπ β β
(πΉβπ) < (πΉβ(π + 1)))) β§ π β β) β 1 β
β) |
34 | 29, 32, 33 | leadd1d 11757 |
. . . . . . . . . . 11
β’ (((π β β β§ (πΉ:ββΆβ β§
βπ β β
(πΉβπ) < (πΉβ(π + 1)))) β§ π β β) β (π β€ (πΉβπ) β (π + 1) β€ ((πΉβπ) + 1))) |
35 | | fveq2 6846 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (πΉβπ) = (πΉβπ)) |
36 | | fvoveq1 7384 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (πΉβ(π + 1)) = (πΉβ(π + 1))) |
37 | 35, 36 | breq12d 5122 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β ((πΉβπ) < (πΉβ(π + 1)) β (πΉβπ) < (πΉβ(π + 1)))) |
38 | 37 | rspcv 3579 |
. . . . . . . . . . . . . . . 16
β’ (π β β β
(βπ β β
(πΉβπ) < (πΉβ(π + 1)) β (πΉβπ) < (πΉβ(π + 1)))) |
39 | 38 | imdistani 570 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§
βπ β β
(πΉβπ) < (πΉβ(π + 1))) β (π β β β§ (πΉβπ) < (πΉβ(π + 1)))) |
40 | | ffvelcdm 7036 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΉ:ββΆβ β§
(π + 1) β β)
β (πΉβ(π + 1)) β
β) |
41 | 26, 40 | sylan2 594 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉ:ββΆβ β§
π β β) β
(πΉβ(π + 1)) β
β) |
42 | | nnltp1le 12567 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΉβπ) β β β§ (πΉβ(π + 1)) β β) β ((πΉβπ) < (πΉβ(π + 1)) β ((πΉβπ) + 1) β€ (πΉβ(π + 1)))) |
43 | 19, 41, 42 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉ:ββΆβ β§
π β β) β
((πΉβπ) < (πΉβ(π + 1)) β ((πΉβπ) + 1) β€ (πΉβ(π + 1)))) |
44 | 43 | biimpa 478 |
. . . . . . . . . . . . . . . 16
β’ (((πΉ:ββΆβ β§
π β β) β§
(πΉβπ) < (πΉβ(π + 1))) β ((πΉβπ) + 1) β€ (πΉβ(π + 1))) |
45 | 44 | anasss 468 |
. . . . . . . . . . . . . . 15
β’ ((πΉ:ββΆβ β§
(π β β β§
(πΉβπ) < (πΉβ(π + 1)))) β ((πΉβπ) + 1) β€ (πΉβ(π + 1))) |
46 | 39, 45 | sylan2 594 |
. . . . . . . . . . . . . 14
β’ ((πΉ:ββΆβ β§
(π β β β§
βπ β β
(πΉβπ) < (πΉβ(π + 1)))) β ((πΉβπ) + 1) β€ (πΉβ(π + 1))) |
47 | 46 | anass1rs 654 |
. . . . . . . . . . . . 13
β’ (((πΉ:ββΆβ β§
βπ β β
(πΉβπ) < (πΉβ(π + 1))) β§ π β β) β ((πΉβπ) + 1) β€ (πΉβ(π + 1))) |
48 | 47 | adantll 713 |
. . . . . . . . . . . 12
β’ (((π β β β§ (πΉ:ββΆβ β§
βπ β β
(πΉβπ) < (πΉβ(π + 1)))) β§ π β β) β ((πΉβπ) + 1) β€ (πΉβ(π + 1))) |
49 | | peano2re 11336 |
. . . . . . . . . . . . . . . 16
β’ (π β β β (π + 1) β
β) |
50 | 28, 49 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β β β (π + 1) β
β) |
51 | 50 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ πΉ:ββΆβ) β§
π β β) β
(π + 1) β
β) |
52 | | peano2nn 12173 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉβπ) β β β ((πΉβπ) + 1) β β) |
53 | 19, 52 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((πΉ:ββΆβ β§
π β β) β
((πΉβπ) + 1) β
β) |
54 | 53 | nnred 12176 |
. . . . . . . . . . . . . . 15
β’ ((πΉ:ββΆβ β§
π β β) β
((πΉβπ) + 1) β
β) |
55 | 54 | adantll 713 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ πΉ:ββΆβ) β§
π β β) β
((πΉβπ) + 1) β
β) |
56 | 40 | nnred 12176 |
. . . . . . . . . . . . . . . 16
β’ ((πΉ:ββΆβ β§
(π + 1) β β)
β (πΉβ(π + 1)) β
β) |
57 | 26, 56 | sylan2 594 |
. . . . . . . . . . . . . . 15
β’ ((πΉ:ββΆβ β§
π β β) β
(πΉβ(π + 1)) β
β) |
58 | 57 | adantll 713 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ πΉ:ββΆβ) β§
π β β) β
(πΉβ(π + 1)) β
β) |
59 | | letr 11257 |
. . . . . . . . . . . . . 14
β’ (((π + 1) β β β§
((πΉβπ) + 1) β β β§
(πΉβ(π + 1)) β β) β
(((π + 1) β€ ((πΉβπ) + 1) β§ ((πΉβπ) + 1) β€ (πΉβ(π + 1))) β (π + 1) β€ (πΉβ(π + 1)))) |
60 | 51, 55, 58, 59 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (((π β β β§ πΉ:ββΆβ) β§
π β β) β
(((π + 1) β€ ((πΉβπ) + 1) β§ ((πΉβπ) + 1) β€ (πΉβ(π + 1))) β (π + 1) β€ (πΉβ(π + 1)))) |
61 | 60 | adantlrr 720 |
. . . . . . . . . . . 12
β’ (((π β β β§ (πΉ:ββΆβ β§
βπ β β
(πΉβπ) < (πΉβ(π + 1)))) β§ π β β) β (((π + 1) β€ ((πΉβπ) + 1) β§ ((πΉβπ) + 1) β€ (πΉβ(π + 1))) β (π + 1) β€ (πΉβ(π + 1)))) |
62 | 48, 61 | mpan2d 693 |
. . . . . . . . . . 11
β’ (((π β β β§ (πΉ:ββΆβ β§
βπ β β
(πΉβπ) < (πΉβ(π + 1)))) β§ π β β) β ((π + 1) β€ ((πΉβπ) + 1) β (π + 1) β€ (πΉβ(π + 1)))) |
63 | 34, 62 | sylbid 239 |
. . . . . . . . . 10
β’ (((π β β β§ (πΉ:ββΆβ β§
βπ β β
(πΉβπ) < (πΉβ(π + 1)))) β§ π β β) β (π β€ (πΉβπ) β (π + 1) β€ (πΉβ(π + 1)))) |
64 | | nnz 12528 |
. . . . . . . . . . . . 13
β’ (π β β β π β
β€) |
65 | 19 | nnzd 12534 |
. . . . . . . . . . . . 13
β’ ((πΉ:ββΆβ β§
π β β) β
(πΉβπ) β β€) |
66 | | eluz 12785 |
. . . . . . . . . . . . 13
β’ ((π β β€ β§ (πΉβπ) β β€) β ((πΉβπ) β (β€β₯βπ) β π β€ (πΉβπ))) |
67 | 64, 65, 66 | syl2an 597 |
. . . . . . . . . . . 12
β’ ((π β β β§ (πΉ:ββΆβ β§
π β β)) β
((πΉβπ) β
(β€β₯βπ) β π β€ (πΉβπ))) |
68 | 67 | adantrlr 722 |
. . . . . . . . . . 11
β’ ((π β β β§ ((πΉ:ββΆβ β§
βπ β β
(πΉβπ) < (πΉβ(π + 1))) β§ π β β)) β ((πΉβπ) β (β€β₯βπ) β π β€ (πΉβπ))) |
69 | 68 | anassrs 469 |
. . . . . . . . . 10
β’ (((π β β β§ (πΉ:ββΆβ β§
βπ β β
(πΉβπ) < (πΉβ(π + 1)))) β§ π β β) β ((πΉβπ) β (β€β₯βπ) β π β€ (πΉβπ))) |
70 | 64 | peano2zd 12618 |
. . . . . . . . . . . . 13
β’ (π β β β (π + 1) β
β€) |
71 | 40 | nnzd 12534 |
. . . . . . . . . . . . . 14
β’ ((πΉ:ββΆβ β§
(π + 1) β β)
β (πΉβ(π + 1)) β
β€) |
72 | 26, 71 | sylan2 594 |
. . . . . . . . . . . . 13
β’ ((πΉ:ββΆβ β§
π β β) β
(πΉβ(π + 1)) β
β€) |
73 | | eluz 12785 |
. . . . . . . . . . . . 13
β’ (((π + 1) β β€ β§
(πΉβ(π + 1)) β β€) β
((πΉβ(π + 1)) β
(β€β₯β(π + 1)) β (π + 1) β€ (πΉβ(π + 1)))) |
74 | 70, 72, 73 | syl2an 597 |
. . . . . . . . . . . 12
β’ ((π β β β§ (πΉ:ββΆβ β§
π β β)) β
((πΉβ(π + 1)) β
(β€β₯β(π + 1)) β (π + 1) β€ (πΉβ(π + 1)))) |
75 | 74 | adantrlr 722 |
. . . . . . . . . . 11
β’ ((π β β β§ ((πΉ:ββΆβ β§
βπ β β
(πΉβπ) < (πΉβ(π + 1))) β§ π β β)) β ((πΉβ(π + 1)) β
(β€β₯β(π + 1)) β (π + 1) β€ (πΉβ(π + 1)))) |
76 | 75 | anassrs 469 |
. . . . . . . . . 10
β’ (((π β β β§ (πΉ:ββΆβ β§
βπ β β
(πΉβπ) < (πΉβ(π + 1)))) β§ π β β) β ((πΉβ(π + 1)) β
(β€β₯β(π + 1)) β (π + 1) β€ (πΉβ(π + 1)))) |
77 | 63, 69, 76 | 3imtr4d 294 |
. . . . . . . . 9
β’ (((π β β β§ (πΉ:ββΆβ β§
βπ β β
(πΉβπ) < (πΉβ(π + 1)))) β§ π β β) β ((πΉβπ) β (β€β₯βπ) β (πΉβ(π + 1)) β
(β€β₯β(π + 1)))) |
78 | | fveq2 6846 |
. . . . . . . . . . 11
β’ (π = (π + 1) β (πΉβπ) = (πΉβ(π + 1))) |
79 | 78 | eleq1d 2819 |
. . . . . . . . . 10
β’ (π = (π + 1) β ((πΉβπ) β (β€β₯β(π + 1)) β (πΉβ(π + 1)) β
(β€β₯β(π + 1)))) |
80 | 79 | rspcev 3583 |
. . . . . . . . 9
β’ (((π + 1) β β β§
(πΉβ(π + 1)) β
(β€β₯β(π + 1))) β βπ β β (πΉβπ) β (β€β₯β(π + 1))) |
81 | 27, 77, 80 | syl6an 683 |
. . . . . . . 8
β’ (((π β β β§ (πΉ:ββΆβ β§
βπ β β
(πΉβπ) < (πΉβ(π + 1)))) β§ π β β) β ((πΉβπ) β (β€β₯βπ) β βπ β β (πΉβπ) β (β€β₯β(π + 1)))) |
82 | 81 | rexlimdva 3149 |
. . . . . . 7
β’ ((π β β β§ (πΉ:ββΆβ β§
βπ β β
(πΉβπ) < (πΉβ(π + 1)))) β (βπ β β (πΉβπ) β (β€β₯βπ) β βπ β β (πΉβπ) β (β€β₯β(π + 1)))) |
83 | | fveq2 6846 |
. . . . . . . . 9
β’ (π = π β (πΉβπ) = (πΉβπ)) |
84 | 83 | eleq1d 2819 |
. . . . . . . 8
β’ (π = π β ((πΉβπ) β (β€β₯β(π + 1)) β (πΉβπ) β (β€β₯β(π + 1)))) |
85 | 84 | cbvrexvw 3225 |
. . . . . . 7
β’
(βπ β
β (πΉβπ) β
(β€β₯β(π + 1)) β βπ β β (πΉβπ) β (β€β₯β(π + 1))) |
86 | 82, 85 | syl6ib 251 |
. . . . . 6
β’ ((π β β β§ (πΉ:ββΆβ β§
βπ β β
(πΉβπ) < (πΉβ(π + 1)))) β (βπ β β (πΉβπ) β (β€β₯βπ) β βπ β β (πΉβπ) β (β€β₯β(π + 1)))) |
87 | 86 | ex 414 |
. . . . 5
β’ (π β β β ((πΉ:ββΆβ β§
βπ β β
(πΉβπ) < (πΉβ(π + 1))) β (βπ β β (πΉβπ) β (β€β₯βπ) β βπ β β (πΉβπ) β (β€β₯β(π + 1))))) |
88 | 87 | a2d 29 |
. . . 4
β’ (π β β β (((πΉ:ββΆβ β§
βπ β β
(πΉβπ) < (πΉβ(π + 1))) β βπ β β (πΉβπ) β (β€β₯βπ)) β ((πΉ:ββΆβ β§ βπ β β (πΉβπ) < (πΉβ(π + 1))) β βπ β β (πΉβπ) β (β€β₯β(π + 1))))) |
89 | 4, 8, 12, 16, 25, 88 | nnind 12179 |
. . 3
β’ (π΄ β β β ((πΉ:ββΆβ β§
βπ β β
(πΉβπ) < (πΉβ(π + 1))) β βπ β β (πΉβπ) β (β€β₯βπ΄))) |
90 | 89 | com12 32 |
. 2
β’ ((πΉ:ββΆβ β§
βπ β β
(πΉβπ) < (πΉβ(π + 1))) β (π΄ β β β βπ β β (πΉβπ) β (β€β₯βπ΄))) |
91 | 90 | 3impia 1118 |
1
β’ ((πΉ:ββΆβ β§
βπ β β
(πΉβπ) < (πΉβ(π + 1)) β§ π΄ β β) β βπ β β (πΉβπ) β (β€β₯βπ΄)) |