Step | Hyp | Ref
| Expression |
1 | | xlimpnfv.m |
. . . . 5
β’ (π β π β β€) |
2 | 1 | ad2antrr 723 |
. . . 4
β’ (((π β§ πΉ~~>*+β) β§ π₯ β β) β π β β€) |
3 | | xlimpnfv.z |
. . . 4
β’ π =
(β€β₯βπ) |
4 | | xlimpnfv.f |
. . . . 5
β’ (π β πΉ:πβΆβ*) |
5 | 4 | ad2antrr 723 |
. . . 4
β’ (((π β§ πΉ~~>*+β) β§ π₯ β β) β πΉ:πβΆβ*) |
6 | | simplr 766 |
. . . 4
β’ (((π β§ πΉ~~>*+β) β§ π₯ β β) β πΉ~~>*+β) |
7 | | simpr 484 |
. . . 4
β’ (((π β§ πΉ~~>*+β) β§ π₯ β β) β π₯ β β) |
8 | 2, 3, 5, 6, 7 | xlimpnfvlem1 45124 |
. . 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 | | simp-4r 781 |
. . . . . . . . . . . 12
β’
(((((π β§ π¦ β β) β§ π β π) β§ π β (β€β₯βπ)) β§ (π¦ + 1) β€ (πΉβπ)) β π¦ β β) |
27 | | rexr 11264 |
. . . . . . . . . . . 12
β’ (π¦ β β β π¦ β
β*) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . 11
β’
(((((π β§ π¦ β β) β§ π β π) β§ π β (β€β₯βπ)) β§ (π¦ + 1) β€ (πΉβπ)) β π¦ β β*) |
29 | | peano2re 11391 |
. . . . . . . . . . . . 13
β’ (π¦ β β β (π¦ + 1) β
β) |
30 | 29 | rexrd 11268 |
. . . . . . . . . . . 12
β’ (π¦ β β β (π¦ + 1) β
β*) |
31 | 26, 30 | syl 17 |
. . . . . . . . . . 11
β’
(((((π β§ π¦ β β) β§ π β π) β§ π β (β€β₯βπ)) β§ (π¦ + 1) β€ (πΉβπ)) β (π¦ + 1) β
β*) |
32 | 4 | 3ad2ant1 1130 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π β§ π β (β€β₯βπ)) β πΉ:πβΆβ*) |
33 | 3 | uztrn2 12845 |
. . . . . . . . . . . . . 14
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
34 | 33 | 3adant1 1127 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π β§ π β (β€β₯βπ)) β π β π) |
35 | 32, 34 | ffvelcdmd 7081 |
. . . . . . . . . . . 12
β’ ((π β§ π β π β§ π β (β€β₯βπ)) β (πΉβπ) β
β*) |
36 | 35 | ad5ant134 1364 |
. . . . . . . . . . 11
β’
(((((π β§ π¦ β β) β§ π β π) β§ π β (β€β₯βπ)) β§ (π¦ + 1) β€ (πΉβπ)) β (πΉβπ) β
β*) |
37 | 26 | ltp1d 12148 |
. . . . . . . . . . 11
β’
(((((π β§ π¦ β β) β§ π β π) β§ π β (β€β₯βπ)) β§ (π¦ + 1) β€ (πΉβπ)) β π¦ < (π¦ + 1)) |
38 | | simpr 484 |
. . . . . . . . . . 11
β’
(((((π β§ π¦ β β) β§ π β π) β§ π β (β€β₯βπ)) β§ (π¦ + 1) β€ (πΉβπ)) β (π¦ + 1) β€ (πΉβπ)) |
39 | 28, 31, 36, 37, 38 | xrltletrd 13146 |
. . . . . . . . . 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 | 29 | adantl 481 |
. . . . . . 7
β’
((βπ₯ β
β βπ β
π βπ β
(β€β₯βπ)π₯ β€ (πΉβπ) β§ π¦ β β) β (π¦ + 1) β β) |
46 | | simpl 482 |
. . . . . . 7
β’
((βπ₯ β
β βπ β
π βπ β
(β€β₯βπ)π₯ β€ (πΉβπ) β§ π¦ β β) β βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ)) |
47 | | breq1 5144 |
. . . . . . . . . 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 | xlimpnfvlem2 45125 |
. 2
β’ ((π β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ)) β πΉ~~>*+β) |
56 | 9, 55 | impbida 798 |
1
β’ (π β (πΉ~~>*+β β βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ))) |