Metamath Proof Explorer

Theorem xlimliminflimsup

Description: A sequence of extended reals converges if and only if its inferior limit and its superior limit are equal. (Contributed by Glauco Siliprandi, 23-Apr-2023)

Ref Expression
Hypotheses xlimliminflimsup.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
xlimliminflimsup.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
xlimliminflimsup.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
Assertion xlimliminflimsup ( 𝜑 → ( 𝐹 ∈ dom ~~>* ↔ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 xlimliminflimsup.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2 xlimliminflimsup.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 xlimliminflimsup.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
4 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) ∧ ( ~~>* ‘ 𝐹 ) ∈ ℝ ) → 𝑀 ∈ ℤ )
5 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) ∧ ( ~~>* ‘ 𝐹 ) ∈ ℝ ) → 𝐹 : 𝑍 ⟶ ℝ* )
6 simpr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) ∧ ( ~~>* ‘ 𝐹 ) ∈ ℝ ) → ( ~~>* ‘ 𝐹 ) ∈ ℝ )
7 xlimdm ⊢ ( 𝐹 ∈ dom ~~>* ↔ 𝐹 ~~>* ( ~~>* ‘ 𝐹 ) )
8 7 biimpi ⊢ ( 𝐹 ∈ dom ~~>* → 𝐹 ~~>* ( ~~>* ‘ 𝐹 ) )
9 8 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) ∧ ( ~~>* ‘ 𝐹 ) ∈ ℝ ) → 𝐹 ~~>* ( ~~>* ‘ 𝐹 ) )
10 4 2 5 6 9 xlimxrre ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) ∧ ( ~~>* ‘ 𝐹 ) ∈ ℝ ) → ∃ 𝑗 ∈ 𝑍 ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ )
11 2 eluzelz2 ⊢ ( 𝑗 ∈ 𝑍 → 𝑗 ∈ ℤ )
12 11 ad2antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) ∧ ( ~~>* ‘ 𝐹 ) ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ ) → 𝑗 ∈ ℤ )
13 eqid ⊢ ( ℤ≥ ‘ 𝑗 ) = ( ℤ≥ ‘ 𝑗 )
14 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) ∧ ( ~~>* ‘ 𝐹 ) ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ )
15 14 frexr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) ∧ ( ~~>* ‘ 𝐹 ) ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ* )
16 9 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) ∧ ( ~~>* ‘ 𝐹 ) ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) → 𝐹 ~~>* ( ~~>* ‘ 𝐹 ) )
17 2 3 fuzxrpmcn ⊢ ( 𝜑 → 𝐹 ∈ ( ℝ* ↑pm ℂ ) )
18 17 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) ∧ ( ~~>* ‘ 𝐹 ) ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) → 𝐹 ∈ ( ℝ* ↑pm ℂ ) )
19 11 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) ∧ ( ~~>* ‘ 𝐹 ) ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ ℤ )
20 18 19 xlimres ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) ∧ ( ~~>* ‘ 𝐹 ) ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ~~>* ( ~~>* ‘ 𝐹 ) ↔ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) ~~>* ( ~~>* ‘ 𝐹 ) ) )
21 16 20 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) ∧ ( ~~>* ‘ 𝐹 ) ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) ~~>* ( ~~>* ‘ 𝐹 ) )
22 21 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) ∧ ( ~~>* ‘ 𝐹 ) ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) ~~>* ( ~~>* ‘ 𝐹 ) )
23 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) ∧ ( ~~>* ‘ 𝐹 ) ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ ) → ( ~~>* ‘ 𝐹 ) ∈ ℝ )
24 12 13 15 22 23 xlimclimdm ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) ∧ ( ~~>* ‘ 𝐹 ) ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) ∈ dom ⇝ )
25 12 13 14 24 climliminflimsupd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) ∧ ( ~~>* ‘ 𝐹 ) ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ ) → ( lim inf ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) ) = ( lim sup ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) ) )
26 11 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝑗 ∈ ℤ )
27 17 elexd ⊢ ( 𝜑 → 𝐹 ∈ V )
28 27 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝐹 ∈ V )
29 3 fdmd ⊢ ( 𝜑 → dom 𝐹 = 𝑍 )
30 26 ssd ⊢ ( 𝜑 → 𝑍 ⊆ ℤ )
31 29 30 eqsstrd ⊢ ( 𝜑 → dom 𝐹 ⊆ ℤ )
32 31 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → dom 𝐹 ⊆ ℤ )
33 26 13 28 32 liminfresuz2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( lim inf ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) ) = ( lim inf ‘ 𝐹 ) )
34 33 eqcomd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( lim inf ‘ 𝐹 ) = ( lim inf ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) ) )
35 34 ad5ant14 ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) ∧ ( ~~>* ‘ 𝐹 ) ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ ) → ( lim inf ‘ 𝐹 ) = ( lim inf ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) ) )
36 26 13 28 32 limsupresuz2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( lim sup ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) ) = ( lim sup ‘ 𝐹 ) )
37 36 eqcomd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( lim sup ‘ 𝐹 ) = ( lim sup ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) ) )
38 37 ad5ant14 ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) ∧ ( ~~>* ‘ 𝐹 ) ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ ) → ( lim sup ‘ 𝐹 ) = ( lim sup ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) ) )
39 25 35 38 3eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) ∧ ( ~~>* ‘ 𝐹 ) ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ℝ ) → ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) )
40 10 39 rexlimddv2 ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) ∧ ( ~~>* ‘ 𝐹 ) ∈ ℝ ) → ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) )
41 simpll ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) ∧ ( ~~>* ‘ 𝐹 ) = +∞ ) → 𝜑 )
42 8 adantr ⊢ ( ( 𝐹 ∈ dom ~~>* ∧ ( ~~>* ‘ 𝐹 ) = +∞ ) → 𝐹 ~~>* ( ~~>* ‘ 𝐹 ) )
43 simpr ⊢ ( ( 𝐹 ∈ dom ~~>* ∧ ( ~~>* ‘ 𝐹 ) = +∞ ) → ( ~~>* ‘ 𝐹 ) = +∞ )
44 42 43 breqtrd ⊢ ( ( 𝐹 ∈ dom ~~>* ∧ ( ~~>* ‘ 𝐹 ) = +∞ ) → 𝐹 ~~>* +∞ )
45 44 adantll ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) ∧ ( ~~>* ‘ 𝐹 ) = +∞ ) → 𝐹 ~~>* +∞ )
46 17 liminfcld ⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) ∈ ℝ* )
47 46 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ~~>* +∞ ) → ( lim inf ‘ 𝐹 ) ∈ ℝ* )
48 17 limsupcld ⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ∈ ℝ* )
49 48 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ~~>* +∞ ) → ( lim sup ‘ 𝐹 ) ∈ ℝ* )
50 1 2 3 liminflelimsupuz ⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) ≤ ( lim sup ‘ 𝐹 ) )
51 50 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ~~>* +∞ ) → ( lim inf ‘ 𝐹 ) ≤ ( lim sup ‘ 𝐹 ) )
52 49 pnfged ⊢ ( ( 𝜑 ∧ 𝐹 ~~>* +∞ ) → ( lim sup ‘ 𝐹 ) ≤ +∞ )
53 1 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ~~>* +∞ ) → 𝑀 ∈ ℤ )
54 3 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ~~>* +∞ ) → 𝐹 : 𝑍 ⟶ ℝ* )
55 simpr ⊢ ( ( 𝜑 ∧ 𝐹 ~~>* +∞ ) → 𝐹 ~~>* +∞ )
56 53 2 54 55 xlimpnfliminf ⊢ ( ( 𝜑 ∧ 𝐹 ~~>* +∞ ) → ( lim inf ‘ 𝐹 ) = +∞ )
57 52 56 breqtrrd ⊢ ( ( 𝜑 ∧ 𝐹 ~~>* +∞ ) → ( lim sup ‘ 𝐹 ) ≤ ( lim inf ‘ 𝐹 ) )
58 47 49 51 57 xrletrid ⊢ ( ( 𝜑 ∧ 𝐹 ~~>* +∞ ) → ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) )
59 41 45 58 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) ∧ ( ~~>* ‘ 𝐹 ) = +∞ ) → ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) )
60 59 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) ∧ ¬ ( ~~>* ‘ 𝐹 ) ∈ ℝ ) ∧ ( ~~>* ‘ 𝐹 ) = +∞ ) → ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) )
61 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) ∧ ¬ ( ~~>* ‘ 𝐹 ) ∈ ℝ ) ∧ ¬ ( ~~>* ‘ 𝐹 ) = +∞ ) → 𝜑 )
62 8 ad2antrr ⊢ ( ( ( 𝐹 ∈ dom ~~>* ∧ ¬ ( ~~>* ‘ 𝐹 ) ∈ ℝ ) ∧ ¬ ( ~~>* ‘ 𝐹 ) = +∞ ) → 𝐹 ~~>* ( ~~>* ‘ 𝐹 ) )
63 xlimcl ⊢ ( 𝐹 ~~>* ( ~~>* ‘ 𝐹 ) → ( ~~>* ‘ 𝐹 ) ∈ ℝ* )
64 8 63 syl ⊢ ( 𝐹 ∈ dom ~~>* → ( ~~>* ‘ 𝐹 ) ∈ ℝ* )
65 64 ad2antrr ⊢ ( ( ( 𝐹 ∈ dom ~~>* ∧ ¬ ( ~~>* ‘ 𝐹 ) ∈ ℝ ) ∧ ¬ ( ~~>* ‘ 𝐹 ) = +∞ ) → ( ~~>* ‘ 𝐹 ) ∈ ℝ* )
66 simplr ⊢ ( ( ( 𝐹 ∈ dom ~~>* ∧ ¬ ( ~~>* ‘ 𝐹 ) ∈ ℝ ) ∧ ¬ ( ~~>* ‘ 𝐹 ) = +∞ ) → ¬ ( ~~>* ‘ 𝐹 ) ∈ ℝ )
67 neqne ⊢ ( ¬ ( ~~>* ‘ 𝐹 ) = +∞ → ( ~~>* ‘ 𝐹 ) ≠ +∞ )
68 67 adantl ⊢ ( ( ( 𝐹 ∈ dom ~~>* ∧ ¬ ( ~~>* ‘ 𝐹 ) ∈ ℝ ) ∧ ¬ ( ~~>* ‘ 𝐹 ) = +∞ ) → ( ~~>* ‘ 𝐹 ) ≠ +∞ )
69 65 66 68 xrnpnfmnf ⊢ ( ( ( 𝐹 ∈ dom ~~>* ∧ ¬ ( ~~>* ‘ 𝐹 ) ∈ ℝ ) ∧ ¬ ( ~~>* ‘ 𝐹 ) = +∞ ) → ( ~~>* ‘ 𝐹 ) = -∞ )
70 62 69 breqtrd ⊢ ( ( ( 𝐹 ∈ dom ~~>* ∧ ¬ ( ~~>* ‘ 𝐹 ) ∈ ℝ ) ∧ ¬ ( ~~>* ‘ 𝐹 ) = +∞ ) → 𝐹 ~~>* -∞ )
71 70 adantlll ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) ∧ ¬ ( ~~>* ‘ 𝐹 ) ∈ ℝ ) ∧ ¬ ( ~~>* ‘ 𝐹 ) = +∞ ) → 𝐹 ~~>* -∞ )
72 46 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ~~>* -∞ ) → ( lim inf ‘ 𝐹 ) ∈ ℝ* )
73 48 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ~~>* -∞ ) → ( lim sup ‘ 𝐹 ) ∈ ℝ* )
74 50 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ~~>* -∞ ) → ( lim inf ‘ 𝐹 ) ≤ ( lim sup ‘ 𝐹 ) )
75 1 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ~~>* -∞ ) → 𝑀 ∈ ℤ )
76 3 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ~~>* -∞ ) → 𝐹 : 𝑍 ⟶ ℝ* )
77 simpr ⊢ ( ( 𝜑 ∧ 𝐹 ~~>* -∞ ) → 𝐹 ~~>* -∞ )
78 75 2 76 77 xlimmnflimsup ⊢ ( ( 𝜑 ∧ 𝐹 ~~>* -∞ ) → ( lim sup ‘ 𝐹 ) = -∞ )
79 72 mnfled ⊢ ( ( 𝜑 ∧ 𝐹 ~~>* -∞ ) → -∞ ≤ ( lim inf ‘ 𝐹 ) )
80 78 79 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝐹 ~~>* -∞ ) → ( lim sup ‘ 𝐹 ) ≤ ( lim inf ‘ 𝐹 ) )
81 72 73 74 80 xrletrid ⊢ ( ( 𝜑 ∧ 𝐹 ~~>* -∞ ) → ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) )
82 61 71 81 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) ∧ ¬ ( ~~>* ‘ 𝐹 ) ∈ ℝ ) ∧ ¬ ( ~~>* ‘ 𝐹 ) = +∞ ) → ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) )
83 60 82 pm2.61dan ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) ∧ ¬ ( ~~>* ‘ 𝐹 ) ∈ ℝ ) → ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) )
84 40 83 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) → ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) )
85 27 adantr ⊢ ( ( 𝜑 ∧ ( lim sup ‘ 𝐹 ) = -∞ ) → 𝐹 ∈ V )
86 mnfxr ⊢ -∞ ∈ ℝ*
87 86 a1i ⊢ ( ( 𝜑 ∧ ( lim sup ‘ 𝐹 ) = -∞ ) → -∞ ∈ ℝ* )
88 simpr ⊢ ( ( 𝜑 ∧ ( lim sup ‘ 𝐹 ) = -∞ ) → ( lim sup ‘ 𝐹 ) = -∞ )
89 1 adantr ⊢ ( ( 𝜑 ∧ ( lim sup ‘ 𝐹 ) = -∞ ) → 𝑀 ∈ ℤ )
90 3 adantr ⊢ ( ( 𝜑 ∧ ( lim sup ‘ 𝐹 ) = -∞ ) → 𝐹 : 𝑍 ⟶ ℝ* )
91 89 2 90 xlimmnflimsup2 ⊢ ( ( 𝜑 ∧ ( lim sup ‘ 𝐹 ) = -∞ ) → ( 𝐹 ~~>* -∞ ↔ ( lim sup ‘ 𝐹 ) = -∞ ) )
92 88 91 mpbird ⊢ ( ( 𝜑 ∧ ( lim sup ‘ 𝐹 ) = -∞ ) → 𝐹 ~~>* -∞ )
93 85 87 92 breldmd ⊢ ( ( 𝜑 ∧ ( lim sup ‘ 𝐹 ) = -∞ ) → 𝐹 ∈ dom ~~>* )
94 93 adantlr ⊢ ( ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) ∧ ( lim sup ‘ 𝐹 ) = -∞ ) → 𝐹 ∈ dom ~~>* )
95 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) ∧ ( lim sup ‘ 𝐹 ) ∈ ℝ ) → 𝑀 ∈ ℤ )
96 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) ∧ ( lim sup ‘ 𝐹 ) ∈ ℝ ) → 𝐹 : 𝑍 ⟶ ℝ* )
97 simpr ⊢ ( ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) ∧ ( lim sup ‘ 𝐹 ) ∈ ℝ ) → ( lim sup ‘ 𝐹 ) ∈ ℝ )
98 97 renepnfd ⊢ ( ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) ∧ ( lim sup ‘ 𝐹 ) ∈ ℝ ) → ( lim sup ‘ 𝐹 ) ≠ +∞ )
99 simplr ⊢ ( ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) ∧ ( lim sup ‘ 𝐹 ) ∈ ℝ ) → ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) )
100 99 97 eqeltrd ⊢ ( ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) ∧ ( lim sup ‘ 𝐹 ) ∈ ℝ ) → ( lim inf ‘ 𝐹 ) ∈ ℝ )
101 100 renemnfd ⊢ ( ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) ∧ ( lim sup ‘ 𝐹 ) ∈ ℝ ) → ( lim inf ‘ 𝐹 ) ≠ -∞ )
102 95 2 96 98 101 liminflimsupxrre ⊢ ( ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) ∧ ( lim sup ‘ 𝐹 ) ∈ ℝ ) → ∃ 𝑚 ∈ 𝑍 ( 𝐹 ↾ ( ℤ≥ ‘ 𝑚 ) ) : ( ℤ≥ ‘ 𝑚 ) ⟶ ℝ )
103 2 eluzelz2 ⊢ ( 𝑚 ∈ 𝑍 → 𝑚 ∈ ℤ )
104 103 ad2antlr ⊢ ( ( ( ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) ∧ ( lim sup ‘ 𝐹 ) ∈ ℝ ) ∧ 𝑚 ∈ 𝑍 ) ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑚 ) ) : ( ℤ≥ ‘ 𝑚 ) ⟶ ℝ ) → 𝑚 ∈ ℤ )
105 eqid ⊢ ( ℤ≥ ‘ 𝑚 ) = ( ℤ≥ ‘ 𝑚 )
106 simpr ⊢ ( ( ( ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) ∧ ( lim sup ‘ 𝐹 ) ∈ ℝ ) ∧ 𝑚 ∈ 𝑍 ) ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑚 ) ) : ( ℤ≥ ‘ 𝑚 ) ⟶ ℝ ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑚 ) ) : ( ℤ≥ ‘ 𝑚 ) ⟶ ℝ )
107 simplll ⊢ ( ( ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) ∧ ( lim sup ‘ 𝐹 ) ∈ ℝ ) ∧ 𝑚 ∈ 𝑍 ) → 𝜑 )
108 simpl ⊢ ( ( ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ∧ ( lim sup ‘ 𝐹 ) ∈ ℝ ) → ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) )
109 simpr ⊢ ( ( ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ∧ ( lim sup ‘ 𝐹 ) ∈ ℝ ) → ( lim sup ‘ 𝐹 ) ∈ ℝ )
110 108 109 eqeltrd ⊢ ( ( ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ∧ ( lim sup ‘ 𝐹 ) ∈ ℝ ) → ( lim inf ‘ 𝐹 ) ∈ ℝ )
111 110 ad4ant23 ⊢ ( ( ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) ∧ ( lim sup ‘ 𝐹 ) ∈ ℝ ) ∧ 𝑚 ∈ 𝑍 ) → ( lim inf ‘ 𝐹 ) ∈ ℝ )
112 simpr ⊢ ( ( ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) ∧ ( lim sup ‘ 𝐹 ) ∈ ℝ ) ∧ 𝑚 ∈ 𝑍 ) → 𝑚 ∈ 𝑍 )
113 103 3ad2ant3 ⊢ ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) ∈ ℝ ∧ 𝑚 ∈ 𝑍 ) → 𝑚 ∈ ℤ )
114 27 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) ∈ ℝ ∧ 𝑚 ∈ 𝑍 ) → 𝐹 ∈ V )
115 31 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) ∈ ℝ ∧ 𝑚 ∈ 𝑍 ) → dom 𝐹 ⊆ ℤ )
116 113 105 114 115 liminfresuz2 ⊢ ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) ∈ ℝ ∧ 𝑚 ∈ 𝑍 ) → ( lim inf ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑚 ) ) ) = ( lim inf ‘ 𝐹 ) )
117 simp2 ⊢ ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) ∈ ℝ ∧ 𝑚 ∈ 𝑍 ) → ( lim inf ‘ 𝐹 ) ∈ ℝ )
118 116 117 eqeltrd ⊢ ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) ∈ ℝ ∧ 𝑚 ∈ 𝑍 ) → ( lim inf ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑚 ) ) ) ∈ ℝ )
119 107 111 112 118 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) ∧ ( lim sup ‘ 𝐹 ) ∈ ℝ ) ∧ 𝑚 ∈ 𝑍 ) → ( lim inf ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑚 ) ) ) ∈ ℝ )
120 119 adantr ⊢ ( ( ( ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) ∧ ( lim sup ‘ 𝐹 ) ∈ ℝ ) ∧ 𝑚 ∈ 𝑍 ) ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑚 ) ) : ( ℤ≥ ‘ 𝑚 ) ⟶ ℝ ) → ( lim inf ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑚 ) ) ) ∈ ℝ )
121 simp2 ⊢ ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ∧ 𝑚 ∈ 𝑍 ) → ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) )
122 103 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → 𝑚 ∈ ℤ )
123 27 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → 𝐹 ∈ V )
124 31 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → dom 𝐹 ⊆ ℤ )
125 122 105 123 124 liminfresuz2 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( lim inf ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑚 ) ) ) = ( lim inf ‘ 𝐹 ) )
126 125 3adant2 ⊢ ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ∧ 𝑚 ∈ 𝑍 ) → ( lim inf ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑚 ) ) ) = ( lim inf ‘ 𝐹 ) )
127 122 105 123 124 limsupresuz2 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( lim sup ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑚 ) ) ) = ( lim sup ‘ 𝐹 ) )
128 127 3adant2 ⊢ ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ∧ 𝑚 ∈ 𝑍 ) → ( lim sup ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑚 ) ) ) = ( lim sup ‘ 𝐹 ) )
129 121 126 128 3eqtr4d ⊢ ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ∧ 𝑚 ∈ 𝑍 ) → ( lim inf ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑚 ) ) ) = ( lim sup ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑚 ) ) ) )
130 129 ad5ant124 ⊢ ( ( ( ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) ∧ ( lim sup ‘ 𝐹 ) ∈ ℝ ) ∧ 𝑚 ∈ 𝑍 ) ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑚 ) ) : ( ℤ≥ ‘ 𝑚 ) ⟶ ℝ ) → ( lim inf ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑚 ) ) ) = ( lim sup ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑚 ) ) ) )
131 104 105 106 climliminflimsup3 ⊢ ( ( ( ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) ∧ ( lim sup ‘ 𝐹 ) ∈ ℝ ) ∧ 𝑚 ∈ 𝑍 ) ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑚 ) ) : ( ℤ≥ ‘ 𝑚 ) ⟶ ℝ ) → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑚 ) ) ∈ dom ⇝ ↔ ( ( lim inf ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑚 ) ) ) ∈ ℝ ∧ ( lim inf ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑚 ) ) ) = ( lim sup ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑚 ) ) ) ) ) )
132 120 130 131 mpbir2and ⊢ ( ( ( ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) ∧ ( lim sup ‘ 𝐹 ) ∈ ℝ ) ∧ 𝑚 ∈ 𝑍 ) ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑚 ) ) : ( ℤ≥ ‘ 𝑚 ) ⟶ ℝ ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑚 ) ) ∈ dom ⇝ )
133 104 105 106 132 dmclimxlim ⊢ ( ( ( ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) ∧ ( lim sup ‘ 𝐹 ) ∈ ℝ ) ∧ 𝑚 ∈ 𝑍 ) ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑚 ) ) : ( ℤ≥ ‘ 𝑚 ) ⟶ ℝ ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑚 ) ) ∈ dom ~~>* )
134 17 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) ∧ ( lim sup ‘ 𝐹 ) ∈ ℝ ) ∧ 𝑚 ∈ 𝑍 ) ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑚 ) ) : ( ℤ≥ ‘ 𝑚 ) ⟶ ℝ ) → 𝐹 ∈ ( ℝ* ↑pm ℂ ) )
135 134 104 xlimresdm ⊢ ( ( ( ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) ∧ ( lim sup ‘ 𝐹 ) ∈ ℝ ) ∧ 𝑚 ∈ 𝑍 ) ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑚 ) ) : ( ℤ≥ ‘ 𝑚 ) ⟶ ℝ ) → ( 𝐹 ∈ dom ~~>* ↔ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑚 ) ) ∈ dom ~~>* ) )
136 133 135 mpbird ⊢ ( ( ( ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) ∧ ( lim sup ‘ 𝐹 ) ∈ ℝ ) ∧ 𝑚 ∈ 𝑍 ) ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑚 ) ) : ( ℤ≥ ‘ 𝑚 ) ⟶ ℝ ) → 𝐹 ∈ dom ~~>* )
137 102 136 rexlimddv2 ⊢ ( ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) ∧ ( lim sup ‘ 𝐹 ) ∈ ℝ ) → 𝐹 ∈ dom ~~>* )
138 137 adantlr ⊢ ( ( ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) ∧ ( lim sup ‘ 𝐹 ) ≠ -∞ ) ∧ ( lim sup ‘ 𝐹 ) ∈ ℝ ) → 𝐹 ∈ dom ~~>* )
139 simpll ⊢ ( ( ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) ∧ ( lim sup ‘ 𝐹 ) ≠ -∞ ) ∧ ¬ ( lim sup ‘ 𝐹 ) ∈ ℝ ) → ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) )
140 simpllr ⊢ ( ( ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) ∧ ( lim sup ‘ 𝐹 ) ≠ -∞ ) ∧ ¬ ( lim sup ‘ 𝐹 ) ∈ ℝ ) → ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) )
141 48 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( lim sup ‘ 𝐹 ) ≠ -∞ ) ∧ ¬ ( lim sup ‘ 𝐹 ) ∈ ℝ ) → ( lim sup ‘ 𝐹 ) ∈ ℝ* )
142 simpr ⊢ ( ( ( 𝜑 ∧ ( lim sup ‘ 𝐹 ) ≠ -∞ ) ∧ ¬ ( lim sup ‘ 𝐹 ) ∈ ℝ ) → ¬ ( lim sup ‘ 𝐹 ) ∈ ℝ )
143 simplr ⊢ ( ( ( 𝜑 ∧ ( lim sup ‘ 𝐹 ) ≠ -∞ ) ∧ ¬ ( lim sup ‘ 𝐹 ) ∈ ℝ ) → ( lim sup ‘ 𝐹 ) ≠ -∞ )
144 141 142 143 xrnmnfpnf ⊢ ( ( ( 𝜑 ∧ ( lim sup ‘ 𝐹 ) ≠ -∞ ) ∧ ¬ ( lim sup ‘ 𝐹 ) ∈ ℝ ) → ( lim sup ‘ 𝐹 ) = +∞ )
145 144 adantllr ⊢ ( ( ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) ∧ ( lim sup ‘ 𝐹 ) ≠ -∞ ) ∧ ¬ ( lim sup ‘ 𝐹 ) ∈ ℝ ) → ( lim sup ‘ 𝐹 ) = +∞ )
146 140 145 eqtrd ⊢ ( ( ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) ∧ ( lim sup ‘ 𝐹 ) ≠ -∞ ) ∧ ¬ ( lim sup ‘ 𝐹 ) ∈ ℝ ) → ( lim inf ‘ 𝐹 ) = +∞ )
147 27 adantr ⊢ ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = +∞ ) → 𝐹 ∈ V )
148 pnfxr ⊢ +∞ ∈ ℝ*
149 148 a1i ⊢ ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = +∞ ) → +∞ ∈ ℝ* )
150 1 2 3 xlimpnfliminf2 ⊢ ( 𝜑 → ( 𝐹 ~~>* +∞ ↔ ( lim inf ‘ 𝐹 ) = +∞ ) )
151 150 biimpar ⊢ ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = +∞ ) → 𝐹 ~~>* +∞ )
152 147 149 151 breldmd ⊢ ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = +∞ ) → 𝐹 ∈ dom ~~>* )
153 152 adantlr ⊢ ( ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) ∧ ( lim inf ‘ 𝐹 ) = +∞ ) → 𝐹 ∈ dom ~~>* )
154 139 146 153 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) ∧ ( lim sup ‘ 𝐹 ) ≠ -∞ ) ∧ ¬ ( lim sup ‘ 𝐹 ) ∈ ℝ ) → 𝐹 ∈ dom ~~>* )
155 138 154 pm2.61dan ⊢ ( ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) ∧ ( lim sup ‘ 𝐹 ) ≠ -∞ ) → 𝐹 ∈ dom ~~>* )
156 94 155 pm2.61dane ⊢ ( ( 𝜑 ∧ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) → 𝐹 ∈ dom ~~>* )
157 84 156 impbida ⊢ ( 𝜑 → ( 𝐹 ∈ dom ~~>* ↔ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) )