Step | Hyp | Ref
| Expression |
1 | | xlimliminflimsup.m |
. . . . . 6
β’ (π β π β β€) |
2 | 1 | ad2antrr 725 |
. . . . 5
β’ (((π β§ πΉ β dom ~~>*) β§ (~~>*βπΉ) β β) β π β
β€) |
3 | | xlimliminflimsup.z |
. . . . 5
β’ π =
(β€β₯βπ) |
4 | | xlimliminflimsup.f |
. . . . . 6
β’ (π β πΉ:πβΆβ*) |
5 | 4 | ad2antrr 725 |
. . . . 5
β’ (((π β§ πΉ β dom ~~>*) β§ (~~>*βπΉ) β β) β πΉ:πβΆβ*) |
6 | | simpr 486 |
. . . . 5
β’ (((π β§ πΉ β dom ~~>*) β§ (~~>*βπΉ) β β) β
(~~>*βπΉ) β
β) |
7 | | xlimdm 44188 |
. . . . . . 7
β’ (πΉ β dom ~~>* β πΉ~~>*(~~>*βπΉ)) |
8 | 7 | biimpi 215 |
. . . . . 6
β’ (πΉ β dom ~~>* β πΉ~~>*(~~>*βπΉ)) |
9 | 8 | ad2antlr 726 |
. . . . 5
β’ (((π β§ πΉ β dom ~~>*) β§ (~~>*βπΉ) β β) β πΉ~~>*(~~>*βπΉ)) |
10 | 2, 3, 5, 6, 9 | xlimxrre 44162 |
. . . 4
β’ (((π β§ πΉ β dom ~~>*) β§ (~~>*βπΉ) β β) β
βπ β π (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) |
11 | 3 | eluzelz2 43728 |
. . . . . . 7
β’ (π β π β π β β€) |
12 | 11 | ad2antlr 726 |
. . . . . 6
β’
(((((π β§ πΉ β dom ~~>*) β§
(~~>*βπΉ) β
β) β§ π β
π) β§ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) β π β
β€) |
13 | | eqid 2733 |
. . . . . 6
β’
(β€β₯βπ) = (β€β₯βπ) |
14 | | simpr 486 |
. . . . . 6
β’
(((((π β§ πΉ β dom ~~>*) β§
(~~>*βπΉ) β
β) β§ π β
π) β§ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) β (πΉ βΎ
(β€β₯βπ)):(β€β₯βπ)βΆβ) |
15 | 14 | frexr 43710 |
. . . . . . 7
β’
(((((π β§ πΉ β dom ~~>*) β§
(~~>*βπΉ) β
β) β§ π β
π) β§ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) β (πΉ βΎ
(β€β₯βπ)):(β€β₯βπ)βΆβ*) |
16 | 9 | adantr 482 |
. . . . . . . . 9
β’ ((((π β§ πΉ β dom ~~>*) β§ (~~>*βπΉ) β β) β§ π β π) β πΉ~~>*(~~>*βπΉ)) |
17 | 3, 4 | fuzxrpmcn 44159 |
. . . . . . . . . . 11
β’ (π β πΉ β (β*
βpm β)) |
18 | 17 | ad3antrrr 729 |
. . . . . . . . . 10
β’ ((((π β§ πΉ β dom ~~>*) β§ (~~>*βπΉ) β β) β§ π β π) β πΉ β (β*
βpm β)) |
19 | 11 | adantl 483 |
. . . . . . . . . 10
β’ ((((π β§ πΉ β dom ~~>*) β§ (~~>*βπΉ) β β) β§ π β π) β π β β€) |
20 | 18, 19 | xlimres 44152 |
. . . . . . . . 9
β’ ((((π β§ πΉ β dom ~~>*) β§ (~~>*βπΉ) β β) β§ π β π) β (πΉ~~>*(~~>*βπΉ) β (πΉ βΎ (β€β₯βπ))~~>*(~~>*βπΉ))) |
21 | 16, 20 | mpbid 231 |
. . . . . . . 8
β’ ((((π β§ πΉ β dom ~~>*) β§ (~~>*βπΉ) β β) β§ π β π) β (πΉ βΎ (β€β₯βπ))~~>*(~~>*βπΉ)) |
22 | 21 | adantr 482 |
. . . . . . 7
β’
(((((π β§ πΉ β dom ~~>*) β§
(~~>*βπΉ) β
β) β§ π β
π) β§ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) β (πΉ βΎ
(β€β₯βπ))~~>*(~~>*βπΉ)) |
23 | | simpllr 775 |
. . . . . . 7
β’
(((((π β§ πΉ β dom ~~>*) β§
(~~>*βπΉ) β
β) β§ π β
π) β§ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) β
(~~>*βπΉ) β
β) |
24 | 12, 13, 15, 22, 23 | xlimclimdm 44185 |
. . . . . 6
β’
(((((π β§ πΉ β dom ~~>*) β§
(~~>*βπΉ) β
β) β§ π β
π) β§ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) β (πΉ βΎ
(β€β₯βπ)) β dom β ) |
25 | 12, 13, 14, 24 | climliminflimsupd 44132 |
. . . . 5
β’
(((((π β§ πΉ β dom ~~>*) β§
(~~>*βπΉ) β
β) β§ π β
π) β§ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) β (lim
infβ(πΉ βΎ
(β€β₯βπ))) = (lim supβ(πΉ βΎ (β€β₯βπ)))) |
26 | 11 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β π) β π β β€) |
27 | 17 | elexd 3467 |
. . . . . . . . 9
β’ (π β πΉ β V) |
28 | 27 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β π) β πΉ β V) |
29 | 4 | fdmd 6683 |
. . . . . . . . . 10
β’ (π β dom πΉ = π) |
30 | 26 | ssd 43382 |
. . . . . . . . . 10
β’ (π β π β β€) |
31 | 29, 30 | eqsstrd 3986 |
. . . . . . . . 9
β’ (π β dom πΉ β β€) |
32 | 31 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β π) β dom πΉ β β€) |
33 | 26, 13, 28, 32 | liminfresuz2 44118 |
. . . . . . 7
β’ ((π β§ π β π) β (lim infβ(πΉ βΎ (β€β₯βπ))) = (lim infβπΉ)) |
34 | 33 | eqcomd 2739 |
. . . . . 6
β’ ((π β§ π β π) β (lim infβπΉ) = (lim infβ(πΉ βΎ (β€β₯βπ)))) |
35 | 34 | ad5ant14 757 |
. . . . 5
β’
(((((π β§ πΉ β dom ~~>*) β§
(~~>*βπΉ) β
β) β§ π β
π) β§ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) β (lim
infβπΉ) = (lim
infβ(πΉ βΎ
(β€β₯βπ)))) |
36 | 26, 13, 28, 32 | limsupresuz2 44040 |
. . . . . . 7
β’ ((π β§ π β π) β (lim supβ(πΉ βΎ (β€β₯βπ))) = (lim supβπΉ)) |
37 | 36 | eqcomd 2739 |
. . . . . 6
β’ ((π β§ π β π) β (lim supβπΉ) = (lim supβ(πΉ βΎ (β€β₯βπ)))) |
38 | 37 | ad5ant14 757 |
. . . . 5
β’
(((((π β§ πΉ β dom ~~>*) β§
(~~>*βπΉ) β
β) β§ π β
π) β§ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) β (lim
supβπΉ) = (lim
supβ(πΉ βΎ
(β€β₯βπ)))) |
39 | 25, 35, 38 | 3eqtr4d 2783 |
. . . 4
β’
(((((π β§ πΉ β dom ~~>*) β§
(~~>*βπΉ) β
β) β§ π β
π) β§ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) β (lim
infβπΉ) = (lim
supβπΉ)) |
40 | 10, 39 | rexlimddv2 44154 |
. . 3
β’ (((π β§ πΉ β dom ~~>*) β§ (~~>*βπΉ) β β) β (lim
infβπΉ) = (lim
supβπΉ)) |
41 | | simpll 766 |
. . . . . 6
β’ (((π β§ πΉ β dom ~~>*) β§ (~~>*βπΉ) = +β) β π) |
42 | 8 | adantr 482 |
. . . . . . . 8
β’ ((πΉ β dom ~~>* β§
(~~>*βπΉ) = +β)
β πΉ~~>*(~~>*βπΉ)) |
43 | | simpr 486 |
. . . . . . . 8
β’ ((πΉ β dom ~~>* β§
(~~>*βπΉ) = +β)
β (~~>*βπΉ) =
+β) |
44 | 42, 43 | breqtrd 5135 |
. . . . . . 7
β’ ((πΉ β dom ~~>* β§
(~~>*βπΉ) = +β)
β πΉ~~>*+β) |
45 | 44 | adantll 713 |
. . . . . 6
β’ (((π β§ πΉ β dom ~~>*) β§ (~~>*βπΉ) = +β) β πΉ~~>*+β) |
46 | 17 | liminfcld 44101 |
. . . . . . . 8
β’ (π β (lim infβπΉ) β
β*) |
47 | 46 | adantr 482 |
. . . . . . 7
β’ ((π β§ πΉ~~>*+β) β (lim infβπΉ) β
β*) |
48 | 17 | limsupcld 44021 |
. . . . . . . 8
β’ (π β (lim supβπΉ) β
β*) |
49 | 48 | adantr 482 |
. . . . . . 7
β’ ((π β§ πΉ~~>*+β) β (lim supβπΉ) β
β*) |
50 | 1, 3, 4 | liminflelimsupuz 44116 |
. . . . . . . 8
β’ (π β (lim infβπΉ) β€ (lim supβπΉ)) |
51 | 50 | adantr 482 |
. . . . . . 7
β’ ((π β§ πΉ~~>*+β) β (lim infβπΉ) β€ (lim supβπΉ)) |
52 | 49 | pnfged 43799 |
. . . . . . . 8
β’ ((π β§ πΉ~~>*+β) β (lim supβπΉ) β€
+β) |
53 | 1 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ πΉ~~>*+β) β π β β€) |
54 | 4 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ πΉ~~>*+β) β πΉ:πβΆβ*) |
55 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ πΉ~~>*+β) β πΉ~~>*+β) |
56 | 53, 3, 54, 55 | xlimpnfliminf 44191 |
. . . . . . . 8
β’ ((π β§ πΉ~~>*+β) β (lim infβπΉ) = +β) |
57 | 52, 56 | breqtrrd 5137 |
. . . . . . 7
β’ ((π β§ πΉ~~>*+β) β (lim supβπΉ) β€ (lim infβπΉ)) |
58 | 47, 49, 51, 57 | xrletrid 13083 |
. . . . . 6
β’ ((π β§ πΉ~~>*+β) β (lim infβπΉ) = (lim supβπΉ)) |
59 | 41, 45, 58 | syl2anc 585 |
. . . . 5
β’ (((π β§ πΉ β dom ~~>*) β§ (~~>*βπΉ) = +β) β (lim
infβπΉ) = (lim
supβπΉ)) |
60 | 59 | adantlr 714 |
. . . 4
β’ ((((π β§ πΉ β dom ~~>*) β§ Β¬
(~~>*βπΉ) β
β) β§ (~~>*βπΉ) = +β) β (lim infβπΉ) = (lim supβπΉ)) |
61 | | simplll 774 |
. . . . 5
β’ ((((π β§ πΉ β dom ~~>*) β§ Β¬
(~~>*βπΉ) β
β) β§ Β¬ (~~>*βπΉ) = +β) β π) |
62 | 8 | ad2antrr 725 |
. . . . . . 7
β’ (((πΉ β dom ~~>* β§ Β¬
(~~>*βπΉ) β
β) β§ Β¬ (~~>*βπΉ) = +β) β πΉ~~>*(~~>*βπΉ)) |
63 | | xlimcl 44153 |
. . . . . . . . . 10
β’ (πΉ~~>*(~~>*βπΉ) β (~~>*βπΉ) β
β*) |
64 | 8, 63 | syl 17 |
. . . . . . . . 9
β’ (πΉ β dom ~~>* β
(~~>*βπΉ) β
β*) |
65 | 64 | ad2antrr 725 |
. . . . . . . 8
β’ (((πΉ β dom ~~>* β§ Β¬
(~~>*βπΉ) β
β) β§ Β¬ (~~>*βπΉ) = +β) β (~~>*βπΉ) β
β*) |
66 | | simplr 768 |
. . . . . . . 8
β’ (((πΉ β dom ~~>* β§ Β¬
(~~>*βπΉ) β
β) β§ Β¬ (~~>*βπΉ) = +β) β Β¬ (~~>*βπΉ) β
β) |
67 | | neqne 2948 |
. . . . . . . . 9
β’ (Β¬
(~~>*βπΉ) = +β
β (~~>*βπΉ) β
+β) |
68 | 67 | adantl 483 |
. . . . . . . 8
β’ (((πΉ β dom ~~>* β§ Β¬
(~~>*βπΉ) β
β) β§ Β¬ (~~>*βπΉ) = +β) β (~~>*βπΉ) β
+β) |
69 | 65, 66, 68 | xrnpnfmnf 43800 |
. . . . . . 7
β’ (((πΉ β dom ~~>* β§ Β¬
(~~>*βπΉ) β
β) β§ Β¬ (~~>*βπΉ) = +β) β (~~>*βπΉ) = -β) |
70 | 62, 69 | breqtrd 5135 |
. . . . . 6
β’ (((πΉ β dom ~~>* β§ Β¬
(~~>*βπΉ) β
β) β§ Β¬ (~~>*βπΉ) = +β) β πΉ~~>*-β) |
71 | 70 | adantlll 717 |
. . . . 5
β’ ((((π β§ πΉ β dom ~~>*) β§ Β¬
(~~>*βπΉ) β
β) β§ Β¬ (~~>*βπΉ) = +β) β πΉ~~>*-β) |
72 | 46 | adantr 482 |
. . . . . 6
β’ ((π β§ πΉ~~>*-β) β (lim infβπΉ) β
β*) |
73 | 48 | adantr 482 |
. . . . . 6
β’ ((π β§ πΉ~~>*-β) β (lim supβπΉ) β
β*) |
74 | 50 | adantr 482 |
. . . . . 6
β’ ((π β§ πΉ~~>*-β) β (lim infβπΉ) β€ (lim supβπΉ)) |
75 | 1 | adantr 482 |
. . . . . . . 8
β’ ((π β§ πΉ~~>*-β) β π β β€) |
76 | 4 | adantr 482 |
. . . . . . . 8
β’ ((π β§ πΉ~~>*-β) β πΉ:πβΆβ*) |
77 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ πΉ~~>*-β) β πΉ~~>*-β) |
78 | 75, 3, 76, 77 | xlimmnflimsup 44187 |
. . . . . . 7
β’ ((π β§ πΉ~~>*-β) β (lim supβπΉ) = -β) |
79 | 72 | mnfled 13064 |
. . . . . . 7
β’ ((π β§ πΉ~~>*-β) β -β β€ (lim
infβπΉ)) |
80 | 78, 79 | eqbrtrd 5131 |
. . . . . 6
β’ ((π β§ πΉ~~>*-β) β (lim supβπΉ) β€ (lim infβπΉ)) |
81 | 72, 73, 74, 80 | xrletrid 13083 |
. . . . 5
β’ ((π β§ πΉ~~>*-β) β (lim infβπΉ) = (lim supβπΉ)) |
82 | 61, 71, 81 | syl2anc 585 |
. . . 4
β’ ((((π β§ πΉ β dom ~~>*) β§ Β¬
(~~>*βπΉ) β
β) β§ Β¬ (~~>*βπΉ) = +β) β (lim infβπΉ) = (lim supβπΉ)) |
83 | 60, 82 | pm2.61dan 812 |
. . 3
β’ (((π β§ πΉ β dom ~~>*) β§ Β¬
(~~>*βπΉ) β
β) β (lim infβπΉ) = (lim supβπΉ)) |
84 | 40, 83 | pm2.61dan 812 |
. 2
β’ ((π β§ πΉ β dom ~~>*) β (lim
infβπΉ) = (lim
supβπΉ)) |
85 | 27 | adantr 482 |
. . . . 5
β’ ((π β§ (lim supβπΉ) = -β) β πΉ β V) |
86 | | mnfxr 11220 |
. . . . . 6
β’ -β
β β* |
87 | 86 | a1i 11 |
. . . . 5
β’ ((π β§ (lim supβπΉ) = -β) β -β
β β*) |
88 | | simpr 486 |
. . . . . 6
β’ ((π β§ (lim supβπΉ) = -β) β (lim
supβπΉ) =
-β) |
89 | 1 | adantr 482 |
. . . . . . 7
β’ ((π β§ (lim supβπΉ) = -β) β π β
β€) |
90 | 4 | adantr 482 |
. . . . . . 7
β’ ((π β§ (lim supβπΉ) = -β) β πΉ:πβΆβ*) |
91 | 89, 3, 90 | xlimmnflimsup2 44183 |
. . . . . 6
β’ ((π β§ (lim supβπΉ) = -β) β (πΉ~~>*-β β (lim
supβπΉ) =
-β)) |
92 | 88, 91 | mpbird 257 |
. . . . 5
β’ ((π β§ (lim supβπΉ) = -β) β πΉ~~>*-β) |
93 | 85, 87, 92 | breldmd 5872 |
. . . 4
β’ ((π β§ (lim supβπΉ) = -β) β πΉ β dom
~~>*) |
94 | 93 | adantlr 714 |
. . 3
β’ (((π β§ (lim infβπΉ) = (lim supβπΉ)) β§ (lim supβπΉ) = -β) β πΉ β dom
~~>*) |
95 | 1 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ (lim infβπΉ) = (lim supβπΉ)) β§ (lim supβπΉ) β β) β π β
β€) |
96 | 4 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ (lim infβπΉ) = (lim supβπΉ)) β§ (lim supβπΉ) β β) β πΉ:πβΆβ*) |
97 | | simpr 486 |
. . . . . . . 8
β’ (((π β§ (lim infβπΉ) = (lim supβπΉ)) β§ (lim supβπΉ) β β) β (lim
supβπΉ) β
β) |
98 | 97 | renepnfd 11214 |
. . . . . . 7
β’ (((π β§ (lim infβπΉ) = (lim supβπΉ)) β§ (lim supβπΉ) β β) β (lim
supβπΉ) β
+β) |
99 | | simplr 768 |
. . . . . . . . 9
β’ (((π β§ (lim infβπΉ) = (lim supβπΉ)) β§ (lim supβπΉ) β β) β (lim
infβπΉ) = (lim
supβπΉ)) |
100 | 99, 97 | eqeltrd 2834 |
. . . . . . . 8
β’ (((π β§ (lim infβπΉ) = (lim supβπΉ)) β§ (lim supβπΉ) β β) β (lim
infβπΉ) β
β) |
101 | 100 | renemnfd 11215 |
. . . . . . 7
β’ (((π β§ (lim infβπΉ) = (lim supβπΉ)) β§ (lim supβπΉ) β β) β (lim
infβπΉ) β
-β) |
102 | 95, 3, 96, 98, 101 | liminflimsupxrre 44148 |
. . . . . 6
β’ (((π β§ (lim infβπΉ) = (lim supβπΉ)) β§ (lim supβπΉ) β β) β
βπ β π (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) |
103 | 3 | eluzelz2 43728 |
. . . . . . . . 9
β’ (π β π β π β β€) |
104 | 103 | ad2antlr 726 |
. . . . . . . 8
β’
(((((π β§ (lim
infβπΉ) = (lim
supβπΉ)) β§ (lim
supβπΉ) β
β) β§ π β
π) β§ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) β π β
β€) |
105 | | eqid 2733 |
. . . . . . . 8
β’
(β€β₯βπ) = (β€β₯βπ) |
106 | | simpr 486 |
. . . . . . . 8
β’
(((((π β§ (lim
infβπΉ) = (lim
supβπΉ)) β§ (lim
supβπΉ) β
β) β§ π β
π) β§ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) β (πΉ βΎ
(β€β₯βπ)):(β€β₯βπ)βΆβ) |
107 | | simplll 774 |
. . . . . . . . . . 11
β’ ((((π β§ (lim infβπΉ) = (lim supβπΉ)) β§ (lim supβπΉ) β β) β§ π β π) β π) |
108 | | simpl 484 |
. . . . . . . . . . . . 13
β’ (((lim
infβπΉ) = (lim
supβπΉ) β§ (lim
supβπΉ) β
β) β (lim infβπΉ) = (lim supβπΉ)) |
109 | | simpr 486 |
. . . . . . . . . . . . 13
β’ (((lim
infβπΉ) = (lim
supβπΉ) β§ (lim
supβπΉ) β
β) β (lim supβπΉ) β β) |
110 | 108, 109 | eqeltrd 2834 |
. . . . . . . . . . . 12
β’ (((lim
infβπΉ) = (lim
supβπΉ) β§ (lim
supβπΉ) β
β) β (lim infβπΉ) β β) |
111 | 110 | ad4ant23 752 |
. . . . . . . . . . 11
β’ ((((π β§ (lim infβπΉ) = (lim supβπΉ)) β§ (lim supβπΉ) β β) β§ π β π) β (lim infβπΉ) β β) |
112 | | simpr 486 |
. . . . . . . . . . 11
β’ ((((π β§ (lim infβπΉ) = (lim supβπΉ)) β§ (lim supβπΉ) β β) β§ π β π) β π β π) |
113 | 103 | 3ad2ant3 1136 |
. . . . . . . . . . . . 13
β’ ((π β§ (lim infβπΉ) β β β§ π β π) β π β β€) |
114 | 27 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
β’ ((π β§ (lim infβπΉ) β β β§ π β π) β πΉ β V) |
115 | 31 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
β’ ((π β§ (lim infβπΉ) β β β§ π β π) β dom πΉ β β€) |
116 | 113, 105,
114, 115 | liminfresuz2 44118 |
. . . . . . . . . . . 12
β’ ((π β§ (lim infβπΉ) β β β§ π β π) β (lim infβ(πΉ βΎ (β€β₯βπ))) = (lim infβπΉ)) |
117 | | simp2 1138 |
. . . . . . . . . . . 12
β’ ((π β§ (lim infβπΉ) β β β§ π β π) β (lim infβπΉ) β β) |
118 | 116, 117 | eqeltrd 2834 |
. . . . . . . . . . 11
β’ ((π β§ (lim infβπΉ) β β β§ π β π) β (lim infβ(πΉ βΎ (β€β₯βπ))) β
β) |
119 | 107, 111,
112, 118 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((((π β§ (lim infβπΉ) = (lim supβπΉ)) β§ (lim supβπΉ) β β) β§ π β π) β (lim infβ(πΉ βΎ (β€β₯βπ))) β
β) |
120 | 119 | adantr 482 |
. . . . . . . . 9
β’
(((((π β§ (lim
infβπΉ) = (lim
supβπΉ)) β§ (lim
supβπΉ) β
β) β§ π β
π) β§ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) β (lim
infβ(πΉ βΎ
(β€β₯βπ))) β β) |
121 | | simp2 1138 |
. . . . . . . . . . 11
β’ ((π β§ (lim infβπΉ) = (lim supβπΉ) β§ π β π) β (lim infβπΉ) = (lim supβπΉ)) |
122 | 103 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β π β β€) |
123 | 27 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β πΉ β V) |
124 | 31 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β dom πΉ β β€) |
125 | 122, 105,
123, 124 | liminfresuz2 44118 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β (lim infβ(πΉ βΎ (β€β₯βπ))) = (lim infβπΉ)) |
126 | 125 | 3adant2 1132 |
. . . . . . . . . . 11
β’ ((π β§ (lim infβπΉ) = (lim supβπΉ) β§ π β π) β (lim infβ(πΉ βΎ (β€β₯βπ))) = (lim infβπΉ)) |
127 | 122, 105,
123, 124 | limsupresuz2 44040 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β (lim supβ(πΉ βΎ (β€β₯βπ))) = (lim supβπΉ)) |
128 | 127 | 3adant2 1132 |
. . . . . . . . . . 11
β’ ((π β§ (lim infβπΉ) = (lim supβπΉ) β§ π β π) β (lim supβ(πΉ βΎ (β€β₯βπ))) = (lim supβπΉ)) |
129 | 121, 126,
128 | 3eqtr4d 2783 |
. . . . . . . . . 10
β’ ((π β§ (lim infβπΉ) = (lim supβπΉ) β§ π β π) β (lim infβ(πΉ βΎ (β€β₯βπ))) = (lim supβ(πΉ βΎ
(β€β₯βπ)))) |
130 | 129 | ad5ant124 1366 |
. . . . . . . . 9
β’
(((((π β§ (lim
infβπΉ) = (lim
supβπΉ)) β§ (lim
supβπΉ) β
β) β§ π β
π) β§ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) β (lim
infβ(πΉ βΎ
(β€β₯βπ))) = (lim supβ(πΉ βΎ (β€β₯βπ)))) |
131 | 104, 105,
106 | climliminflimsup3 44141 |
. . . . . . . . 9
β’
(((((π β§ (lim
infβπΉ) = (lim
supβπΉ)) β§ (lim
supβπΉ) β
β) β§ π β
π) β§ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) β ((πΉ βΎ
(β€β₯βπ)) β dom β β ((lim
infβ(πΉ βΎ
(β€β₯βπ))) β β β§ (lim
infβ(πΉ βΎ
(β€β₯βπ))) = (lim supβ(πΉ βΎ (β€β₯βπ)))))) |
132 | 120, 130,
131 | mpbir2and 712 |
. . . . . . . 8
β’
(((((π β§ (lim
infβπΉ) = (lim
supβπΉ)) β§ (lim
supβπΉ) β
β) β§ π β
π) β§ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) β (πΉ βΎ
(β€β₯βπ)) β dom β ) |
133 | 104, 105,
106, 132 | dmclimxlim 44182 |
. . . . . . 7
β’
(((((π β§ (lim
infβπΉ) = (lim
supβπΉ)) β§ (lim
supβπΉ) β
β) β§ π β
π) β§ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) β (πΉ βΎ
(β€β₯βπ)) β dom ~~>*) |
134 | 17 | ad4antr 731 |
. . . . . . . 8
β’
(((((π β§ (lim
infβπΉ) = (lim
supβπΉ)) β§ (lim
supβπΉ) β
β) β§ π β
π) β§ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) β πΉ β (β*
βpm β)) |
135 | 134, 104 | xlimresdm 44190 |
. . . . . . 7
β’
(((((π β§ (lim
infβπΉ) = (lim
supβπΉ)) β§ (lim
supβπΉ) β
β) β§ π β
π) β§ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) β (πΉ β dom ~~>* β (πΉ βΎ
(β€β₯βπ)) β dom ~~>*)) |
136 | 133, 135 | mpbird 257 |
. . . . . 6
β’
(((((π β§ (lim
infβπΉ) = (lim
supβπΉ)) β§ (lim
supβπΉ) β
β) β§ π β
π) β§ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆβ) β πΉ β dom
~~>*) |
137 | 102, 136 | rexlimddv2 44154 |
. . . . 5
β’ (((π β§ (lim infβπΉ) = (lim supβπΉ)) β§ (lim supβπΉ) β β) β πΉ β dom
~~>*) |
138 | 137 | adantlr 714 |
. . . 4
β’ ((((π β§ (lim infβπΉ) = (lim supβπΉ)) β§ (lim supβπΉ) β -β) β§ (lim
supβπΉ) β
β) β πΉ β
dom ~~>*) |
139 | | simpll 766 |
. . . . 5
β’ ((((π β§ (lim infβπΉ) = (lim supβπΉ)) β§ (lim supβπΉ) β -β) β§ Β¬
(lim supβπΉ) β
β) β (π β§ (lim
infβπΉ) = (lim
supβπΉ))) |
140 | | simpllr 775 |
. . . . . 6
β’ ((((π β§ (lim infβπΉ) = (lim supβπΉ)) β§ (lim supβπΉ) β -β) β§ Β¬
(lim supβπΉ) β
β) β (lim infβπΉ) = (lim supβπΉ)) |
141 | 48 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ (lim supβπΉ) β -β) β§ Β¬
(lim supβπΉ) β
β) β (lim supβπΉ) β
β*) |
142 | | simpr 486 |
. . . . . . . 8
β’ (((π β§ (lim supβπΉ) β -β) β§ Β¬
(lim supβπΉ) β
β) β Β¬ (lim supβπΉ) β β) |
143 | | simplr 768 |
. . . . . . . 8
β’ (((π β§ (lim supβπΉ) β -β) β§ Β¬
(lim supβπΉ) β
β) β (lim supβπΉ) β -β) |
144 | 141, 142,
143 | xrnmnfpnf 43385 |
. . . . . . 7
β’ (((π β§ (lim supβπΉ) β -β) β§ Β¬
(lim supβπΉ) β
β) β (lim supβπΉ) = +β) |
145 | 144 | adantllr 718 |
. . . . . 6
β’ ((((π β§ (lim infβπΉ) = (lim supβπΉ)) β§ (lim supβπΉ) β -β) β§ Β¬
(lim supβπΉ) β
β) β (lim supβπΉ) = +β) |
146 | 140, 145 | eqtrd 2773 |
. . . . 5
β’ ((((π β§ (lim infβπΉ) = (lim supβπΉ)) β§ (lim supβπΉ) β -β) β§ Β¬
(lim supβπΉ) β
β) β (lim infβπΉ) = +β) |
147 | 27 | adantr 482 |
. . . . . . 7
β’ ((π β§ (lim infβπΉ) = +β) β πΉ β V) |
148 | | pnfxr 11217 |
. . . . . . . 8
β’ +β
β β* |
149 | 148 | a1i 11 |
. . . . . . 7
β’ ((π β§ (lim infβπΉ) = +β) β +β
β β*) |
150 | 1, 3, 4 | xlimpnfliminf2 44192 |
. . . . . . . 8
β’ (π β (πΉ~~>*+β β (lim infβπΉ) = +β)) |
151 | 150 | biimpar 479 |
. . . . . . 7
β’ ((π β§ (lim infβπΉ) = +β) β πΉ~~>*+β) |
152 | 147, 149,
151 | breldmd 5872 |
. . . . . 6
β’ ((π β§ (lim infβπΉ) = +β) β πΉ β dom
~~>*) |
153 | 152 | adantlr 714 |
. . . . 5
β’ (((π β§ (lim infβπΉ) = (lim supβπΉ)) β§ (lim infβπΉ) = +β) β πΉ β dom
~~>*) |
154 | 139, 146,
153 | syl2anc 585 |
. . . 4
β’ ((((π β§ (lim infβπΉ) = (lim supβπΉ)) β§ (lim supβπΉ) β -β) β§ Β¬
(lim supβπΉ) β
β) β πΉ β
dom ~~>*) |
155 | 138, 154 | pm2.61dan 812 |
. . 3
β’ (((π β§ (lim infβπΉ) = (lim supβπΉ)) β§ (lim supβπΉ) β -β) β πΉ β dom
~~>*) |
156 | 94, 155 | pm2.61dane 3029 |
. 2
β’ ((π β§ (lim infβπΉ) = (lim supβπΉ)) β πΉ β dom ~~>*) |
157 | 84, 156 | impbida 800 |
1
β’ (π β (πΉ β dom ~~>* β (lim infβπΉ) = (lim supβπΉ))) |