Step | Hyp | Ref
| Expression |
1 | | nfcv 2902 |
. . . 4
β’
β²ππΉ |
2 | | limsupreuz.2 |
. . . 4
β’ (π β π β β€) |
3 | | limsupreuz.3 |
. . . 4
β’ π =
(β€β₯βπ) |
4 | | limsupreuz.4 |
. . . . 5
β’ (π β πΉ:πβΆβ) |
5 | 4 | frexr 43773 |
. . . 4
β’ (π β πΉ:πβΆβ*) |
6 | 1, 2, 3, 5 | limsupre3uzlem 44129 |
. . 3
β’ (π β ((lim supβπΉ) β β β
(βπ¦ β β
βπ β π βπ β (β€β₯βπ)π¦ β€ (πΉβπ) β§ βπ¦ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π¦))) |
7 | | breq1 5128 |
. . . . . . . . 9
β’ (π¦ = π₯ β (π¦ β€ (πΉβπ) β π₯ β€ (πΉβπ))) |
8 | 7 | rexbidv 3177 |
. . . . . . . 8
β’ (π¦ = π₯ β (βπ β (β€β₯βπ)π¦ β€ (πΉβπ) β βπ β (β€β₯βπ)π₯ β€ (πΉβπ))) |
9 | 8 | ralbidv 3176 |
. . . . . . 7
β’ (π¦ = π₯ β (βπ β π βπ β (β€β₯βπ)π¦ β€ (πΉβπ) β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ))) |
10 | | fveq2 6862 |
. . . . . . . . . . 11
β’ (π = π β (β€β₯βπ) =
(β€β₯βπ)) |
11 | 10 | rexeqdv 3325 |
. . . . . . . . . 10
β’ (π = π β (βπ β (β€β₯βπ)π₯ β€ (πΉβπ) β βπ β (β€β₯βπ)π₯ β€ (πΉβπ))) |
12 | | nfcv 2902 |
. . . . . . . . . . . . 13
β’
β²ππ₯ |
13 | | nfcv 2902 |
. . . . . . . . . . . . 13
β’
β²π
β€ |
14 | | limsupreuz.1 |
. . . . . . . . . . . . . 14
β’
β²ππΉ |
15 | | nfcv 2902 |
. . . . . . . . . . . . . 14
β’
β²ππ |
16 | 14, 15 | nffv 6872 |
. . . . . . . . . . . . 13
β’
β²π(πΉβπ) |
17 | 12, 13, 16 | nfbr 5172 |
. . . . . . . . . . . 12
β’
β²π π₯ β€ (πΉβπ) |
18 | | nfv 1917 |
. . . . . . . . . . . 12
β’
β²π π₯ β€ (πΉβπ) |
19 | | fveq2 6862 |
. . . . . . . . . . . . 13
β’ (π = π β (πΉβπ) = (πΉβπ)) |
20 | 19 | breq2d 5137 |
. . . . . . . . . . . 12
β’ (π = π β (π₯ β€ (πΉβπ) β π₯ β€ (πΉβπ))) |
21 | 17, 18, 20 | cbvrexw 3301 |
. . . . . . . . . . 11
β’
(βπ β
(β€β₯βπ)π₯ β€ (πΉβπ) β βπ β (β€β₯βπ)π₯ β€ (πΉβπ)) |
22 | 21 | a1i 11 |
. . . . . . . . . 10
β’ (π = π β (βπ β (β€β₯βπ)π₯ β€ (πΉβπ) β βπ β (β€β₯βπ)π₯ β€ (πΉβπ))) |
23 | 11, 22 | bitrd 278 |
. . . . . . . . 9
β’ (π = π β (βπ β (β€β₯βπ)π₯ β€ (πΉβπ) β βπ β (β€β₯βπ)π₯ β€ (πΉβπ))) |
24 | 23 | cbvralvw 3233 |
. . . . . . . 8
β’
(βπ β
π βπ β (β€β₯βπ)π₯ β€ (πΉβπ) β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ)) |
25 | 24 | a1i 11 |
. . . . . . 7
β’ (π¦ = π₯ β (βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ) β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ))) |
26 | 9, 25 | bitrd 278 |
. . . . . 6
β’ (π¦ = π₯ β (βπ β π βπ β (β€β₯βπ)π¦ β€ (πΉβπ) β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ))) |
27 | 26 | cbvrexvw 3234 |
. . . . 5
β’
(βπ¦ β
β βπ β
π βπ β (β€β₯βπ)π¦ β€ (πΉβπ) β βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ)) |
28 | | breq2 5129 |
. . . . . . . . 9
β’ (π¦ = π₯ β ((πΉβπ) β€ π¦ β (πΉβπ) β€ π₯)) |
29 | 28 | ralbidv 3176 |
. . . . . . . 8
β’ (π¦ = π₯ β (βπ β (β€β₯βπ)(πΉβπ) β€ π¦ β βπ β (β€β₯βπ)(πΉβπ) β€ π₯)) |
30 | 29 | rexbidv 3177 |
. . . . . . 7
β’ (π¦ = π₯ β (βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π¦ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯)) |
31 | 10 | raleqdv 3324 |
. . . . . . . . . 10
β’ (π = π β (βπ β (β€β₯βπ)(πΉβπ) β€ π₯ β βπ β (β€β₯βπ)(πΉβπ) β€ π₯)) |
32 | 16, 13, 12 | nfbr 5172 |
. . . . . . . . . . . 12
β’
β²π(πΉβπ) β€ π₯ |
33 | | nfv 1917 |
. . . . . . . . . . . 12
β’
β²π(πΉβπ) β€ π₯ |
34 | 19 | breq1d 5135 |
. . . . . . . . . . . 12
β’ (π = π β ((πΉβπ) β€ π₯ β (πΉβπ) β€ π₯)) |
35 | 32, 33, 34 | cbvralw 3300 |
. . . . . . . . . . 11
β’
(βπ β
(β€β₯βπ)(πΉβπ) β€ π₯ β βπ β (β€β₯βπ)(πΉβπ) β€ π₯) |
36 | 35 | a1i 11 |
. . . . . . . . . 10
β’ (π = π β (βπ β (β€β₯βπ)(πΉβπ) β€ π₯ β βπ β (β€β₯βπ)(πΉβπ) β€ π₯)) |
37 | 31, 36 | bitrd 278 |
. . . . . . . . 9
β’ (π = π β (βπ β (β€β₯βπ)(πΉβπ) β€ π₯ β βπ β (β€β₯βπ)(πΉβπ) β€ π₯)) |
38 | 37 | cbvrexvw 3234 |
. . . . . . . 8
β’
(βπ β
π βπ β
(β€β₯βπ)(πΉβπ) β€ π₯ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) |
39 | 38 | a1i 11 |
. . . . . . 7
β’ (π¦ = π₯ β (βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯)) |
40 | 30, 39 | bitrd 278 |
. . . . . 6
β’ (π¦ = π₯ β (βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π¦ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯)) |
41 | 40 | cbvrexvw 3234 |
. . . . 5
β’
(βπ¦ β
β βπ β
π βπ β
(β€β₯βπ)(πΉβπ) β€ π¦ β βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) |
42 | 27, 41 | anbi12i 627 |
. . . 4
β’
((βπ¦ β
β βπ β
π βπ β (β€β₯βπ)π¦ β€ (πΉβπ) β§ βπ¦ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π¦) β (βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ) β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯)) |
43 | 42 | a1i 11 |
. . 3
β’ (π β ((βπ¦ β β βπ β π βπ β (β€β₯βπ)π¦ β€ (πΉβπ) β§ βπ¦ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π¦) β (βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ) β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯))) |
44 | 6, 43 | bitrd 278 |
. 2
β’ (π β ((lim supβπΉ) β β β
(βπ₯ β β
βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ) β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯))) |
45 | | nfv 1917 |
. . . . . . . 8
β’
β²π(πΉβπ) β€ π₯ |
46 | | nfcv 2902 |
. . . . . . . . . 10
β’
β²ππ |
47 | 14, 46 | nffv 6872 |
. . . . . . . . 9
β’
β²π(πΉβπ) |
48 | 47, 13, 12 | nfbr 5172 |
. . . . . . . 8
β’
β²π(πΉβπ) β€ π₯ |
49 | | fveq2 6862 |
. . . . . . . . 9
β’ (π = π β (πΉβπ) = (πΉβπ)) |
50 | 49 | breq1d 5135 |
. . . . . . . 8
β’ (π = π β ((πΉβπ) β€ π₯ β (πΉβπ) β€ π₯)) |
51 | 45, 48, 50 | cbvralw 3300 |
. . . . . . 7
β’
(βπ β
(β€β₯βπ)(πΉβπ) β€ π₯ β βπ β (β€β₯βπ)(πΉβπ) β€ π₯) |
52 | 51 | rexbii 3093 |
. . . . . 6
β’
(βπ β
π βπ β
(β€β₯βπ)(πΉβπ) β€ π₯ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) |
53 | 52 | rexbii 3093 |
. . . . 5
β’
(βπ₯ β
β βπ β
π βπ β
(β€β₯βπ)(πΉβπ) β€ π₯ β βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) |
54 | 53 | a1i 11 |
. . . 4
β’ (π β (βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯ β βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯)) |
55 | | nfv 1917 |
. . . . 5
β’
β²ππ |
56 | 4 | adantr 481 |
. . . . . 6
β’ ((π β§ π β π) β πΉ:πβΆβ) |
57 | | simpr 485 |
. . . . . 6
β’ ((π β§ π β π) β π β π) |
58 | 56, 57 | ffvelcdmd 7056 |
. . . . 5
β’ ((π β§ π β π) β (πΉβπ) β β) |
59 | 55, 2, 3, 58 | uzub 43819 |
. . . 4
β’ (π β (βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯ β βπ₯ β β βπ β π (πΉβπ) β€ π₯)) |
60 | | eqcom 2738 |
. . . . . . . . . 10
β’ (π = π β π = π) |
61 | 60 | imbi1i 349 |
. . . . . . . . 9
β’ ((π = π β ((πΉβπ) β€ π₯ β (πΉβπ) β€ π₯)) β (π = π β ((πΉβπ) β€ π₯ β (πΉβπ) β€ π₯))) |
62 | | bicom 221 |
. . . . . . . . . 10
β’ (((πΉβπ) β€ π₯ β (πΉβπ) β€ π₯) β ((πΉβπ) β€ π₯ β (πΉβπ) β€ π₯)) |
63 | 62 | imbi2i 335 |
. . . . . . . . 9
β’ ((π = π β ((πΉβπ) β€ π₯ β (πΉβπ) β€ π₯)) β (π = π β ((πΉβπ) β€ π₯ β (πΉβπ) β€ π₯))) |
64 | 61, 63 | bitri 274 |
. . . . . . . 8
β’ ((π = π β ((πΉβπ) β€ π₯ β (πΉβπ) β€ π₯)) β (π = π β ((πΉβπ) β€ π₯ β (πΉβπ) β€ π₯))) |
65 | 50, 64 | mpbi 229 |
. . . . . . 7
β’ (π = π β ((πΉβπ) β€ π₯ β (πΉβπ) β€ π₯)) |
66 | 48, 45, 65 | cbvralw 3300 |
. . . . . 6
β’
(βπ β
π (πΉβπ) β€ π₯ β βπ β π (πΉβπ) β€ π₯) |
67 | 66 | rexbii 3093 |
. . . . 5
β’
(βπ₯ β
β βπ β
π (πΉβπ) β€ π₯ β βπ₯ β β βπ β π (πΉβπ) β€ π₯) |
68 | 67 | a1i 11 |
. . . 4
β’ (π β (βπ₯ β β βπ β π (πΉβπ) β€ π₯ β βπ₯ β β βπ β π (πΉβπ) β€ π₯)) |
69 | 54, 59, 68 | 3bitrd 304 |
. . 3
β’ (π β (βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯ β βπ₯ β β βπ β π (πΉβπ) β€ π₯)) |
70 | 69 | anbi2d 629 |
. 2
β’ (π β ((βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ) β§ βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) β (βπ₯ β β βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ) β§ βπ₯ β β βπ β π (πΉβπ) β€ π₯))) |
71 | 44, 70 | bitrd 278 |
1
β’ (π β ((lim supβπΉ) β β β
(βπ₯ β β
βπ β π βπ β (β€β₯βπ)π₯ β€ (πΉβπ) β§ βπ₯ β β βπ β π (πΉβπ) β€ π₯))) |