Step | Hyp | Ref
| Expression |
1 | | lmnn.4 |
. 2
β’ (π β π β π) |
2 | | rpreccl 12949 |
. . . . . . . 8
β’ (π₯ β β+
β (1 / π₯) β
β+) |
3 | 2 | adantl 483 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β (1 /
π₯) β
β+) |
4 | 3 | rpred 12965 |
. . . . . 6
β’ ((π β§ π₯ β β+) β (1 /
π₯) β
β) |
5 | 3 | rpge0d 12969 |
. . . . . 6
β’ ((π β§ π₯ β β+) β 0 β€ (1
/ π₯)) |
6 | | flge0nn0 13734 |
. . . . . 6
β’ (((1 /
π₯) β β β§ 0
β€ (1 / π₯)) β
(ββ(1 / π₯))
β β0) |
7 | 4, 5, 6 | syl2anc 585 |
. . . . 5
β’ ((π β§ π₯ β β+) β
(ββ(1 / π₯))
β β0) |
8 | | nn0p1nn 12460 |
. . . . 5
β’
((ββ(1 / π₯)) β β0 β
((ββ(1 / π₯)) +
1) β β) |
9 | 7, 8 | syl 17 |
. . . 4
β’ ((π β§ π₯ β β+) β
((ββ(1 / π₯)) +
1) β β) |
10 | | lmnn.3 |
. . . . . . . 8
β’ (π β π· β (βMetβπ)) |
11 | 10 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(1 / π₯)) + 1))) β π· β (βMetβπ)) |
12 | | lmnn.5 |
. . . . . . . . 9
β’ (π β πΉ:ββΆπ) |
13 | 12 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(1 / π₯)) + 1))) β πΉ:ββΆπ) |
14 | | eluznn 12851 |
. . . . . . . . 9
β’
((((ββ(1 / π₯)) + 1) β β β§ π β
(β€β₯β((ββ(1 / π₯)) + 1))) β π β β) |
15 | 9, 14 | sylan 581 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(1 / π₯)) + 1))) β π β β) |
16 | 13, 15 | ffvelcdmd 7040 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(1 / π₯)) + 1))) β (πΉβπ) β π) |
17 | 1 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(1 / π₯)) + 1))) β π β π) |
18 | | xmetcl 23707 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ (πΉβπ) β π β§ π β π) β ((πΉβπ)π·π) β
β*) |
19 | 11, 16, 17, 18 | syl3anc 1372 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(1 / π₯)) + 1))) β ((πΉβπ)π·π) β
β*) |
20 | 15 | nnrecred 12212 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(1 / π₯)) + 1))) β (1 / π) β β) |
21 | 20 | rexrd 11213 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(1 / π₯)) + 1))) β (1 / π) β
β*) |
22 | | rpxr 12932 |
. . . . . . 7
β’ (π₯ β β+
β π₯ β
β*) |
23 | 22 | ad2antlr 726 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(1 / π₯)) + 1))) β π₯ β β*) |
24 | | lmnn.6 |
. . . . . . . 8
β’ ((π β§ π β β) β ((πΉβπ)π·π) < (1 / π)) |
25 | 24 | adantlr 714 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β β) β ((πΉβπ)π·π) < (1 / π)) |
26 | 15, 25 | syldan 592 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(1 / π₯)) + 1))) β ((πΉβπ)π·π) < (1 / π)) |
27 | 4 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(1 / π₯)) + 1))) β (1 / π₯) β β) |
28 | 9 | nnred 12176 |
. . . . . . . . 9
β’ ((π β§ π₯ β β+) β
((ββ(1 / π₯)) +
1) β β) |
29 | 28 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(1 / π₯)) + 1))) β ((ββ(1 / π₯)) + 1) β
β) |
30 | 15 | nnred 12176 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(1 / π₯)) + 1))) β π β β) |
31 | | flltp1 13714 |
. . . . . . . . 9
β’ ((1 /
π₯) β β β (1
/ π₯) <
((ββ(1 / π₯)) +
1)) |
32 | 27, 31 | syl 17 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(1 / π₯)) + 1))) β (1 / π₯) < ((ββ(1 / π₯)) + 1)) |
33 | | eluzle 12784 |
. . . . . . . . 9
β’ (π β
(β€β₯β((ββ(1 / π₯)) + 1)) β ((ββ(1 / π₯)) + 1) β€ π) |
34 | 33 | adantl 483 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(1 / π₯)) + 1))) β ((ββ(1 / π₯)) + 1) β€ π) |
35 | 27, 29, 30, 32, 34 | ltletrd 11323 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(1 / π₯)) + 1))) β (1 / π₯) < π) |
36 | | simplr 768 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(1 / π₯)) + 1))) β π₯ β β+) |
37 | | rpregt0 12937 |
. . . . . . . . 9
β’ (π₯ β β+
β (π₯ β β
β§ 0 < π₯)) |
38 | | nnrp 12934 |
. . . . . . . . . 10
β’ (π β β β π β
β+) |
39 | 38 | rpregt0d 12971 |
. . . . . . . . 9
β’ (π β β β (π β β β§ 0 <
π)) |
40 | | ltrec1 12050 |
. . . . . . . . 9
β’ (((π₯ β β β§ 0 <
π₯) β§ (π β β β§ 0 <
π)) β ((1 / π₯) < π β (1 / π) < π₯)) |
41 | 37, 39, 40 | syl2an 597 |
. . . . . . . 8
β’ ((π₯ β β+
β§ π β β)
β ((1 / π₯) < π β (1 / π) < π₯)) |
42 | 36, 15, 41 | syl2anc 585 |
. . . . . . 7
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(1 / π₯)) + 1))) β ((1 / π₯) < π β (1 / π) < π₯)) |
43 | 35, 42 | mpbid 231 |
. . . . . 6
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(1 / π₯)) + 1))) β (1 / π) < π₯) |
44 | 19, 21, 23, 26, 43 | xrlttrd 13087 |
. . . . 5
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯β((ββ(1 / π₯)) + 1))) β ((πΉβπ)π·π) < π₯) |
45 | 44 | ralrimiva 3140 |
. . . 4
β’ ((π β§ π₯ β β+) β
βπ β
(β€β₯β((ββ(1 / π₯)) + 1))((πΉβπ)π·π) < π₯) |
46 | | fveq2 6846 |
. . . . . 6
β’ (π = ((ββ(1 / π₯)) + 1) β
(β€β₯βπ) =
(β€β₯β((ββ(1 / π₯)) + 1))) |
47 | 46 | raleqdv 3312 |
. . . . 5
β’ (π = ((ββ(1 / π₯)) + 1) β (βπ β
(β€β₯βπ)((πΉβπ)π·π) < π₯ β βπ β
(β€β₯β((ββ(1 / π₯)) + 1))((πΉβπ)π·π) < π₯)) |
48 | 47 | rspcev 3583 |
. . . 4
β’
((((ββ(1 / π₯)) + 1) β β β§ βπ β
(β€β₯β((ββ(1 / π₯)) + 1))((πΉβπ)π·π) < π₯) β βπ β β βπ β (β€β₯βπ)((πΉβπ)π·π) < π₯) |
49 | 9, 45, 48 | syl2anc 585 |
. . 3
β’ ((π β§ π₯ β β+) β
βπ β β
βπ β
(β€β₯βπ)((πΉβπ)π·π) < π₯) |
50 | 49 | ralrimiva 3140 |
. 2
β’ (π β βπ₯ β β+ βπ β β βπ β
(β€β₯βπ)((πΉβπ)π·π) < π₯) |
51 | | lmnn.2 |
. . 3
β’ π½ = (MetOpenβπ·) |
52 | | nnuz 12814 |
. . 3
β’ β =
(β€β₯β1) |
53 | | 1zzd 12542 |
. . 3
β’ (π β 1 β
β€) |
54 | | eqidd 2734 |
. . 3
β’ ((π β§ π β β) β (πΉβπ) = (πΉβπ)) |
55 | 51, 10, 52, 53, 54, 12 | lmmbrf 24649 |
. 2
β’ (π β (πΉ(βπ‘βπ½)π β (π β π β§ βπ₯ β β+ βπ β β βπ β
(β€β₯βπ)((πΉβπ)π·π) < π₯))) |
56 | 1, 50, 55 | mpbir2and 712 |
1
β’ (π β πΉ(βπ‘βπ½)π) |