Step | Hyp | Ref
| Expression |
1 | | nfv 1918 |
. . . . . 6
β’
β²ππ |
2 | | nfcv 2904 |
. . . . . 6
β’
β²ππΉ |
3 | | limsupubuz.z |
. . . . . . . 8
β’ π =
(β€β₯βπ) |
4 | | uzssre 12844 |
. . . . . . . 8
β’
(β€β₯βπ) β β |
5 | 3, 4 | eqsstri 4017 |
. . . . . . 7
β’ π β
β |
6 | 5 | a1i 11 |
. . . . . 6
β’ (π β π β β) |
7 | | limsupubuz.f |
. . . . . . 7
β’ (π β πΉ:πβΆβ) |
8 | 7 | frexr 44095 |
. . . . . 6
β’ (π β πΉ:πβΆβ*) |
9 | | limsupubuz.n |
. . . . . 6
β’ (π β (lim supβπΉ) β
+β) |
10 | 1, 2, 6, 8, 9 | limsupub 44420 |
. . . . 5
β’ (π β βπ¦ β β βπ β β βπ β π (π β€ π β (πΉβπ) β€ π¦)) |
11 | 10 | adantr 482 |
. . . 4
β’ ((π β§ π β β€) β βπ¦ β β βπ β β βπ β π (π β€ π β (πΉβπ) β€ π¦)) |
12 | | nfv 1918 |
. . . . . . . . . . 11
β’
β²π π β β€ |
13 | 1, 12 | nfan 1903 |
. . . . . . . . . 10
β’
β²π(π β§ π β β€) |
14 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π π¦ β β |
15 | 13, 14 | nfan 1903 |
. . . . . . . . 9
β’
β²π((π β§ π β β€) β§ π¦ β β) |
16 | | nfv 1918 |
. . . . . . . . 9
β’
β²π π β β |
17 | 15, 16 | nfan 1903 |
. . . . . . . 8
β’
β²π(((π β§ π β β€) β§ π¦ β β) β§ π β β) |
18 | | nfra1 3282 |
. . . . . . . 8
β’
β²πβπ β π (π β€ π β (πΉβπ) β€ π¦) |
19 | 17, 18 | nfan 1903 |
. . . . . . 7
β’
β²π((((π β§ π β β€) β§ π¦ β β) β§ π β β) β§ βπ β π (π β€ π β (πΉβπ) β€ π¦)) |
20 | | nfmpt1 5257 |
. . . . . . . . . . 11
β’
β²π(π β (π...if((ββπ) β€ π, π, (ββπ))) β¦ (πΉβπ)) |
21 | 20 | nfrn 5952 |
. . . . . . . . . 10
β’
β²πran
(π β (π...if((ββπ) β€ π, π, (ββπ))) β¦ (πΉβπ)) |
22 | | nfcv 2904 |
. . . . . . . . . 10
β’
β²πβ |
23 | | nfcv 2904 |
. . . . . . . . . 10
β’
β²π
< |
24 | 21, 22, 23 | nfsup 9446 |
. . . . . . . . 9
β’
β²πsup(ran (π β (π...if((ββπ) β€ π, π, (ββπ))) β¦ (πΉβπ)), β, < ) |
25 | | nfcv 2904 |
. . . . . . . . 9
β’
β²π
β€ |
26 | | nfcv 2904 |
. . . . . . . . 9
β’
β²ππ¦ |
27 | 24, 25, 26 | nfbr 5196 |
. . . . . . . 8
β’
β²πsup(ran
(π β (π...if((ββπ) β€ π, π, (ββπ))) β¦ (πΉβπ)), β, < ) β€ π¦ |
28 | 27, 26, 24 | nfif 4559 |
. . . . . . 7
β’
β²πif(sup(ran (π β (π...if((ββπ) β€ π, π, (ββπ))) β¦ (πΉβπ)), β, < ) β€ π¦, π¦, sup(ran (π β (π...if((ββπ) β€ π, π, (ββπ))) β¦ (πΉβπ)), β, < )) |
29 | | breq2 5153 |
. . . . . . . . . . . 12
β’ (π = π β (π β€ π β π β€ π)) |
30 | | fveq2 6892 |
. . . . . . . . . . . . 13
β’ (π = π β (πΉβπ) = (πΉβπ)) |
31 | 30 | breq1d 5159 |
. . . . . . . . . . . 12
β’ (π = π β ((πΉβπ) β€ π¦ β (πΉβπ) β€ π¦)) |
32 | 29, 31 | imbi12d 345 |
. . . . . . . . . . 11
β’ (π = π β ((π β€ π β (πΉβπ) β€ π¦) β (π β€ π β (πΉβπ) β€ π¦))) |
33 | 32 | cbvralvw 3235 |
. . . . . . . . . 10
β’
(βπ β
π (π β€ π β (πΉβπ) β€ π¦) β βπ β π (π β€ π β (πΉβπ) β€ π¦)) |
34 | 33 | biimpi 215 |
. . . . . . . . 9
β’
(βπ β
π (π β€ π β (πΉβπ) β€ π¦) β βπ β π (π β€ π β (πΉβπ) β€ π¦)) |
35 | 34 | adantl 483 |
. . . . . . . 8
β’
(((((π β§ π β β€) β§ π¦ β β) β§ π β β) β§
βπ β π (π β€ π β (πΉβπ) β€ π¦)) β βπ β π (π β€ π β (πΉβπ) β€ π¦)) |
36 | | simp-4r 783 |
. . . . . . . 8
β’
(((((π β§ π β β€) β§ π¦ β β) β§ π β β) β§
βπ β π (π β€ π β (πΉβπ) β€ π¦)) β π β β€) |
37 | 35, 36 | syldan 592 |
. . . . . . 7
β’
(((((π β§ π β β€) β§ π¦ β β) β§ π β β) β§
βπ β π (π β€ π β (πΉβπ) β€ π¦)) β π β β€) |
38 | 7 | ad4antr 731 |
. . . . . . . 8
β’
(((((π β§ π β β€) β§ π¦ β β) β§ π β β) β§
βπ β π (π β€ π β (πΉβπ) β€ π¦)) β πΉ:πβΆβ) |
39 | 35, 38 | syldan 592 |
. . . . . . 7
β’
(((((π β§ π β β€) β§ π¦ β β) β§ π β β) β§
βπ β π (π β€ π β (πΉβπ) β€ π¦)) β πΉ:πβΆβ) |
40 | | simpllr 775 |
. . . . . . . 8
β’
(((((π β§ π β β€) β§ π¦ β β) β§ π β β) β§
βπ β π (π β€ π β (πΉβπ) β€ π¦)) β π¦ β β) |
41 | 35, 40 | syldan 592 |
. . . . . . 7
β’
(((((π β§ π β β€) β§ π¦ β β) β§ π β β) β§
βπ β π (π β€ π β (πΉβπ) β€ π¦)) β π¦ β β) |
42 | | simplr 768 |
. . . . . . . 8
β’
(((((π β§ π β β€) β§ π¦ β β) β§ π β β) β§
βπ β π (π β€ π β (πΉβπ) β€ π¦)) β π β β) |
43 | 35, 42 | syldan 592 |
. . . . . . 7
β’
(((((π β§ π β β€) β§ π¦ β β) β§ π β β) β§
βπ β π (π β€ π β (πΉβπ) β€ π¦)) β π β β) |
44 | 33 | biimpri 227 |
. . . . . . . 8
β’
(βπ β
π (π β€ π β (πΉβπ) β€ π¦) β βπ β π (π β€ π β (πΉβπ) β€ π¦)) |
45 | 35, 44 | syl 17 |
. . . . . . 7
β’
(((((π β§ π β β€) β§ π¦ β β) β§ π β β) β§
βπ β π (π β€ π β (πΉβπ) β€ π¦)) β βπ β π (π β€ π β (πΉβπ) β€ π¦)) |
46 | | eqid 2733 |
. . . . . . 7
β’
if((ββπ)
β€ π, π, (ββπ)) = if((ββπ) β€ π, π, (ββπ)) |
47 | | eqid 2733 |
. . . . . . 7
β’ sup(ran
(π β (π...if((ββπ) β€ π, π, (ββπ))) β¦ (πΉβπ)), β, < ) = sup(ran (π β (π...if((ββπ) β€ π, π, (ββπ))) β¦ (πΉβπ)), β, < ) |
48 | | eqid 2733 |
. . . . . . 7
β’
if(sup(ran (π β
(π...if((ββπ) β€ π, π, (ββπ))) β¦ (πΉβπ)), β, < ) β€ π¦, π¦, sup(ran (π β (π...if((ββπ) β€ π, π, (ββπ))) β¦ (πΉβπ)), β, < )) = if(sup(ran (π β (π...if((ββπ) β€ π, π, (ββπ))) β¦ (πΉβπ)), β, < ) β€ π¦, π¦, sup(ran (π β (π...if((ββπ) β€ π, π, (ββπ))) β¦ (πΉβπ)), β, < )) |
49 | 19, 28, 37, 3, 39, 41, 43, 45, 46, 47, 48 | limsupubuzlem 44428 |
. . . . . 6
β’
(((((π β§ π β β€) β§ π¦ β β) β§ π β β) β§
βπ β π (π β€ π β (πΉβπ) β€ π¦)) β βπ₯ β β βπ β π (πΉβπ) β€ π₯) |
50 | 49 | rexlimdva2 3158 |
. . . . 5
β’ (((π β§ π β β€) β§ π¦ β β) β (βπ β β βπ β π (π β€ π β (πΉβπ) β€ π¦) β βπ₯ β β βπ β π (πΉβπ) β€ π₯)) |
51 | 50 | rexlimdva 3156 |
. . . 4
β’ ((π β§ π β β€) β (βπ¦ β β βπ β β βπ β π (π β€ π β (πΉβπ) β€ π¦) β βπ₯ β β βπ β π (πΉβπ) β€ π₯)) |
52 | 11, 51 | mpd 15 |
. . 3
β’ ((π β§ π β β€) β βπ₯ β β βπ β π (πΉβπ) β€ π₯) |
53 | 3 | a1i 11 |
. . . . . 6
β’ (Β¬
π β β€ β
π =
(β€β₯βπ)) |
54 | | uz0 44122 |
. . . . . 6
β’ (Β¬
π β β€ β
(β€β₯βπ) = β
) |
55 | 53, 54 | eqtrd 2773 |
. . . . 5
β’ (Β¬
π β β€ β
π =
β
) |
56 | | 0red 11217 |
. . . . . 6
β’ (π = β
β 0 β
β) |
57 | | rzal 4509 |
. . . . . 6
β’ (π = β
β βπ β π (πΉβπ) β€ 0) |
58 | | brralrspcev 5209 |
. . . . . 6
β’ ((0
β β β§ βπ β π (πΉβπ) β€ 0) β βπ₯ β β βπ β π (πΉβπ) β€ π₯) |
59 | 56, 57, 58 | syl2anc 585 |
. . . . 5
β’ (π = β
β βπ₯ β β βπ β π (πΉβπ) β€ π₯) |
60 | 55, 59 | syl 17 |
. . . 4
β’ (Β¬
π β β€ β
βπ₯ β β
βπ β π (πΉβπ) β€ π₯) |
61 | 60 | adantl 483 |
. . 3
β’ ((π β§ Β¬ π β β€) β βπ₯ β β βπ β π (πΉβπ) β€ π₯) |
62 | 52, 61 | pm2.61dan 812 |
. 2
β’ (π β βπ₯ β β βπ β π (πΉβπ) β€ π₯) |
63 | | limsupubuz.j |
. . . . . 6
β’
β²ππΉ |
64 | | nfcv 2904 |
. . . . . 6
β’
β²ππ |
65 | 63, 64 | nffv 6902 |
. . . . 5
β’
β²π(πΉβπ) |
66 | | nfcv 2904 |
. . . . 5
β’
β²π
β€ |
67 | | nfcv 2904 |
. . . . 5
β’
β²ππ₯ |
68 | 65, 66, 67 | nfbr 5196 |
. . . 4
β’
β²π(πΉβπ) β€ π₯ |
69 | | nfv 1918 |
. . . 4
β’
β²π(πΉβπ) β€ π₯ |
70 | | fveq2 6892 |
. . . . 5
β’ (π = π β (πΉβπ) = (πΉβπ)) |
71 | 70 | breq1d 5159 |
. . . 4
β’ (π = π β ((πΉβπ) β€ π₯ β (πΉβπ) β€ π₯)) |
72 | 68, 69, 71 | cbvralw 3304 |
. . 3
β’
(βπ β
π (πΉβπ) β€ π₯ β βπ β π (πΉβπ) β€ π₯) |
73 | 72 | rexbii 3095 |
. 2
β’
(βπ₯ β
β βπ β
π (πΉβπ) β€ π₯ β βπ₯ β β βπ β π (πΉβπ) β€ π₯) |
74 | 62, 73 | sylib 217 |
1
β’ (π β βπ₯ β β βπ β π (πΉβπ) β€ π₯) |