Step | Hyp | Ref
| Expression |
1 | | incsequz 36257 |
. 2
β’ ((πΉ:ββΆβ β§
βπ β β
(πΉβπ) < (πΉβ(π + 1)) β§ π΄ β β) β βπ β β (πΉβπ) β (β€β₯βπ΄)) |
2 | | nnssre 12165 |
. . . . . . . 8
β’ β
β β |
3 | | ltso 11243 |
. . . . . . . . 9
β’ < Or
β |
4 | | sopo 5568 |
. . . . . . . . 9
β’ ( < Or
β β < Po β) |
5 | 3, 4 | ax-mp 5 |
. . . . . . . 8
β’ < Po
β |
6 | | poss 5551 |
. . . . . . . 8
β’ (β
β β β ( < Po β β < Po
β)) |
7 | 2, 5, 6 | mp2 9 |
. . . . . . 7
β’ < Po
β |
8 | | seqpo 36256 |
. . . . . . 7
β’ (( <
Po β β§ πΉ:ββΆβ) β
(βπ β β
(πΉβπ) < (πΉβ(π + 1)) β βπ β β βπ β (β€β₯β(π + 1))(πΉβπ) < (πΉβπ))) |
9 | 7, 8 | mpan 689 |
. . . . . 6
β’ (πΉ:ββΆβ β
(βπ β β
(πΉβπ) < (πΉβ(π + 1)) β βπ β β βπ β (β€β₯β(π + 1))(πΉβπ) < (πΉβπ))) |
10 | 9 | biimpd 228 |
. . . . 5
β’ (πΉ:ββΆβ β
(βπ β β
(πΉβπ) < (πΉβ(π + 1)) β βπ β β βπ β (β€β₯β(π + 1))(πΉβπ) < (πΉβπ))) |
11 | 10 | imdistani 570 |
. . . 4
β’ ((πΉ:ββΆβ β§
βπ β β
(πΉβπ) < (πΉβ(π + 1))) β (πΉ:ββΆβ β§ βπ β β βπ β
(β€β₯β(π + 1))(πΉβπ) < (πΉβπ))) |
12 | | uzp1 12812 |
. . . . . . . . 9
β’ (π β
(β€β₯βπ) β (π = π β¨ π β (β€β₯β(π + 1)))) |
13 | | fveq2 6846 |
. . . . . . . . . . . . 13
β’ (π = π β (πΉβπ) = (πΉβπ)) |
14 | 13 | adantl 483 |
. . . . . . . . . . . 12
β’ (((πΉ:ββΆβ β§
π β β) β§
π = π) β (πΉβπ) = (πΉβπ)) |
15 | | ffvelcdm 7036 |
. . . . . . . . . . . . . . 15
β’ ((πΉ:ββΆβ β§
π β β) β
(πΉβπ) β β) |
16 | 15 | nnzd 12534 |
. . . . . . . . . . . . . 14
β’ ((πΉ:ββΆβ β§
π β β) β
(πΉβπ) β β€) |
17 | | uzid 12786 |
. . . . . . . . . . . . . 14
β’ ((πΉβπ) β β€ β (πΉβπ) β (β€β₯β(πΉβπ))) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . . 13
β’ ((πΉ:ββΆβ β§
π β β) β
(πΉβπ) β (β€β₯β(πΉβπ))) |
19 | 18 | adantr 482 |
. . . . . . . . . . . 12
β’ (((πΉ:ββΆβ β§
π β β) β§
π = π) β (πΉβπ) β (β€β₯β(πΉβπ))) |
20 | 14, 19 | eqeltrd 2834 |
. . . . . . . . . . 11
β’ (((πΉ:ββΆβ β§
π β β) β§
π = π) β (πΉβπ) β (β€β₯β(πΉβπ))) |
21 | 20 | adantllr 718 |
. . . . . . . . . 10
β’ ((((πΉ:ββΆβ β§
βπ β β
βπ β
(β€β₯β(π + 1))(πΉβπ) < (πΉβπ)) β§ π β β) β§ π = π) β (πΉβπ) β (β€β₯β(πΉβπ))) |
22 | | fvoveq1 7384 |
. . . . . . . . . . . . . . 15
β’ (π = π β (β€β₯β(π + 1)) =
(β€β₯β(π + 1))) |
23 | | fveq2 6846 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (πΉβπ) = (πΉβπ)) |
24 | 23 | breq1d 5119 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((πΉβπ) < (πΉβπ) β (πΉβπ) < (πΉβπ))) |
25 | 22, 24 | raleqbidv 3318 |
. . . . . . . . . . . . . 14
β’ (π = π β (βπ β (β€β₯β(π + 1))(πΉβπ) < (πΉβπ) β βπ β (β€β₯β(π + 1))(πΉβπ) < (πΉβπ))) |
26 | 25 | rspccva 3582 |
. . . . . . . . . . . . 13
β’
((βπ β
β βπ β
(β€β₯β(π + 1))(πΉβπ) < (πΉβπ) β§ π β β) β βπ β
(β€β₯β(π + 1))(πΉβπ) < (πΉβπ)) |
27 | | fveq2 6846 |
. . . . . . . . . . . . . . 15
β’ (π = π β (πΉβπ) = (πΉβπ)) |
28 | 27 | breq2d 5121 |
. . . . . . . . . . . . . 14
β’ (π = π β ((πΉβπ) < (πΉβπ) β (πΉβπ) < (πΉβπ))) |
29 | 28 | rspccva 3582 |
. . . . . . . . . . . . 13
β’
((βπ β
(β€β₯β(π + 1))(πΉβπ) < (πΉβπ) β§ π β (β€β₯β(π + 1))) β (πΉβπ) < (πΉβπ)) |
30 | 26, 29 | sylan 581 |
. . . . . . . . . . . 12
β’
(((βπ β
β βπ β
(β€β₯β(π + 1))(πΉβπ) < (πΉβπ) β§ π β β) β§ π β (β€β₯β(π + 1))) β (πΉβπ) < (πΉβπ)) |
31 | 30 | adantlll 717 |
. . . . . . . . . . 11
β’ ((((πΉ:ββΆβ β§
βπ β β
βπ β
(β€β₯β(π + 1))(πΉβπ) < (πΉβπ)) β§ π β β) β§ π β (β€β₯β(π + 1))) β (πΉβπ) < (πΉβπ)) |
32 | 16 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((πΉ:ββΆβ β§
π β β) β§
π β
(β€β₯β(π + 1))) β (πΉβπ) β β€) |
33 | | peano2nn 12173 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β (π + 1) β
β) |
34 | | elnnuz 12815 |
. . . . . . . . . . . . . . . . 17
β’ ((π + 1) β β β
(π + 1) β
(β€β₯β1)) |
35 | 33, 34 | sylib 217 |
. . . . . . . . . . . . . . . 16
β’ (π β β β (π + 1) β
(β€β₯β1)) |
36 | | uztrn 12789 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β
(β€β₯β(π + 1)) β§ (π + 1) β
(β€β₯β1)) β π β
(β€β₯β1)) |
37 | 36 | ancoms 460 |
. . . . . . . . . . . . . . . . 17
β’ (((π + 1) β
(β€β₯β1) β§ π β (β€β₯β(π + 1))) β π β
(β€β₯β1)) |
38 | | elnnuz 12815 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β π β
(β€β₯β1)) |
39 | 37, 38 | sylibr 233 |
. . . . . . . . . . . . . . . 16
β’ (((π + 1) β
(β€β₯β1) β§ π β (β€β₯β(π + 1))) β π β
β) |
40 | 35, 39 | sylan 581 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π β
(β€β₯β(π + 1))) β π β β) |
41 | | ffvelcdm 7036 |
. . . . . . . . . . . . . . . 16
β’ ((πΉ:ββΆβ β§
π β β) β
(πΉβπ) β β) |
42 | 41 | nnzd 12534 |
. . . . . . . . . . . . . . 15
β’ ((πΉ:ββΆβ β§
π β β) β
(πΉβπ) β β€) |
43 | 40, 42 | sylan2 594 |
. . . . . . . . . . . . . 14
β’ ((πΉ:ββΆβ β§
(π β β β§
π β
(β€β₯β(π + 1)))) β (πΉβπ) β β€) |
44 | 43 | anassrs 469 |
. . . . . . . . . . . . 13
β’ (((πΉ:ββΆβ β§
π β β) β§
π β
(β€β₯β(π + 1))) β (πΉβπ) β β€) |
45 | | zre 12511 |
. . . . . . . . . . . . . . 15
β’ ((πΉβπ) β β€ β (πΉβπ) β β) |
46 | | zre 12511 |
. . . . . . . . . . . . . . 15
β’ ((πΉβπ) β β€ β (πΉβπ) β β) |
47 | | ltle 11251 |
. . . . . . . . . . . . . . 15
β’ (((πΉβπ) β β β§ (πΉβπ) β β) β ((πΉβπ) < (πΉβπ) β (πΉβπ) β€ (πΉβπ))) |
48 | 45, 46, 47 | syl2an 597 |
. . . . . . . . . . . . . 14
β’ (((πΉβπ) β β€ β§ (πΉβπ) β β€) β ((πΉβπ) < (πΉβπ) β (πΉβπ) β€ (πΉβπ))) |
49 | | eluz 12785 |
. . . . . . . . . . . . . 14
β’ (((πΉβπ) β β€ β§ (πΉβπ) β β€) β ((πΉβπ) β (β€β₯β(πΉβπ)) β (πΉβπ) β€ (πΉβπ))) |
50 | 48, 49 | sylibrd 259 |
. . . . . . . . . . . . 13
β’ (((πΉβπ) β β€ β§ (πΉβπ) β β€) β ((πΉβπ) < (πΉβπ) β (πΉβπ) β (β€β₯β(πΉβπ)))) |
51 | 32, 44, 50 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((πΉ:ββΆβ β§
π β β) β§
π β
(β€β₯β(π + 1))) β ((πΉβπ) < (πΉβπ) β (πΉβπ) β (β€β₯β(πΉβπ)))) |
52 | 51 | adantllr 718 |
. . . . . . . . . . 11
β’ ((((πΉ:ββΆβ β§
βπ β β
βπ β
(β€β₯β(π + 1))(πΉβπ) < (πΉβπ)) β§ π β β) β§ π β (β€β₯β(π + 1))) β ((πΉβπ) < (πΉβπ) β (πΉβπ) β (β€β₯β(πΉβπ)))) |
53 | 31, 52 | mpd 15 |
. . . . . . . . . 10
β’ ((((πΉ:ββΆβ β§
βπ β β
βπ β
(β€β₯β(π + 1))(πΉβπ) < (πΉβπ)) β§ π β β) β§ π β (β€β₯β(π + 1))) β (πΉβπ) β (β€β₯β(πΉβπ))) |
54 | 21, 53 | jaodan 957 |
. . . . . . . . 9
β’ ((((πΉ:ββΆβ β§
βπ β β
βπ β
(β€β₯β(π + 1))(πΉβπ) < (πΉβπ)) β§ π β β) β§ (π = π β¨ π β (β€β₯β(π + 1)))) β (πΉβπ) β (β€β₯β(πΉβπ))) |
55 | 12, 54 | sylan2 594 |
. . . . . . . 8
β’ ((((πΉ:ββΆβ β§
βπ β β
βπ β
(β€β₯β(π + 1))(πΉβπ) < (πΉβπ)) β§ π β β) β§ π β (β€β₯βπ)) β (πΉβπ) β (β€β₯β(πΉβπ))) |
56 | | uztrn 12789 |
. . . . . . . . 9
β’ (((πΉβπ) β (β€β₯β(πΉβπ)) β§ (πΉβπ) β (β€β₯βπ΄)) β (πΉβπ) β (β€β₯βπ΄)) |
57 | 56 | ex 414 |
. . . . . . . 8
β’ ((πΉβπ) β (β€β₯β(πΉβπ)) β ((πΉβπ) β (β€β₯βπ΄) β (πΉβπ) β (β€β₯βπ΄))) |
58 | 55, 57 | syl 17 |
. . . . . . 7
β’ ((((πΉ:ββΆβ β§
βπ β β
βπ β
(β€β₯β(π + 1))(πΉβπ) < (πΉβπ)) β§ π β β) β§ π β (β€β₯βπ)) β ((πΉβπ) β (β€β₯βπ΄) β (πΉβπ) β (β€β₯βπ΄))) |
59 | 58 | adantllr 718 |
. . . . . 6
β’
(((((πΉ:ββΆβ β§ βπ β β βπ β
(β€β₯β(π + 1))(πΉβπ) < (πΉβπ)) β§ π΄ β β) β§ π β β) β§ π β (β€β₯βπ)) β ((πΉβπ) β (β€β₯βπ΄) β (πΉβπ) β (β€β₯βπ΄))) |
60 | 59 | ralrimdva 3148 |
. . . . 5
β’ ((((πΉ:ββΆβ β§
βπ β β
βπ β
(β€β₯β(π + 1))(πΉβπ) < (πΉβπ)) β§ π΄ β β) β§ π β β) β ((πΉβπ) β (β€β₯βπ΄) β βπ β
(β€β₯βπ)(πΉβπ) β (β€β₯βπ΄))) |
61 | 60 | ex 414 |
. . . 4
β’ (((πΉ:ββΆβ β§
βπ β β
βπ β
(β€β₯β(π + 1))(πΉβπ) < (πΉβπ)) β§ π΄ β β) β (π β β β ((πΉβπ) β (β€β₯βπ΄) β βπ β
(β€β₯βπ)(πΉβπ) β (β€β₯βπ΄)))) |
62 | 11, 61 | stoic3 1779 |
. . 3
β’ ((πΉ:ββΆβ β§
βπ β β
(πΉβπ) < (πΉβ(π + 1)) β§ π΄ β β) β (π β β β ((πΉβπ) β (β€β₯βπ΄) β βπ β
(β€β₯βπ)(πΉβπ) β (β€β₯βπ΄)))) |
63 | 62 | reximdvai 3159 |
. 2
β’ ((πΉ:ββΆβ β§
βπ β β
(πΉβπ) < (πΉβ(π + 1)) β§ π΄ β β) β (βπ β β (πΉβπ) β (β€β₯βπ΄) β βπ β β βπ β
(β€β₯βπ)(πΉβπ) β (β€β₯βπ΄))) |
64 | 1, 63 | mpd 15 |
1
β’ ((πΉ:ββΆβ β§
βπ β β
(πΉβπ) < (πΉβ(π + 1)) β§ π΄ β β) β βπ β β βπ β
(β€β₯βπ)(πΉβπ) β (β€β₯βπ΄)) |