Step | Hyp | Ref
| Expression |
1 | | nfv 1918 |
. . . . 5
β’
β²ππ |
2 | | reex 11152 |
. . . . . . 7
β’ β
β V |
3 | 2 | a1i 11 |
. . . . . 6
β’ (π β β β
V) |
4 | | limsupmnflem.a |
. . . . . 6
β’ (π β π΄ β β) |
5 | 3, 4 | ssexd 5287 |
. . . . 5
β’ (π β π΄ β V) |
6 | | limsupmnflem.f |
. . . . 5
β’ (π β πΉ:π΄βΆβ*) |
7 | | limsupmnflem.g |
. . . . 5
β’ πΊ = (π β β β¦ sup((πΉ β (π[,)+β)), β*, <
)) |
8 | 1, 5, 6, 7 | limsupval3 44035 |
. . . 4
β’ (π β (lim supβπΉ) = inf(ran πΊ, β*, <
)) |
9 | 7 | rneqi 5898 |
. . . . . 6
β’ ran πΊ = ran (π β β β¦ sup((πΉ β (π[,)+β)), β*, <
)) |
10 | 9 | infeq1i 9424 |
. . . . 5
β’ inf(ran
πΊ, β*,
< ) = inf(ran (π β
β β¦ sup((πΉ
β (π[,)+β)),
β*, < )), β*, < ) |
11 | 10 | a1i 11 |
. . . 4
β’ (π β inf(ran πΊ, β*, < ) = inf(ran
(π β β β¦
sup((πΉ β (π[,)+β)),
β*, < )), β*, < )) |
12 | 8, 11 | eqtrd 2772 |
. . 3
β’ (π β (lim supβπΉ) = inf(ran (π β β β¦ sup((πΉ β (π[,)+β)), β*, < )),
β*, < )) |
13 | 12 | eqeq1d 2734 |
. 2
β’ (π β ((lim supβπΉ) = -β β inf(ran
(π β β β¦
sup((πΉ β (π[,)+β)),
β*, < )), β*, < ) =
-β)) |
14 | | nfv 1918 |
. . 3
β’
β²π₯π |
15 | 6 | fimassd 43556 |
. . . . 5
β’ (π β (πΉ β (π[,)+β)) β
β*) |
16 | 15 | adantr 482 |
. . . 4
β’ ((π β§ π β β) β (πΉ β (π[,)+β)) β
β*) |
17 | 16 | supxrcld 43421 |
. . 3
β’ ((π β§ π β β) β sup((πΉ β (π[,)+β)), β*, < )
β β*) |
18 | 1, 14, 17 | infxrunb3rnmpt 43765 |
. 2
β’ (π β (βπ₯ β β βπ β β sup((πΉ β (π[,)+β)), β*, < )
β€ π₯ β inf(ran
(π β β β¦
sup((πΉ β (π[,)+β)),
β*, < )), β*, < ) =
-β)) |
19 | 15 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β β) β (πΉ β (π[,)+β)) β
β*) |
20 | | ressxr 11209 |
. . . . . . . . 9
β’ β
β β* |
21 | 20 | a1i 11 |
. . . . . . . 8
β’ (π β β β
β*) |
22 | 21 | sselda 3948 |
. . . . . . 7
β’ ((π β§ π₯ β β) β π₯ β β*) |
23 | | supxrleub 13256 |
. . . . . . 7
β’ (((πΉ β (π[,)+β)) β β*
β§ π₯ β
β*) β (sup((πΉ β (π[,)+β)), β*, < )
β€ π₯ β βπ¦ β (πΉ β (π[,)+β))π¦ β€ π₯)) |
24 | 19, 22, 23 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π₯ β β) β (sup((πΉ β (π[,)+β)), β*, < )
β€ π₯ β βπ¦ β (πΉ β (π[,)+β))π¦ β€ π₯)) |
25 | 24 | adantr 482 |
. . . . 5
β’ (((π β§ π₯ β β) β§ π β β) β (sup((πΉ β (π[,)+β)), β*, < )
β€ π₯ β βπ¦ β (πΉ β (π[,)+β))π¦ β€ π₯)) |
26 | 6 | ffnd 6675 |
. . . . . . . . . . . . . 14
β’ (π β πΉ Fn π΄) |
27 | 26 | ad3antrrr 729 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β) β§ π β π΄) β§ π β€ π) β πΉ Fn π΄) |
28 | | simplr 768 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β) β§ π β π΄) β§ π β€ π) β π β π΄) |
29 | 20 | sseli 3944 |
. . . . . . . . . . . . . . 15
β’ (π β β β π β
β*) |
30 | 29 | ad3antlr 730 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β β) β§ π β π΄) β§ π β€ π) β π β β*) |
31 | | pnfxr 11219 |
. . . . . . . . . . . . . . 15
β’ +β
β β* |
32 | 31 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β β) β§ π β π΄) β§ π β€ π) β +β β
β*) |
33 | 20 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π΄) β β β
β*) |
34 | 4 | sselda 3948 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π΄) β π β β) |
35 | 33, 34 | sseldd 3949 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π΄) β π β β*) |
36 | 35 | ad4ant13 750 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β β) β§ π β π΄) β§ π β€ π) β π β β*) |
37 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β β) β§ π β π΄) β§ π β€ π) β π β€ π) |
38 | 34 | ltpnfd 13052 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π΄) β π < +β) |
39 | 38 | ad4ant13 750 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β β) β§ π β π΄) β§ π β€ π) β π < +β) |
40 | 30, 32, 36, 37, 39 | elicod 13325 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β) β§ π β π΄) β§ π β€ π) β π β (π[,)+β)) |
41 | 27, 28, 40 | fnfvimad 7190 |
. . . . . . . . . . . 12
β’ ((((π β§ π β β) β§ π β π΄) β§ π β€ π) β (πΉβπ) β (πΉ β (π[,)+β))) |
42 | 41 | adantllr 718 |
. . . . . . . . . . 11
β’
(((((π β§ π β β) β§
βπ¦ β (πΉ β (π[,)+β))π¦ β€ π₯) β§ π β π΄) β§ π β€ π) β (πΉβπ) β (πΉ β (π[,)+β))) |
43 | | simpllr 775 |
. . . . . . . . . . 11
β’
(((((π β§ π β β) β§
βπ¦ β (πΉ β (π[,)+β))π¦ β€ π₯) β§ π β π΄) β§ π β€ π) β βπ¦ β (πΉ β (π[,)+β))π¦ β€ π₯) |
44 | | breq1 5114 |
. . . . . . . . . . . 12
β’ (π¦ = (πΉβπ) β (π¦ β€ π₯ β (πΉβπ) β€ π₯)) |
45 | 44 | rspcva 3581 |
. . . . . . . . . . 11
β’ (((πΉβπ) β (πΉ β (π[,)+β)) β§ βπ¦ β (πΉ β (π[,)+β))π¦ β€ π₯) β (πΉβπ) β€ π₯) |
46 | 42, 43, 45 | syl2anc 585 |
. . . . . . . . . 10
β’
(((((π β§ π β β) β§
βπ¦ β (πΉ β (π[,)+β))π¦ β€ π₯) β§ π β π΄) β§ π β€ π) β (πΉβπ) β€ π₯) |
47 | 46 | adantl4r 754 |
. . . . . . . . 9
β’
((((((π β§ π₯ β β) β§ π β β) β§
βπ¦ β (πΉ β (π[,)+β))π¦ β€ π₯) β§ π β π΄) β§ π β€ π) β (πΉβπ) β€ π₯) |
48 | 47 | ex 414 |
. . . . . . . 8
β’
(((((π β§ π₯ β β) β§ π β β) β§
βπ¦ β (πΉ β (π[,)+β))π¦ β€ π₯) β§ π β π΄) β (π β€ π β (πΉβπ) β€ π₯)) |
49 | 48 | ralrimiva 3140 |
. . . . . . 7
β’ ((((π β§ π₯ β β) β§ π β β) β§ βπ¦ β (πΉ β (π[,)+β))π¦ β€ π₯) β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) |
50 | 49 | ex 414 |
. . . . . 6
β’ (((π β§ π₯ β β) β§ π β β) β (βπ¦ β (πΉ β (π[,)+β))π¦ β€ π₯ β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯))) |
51 | | nfcv 2903 |
. . . . . . . . . . . . . 14
β’
β²ππΉ |
52 | 26 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β (πΉ β (π[,)+β))) β πΉ Fn π΄) |
53 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β (πΉ β (π[,)+β))) β π¦ β (πΉ β (π[,)+β))) |
54 | 51, 52, 53 | fvelimad 6915 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β (πΉ β (π[,)+β))) β βπ β (π΄ β© (π[,)+β))(πΉβπ) = π¦) |
55 | 54 | ad4ant14 751 |
. . . . . . . . . . . 12
β’ ((((π β§ π β β) β§ βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) β§ π¦ β (πΉ β (π[,)+β))) β βπ β (π΄ β© (π[,)+β))(πΉβπ) = π¦) |
56 | | nfv 1918 |
. . . . . . . . . . . . . . 15
β’
β²π(π β§ π β β) |
57 | | nfra1 3266 |
. . . . . . . . . . . . . . 15
β’
β²πβπ β π΄ (π β€ π β (πΉβπ) β€ π₯) |
58 | 56, 57 | nfan 1903 |
. . . . . . . . . . . . . 14
β’
β²π((π β§ π β β) β§ βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) |
59 | | nfv 1918 |
. . . . . . . . . . . . . 14
β’
β²π π¦ β€ π₯ |
60 | 29 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§ π β (π΄ β© (π[,)+β))) β π β β*) |
61 | 31 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§ π β (π΄ β© (π[,)+β))) β +β β
β*) |
62 | | elinel2 4162 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (π΄ β© (π[,)+β)) β π β (π[,)+β)) |
63 | 62 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§ π β (π΄ β© (π[,)+β))) β π β (π[,)+β)) |
64 | 60, 61, 63 | icogelbd 43898 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ π β (π΄ β© (π[,)+β))) β π β€ π) |
65 | 64 | adantlr 714 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β β§
βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) β§ π β (π΄ β© (π[,)+β))) β π β€ π) |
66 | | elinel1 4161 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (π΄ β© (π[,)+β)) β π β π΄) |
67 | 66 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’
((βπ β
π΄ (π β€ π β (πΉβπ) β€ π₯) β§ π β (π΄ β© (π[,)+β))) β π β π΄) |
68 | | rspa 3230 |
. . . . . . . . . . . . . . . . . . . 20
β’
((βπ β
π΄ (π β€ π β (πΉβπ) β€ π₯) β§ π β π΄) β (π β€ π β (πΉβπ) β€ π₯)) |
69 | 67, 68 | syldan 592 |
. . . . . . . . . . . . . . . . . . 19
β’
((βπ β
π΄ (π β€ π β (πΉβπ) β€ π₯) β§ π β (π΄ β© (π[,)+β))) β (π β€ π β (πΉβπ) β€ π₯)) |
70 | 69 | adantll 713 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β β§
βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) β§ π β (π΄ β© (π[,)+β))) β (π β€ π β (πΉβπ) β€ π₯)) |
71 | 65, 70 | mpd 15 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§
βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) β§ π β (π΄ β© (π[,)+β))) β (πΉβπ) β€ π₯) |
72 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πΉβπ) = π¦ β (πΉβπ) = π¦) |
73 | 72 | eqcomd 2738 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΉβπ) = π¦ β π¦ = (πΉβπ)) |
74 | 73 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πΉβπ) β€ π₯ β§ (πΉβπ) = π¦) β π¦ = (πΉβπ)) |
75 | | simpl 484 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πΉβπ) β€ π₯ β§ (πΉβπ) = π¦) β (πΉβπ) β€ π₯) |
76 | 74, 75 | eqbrtrd 5133 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΉβπ) β€ π₯ β§ (πΉβπ) = π¦) β π¦ β€ π₯) |
77 | 76 | ex 414 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉβπ) β€ π₯ β ((πΉβπ) = π¦ β π¦ β€ π₯)) |
78 | 71, 77 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§
βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) β§ π β (π΄ β© (π[,)+β))) β ((πΉβπ) = π¦ β π¦ β€ π₯)) |
79 | 78 | adantlll 717 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β β) β§ βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) β§ π β (π΄ β© (π[,)+β))) β ((πΉβπ) = π¦ β π¦ β€ π₯)) |
80 | 79 | ex 414 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) β (π β (π΄ β© (π[,)+β)) β ((πΉβπ) = π¦ β π¦ β€ π₯))) |
81 | 58, 59, 80 | rexlimd 3248 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) β (βπ β (π΄ β© (π[,)+β))(πΉβπ) = π¦ β π¦ β€ π₯)) |
82 | 81 | imp 408 |
. . . . . . . . . . . 12
β’ ((((π β§ π β β) β§ βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) β§ βπ β (π΄ β© (π[,)+β))(πΉβπ) = π¦) β π¦ β€ π₯) |
83 | 55, 82 | syldan 592 |
. . . . . . . . . . 11
β’ ((((π β§ π β β) β§ βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) β§ π¦ β (πΉ β (π[,)+β))) β π¦ β€ π₯) |
84 | 83 | ralrimiva 3140 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) β βπ¦ β (πΉ β (π[,)+β))π¦ β€ π₯) |
85 | 84 | adantllr 718 |
. . . . . . . . 9
β’ ((((π β§ π₯ β β) β§ π β β) β§ βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) β βπ¦ β (πΉ β (π[,)+β))π¦ β€ π₯) |
86 | 24 | ad2antrr 725 |
. . . . . . . . 9
β’ ((((π β§ π₯ β β) β§ π β β) β§ βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) β (sup((πΉ β (π[,)+β)), β*, < )
β€ π₯ β βπ¦ β (πΉ β (π[,)+β))π¦ β€ π₯)) |
87 | 85, 86 | mpbird 257 |
. . . . . . . 8
β’ ((((π β§ π₯ β β) β§ π β β) β§ βπ β π΄ (π β€ π β (πΉβπ) β€ π₯)) β sup((πΉ β (π[,)+β)), β*, < )
β€ π₯) |
88 | 87 | ex 414 |
. . . . . . 7
β’ (((π β§ π₯ β β) β§ π β β) β (βπ β π΄ (π β€ π β (πΉβπ) β€ π₯) β sup((πΉ β (π[,)+β)), β*, < )
β€ π₯)) |
89 | 88, 25 | sylibd 238 |
. . . . . 6
β’ (((π β§ π₯ β β) β§ π β β) β (βπ β π΄ (π β€ π β (πΉβπ) β€ π₯) β βπ¦ β (πΉ β (π[,)+β))π¦ β€ π₯)) |
90 | 50, 89 | impbid 211 |
. . . . 5
β’ (((π β§ π₯ β β) β§ π β β) β (βπ¦ β (πΉ β (π[,)+β))π¦ β€ π₯ β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯))) |
91 | 25, 90 | bitrd 279 |
. . . 4
β’ (((π β§ π₯ β β) β§ π β β) β (sup((πΉ β (π[,)+β)), β*, < )
β€ π₯ β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯))) |
92 | 91 | rexbidva 3170 |
. . 3
β’ ((π β§ π₯ β β) β (βπ β β sup((πΉ β (π[,)+β)), β*, < )
β€ π₯ β βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯))) |
93 | 92 | ralbidva 3169 |
. 2
β’ (π β (βπ₯ β β βπ β β sup((πΉ β (π[,)+β)), β*, < )
β€ π₯ β βπ₯ β β βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ π₯))) |
94 | 13, 18, 93 | 3bitr2d 307 |
1
β’ (π β ((lim supβπΉ) = -β β
βπ₯ β β
βπ β β
βπ β π΄ (π β€ π β (πΉβπ) β€ π₯))) |