Step | Hyp | Ref
| Expression |
1 | | rpnnen1lem.n |
. . . 4
β’ β
β V |
2 | 1 | mptex 7221 |
. . 3
β’ (π β β β¦
(sup(π, β, < ) /
π)) β
V |
3 | | rpnnen1lem.2 |
. . . 4
β’ πΉ = (π₯ β β β¦ (π β β β¦ (sup(π, β, < ) / π))) |
4 | 3 | fvmpt2 7006 |
. . 3
β’ ((π₯ β β β§ (π β β β¦
(sup(π, β, < ) /
π)) β V) β (πΉβπ₯) = (π β β β¦ (sup(π, β, < ) / π))) |
5 | 2, 4 | mpan2 689 |
. 2
β’ (π₯ β β β (πΉβπ₯) = (π β β β¦ (sup(π, β, < ) / π))) |
6 | | rpnnen1lem.1 |
. . . . . . 7
β’ π = {π β β€ β£ (π / π) < π₯} |
7 | | ssrab2 4076 |
. . . . . . 7
β’ {π β β€ β£ (π / π) < π₯} β β€ |
8 | 6, 7 | eqsstri 4015 |
. . . . . 6
β’ π β
β€ |
9 | 8 | a1i 11 |
. . . . . . 7
β’ ((π₯ β β β§ π β β) β π β
β€) |
10 | | nnre 12215 |
. . . . . . . . . . . 12
β’ (π β β β π β
β) |
11 | | remulcl 11191 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π₯ β β) β (π Β· π₯) β β) |
12 | 11 | ancoms 459 |
. . . . . . . . . . . 12
β’ ((π₯ β β β§ π β β) β (π Β· π₯) β β) |
13 | 10, 12 | sylan2 593 |
. . . . . . . . . . 11
β’ ((π₯ β β β§ π β β) β (π Β· π₯) β β) |
14 | | btwnz 12661 |
. . . . . . . . . . . 12
β’ ((π Β· π₯) β β β (βπ β β€ π < (π Β· π₯) β§ βπ β β€ (π Β· π₯) < π)) |
15 | 14 | simpld 495 |
. . . . . . . . . . 11
β’ ((π Β· π₯) β β β βπ β β€ π < (π Β· π₯)) |
16 | 13, 15 | syl 17 |
. . . . . . . . . 10
β’ ((π₯ β β β§ π β β) β
βπ β β€
π < (π Β· π₯)) |
17 | | zre 12558 |
. . . . . . . . . . . . 13
β’ (π β β€ β π β
β) |
18 | 17 | adantl 482 |
. . . . . . . . . . . 12
β’ (((π₯ β β β§ π β β) β§ π β β€) β π β
β) |
19 | | simpll 765 |
. . . . . . . . . . . 12
β’ (((π₯ β β β§ π β β) β§ π β β€) β π₯ β
β) |
20 | | nngt0 12239 |
. . . . . . . . . . . . . 14
β’ (π β β β 0 <
π) |
21 | 10, 20 | jca 512 |
. . . . . . . . . . . . 13
β’ (π β β β (π β β β§ 0 <
π)) |
22 | 21 | ad2antlr 725 |
. . . . . . . . . . . 12
β’ (((π₯ β β β§ π β β) β§ π β β€) β (π β β β§ 0 <
π)) |
23 | | ltdivmul 12085 |
. . . . . . . . . . . 12
β’ ((π β β β§ π₯ β β β§ (π β β β§ 0 <
π)) β ((π / π) < π₯ β π < (π Β· π₯))) |
24 | 18, 19, 22, 23 | syl3anc 1371 |
. . . . . . . . . . 11
β’ (((π₯ β β β§ π β β) β§ π β β€) β ((π / π) < π₯ β π < (π Β· π₯))) |
25 | 24 | rexbidva 3176 |
. . . . . . . . . 10
β’ ((π₯ β β β§ π β β) β
(βπ β β€
(π / π) < π₯ β βπ β β€ π < (π Β· π₯))) |
26 | 16, 25 | mpbird 256 |
. . . . . . . . 9
β’ ((π₯ β β β§ π β β) β
βπ β β€
(π / π) < π₯) |
27 | | rabn0 4384 |
. . . . . . . . 9
β’ ({π β β€ β£ (π / π) < π₯} β β
β βπ β β€ (π / π) < π₯) |
28 | 26, 27 | sylibr 233 |
. . . . . . . 8
β’ ((π₯ β β β§ π β β) β {π β β€ β£ (π / π) < π₯} β β
) |
29 | 6 | neeq1i 3005 |
. . . . . . . 8
β’ (π β β
β {π β β€ β£ (π / π) < π₯} β β
) |
30 | 28, 29 | sylibr 233 |
. . . . . . 7
β’ ((π₯ β β β§ π β β) β π β β
) |
31 | 6 | reqabi 3454 |
. . . . . . . . . 10
β’ (π β π β (π β β€ β§ (π / π) < π₯)) |
32 | 10 | ad2antlr 725 |
. . . . . . . . . . . . . 14
β’ (((π₯ β β β§ π β β) β§ π β β€) β π β
β) |
33 | 32, 19, 11 | syl2anc 584 |
. . . . . . . . . . . . 13
β’ (((π₯ β β β§ π β β) β§ π β β€) β (π Β· π₯) β β) |
34 | | ltle 11298 |
. . . . . . . . . . . . 13
β’ ((π β β β§ (π Β· π₯) β β) β (π < (π Β· π₯) β π β€ (π Β· π₯))) |
35 | 18, 33, 34 | syl2anc 584 |
. . . . . . . . . . . 12
β’ (((π₯ β β β§ π β β) β§ π β β€) β (π < (π Β· π₯) β π β€ (π Β· π₯))) |
36 | 24, 35 | sylbid 239 |
. . . . . . . . . . 11
β’ (((π₯ β β β§ π β β) β§ π β β€) β ((π / π) < π₯ β π β€ (π Β· π₯))) |
37 | 36 | impr 455 |
. . . . . . . . . 10
β’ (((π₯ β β β§ π β β) β§ (π β β€ β§ (π / π) < π₯)) β π β€ (π Β· π₯)) |
38 | 31, 37 | sylan2b 594 |
. . . . . . . . 9
β’ (((π₯ β β β§ π β β) β§ π β π) β π β€ (π Β· π₯)) |
39 | 38 | ralrimiva 3146 |
. . . . . . . 8
β’ ((π₯ β β β§ π β β) β
βπ β π π β€ (π Β· π₯)) |
40 | | breq2 5151 |
. . . . . . . . . 10
β’ (π¦ = (π Β· π₯) β (π β€ π¦ β π β€ (π Β· π₯))) |
41 | 40 | ralbidv 3177 |
. . . . . . . . 9
β’ (π¦ = (π Β· π₯) β (βπ β π π β€ π¦ β βπ β π π β€ (π Β· π₯))) |
42 | 41 | rspcev 3612 |
. . . . . . . 8
β’ (((π Β· π₯) β β β§ βπ β π π β€ (π Β· π₯)) β βπ¦ β β βπ β π π β€ π¦) |
43 | 13, 39, 42 | syl2anc 584 |
. . . . . . 7
β’ ((π₯ β β β§ π β β) β
βπ¦ β β
βπ β π π β€ π¦) |
44 | | suprzcl 12638 |
. . . . . . 7
β’ ((π β β€ β§ π β β
β§ βπ¦ β β βπ β π π β€ π¦) β sup(π, β, < ) β π) |
45 | 9, 30, 43, 44 | syl3anc 1371 |
. . . . . 6
β’ ((π₯ β β β§ π β β) β
sup(π, β, < )
β π) |
46 | 8, 45 | sselid 3979 |
. . . . 5
β’ ((π₯ β β β§ π β β) β
sup(π, β, < )
β β€) |
47 | | znq 12932 |
. . . . 5
β’
((sup(π, β,
< ) β β€ β§ π β β) β (sup(π, β, < ) / π) β
β) |
48 | 46, 47 | sylancom 588 |
. . . 4
β’ ((π₯ β β β§ π β β) β
(sup(π, β, < ) /
π) β
β) |
49 | | eqid 2732 |
. . . 4
β’ (π β β β¦
(sup(π, β, < ) /
π)) = (π β β β¦ (sup(π, β, < ) / π)) |
50 | 48, 49 | fmptd 7110 |
. . 3
β’ (π₯ β β β (π β β β¦
(sup(π, β, < ) /
π)):ββΆβ) |
51 | | rpnnen1lem.q |
. . . 4
β’ β
β V |
52 | 51, 1 | elmap 8861 |
. . 3
β’ ((π β β β¦
(sup(π, β, < ) /
π)) β (β
βm β) β (π β β β¦ (sup(π, β, < ) / π)):ββΆβ) |
53 | 50, 52 | sylibr 233 |
. 2
β’ (π₯ β β β (π β β β¦
(sup(π, β, < ) /
π)) β (β
βm β)) |
54 | 5, 53 | eqeltrd 2833 |
1
β’ (π₯ β β β (πΉβπ₯) β (β βm
β)) |