Step | Hyp | Ref
| Expression |
1 | | rpnnen1lem.1 |
. . . 4
β’ π = {π β β€ β£ (π / π) < π₯} |
2 | | rpnnen1lem.2 |
. . . 4
β’ πΉ = (π₯ β β β¦ (π β β β¦ (sup(π, β, < ) / π))) |
3 | | rpnnen1lem.n |
. . . 4
β’ β
β V |
4 | | rpnnen1lem.q |
. . . 4
β’ β
β V |
5 | 1, 2, 3, 4 | rpnnen1lem3 12928 |
. . 3
β’ (π₯ β β β
βπ β ran (πΉβπ₯)π β€ π₯) |
6 | 1, 2, 3, 4 | rpnnen1lem1 12927 |
. . . . . 6
β’ (π₯ β β β (πΉβπ₯) β (β βm
β)) |
7 | 4, 3 | elmap 8831 |
. . . . . 6
β’ ((πΉβπ₯) β (β βm β)
β (πΉβπ₯):ββΆβ) |
8 | 6, 7 | sylib 217 |
. . . . 5
β’ (π₯ β β β (πΉβπ₯):ββΆβ) |
9 | | frn 6695 |
. . . . . 6
β’ ((πΉβπ₯):ββΆβ β ran (πΉβπ₯) β β) |
10 | | qssre 12908 |
. . . . . 6
β’ β
β β |
11 | 9, 10 | sstrdi 3974 |
. . . . 5
β’ ((πΉβπ₯):ββΆβ β ran (πΉβπ₯) β β) |
12 | 8, 11 | syl 17 |
. . . 4
β’ (π₯ β β β ran
(πΉβπ₯) β β) |
13 | | 1nn 12188 |
. . . . . . . 8
β’ 1 β
β |
14 | 13 | ne0ii 4317 |
. . . . . . 7
β’ β
β β
|
15 | | fdm 6697 |
. . . . . . . 8
β’ ((πΉβπ₯):ββΆβ β dom (πΉβπ₯) = β) |
16 | 15 | neeq1d 2999 |
. . . . . . 7
β’ ((πΉβπ₯):ββΆβ β (dom (πΉβπ₯) β β
β β β
β
)) |
17 | 14, 16 | mpbiri 257 |
. . . . . 6
β’ ((πΉβπ₯):ββΆβ β dom (πΉβπ₯) β β
) |
18 | | dm0rn0 5900 |
. . . . . . 7
β’ (dom
(πΉβπ₯) = β
β ran (πΉβπ₯) = β
) |
19 | 18 | necon3bii 2992 |
. . . . . 6
β’ (dom
(πΉβπ₯) β β
β ran (πΉβπ₯) β β
) |
20 | 17, 19 | sylib 217 |
. . . . 5
β’ ((πΉβπ₯):ββΆβ β ran (πΉβπ₯) β β
) |
21 | 8, 20 | syl 17 |
. . . 4
β’ (π₯ β β β ran
(πΉβπ₯) β β
) |
22 | | breq2 5129 |
. . . . . . 7
β’ (π¦ = π₯ β (π β€ π¦ β π β€ π₯)) |
23 | 22 | ralbidv 3176 |
. . . . . 6
β’ (π¦ = π₯ β (βπ β ran (πΉβπ₯)π β€ π¦ β βπ β ran (πΉβπ₯)π β€ π₯)) |
24 | 23 | rspcev 3595 |
. . . . 5
β’ ((π₯ β β β§
βπ β ran (πΉβπ₯)π β€ π₯) β βπ¦ β β βπ β ran (πΉβπ₯)π β€ π¦) |
25 | 5, 24 | mpdan 685 |
. . . 4
β’ (π₯ β β β
βπ¦ β β
βπ β ran (πΉβπ₯)π β€ π¦) |
26 | | id 22 |
. . . 4
β’ (π₯ β β β π₯ β
β) |
27 | | suprleub 12145 |
. . . 4
β’ (((ran
(πΉβπ₯) β β β§ ran (πΉβπ₯) β β
β§ βπ¦ β β βπ β ran (πΉβπ₯)π β€ π¦) β§ π₯ β β) β (sup(ran (πΉβπ₯), β, < ) β€ π₯ β βπ β ran (πΉβπ₯)π β€ π₯)) |
28 | 12, 21, 25, 26, 27 | syl31anc 1373 |
. . 3
β’ (π₯ β β β (sup(ran
(πΉβπ₯), β, < ) β€ π₯ β βπ β ran (πΉβπ₯)π β€ π₯)) |
29 | 5, 28 | mpbird 256 |
. 2
β’ (π₯ β β β sup(ran
(πΉβπ₯), β, < ) β€ π₯) |
30 | 1, 2, 3, 4 | rpnnen1lem4 12929 |
. . . . . . . . 9
β’ (π₯ β β β sup(ran
(πΉβπ₯), β, < ) β
β) |
31 | | resubcl 11489 |
. . . . . . . . 9
β’ ((π₯ β β β§ sup(ran
(πΉβπ₯), β, < ) β β) β
(π₯ β sup(ran (πΉβπ₯), β, < )) β
β) |
32 | 30, 31 | mpdan 685 |
. . . . . . . 8
β’ (π₯ β β β (π₯ β sup(ran (πΉβπ₯), β, < )) β
β) |
33 | 32 | adantr 481 |
. . . . . . 7
β’ ((π₯ β β β§ sup(ran
(πΉβπ₯), β, < ) < π₯) β (π₯ β sup(ran (πΉβπ₯), β, < )) β
β) |
34 | | posdif 11672 |
. . . . . . . . . 10
β’ ((sup(ran
(πΉβπ₯), β, < ) β β β§ π₯ β β) β (sup(ran
(πΉβπ₯), β, < ) < π₯ β 0 < (π₯ β sup(ran (πΉβπ₯), β, < )))) |
35 | 30, 34 | mpancom 686 |
. . . . . . . . 9
β’ (π₯ β β β (sup(ran
(πΉβπ₯), β, < ) < π₯ β 0 < (π₯ β sup(ran (πΉβπ₯), β, < )))) |
36 | 35 | biimpa 477 |
. . . . . . . 8
β’ ((π₯ β β β§ sup(ran
(πΉβπ₯), β, < ) < π₯) β 0 < (π₯ β sup(ran (πΉβπ₯), β, < ))) |
37 | 36 | gt0ne0d 11743 |
. . . . . . 7
β’ ((π₯ β β β§ sup(ran
(πΉβπ₯), β, < ) < π₯) β (π₯ β sup(ran (πΉβπ₯), β, < )) β 0) |
38 | 33, 37 | rereccld 12006 |
. . . . . 6
β’ ((π₯ β β β§ sup(ran
(πΉβπ₯), β, < ) < π₯) β (1 / (π₯ β sup(ran (πΉβπ₯), β, < ))) β
β) |
39 | | arch 12434 |
. . . . . 6
β’ ((1 /
(π₯ β sup(ran (πΉβπ₯), β, < ))) β β β
βπ β β (1
/ (π₯ β sup(ran (πΉβπ₯), β, < ))) < π) |
40 | 38, 39 | syl 17 |
. . . . 5
β’ ((π₯ β β β§ sup(ran
(πΉβπ₯), β, < ) < π₯) β βπ β β (1 / (π₯ β sup(ran (πΉβπ₯), β, < ))) < π) |
41 | 40 | ex 413 |
. . . 4
β’ (π₯ β β β (sup(ran
(πΉβπ₯), β, < ) < π₯ β βπ β β (1 / (π₯ β sup(ran (πΉβπ₯), β, < ))) < π)) |
42 | 1, 2 | rpnnen1lem2 12926 |
. . . . . . . . 9
β’ ((π₯ β β β§ π β β) β
sup(π, β, < )
β β€) |
43 | 42 | zred 12631 |
. . . . . . . 8
β’ ((π₯ β β β§ π β β) β
sup(π, β, < )
β β) |
44 | 43 | 3adant3 1132 |
. . . . . . 7
β’ ((π₯ β β β§ π β β β§ (1 /
(π₯ β sup(ran (πΉβπ₯), β, < ))) < π) β sup(π, β, < ) β
β) |
45 | 44 | ltp1d 12109 |
. . . . . 6
β’ ((π₯ β β β§ π β β β§ (1 /
(π₯ β sup(ran (πΉβπ₯), β, < ))) < π) β sup(π, β, < ) < (sup(π, β, < ) +
1)) |
46 | 33, 36 | jca 512 |
. . . . . . . . . . . . 13
β’ ((π₯ β β β§ sup(ran
(πΉβπ₯), β, < ) < π₯) β ((π₯ β sup(ran (πΉβπ₯), β, < )) β β β§ 0
< (π₯ β sup(ran
(πΉβπ₯), β, < )))) |
47 | | nnre 12184 |
. . . . . . . . . . . . . 14
β’ (π β β β π β
β) |
48 | | nngt0 12208 |
. . . . . . . . . . . . . 14
β’ (π β β β 0 <
π) |
49 | 47, 48 | jca 512 |
. . . . . . . . . . . . 13
β’ (π β β β (π β β β§ 0 <
π)) |
50 | | ltrec1 12066 |
. . . . . . . . . . . . 13
β’ ((((π₯ β sup(ran (πΉβπ₯), β, < )) β β β§ 0
< (π₯ β sup(ran
(πΉβπ₯), β, < ))) β§ (π β β β§ 0 <
π)) β ((1 / (π₯ β sup(ran (πΉβπ₯), β, < ))) < π β (1 / π) < (π₯ β sup(ran (πΉβπ₯), β, < )))) |
51 | 46, 49, 50 | syl2an 596 |
. . . . . . . . . . . 12
β’ (((π₯ β β β§ sup(ran
(πΉβπ₯), β, < ) < π₯) β§ π β β) β ((1 / (π₯ β sup(ran (πΉβπ₯), β, < ))) < π β (1 / π) < (π₯ β sup(ran (πΉβπ₯), β, < )))) |
52 | 30 | ad2antrr 724 |
. . . . . . . . . . . . . 14
β’ (((π₯ β β β§ sup(ran
(πΉβπ₯), β, < ) < π₯) β§ π β β) β sup(ran (πΉβπ₯), β, < ) β
β) |
53 | | nnrecre 12219 |
. . . . . . . . . . . . . . 15
β’ (π β β β (1 /
π) β
β) |
54 | 53 | adantl 482 |
. . . . . . . . . . . . . 14
β’ (((π₯ β β β§ sup(ran
(πΉβπ₯), β, < ) < π₯) β§ π β β) β (1 / π) β
β) |
55 | | simpll 765 |
. . . . . . . . . . . . . 14
β’ (((π₯ β β β§ sup(ran
(πΉβπ₯), β, < ) < π₯) β§ π β β) β π₯ β β) |
56 | 52, 54, 55 | ltaddsub2d 11780 |
. . . . . . . . . . . . 13
β’ (((π₯ β β β§ sup(ran
(πΉβπ₯), β, < ) < π₯) β§ π β β) β ((sup(ran (πΉβπ₯), β, < ) + (1 / π)) < π₯ β (1 / π) < (π₯ β sup(ran (πΉβπ₯), β, < )))) |
57 | 12 | adantr 481 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β β β§ π β β) β ran
(πΉβπ₯) β β) |
58 | | ffn 6688 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΉβπ₯):ββΆβ β (πΉβπ₯) Fn β) |
59 | 8, 58 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β β β (πΉβπ₯) Fn β) |
60 | | fnfvelrn 7051 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΉβπ₯) Fn β β§ π β β) β ((πΉβπ₯)βπ) β ran (πΉβπ₯)) |
61 | 59, 60 | sylan 580 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β β β§ π β β) β ((πΉβπ₯)βπ) β ran (πΉβπ₯)) |
62 | 57, 61 | sseldd 3963 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β β β§ π β β) β ((πΉβπ₯)βπ) β β) |
63 | 30 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β β β§ π β β) β sup(ran
(πΉβπ₯), β, < ) β
β) |
64 | 53 | adantl 482 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β β β§ π β β) β (1 /
π) β
β) |
65 | 12, 21, 25 | 3jca 1128 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β β β (ran
(πΉβπ₯) β β β§ ran (πΉβπ₯) β β
β§ βπ¦ β β βπ β ran (πΉβπ₯)π β€ π¦)) |
66 | 65 | adantr 481 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β β β§ π β β) β (ran
(πΉβπ₯) β β β§ ran (πΉβπ₯) β β
β§ βπ¦ β β βπ β ran (πΉβπ₯)π β€ π¦)) |
67 | | suprub 12140 |
. . . . . . . . . . . . . . . . 17
β’ (((ran
(πΉβπ₯) β β β§ ran (πΉβπ₯) β β
β§ βπ¦ β β βπ β ran (πΉβπ₯)π β€ π¦) β§ ((πΉβπ₯)βπ) β ran (πΉβπ₯)) β ((πΉβπ₯)βπ) β€ sup(ran (πΉβπ₯), β, < )) |
68 | 66, 61, 67 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β β β§ π β β) β ((πΉβπ₯)βπ) β€ sup(ran (πΉβπ₯), β, < )) |
69 | 62, 63, 64, 68 | leadd1dd 11793 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β β§ π β β) β (((πΉβπ₯)βπ) + (1 / π)) β€ (sup(ran (πΉβπ₯), β, < ) + (1 / π))) |
70 | 62, 64 | readdcld 11208 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β β β§ π β β) β (((πΉβπ₯)βπ) + (1 / π)) β β) |
71 | | readdcl 11158 |
. . . . . . . . . . . . . . . . 17
β’ ((sup(ran
(πΉβπ₯), β, < ) β β β§ (1 /
π) β β) β
(sup(ran (πΉβπ₯), β, < ) + (1 / π)) β
β) |
72 | 30, 53, 71 | syl2an 596 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β β β§ π β β) β (sup(ran
(πΉβπ₯), β, < ) + (1 / π)) β β) |
73 | | simpl 483 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β β β§ π β β) β π₯ β
β) |
74 | | lelttr 11269 |
. . . . . . . . . . . . . . . . 17
β’
(((((πΉβπ₯)βπ) + (1 / π)) β β β§ (sup(ran (πΉβπ₯), β, < ) + (1 / π)) β β β§ π₯ β β) β (((((πΉβπ₯)βπ) + (1 / π)) β€ (sup(ran (πΉβπ₯), β, < ) + (1 / π)) β§ (sup(ran (πΉβπ₯), β, < ) + (1 / π)) < π₯) β (((πΉβπ₯)βπ) + (1 / π)) < π₯)) |
75 | 74 | expd 416 |
. . . . . . . . . . . . . . . 16
β’
(((((πΉβπ₯)βπ) + (1 / π)) β β β§ (sup(ran (πΉβπ₯), β, < ) + (1 / π)) β β β§ π₯ β β) β ((((πΉβπ₯)βπ) + (1 / π)) β€ (sup(ran (πΉβπ₯), β, < ) + (1 / π)) β ((sup(ran (πΉβπ₯), β, < ) + (1 / π)) < π₯ β (((πΉβπ₯)βπ) + (1 / π)) < π₯))) |
76 | 70, 72, 73, 75 | syl3anc 1371 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β β§ π β β) β
((((πΉβπ₯)βπ) + (1 / π)) β€ (sup(ran (πΉβπ₯), β, < ) + (1 / π)) β ((sup(ran (πΉβπ₯), β, < ) + (1 / π)) < π₯ β (((πΉβπ₯)βπ) + (1 / π)) < π₯))) |
77 | 69, 76 | mpd 15 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β β§ π β β) β
((sup(ran (πΉβπ₯), β, < ) + (1 / π)) < π₯ β (((πΉβπ₯)βπ) + (1 / π)) < π₯)) |
78 | 77 | adantlr 713 |
. . . . . . . . . . . . 13
β’ (((π₯ β β β§ sup(ran
(πΉβπ₯), β, < ) < π₯) β§ π β β) β ((sup(ran (πΉβπ₯), β, < ) + (1 / π)) < π₯ β (((πΉβπ₯)βπ) + (1 / π)) < π₯)) |
79 | 56, 78 | sylbird 259 |
. . . . . . . . . . . 12
β’ (((π₯ β β β§ sup(ran
(πΉβπ₯), β, < ) < π₯) β§ π β β) β ((1 / π) < (π₯ β sup(ran (πΉβπ₯), β, < )) β (((πΉβπ₯)βπ) + (1 / π)) < π₯)) |
80 | 51, 79 | sylbid 239 |
. . . . . . . . . . 11
β’ (((π₯ β β β§ sup(ran
(πΉβπ₯), β, < ) < π₯) β§ π β β) β ((1 / (π₯ β sup(ran (πΉβπ₯), β, < ))) < π β (((πΉβπ₯)βπ) + (1 / π)) < π₯)) |
81 | 42 | peano2zd 12634 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β β β§ π β β) β
(sup(π, β, < ) +
1) β β€) |
82 | | oveq1 7384 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (sup(π, β, < ) + 1) β (π / π) = ((sup(π, β, < ) + 1) / π)) |
83 | 82 | breq1d 5135 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (sup(π, β, < ) + 1) β ((π / π) < π₯ β ((sup(π, β, < ) + 1) / π) < π₯)) |
84 | 83, 1 | elrab2 3666 |
. . . . . . . . . . . . . . . . 17
β’
((sup(π, β,
< ) + 1) β π β
((sup(π, β, < ) +
1) β β€ β§ ((sup(π, β, < ) + 1) / π) < π₯)) |
85 | 84 | biimpri 227 |
. . . . . . . . . . . . . . . 16
β’
(((sup(π, β,
< ) + 1) β β€ β§ ((sup(π, β, < ) + 1) / π) < π₯) β (sup(π, β, < ) + 1) β π) |
86 | 81, 85 | sylan 580 |
. . . . . . . . . . . . . . 15
β’ (((π₯ β β β§ π β β) β§
((sup(π, β, < ) +
1) / π) < π₯) β (sup(π, β, < ) + 1) β π) |
87 | | ssrab2 4057 |
. . . . . . . . . . . . . . . . . . . 20
β’ {π β β€ β£ (π / π) < π₯} β β€ |
88 | 1, 87 | eqsstri 3996 |
. . . . . . . . . . . . . . . . . . 19
β’ π β
β€ |
89 | | zssre 12530 |
. . . . . . . . . . . . . . . . . . 19
β’ β€
β β |
90 | 88, 89 | sstri 3971 |
. . . . . . . . . . . . . . . . . 18
β’ π β
β |
91 | 90 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β β β§ π β β) β π β
β) |
92 | | remulcl 11160 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β β β§ π₯ β β) β (π Β· π₯) β β) |
93 | 92 | ancoms 459 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π₯ β β β§ π β β) β (π Β· π₯) β β) |
94 | 47, 93 | sylan2 593 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π₯ β β β§ π β β) β (π Β· π₯) β β) |
95 | | btwnz 12630 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π Β· π₯) β β β (βπ β β€ π < (π Β· π₯) β§ βπ β β€ (π Β· π₯) < π)) |
96 | 95 | simpld 495 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π Β· π₯) β β β βπ β β€ π < (π Β· π₯)) |
97 | 94, 96 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π₯ β β β§ π β β) β
βπ β β€
π < (π Β· π₯)) |
98 | | zre 12527 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β€ β π β
β) |
99 | 98 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π₯ β β β§ π β β) β§ π β β€) β π β
β) |
100 | | simpll 765 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π₯ β β β§ π β β) β§ π β β€) β π₯ β
β) |
101 | 49 | ad2antlr 725 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π₯ β β β§ π β β) β§ π β β€) β (π β β β§ 0 <
π)) |
102 | | ltdivmul 12054 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β β β§ π₯ β β β§ (π β β β§ 0 <
π)) β ((π / π) < π₯ β π < (π Β· π₯))) |
103 | 99, 100, 101, 102 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π₯ β β β§ π β β) β§ π β β€) β ((π / π) < π₯ β π < (π Β· π₯))) |
104 | 103 | rexbidva 3175 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π₯ β β β§ π β β) β
(βπ β β€
(π / π) < π₯ β βπ β β€ π < (π Β· π₯))) |
105 | 97, 104 | mpbird 256 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π₯ β β β§ π β β) β
βπ β β€
(π / π) < π₯) |
106 | | rabn0 4365 |
. . . . . . . . . . . . . . . . . . 19
β’ ({π β β€ β£ (π / π) < π₯} β β
β βπ β β€ (π / π) < π₯) |
107 | 105, 106 | sylibr 233 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ β β β§ π β β) β {π β β€ β£ (π / π) < π₯} β β
) |
108 | 1 | neeq1i 3004 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β
β {π β β€ β£ (π / π) < π₯} β β
) |
109 | 107, 108 | sylibr 233 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β β β§ π β β) β π β β
) |
110 | 1 | reqabi 3440 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π β (π β β€ β§ (π / π) < π₯)) |
111 | 47 | ad2antlr 725 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π₯ β β β§ π β β) β§ π β β€) β π β
β) |
112 | 111, 100,
92 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π₯ β β β§ π β β) β§ π β β€) β (π Β· π₯) β β) |
113 | | ltle 11267 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β β β§ (π Β· π₯) β β) β (π < (π Β· π₯) β π β€ (π Β· π₯))) |
114 | 99, 112, 113 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π₯ β β β§ π β β) β§ π β β€) β (π < (π Β· π₯) β π β€ (π Β· π₯))) |
115 | 103, 114 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π₯ β β β§ π β β) β§ π β β€) β ((π / π) < π₯ β π β€ (π Β· π₯))) |
116 | 115 | impr 455 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π₯ β β β§ π β β) β§ (π β β€ β§ (π / π) < π₯)) β π β€ (π Β· π₯)) |
117 | 110, 116 | sylan2b 594 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π₯ β β β§ π β β) β§ π β π) β π β€ (π Β· π₯)) |
118 | 117 | ralrimiva 3145 |
. . . . . . . . . . . . . . . . . 18
β’ ((π₯ β β β§ π β β) β
βπ β π π β€ (π Β· π₯)) |
119 | | breq2 5129 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ = (π Β· π₯) β (π β€ π¦ β π β€ (π Β· π₯))) |
120 | 119 | ralbidv 3176 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ = (π Β· π₯) β (βπ β π π β€ π¦ β βπ β π π β€ (π Β· π₯))) |
121 | 120 | rspcev 3595 |
. . . . . . . . . . . . . . . . . 18
β’ (((π Β· π₯) β β β§ βπ β π π β€ (π Β· π₯)) β βπ¦ β β βπ β π π β€ π¦) |
122 | 94, 118, 121 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β β β§ π β β) β
βπ¦ β β
βπ β π π β€ π¦) |
123 | 91, 109, 122 | 3jca 1128 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β β β§ π β β) β (π β β β§ π β β
β§ βπ¦ β β βπ β π π β€ π¦)) |
124 | | suprub 12140 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ π β β
β§ βπ¦ β β βπ β π π β€ π¦) β§ (sup(π, β, < ) + 1) β π) β (sup(π, β, < ) + 1) β€ sup(π, β, <
)) |
125 | 123, 124 | sylan 580 |
. . . . . . . . . . . . . . 15
β’ (((π₯ β β β§ π β β) β§
(sup(π, β, < ) +
1) β π) β
(sup(π, β, < ) +
1) β€ sup(π, β,
< )) |
126 | 86, 125 | syldan 591 |
. . . . . . . . . . . . . 14
β’ (((π₯ β β β§ π β β) β§
((sup(π, β, < ) +
1) / π) < π₯) β (sup(π, β, < ) + 1) β€ sup(π, β, <
)) |
127 | 126 | ex 413 |
. . . . . . . . . . . . 13
β’ ((π₯ β β β§ π β β) β
(((sup(π, β, < ) +
1) / π) < π₯ β (sup(π, β, < ) + 1) β€ sup(π, β, <
))) |
128 | 42 | zcnd 12632 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β β β§ π β β) β
sup(π, β, < )
β β) |
129 | | 1cnd 11174 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β β β§ π β β) β 1 β
β) |
130 | | nncn 12185 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β π β
β) |
131 | | nnne0 12211 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β π β 0) |
132 | 130, 131 | jca 512 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β (π β β β§ π β 0)) |
133 | 132 | adantl 482 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β β β§ π β β) β (π β β β§ π β 0)) |
134 | | divdir 11862 |
. . . . . . . . . . . . . . . 16
β’
((sup(π, β,
< ) β β β§ 1 β β β§ (π β β β§ π β 0)) β ((sup(π, β, < ) + 1) / π) = ((sup(π, β, < ) / π) + (1 / π))) |
135 | 128, 129,
133, 134 | syl3anc 1371 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β β§ π β β) β
((sup(π, β, < ) +
1) / π) = ((sup(π, β, < ) / π) + (1 / π))) |
136 | 3 | mptex 7193 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β¦
(sup(π, β, < ) /
π)) β
V |
137 | 2 | fvmpt2 6979 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π₯ β β β§ (π β β β¦
(sup(π, β, < ) /
π)) β V) β (πΉβπ₯) = (π β β β¦ (sup(π, β, < ) / π))) |
138 | 136, 137 | mpan2 689 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β β β (πΉβπ₯) = (π β β β¦ (sup(π, β, < ) / π))) |
139 | 138 | fveq1d 6864 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β β β ((πΉβπ₯)βπ) = ((π β β β¦ (sup(π, β, < ) / π))βπ)) |
140 | | ovex 7410 |
. . . . . . . . . . . . . . . . . 18
β’
(sup(π, β,
< ) / π) β
V |
141 | | eqid 2731 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β¦
(sup(π, β, < ) /
π)) = (π β β β¦ (sup(π, β, < ) / π)) |
142 | 141 | fvmpt2 6979 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ (sup(π, β, < ) / π) β V) β ((π β β β¦
(sup(π, β, < ) /
π))βπ) = (sup(π, β, < ) / π)) |
143 | 140, 142 | mpan2 689 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β ((π β β β¦
(sup(π, β, < ) /
π))βπ) = (sup(π, β, < ) / π)) |
144 | 139, 143 | sylan9eq 2791 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β β β§ π β β) β ((πΉβπ₯)βπ) = (sup(π, β, < ) / π)) |
145 | 144 | oveq1d 7392 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β β β§ π β β) β (((πΉβπ₯)βπ) + (1 / π)) = ((sup(π, β, < ) / π) + (1 / π))) |
146 | 135, 145 | eqtr4d 2774 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β β§ π β β) β
((sup(π, β, < ) +
1) / π) = (((πΉβπ₯)βπ) + (1 / π))) |
147 | 146 | breq1d 5135 |
. . . . . . . . . . . . 13
β’ ((π₯ β β β§ π β β) β
(((sup(π, β, < ) +
1) / π) < π₯ β (((πΉβπ₯)βπ) + (1 / π)) < π₯)) |
148 | 81 | zred 12631 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β β§ π β β) β
(sup(π, β, < ) +
1) β β) |
149 | 148, 43 | lenltd 11325 |
. . . . . . . . . . . . 13
β’ ((π₯ β β β§ π β β) β
((sup(π, β, < ) +
1) β€ sup(π, β,
< ) β Β¬ sup(π,
β, < ) < (sup(π, β, < ) + 1))) |
150 | 127, 147,
149 | 3imtr3d 292 |
. . . . . . . . . . . 12
β’ ((π₯ β β β§ π β β) β
((((πΉβπ₯)βπ) + (1 / π)) < π₯ β Β¬ sup(π, β, < ) < (sup(π, β, < ) +
1))) |
151 | 150 | adantlr 713 |
. . . . . . . . . . 11
β’ (((π₯ β β β§ sup(ran
(πΉβπ₯), β, < ) < π₯) β§ π β β) β ((((πΉβπ₯)βπ) + (1 / π)) < π₯ β Β¬ sup(π, β, < ) < (sup(π, β, < ) +
1))) |
152 | 80, 151 | syld 47 |
. . . . . . . . . 10
β’ (((π₯ β β β§ sup(ran
(πΉβπ₯), β, < ) < π₯) β§ π β β) β ((1 / (π₯ β sup(ran (πΉβπ₯), β, < ))) < π β Β¬ sup(π, β, < ) < (sup(π, β, < ) +
1))) |
153 | 152 | exp31 420 |
. . . . . . . . 9
β’ (π₯ β β β (sup(ran
(πΉβπ₯), β, < ) < π₯ β (π β β β ((1 / (π₯ β sup(ran (πΉβπ₯), β, < ))) < π β Β¬ sup(π, β, < ) < (sup(π, β, < ) +
1))))) |
154 | 153 | com4l 92 |
. . . . . . . 8
β’ (sup(ran
(πΉβπ₯), β, < ) < π₯ β (π β β β ((1 / (π₯ β sup(ran (πΉβπ₯), β, < ))) < π β (π₯ β β β Β¬ sup(π, β, < ) <
(sup(π, β, < ) +
1))))) |
155 | 154 | com14 96 |
. . . . . . 7
β’ (π₯ β β β (π β β β ((1 /
(π₯ β sup(ran (πΉβπ₯), β, < ))) < π β (sup(ran (πΉβπ₯), β, < ) < π₯ β Β¬ sup(π, β, < ) < (sup(π, β, < ) +
1))))) |
156 | 155 | 3imp 1111 |
. . . . . 6
β’ ((π₯ β β β§ π β β β§ (1 /
(π₯ β sup(ran (πΉβπ₯), β, < ))) < π) β (sup(ran (πΉβπ₯), β, < ) < π₯ β Β¬ sup(π, β, < ) < (sup(π, β, < ) +
1))) |
157 | 45, 156 | mt2d 136 |
. . . . 5
β’ ((π₯ β β β§ π β β β§ (1 /
(π₯ β sup(ran (πΉβπ₯), β, < ))) < π) β Β¬ sup(ran (πΉβπ₯), β, < ) < π₯) |
158 | 157 | rexlimdv3a 3158 |
. . . 4
β’ (π₯ β β β
(βπ β β (1
/ (π₯ β sup(ran (πΉβπ₯), β, < ))) < π β Β¬ sup(ran (πΉβπ₯), β, < ) < π₯)) |
159 | 41, 158 | syld 47 |
. . 3
β’ (π₯ β β β (sup(ran
(πΉβπ₯), β, < ) < π₯ β Β¬ sup(ran (πΉβπ₯), β, < ) < π₯)) |
160 | 159 | pm2.01d 189 |
. 2
β’ (π₯ β β β Β¬
sup(ran (πΉβπ₯), β, < ) < π₯) |
161 | | eqlelt 11266 |
. . 3
β’ ((sup(ran
(πΉβπ₯), β, < ) β β β§ π₯ β β) β (sup(ran
(πΉβπ₯), β, < ) = π₯ β (sup(ran (πΉβπ₯), β, < ) β€ π₯ β§ Β¬ sup(ran (πΉβπ₯), β, < ) < π₯))) |
162 | 30, 161 | mpancom 686 |
. 2
β’ (π₯ β β β (sup(ran
(πΉβπ₯), β, < ) = π₯ β (sup(ran (πΉβπ₯), β, < ) β€ π₯ β§ Β¬ sup(ran (πΉβπ₯), β, < ) < π₯))) |
163 | 29, 160, 162 | mpbir2and 711 |
1
β’ (π₯ β β β sup(ran
(πΉβπ₯), β, < ) = π₯) |