Step | Hyp | Ref
| Expression |
1 | | xlimpnfv.m |
. . . . 5
β’ (π β π β β€) |
2 | 1 | ad2antrr 725 |
. . . 4
β’ (((π β§ πΉ~~>*+β) β§ π₯ β β) β π β β€) |
3 | | xlimpnfv.z |
. . . 4
β’ π =
(β€β₯βπ) |
4 | | xlimpnfv.f |
. . . . 5
β’ (π β πΉ:πβΆβ*) |
5 | 4 | ad2antrr 725 |
. . . 4
β’ (((π β§ πΉ~~>*+β) β§ π₯ β β) β πΉ:πβΆβ*) |
6 | | simplr 768 |
. . . 4
β’ (((π β§ πΉ~~>*+β) β§ π₯ β β) β πΉ~~>*+β) |
7 | | simpr 486 |
. . . 4
β’ (((π β§ πΉ~~>*+β) β§ π₯ β β) β π₯ β β) |
8 | 2, 3, 5, 6, 7 | xlimpnfvlem1 44163 |
. . 3
β’ (((π β§ πΉ~~>*+β) β§ π₯ β β) β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ)) |
9 | 8 | ralrimiva 3140 |
. 2
β’ ((π β§ πΉ~~>*+β) β βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ)) |
10 | | nfv 1918 |
. . . 4
β’
β²ππ |
11 | | nfcv 2904 |
. . . . 5
β’
β²πβ |
12 | | nfcv 2904 |
. . . . . 6
β’
β²ππ |
13 | | nfra1 3266 |
. . . . . 6
β’
β²πβπ β (β€β₯βπ)π₯ β€ (πΉβπ) |
14 | 12, 13 | nfrexw 3295 |
. . . . 5
β’
β²πβπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ) |
15 | 11, 14 | nfralw 3293 |
. . . 4
β’
β²πβπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ) |
16 | 10, 15 | nfan 1903 |
. . 3
β’
β²π(π β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ)) |
17 | | nfv 1918 |
. . . 4
β’
β²ππ |
18 | | nfcv 2904 |
. . . . 5
β’
β²πβ |
19 | | nfre1 3267 |
. . . . 5
β’
β²πβπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ) |
20 | 18, 19 | nfralw 3293 |
. . . 4
β’
β²πβπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ) |
21 | 17, 20 | nfan 1903 |
. . 3
β’
β²π(π β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ)) |
22 | 1 | adantr 482 |
. . 3
β’ ((π β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ)) β π β β€) |
23 | 4 | adantr 482 |
. . 3
β’ ((π β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ)) β πΉ:πβΆβ*) |
24 | | nfv 1918 |
. . . . . 6
β’
β²π π¦ β β |
25 | 21, 24 | nfan 1903 |
. . . . 5
β’
β²π((π β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ)) β§ π¦ β β) |
26 | | simp-4r 783 |
. . . . . . . . . . . 12
β’
(((((π β§ π¦ β β) β§ π β π) β§ π β (β€β₯βπ)) β§ (π¦ + 1) β€ (πΉβπ)) β π¦ β β) |
27 | | rexr 11206 |
. . . . . . . . . . . 12
β’ (π¦ β β β π¦ β
β*) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . 11
β’
(((((π β§ π¦ β β) β§ π β π) β§ π β (β€β₯βπ)) β§ (π¦ + 1) β€ (πΉβπ)) β π¦ β β*) |
29 | | peano2re 11333 |
. . . . . . . . . . . . 13
β’ (π¦ β β β (π¦ + 1) β
β) |
30 | 29 | rexrd 11210 |
. . . . . . . . . . . 12
β’ (π¦ β β β (π¦ + 1) β
β*) |
31 | 26, 30 | syl 17 |
. . . . . . . . . . 11
β’
(((((π β§ π¦ β β) β§ π β π) β§ π β (β€β₯βπ)) β§ (π¦ + 1) β€ (πΉβπ)) β (π¦ + 1) β
β*) |
32 | 4 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π β§ π β (β€β₯βπ)) β πΉ:πβΆβ*) |
33 | 3 | uztrn2 12787 |
. . . . . . . . . . . . . 14
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
34 | 33 | 3adant1 1131 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π β§ π β (β€β₯βπ)) β π β π) |
35 | 32, 34 | ffvelcdmd 7037 |
. . . . . . . . . . . 12
β’ ((π β§ π β π β§ π β (β€β₯βπ)) β (πΉβπ) β
β*) |
36 | 35 | ad5ant134 1368 |
. . . . . . . . . . 11
β’
(((((π β§ π¦ β β) β§ π β π) β§ π β (β€β₯βπ)) β§ (π¦ + 1) β€ (πΉβπ)) β (πΉβπ) β
β*) |
37 | 26 | ltp1d 12090 |
. . . . . . . . . . 11
β’
(((((π β§ π¦ β β) β§ π β π) β§ π β (β€β₯βπ)) β§ (π¦ + 1) β€ (πΉβπ)) β π¦ < (π¦ + 1)) |
38 | | simpr 486 |
. . . . . . . . . . 11
β’
(((((π β§ π¦ β β) β§ π β π) β§ π β (β€β₯βπ)) β§ (π¦ + 1) β€ (πΉβπ)) β (π¦ + 1) β€ (πΉβπ)) |
39 | 28, 31, 36, 37, 38 | xrltletrd 13086 |
. . . . . . . . . 10
β’
(((((π β§ π¦ β β) β§ π β π) β§ π β (β€β₯βπ)) β§ (π¦ + 1) β€ (πΉβπ)) β π¦ < (πΉβπ)) |
40 | 39 | ex 414 |
. . . . . . . . 9
β’ ((((π β§ π¦ β β) β§ π β π) β§ π β (β€β₯βπ)) β ((π¦ + 1) β€ (πΉβπ) β π¦ < (πΉβπ))) |
41 | 40 | ralimdva 3161 |
. . . . . . . 8
β’ (((π β§ π¦ β β) β§ π β π) β (βπ β (β€β₯βπ)(π¦ + 1) β€ (πΉβπ) β βπ β (β€β₯βπ)π¦ < (πΉβπ))) |
42 | 41 | imp 408 |
. . . . . . 7
β’ ((((π β§ π¦ β β) β§ π β π) β§ βπ β (β€β₯βπ)(π¦ + 1) β€ (πΉβπ)) β βπ β (β€β₯βπ)π¦ < (πΉβπ)) |
43 | 42 | adantl3r 749 |
. . . . . 6
β’
(((((π β§
βπ₯ β β
βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ)) β§ π¦ β β) β§ π β π) β§ βπ β (β€β₯βπ)(π¦ + 1) β€ (πΉβπ)) β βπ β (β€β₯βπ)π¦ < (πΉβπ)) |
44 | 43 | 3impa 1111 |
. . . . 5
β’ ((((π β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ)) β§ π¦ β β) β§ π β π β§ βπ β (β€β₯βπ)(π¦ + 1) β€ (πΉβπ)) β βπ β (β€β₯βπ)π¦ < (πΉβπ)) |
45 | 29 | adantl 483 |
. . . . . . 7
β’
((βπ₯ β
β βπ β
π βπ β
(β€β₯βπ)π₯ β€ (πΉβπ) β§ π¦ β β) β (π¦ + 1) β β) |
46 | | simpl 484 |
. . . . . . 7
β’
((βπ₯ β
β βπ β
π βπ β
(β€β₯βπ)π₯ β€ (πΉβπ) β§ π¦ β β) β βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ)) |
47 | | breq1 5109 |
. . . . . . . . . 10
β’ (π₯ = (π¦ + 1) β (π₯ β€ (πΉβπ) β (π¦ + 1) β€ (πΉβπ))) |
48 | 47 | ralbidv 3171 |
. . . . . . . . 9
β’ (π₯ = (π¦ + 1) β (βπ β (β€β₯βπ)π₯ β€ (πΉβπ) β βπ β (β€β₯βπ)(π¦ + 1) β€ (πΉβπ))) |
49 | 48 | rexbidv 3172 |
. . . . . . . 8
β’ (π₯ = (π¦ + 1) β (βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ) β βπ β π βπ β (β€β₯βπ)(π¦ + 1) β€ (πΉβπ))) |
50 | 49 | rspcva 3578 |
. . . . . . 7
β’ (((π¦ + 1) β β β§
βπ₯ β β
βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ)) β βπ β π βπ β (β€β₯βπ)(π¦ + 1) β€ (πΉβπ)) |
51 | 45, 46, 50 | syl2anc 585 |
. . . . . 6
β’
((βπ₯ β
β βπ β
π βπ β
(β€β₯βπ)π₯ β€ (πΉβπ) β§ π¦ β β) β βπ β π βπ β (β€β₯βπ)(π¦ + 1) β€ (πΉβπ)) |
52 | 51 | adantll 713 |
. . . . 5
β’ (((π β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ)) β§ π¦ β β) β βπ β π βπ β (β€β₯βπ)(π¦ + 1) β€ (πΉβπ)) |
53 | 25, 44, 52 | reximdd 43450 |
. . . 4
β’ (((π β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ)) β§ π¦ β β) β βπ β π βπ β (β€β₯βπ)π¦ < (πΉβπ)) |
54 | 53 | ralrimiva 3140 |
. . 3
β’ ((π β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ)) β βπ¦ β β βπ β π βπ β (β€β₯βπ)π¦ < (πΉβπ)) |
55 | 16, 21, 22, 3, 23, 54 | xlimpnfvlem2 44164 |
. 2
β’ ((π β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ)) β πΉ~~>*+β) |
56 | 9, 55 | impbida 800 |
1
β’ (π β (πΉ~~>*+β β βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ))) |