Step | Hyp | Ref
| Expression |
1 | | xlimmnfv.m |
. . . . 5
β’ (π β π β β€) |
2 | 1 | ad2antrr 723 |
. . . 4
β’ (((π β§ πΉ~~>*-β) β§ π₯ β β) β π β β€) |
3 | | xlimmnfv.z |
. . . 4
β’ π =
(β€β₯βπ) |
4 | | xlimmnfv.f |
. . . . 5
β’ (π β πΉ:πβΆβ*) |
5 | 4 | ad2antrr 723 |
. . . 4
β’ (((π β§ πΉ~~>*-β) β§ π₯ β β) β πΉ:πβΆβ*) |
6 | | simplr 766 |
. . . 4
β’ (((π β§ πΉ~~>*-β) β§ π₯ β β) β πΉ~~>*-β) |
7 | | simpr 484 |
. . . 4
β’ (((π β§ πΉ~~>*-β) β§ π₯ β β) β π₯ β β) |
8 | 2, 3, 5, 6, 7 | xlimmnfvlem1 45120 |
. . 3
β’ (((π β§ πΉ~~>*-β) β§ π₯ β β) β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) |
9 | 8 | ralrimiva 3140 |
. 2
β’ ((π β§ πΉ~~>*-β) β βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) |
10 | | nfv 1909 |
. . . 4
β’
β²ππ |
11 | | nfcv 2897 |
. . . . 5
β’
β²πβ |
12 | | nfcv 2897 |
. . . . . 6
β’
β²ππ |
13 | | nfra1 3275 |
. . . . . 6
β’
β²πβπ β (β€β₯βπ)(πΉβπ) β€ π₯ |
14 | 12, 13 | nfrexw 3304 |
. . . . 5
β’
β²πβπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯ |
15 | 11, 14 | nfralw 3302 |
. . . 4
β’
β²πβπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯ |
16 | 10, 15 | nfan 1894 |
. . 3
β’
β²π(π β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) |
17 | | nfv 1909 |
. . . 4
β’
β²ππ |
18 | | nfcv 2897 |
. . . . 5
β’
β²πβ |
19 | | nfre1 3276 |
. . . . 5
β’
β²πβπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯ |
20 | 18, 19 | nfralw 3302 |
. . . 4
β’
β²πβπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯ |
21 | 17, 20 | nfan 1894 |
. . 3
β’
β²π(π β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) |
22 | 1 | adantr 480 |
. . 3
β’ ((π β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) β π β β€) |
23 | 4 | adantr 480 |
. . 3
β’ ((π β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) β πΉ:πβΆβ*) |
24 | | nfv 1909 |
. . . . . 6
β’
β²π π¦ β β |
25 | 21, 24 | nfan 1894 |
. . . . 5
β’
β²π((π β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) β§ π¦ β β) |
26 | 4 | 3ad2ant1 1130 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π β§ π β (β€β₯βπ)) β πΉ:πβΆβ*) |
27 | 3 | uztrn2 12845 |
. . . . . . . . . . . . . 14
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
28 | 27 | 3adant1 1127 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π β§ π β (β€β₯βπ)) β π β π) |
29 | 26, 28 | ffvelcdmd 7081 |
. . . . . . . . . . . 12
β’ ((π β§ π β π β§ π β (β€β₯βπ)) β (πΉβπ) β
β*) |
30 | 29 | ad5ant134 1364 |
. . . . . . . . . . 11
β’
(((((π β§ π¦ β β) β§ π β π) β§ π β (β€β₯βπ)) β§ (πΉβπ) β€ (π¦ β 1)) β (πΉβπ) β
β*) |
31 | | simp-4r 781 |
. . . . . . . . . . . 12
β’
(((((π β§ π¦ β β) β§ π β π) β§ π β (β€β₯βπ)) β§ (πΉβπ) β€ (π¦ β 1)) β π¦ β β) |
32 | | peano2rem 11531 |
. . . . . . . . . . . . 13
β’ (π¦ β β β (π¦ β 1) β
β) |
33 | 32 | rexrd 11268 |
. . . . . . . . . . . 12
β’ (π¦ β β β (π¦ β 1) β
β*) |
34 | 31, 33 | syl 17 |
. . . . . . . . . . 11
β’
(((((π β§ π¦ β β) β§ π β π) β§ π β (β€β₯βπ)) β§ (πΉβπ) β€ (π¦ β 1)) β (π¦ β 1) β
β*) |
35 | | rexr 11264 |
. . . . . . . . . . . 12
β’ (π¦ β β β π¦ β
β*) |
36 | 35 | ad4antlr 730 |
. . . . . . . . . . 11
β’
(((((π β§ π¦ β β) β§ π β π) β§ π β (β€β₯βπ)) β§ (πΉβπ) β€ (π¦ β 1)) β π¦ β β*) |
37 | | simpr 484 |
. . . . . . . . . . 11
β’
(((((π β§ π¦ β β) β§ π β π) β§ π β (β€β₯βπ)) β§ (πΉβπ) β€ (π¦ β 1)) β (πΉβπ) β€ (π¦ β 1)) |
38 | 31 | ltm1d 12150 |
. . . . . . . . . . 11
β’
(((((π β§ π¦ β β) β§ π β π) β§ π β (β€β₯βπ)) β§ (πΉβπ) β€ (π¦ β 1)) β (π¦ β 1) < π¦) |
39 | 30, 34, 36, 37, 38 | xrlelttrd 13145 |
. . . . . . . . . 10
β’
(((((π β§ π¦ β β) β§ π β π) β§ π β (β€β₯βπ)) β§ (πΉβπ) β€ (π¦ β 1)) β (πΉβπ) < π¦) |
40 | 39 | ex 412 |
. . . . . . . . 9
β’ ((((π β§ π¦ β β) β§ π β π) β§ π β (β€β₯βπ)) β ((πΉβπ) β€ (π¦ β 1) β (πΉβπ) < π¦)) |
41 | 40 | ralimdva 3161 |
. . . . . . . 8
β’ (((π β§ π¦ β β) β§ π β π) β (βπ β (β€β₯βπ)(πΉβπ) β€ (π¦ β 1) β βπ β (β€β₯βπ)(πΉβπ) < π¦)) |
42 | 41 | imp 406 |
. . . . . . 7
β’ ((((π β§ π¦ β β) β§ π β π) β§ βπ β (β€β₯βπ)(πΉβπ) β€ (π¦ β 1)) β βπ β
(β€β₯βπ)(πΉβπ) < π¦) |
43 | 42 | adantl3r 747 |
. . . . . 6
β’
(((((π β§
βπ₯ β β
βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) β§ π¦ β β) β§ π β π) β§ βπ β (β€β₯βπ)(πΉβπ) β€ (π¦ β 1)) β βπ β
(β€β₯βπ)(πΉβπ) < π¦) |
44 | 43 | 3impa 1107 |
. . . . 5
β’ ((((π β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) β§ π¦ β β) β§ π β π β§ βπ β (β€β₯βπ)(πΉβπ) β€ (π¦ β 1)) β βπ β
(β€β₯βπ)(πΉβπ) < π¦) |
45 | 32 | adantl 481 |
. . . . . . 7
β’
((βπ₯ β
β βπ β
π βπ β
(β€β₯βπ)(πΉβπ) β€ π₯ β§ π¦ β β) β (π¦ β 1) β β) |
46 | | simpl 482 |
. . . . . . 7
β’
((βπ₯ β
β βπ β
π βπ β
(β€β₯βπ)(πΉβπ) β€ π₯ β§ π¦ β β) β βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) |
47 | | breq2 5145 |
. . . . . . . . . 10
β’ (π₯ = (π¦ β 1) β ((πΉβπ) β€ π₯ β (πΉβπ) β€ (π¦ β 1))) |
48 | 47 | ralbidv 3171 |
. . . . . . . . 9
β’ (π₯ = (π¦ β 1) β (βπ β
(β€β₯βπ)(πΉβπ) β€ π₯ β βπ β (β€β₯βπ)(πΉβπ) β€ (π¦ β 1))) |
49 | 48 | rexbidv 3172 |
. . . . . . . 8
β’ (π₯ = (π¦ β 1) β (βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ (π¦ β 1))) |
50 | 49 | rspcva 3604 |
. . . . . . 7
β’ (((π¦ β 1) β β β§
βπ₯ β β
βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ (π¦ β 1)) |
51 | 45, 46, 50 | syl2anc 583 |
. . . . . 6
β’
((βπ₯ β
β βπ β
π βπ β
(β€β₯βπ)(πΉβπ) β€ π₯ β§ π¦ β β) β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ (π¦ β 1)) |
52 | 51 | adantll 711 |
. . . . 5
β’ (((π β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) β§ π¦ β β) β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ (π¦ β 1)) |
53 | 25, 44, 52 | reximdd 44416 |
. . . 4
β’ (((π β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) β§ π¦ β β) β βπ β π βπ β (β€β₯βπ)(πΉβπ) < π¦) |
54 | 53 | ralrimiva 3140 |
. . 3
β’ ((π β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) β βπ¦ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) < π¦) |
55 | 16, 21, 22, 3, 23, 54 | xlimmnfvlem2 45121 |
. 2
β’ ((π β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) β πΉ~~>*-β) |
56 | 9, 55 | impbida 798 |
1
β’ (π β (πΉ~~>*-β β βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯)) |