Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  xlimliminflimsup Structured version   Visualization version   GIF version

Theorem xlimliminflimsup 43791
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.)
Hypotheses
Ref Expression
xlimliminflimsup.m (𝜑𝑀 ∈ ℤ)
xlimliminflimsup.z 𝑍 = (ℤ𝑀)
xlimliminflimsup.f (𝜑𝐹:𝑍⟶ℝ*)
Assertion
Ref Expression
xlimliminflimsup (𝜑 → (𝐹 ∈ dom ~~>* ↔ (lim inf‘𝐹) = (lim sup‘𝐹)))

Proof of Theorem xlimliminflimsup
Dummy variables 𝑗 𝑚 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 xlimliminflimsup.m . . . . . 6 (𝜑𝑀 ∈ ℤ)
21ad2antrr 723 . . . . 5 (((𝜑𝐹 ∈ dom ~~>*) ∧ (~~>*‘𝐹) ∈ ℝ) → 𝑀 ∈ ℤ)
3 xlimliminflimsup.z . . . . 5 𝑍 = (ℤ𝑀)
4 xlimliminflimsup.f . . . . . 6 (𝜑𝐹:𝑍⟶ℝ*)
54ad2antrr 723 . . . . 5 (((𝜑𝐹 ∈ dom ~~>*) ∧ (~~>*‘𝐹) ∈ ℝ) → 𝐹:𝑍⟶ℝ*)
6 simpr 485 . . . . 5 (((𝜑𝐹 ∈ dom ~~>*) ∧ (~~>*‘𝐹) ∈ ℝ) → (~~>*‘𝐹) ∈ ℝ)
7 xlimdm 43786 . . . . . . 7 (𝐹 ∈ dom ~~>* ↔ 𝐹~~>*(~~>*‘𝐹))
87biimpi 215 . . . . . 6 (𝐹 ∈ dom ~~>* → 𝐹~~>*(~~>*‘𝐹))
98ad2antlr 724 . . . . 5 (((𝜑𝐹 ∈ dom ~~>*) ∧ (~~>*‘𝐹) ∈ ℝ) → 𝐹~~>*(~~>*‘𝐹))
102, 3, 5, 6, 9xlimxrre 43760 . . . 4 (((𝜑𝐹 ∈ dom ~~>*) ∧ (~~>*‘𝐹) ∈ ℝ) → ∃𝑗𝑍 (𝐹 ↾ (ℤ𝑗)):(ℤ𝑗)⟶ℝ)
113eluzelz2 43330 . . . . . . 7 (𝑗𝑍𝑗 ∈ ℤ)
1211ad2antlr 724 . . . . . 6 (((((𝜑𝐹 ∈ dom ~~>*) ∧ (~~>*‘𝐹) ∈ ℝ) ∧ 𝑗𝑍) ∧ (𝐹 ↾ (ℤ𝑗)):(ℤ𝑗)⟶ℝ) → 𝑗 ∈ ℤ)
13 eqid 2736 . . . . . 6 (ℤ𝑗) = (ℤ𝑗)
14 simpr 485 . . . . . 6 (((((𝜑𝐹 ∈ dom ~~>*) ∧ (~~>*‘𝐹) ∈ ℝ) ∧ 𝑗𝑍) ∧ (𝐹 ↾ (ℤ𝑗)):(ℤ𝑗)⟶ℝ) → (𝐹 ↾ (ℤ𝑗)):(ℤ𝑗)⟶ℝ)
1514frexr 43311 . . . . . . 7 (((((𝜑𝐹 ∈ dom ~~>*) ∧ (~~>*‘𝐹) ∈ ℝ) ∧ 𝑗𝑍) ∧ (𝐹 ↾ (ℤ𝑗)):(ℤ𝑗)⟶ℝ) → (𝐹 ↾ (ℤ𝑗)):(ℤ𝑗)⟶ℝ*)
169adantr 481 . . . . . . . . 9 ((((𝜑𝐹 ∈ dom ~~>*) ∧ (~~>*‘𝐹) ∈ ℝ) ∧ 𝑗𝑍) → 𝐹~~>*(~~>*‘𝐹))
173, 4fuzxrpmcn 43757 . . . . . . . . . . 11 (𝜑𝐹 ∈ (ℝ*pm ℂ))
1817ad3antrrr 727 . . . . . . . . . 10 ((((𝜑𝐹 ∈ dom ~~>*) ∧ (~~>*‘𝐹) ∈ ℝ) ∧ 𝑗𝑍) → 𝐹 ∈ (ℝ*pm ℂ))
1911adantl 482 . . . . . . . . . 10 ((((𝜑𝐹 ∈ dom ~~>*) ∧ (~~>*‘𝐹) ∈ ℝ) ∧ 𝑗𝑍) → 𝑗 ∈ ℤ)
2018, 19xlimres 43750 . . . . . . . . 9 ((((𝜑𝐹 ∈ dom ~~>*) ∧ (~~>*‘𝐹) ∈ ℝ) ∧ 𝑗𝑍) → (𝐹~~>*(~~>*‘𝐹) ↔ (𝐹 ↾ (ℤ𝑗))~~>*(~~>*‘𝐹)))
2116, 20mpbid 231 . . . . . . . 8 ((((𝜑𝐹 ∈ dom ~~>*) ∧ (~~>*‘𝐹) ∈ ℝ) ∧ 𝑗𝑍) → (𝐹 ↾ (ℤ𝑗))~~>*(~~>*‘𝐹))
2221adantr 481 . . . . . . 7 (((((𝜑𝐹 ∈ dom ~~>*) ∧ (~~>*‘𝐹) ∈ ℝ) ∧ 𝑗𝑍) ∧ (𝐹 ↾ (ℤ𝑗)):(ℤ𝑗)⟶ℝ) → (𝐹 ↾ (ℤ𝑗))~~>*(~~>*‘𝐹))
23 simpllr 773 . . . . . . 7 (((((𝜑𝐹 ∈ dom ~~>*) ∧ (~~>*‘𝐹) ∈ ℝ) ∧ 𝑗𝑍) ∧ (𝐹 ↾ (ℤ𝑗)):(ℤ𝑗)⟶ℝ) → (~~>*‘𝐹) ∈ ℝ)
2412, 13, 15, 22, 23xlimclimdm 43783 . . . . . 6 (((((𝜑𝐹 ∈ dom ~~>*) ∧ (~~>*‘𝐹) ∈ ℝ) ∧ 𝑗𝑍) ∧ (𝐹 ↾ (ℤ𝑗)):(ℤ𝑗)⟶ℝ) → (𝐹 ↾ (ℤ𝑗)) ∈ dom ⇝ )
2512, 13, 14, 24climliminflimsupd 43730 . . . . 5 (((((𝜑𝐹 ∈ dom ~~>*) ∧ (~~>*‘𝐹) ∈ ℝ) ∧ 𝑗𝑍) ∧ (𝐹 ↾ (ℤ𝑗)):(ℤ𝑗)⟶ℝ) → (lim inf‘(𝐹 ↾ (ℤ𝑗))) = (lim sup‘(𝐹 ↾ (ℤ𝑗))))
2611adantl 482 . . . . . . . 8 ((𝜑𝑗𝑍) → 𝑗 ∈ ℤ)
2717elexd 3461 . . . . . . . . 9 (𝜑𝐹 ∈ V)
2827adantr 481 . . . . . . . 8 ((𝜑𝑗𝑍) → 𝐹 ∈ V)
294fdmd 6663 . . . . . . . . . 10 (𝜑 → dom 𝐹 = 𝑍)
3026ssd 43002 . . . . . . . . . 10 (𝜑𝑍 ⊆ ℤ)
3129, 30eqsstrd 3970 . . . . . . . . 9 (𝜑 → dom 𝐹 ⊆ ℤ)
3231adantr 481 . . . . . . . 8 ((𝜑𝑗𝑍) → dom 𝐹 ⊆ ℤ)
3326, 13, 28, 32liminfresuz2 43716 . . . . . . 7 ((𝜑𝑗𝑍) → (lim inf‘(𝐹 ↾ (ℤ𝑗))) = (lim inf‘𝐹))
3433eqcomd 2742 . . . . . 6 ((𝜑𝑗𝑍) → (lim inf‘𝐹) = (lim inf‘(𝐹 ↾ (ℤ𝑗))))
3534ad5ant14 755 . . . . 5 (((((𝜑𝐹 ∈ dom ~~>*) ∧ (~~>*‘𝐹) ∈ ℝ) ∧ 𝑗𝑍) ∧ (𝐹 ↾ (ℤ𝑗)):(ℤ𝑗)⟶ℝ) → (lim inf‘𝐹) = (lim inf‘(𝐹 ↾ (ℤ𝑗))))
3626, 13, 28, 32limsupresuz2 43638 . . . . . . 7 ((𝜑𝑗𝑍) → (lim sup‘(𝐹 ↾ (ℤ𝑗))) = (lim sup‘𝐹))
3736eqcomd 2742 . . . . . 6 ((𝜑𝑗𝑍) → (lim sup‘𝐹) = (lim sup‘(𝐹 ↾ (ℤ𝑗))))
3837ad5ant14 755 . . . . 5 (((((𝜑𝐹 ∈ dom ~~>*) ∧ (~~>*‘𝐹) ∈ ℝ) ∧ 𝑗𝑍) ∧ (𝐹 ↾ (ℤ𝑗)):(ℤ𝑗)⟶ℝ) → (lim sup‘𝐹) = (lim sup‘(𝐹 ↾ (ℤ𝑗))))
3925, 35, 383eqtr4d 2786 . . . 4 (((((𝜑𝐹 ∈ dom ~~>*) ∧ (~~>*‘𝐹) ∈ ℝ) ∧ 𝑗𝑍) ∧ (𝐹 ↾ (ℤ𝑗)):(ℤ𝑗)⟶ℝ) → (lim inf‘𝐹) = (lim sup‘𝐹))
4010, 39rexlimddv2 43752 . . 3 (((𝜑𝐹 ∈ dom ~~>*) ∧ (~~>*‘𝐹) ∈ ℝ) → (lim inf‘𝐹) = (lim sup‘𝐹))
41 simpll 764 . . . . . 6 (((𝜑𝐹 ∈ dom ~~>*) ∧ (~~>*‘𝐹) = +∞) → 𝜑)
428adantr 481 . . . . . . . 8 ((𝐹 ∈ dom ~~>* ∧ (~~>*‘𝐹) = +∞) → 𝐹~~>*(~~>*‘𝐹))
43 simpr 485 . . . . . . . 8 ((𝐹 ∈ dom ~~>* ∧ (~~>*‘𝐹) = +∞) → (~~>*‘𝐹) = +∞)
4442, 43breqtrd 5119 . . . . . . 7 ((𝐹 ∈ dom ~~>* ∧ (~~>*‘𝐹) = +∞) → 𝐹~~>*+∞)
4544adantll 711 . . . . . 6 (((𝜑𝐹 ∈ dom ~~>*) ∧ (~~>*‘𝐹) = +∞) → 𝐹~~>*+∞)
4617liminfcld 43699 . . . . . . . 8 (𝜑 → (lim inf‘𝐹) ∈ ℝ*)
4746adantr 481 . . . . . . 7 ((𝜑𝐹~~>*+∞) → (lim inf‘𝐹) ∈ ℝ*)
4817limsupcld 43619 . . . . . . . 8 (𝜑 → (lim sup‘𝐹) ∈ ℝ*)
4948adantr 481 . . . . . . 7 ((𝜑𝐹~~>*+∞) → (lim sup‘𝐹) ∈ ℝ*)
501, 3, 4liminflelimsupuz 43714 . . . . . . . 8 (𝜑 → (lim inf‘𝐹) ≤ (lim sup‘𝐹))
5150adantr 481 . . . . . . 7 ((𝜑𝐹~~>*+∞) → (lim inf‘𝐹) ≤ (lim sup‘𝐹))
5249pnfged 43401 . . . . . . . 8 ((𝜑𝐹~~>*+∞) → (lim sup‘𝐹) ≤ +∞)
531adantr 481 . . . . . . . . 9 ((𝜑𝐹~~>*+∞) → 𝑀 ∈ ℤ)
544adantr 481 . . . . . . . . 9 ((𝜑𝐹~~>*+∞) → 𝐹:𝑍⟶ℝ*)
55 simpr 485 . . . . . . . . 9 ((𝜑𝐹~~>*+∞) → 𝐹~~>*+∞)
5653, 3, 54, 55xlimpnfliminf 43789 . . . . . . . 8 ((𝜑𝐹~~>*+∞) → (lim inf‘𝐹) = +∞)
5752, 56breqtrrd 5121 . . . . . . 7 ((𝜑𝐹~~>*+∞) → (lim sup‘𝐹) ≤ (lim inf‘𝐹))
5847, 49, 51, 57xrletrid 12991 . . . . . 6 ((𝜑𝐹~~>*+∞) → (lim inf‘𝐹) = (lim sup‘𝐹))
5941, 45, 58syl2anc 584 . . . . 5 (((𝜑𝐹 ∈ dom ~~>*) ∧ (~~>*‘𝐹) = +∞) → (lim inf‘𝐹) = (lim sup‘𝐹))
6059adantlr 712 . . . 4 ((((𝜑𝐹 ∈ dom ~~>*) ∧ ¬ (~~>*‘𝐹) ∈ ℝ) ∧ (~~>*‘𝐹) = +∞) → (lim inf‘𝐹) = (lim sup‘𝐹))
61 simplll 772 . . . . 5 ((((𝜑𝐹 ∈ dom ~~>*) ∧ ¬ (~~>*‘𝐹) ∈ ℝ) ∧ ¬ (~~>*‘𝐹) = +∞) → 𝜑)
628ad2antrr 723 . . . . . . 7 (((𝐹 ∈ dom ~~>* ∧ ¬ (~~>*‘𝐹) ∈ ℝ) ∧ ¬ (~~>*‘𝐹) = +∞) → 𝐹~~>*(~~>*‘𝐹))
63 xlimcl 43751 . . . . . . . . . 10 (𝐹~~>*(~~>*‘𝐹) → (~~>*‘𝐹) ∈ ℝ*)
648, 63syl 17 . . . . . . . . 9 (𝐹 ∈ dom ~~>* → (~~>*‘𝐹) ∈ ℝ*)
6564ad2antrr 723 . . . . . . . 8 (((𝐹 ∈ dom ~~>* ∧ ¬ (~~>*‘𝐹) ∈ ℝ) ∧ ¬ (~~>*‘𝐹) = +∞) → (~~>*‘𝐹) ∈ ℝ*)
66 simplr 766 . . . . . . . 8 (((𝐹 ∈ dom ~~>* ∧ ¬ (~~>*‘𝐹) ∈ ℝ) ∧ ¬ (~~>*‘𝐹) = +∞) → ¬ (~~>*‘𝐹) ∈ ℝ)
67 neqne 2948 . . . . . . . . 9 (¬ (~~>*‘𝐹) = +∞ → (~~>*‘𝐹) ≠ +∞)
6867adantl 482 . . . . . . . 8 (((𝐹 ∈ dom ~~>* ∧ ¬ (~~>*‘𝐹) ∈ ℝ) ∧ ¬ (~~>*‘𝐹) = +∞) → (~~>*‘𝐹) ≠ +∞)
6965, 66, 68xrnpnfmnf 43402 . . . . . . 7 (((𝐹 ∈ dom ~~>* ∧ ¬ (~~>*‘𝐹) ∈ ℝ) ∧ ¬ (~~>*‘𝐹) = +∞) → (~~>*‘𝐹) = -∞)
7062, 69breqtrd 5119 . . . . . 6 (((𝐹 ∈ dom ~~>* ∧ ¬ (~~>*‘𝐹) ∈ ℝ) ∧ ¬ (~~>*‘𝐹) = +∞) → 𝐹~~>*-∞)
7170adantlll 715 . . . . 5 ((((𝜑𝐹 ∈ dom ~~>*) ∧ ¬ (~~>*‘𝐹) ∈ ℝ) ∧ ¬ (~~>*‘𝐹) = +∞) → 𝐹~~>*-∞)
7246adantr 481 . . . . . 6 ((𝜑𝐹~~>*-∞) → (lim inf‘𝐹) ∈ ℝ*)
7348adantr 481 . . . . . 6 ((𝜑𝐹~~>*-∞) → (lim sup‘𝐹) ∈ ℝ*)
7450adantr 481 . . . . . 6 ((𝜑𝐹~~>*-∞) → (lim inf‘𝐹) ≤ (lim sup‘𝐹))
751adantr 481 . . . . . . . 8 ((𝜑𝐹~~>*-∞) → 𝑀 ∈ ℤ)
764adantr 481 . . . . . . . 8 ((𝜑𝐹~~>*-∞) → 𝐹:𝑍⟶ℝ*)
77 simpr 485 . . . . . . . 8 ((𝜑𝐹~~>*-∞) → 𝐹~~>*-∞)
7875, 3, 76, 77xlimmnflimsup 43785 . . . . . . 7 ((𝜑𝐹~~>*-∞) → (lim sup‘𝐹) = -∞)
7972mnfled 43315 . . . . . . 7 ((𝜑𝐹~~>*-∞) → -∞ ≤ (lim inf‘𝐹))
8078, 79eqbrtrd 5115 . . . . . 6 ((𝜑𝐹~~>*-∞) → (lim sup‘𝐹) ≤ (lim inf‘𝐹))
8172, 73, 74, 80xrletrid 12991 . . . . 5 ((𝜑𝐹~~>*-∞) → (lim inf‘𝐹) = (lim sup‘𝐹))
8261, 71, 81syl2anc 584 . . . 4 ((((𝜑𝐹 ∈ dom ~~>*) ∧ ¬ (~~>*‘𝐹) ∈ ℝ) ∧ ¬ (~~>*‘𝐹) = +∞) → (lim inf‘𝐹) = (lim sup‘𝐹))
8360, 82pm2.61dan 810 . . 3 (((𝜑𝐹 ∈ dom ~~>*) ∧ ¬ (~~>*‘𝐹) ∈ ℝ) → (lim inf‘𝐹) = (lim sup‘𝐹))
8440, 83pm2.61dan 810 . 2 ((𝜑𝐹 ∈ dom ~~>*) → (lim inf‘𝐹) = (lim sup‘𝐹))
8527adantr 481 . . . . 5 ((𝜑 ∧ (lim sup‘𝐹) = -∞) → 𝐹 ∈ V)
86 mnfxr 11134 . . . . . 6 -∞ ∈ ℝ*
8786a1i 11 . . . . 5 ((𝜑 ∧ (lim sup‘𝐹) = -∞) → -∞ ∈ ℝ*)
88 simpr 485 . . . . . 6 ((𝜑 ∧ (lim sup‘𝐹) = -∞) → (lim sup‘𝐹) = -∞)
891adantr 481 . . . . . . 7 ((𝜑 ∧ (lim sup‘𝐹) = -∞) → 𝑀 ∈ ℤ)
904adantr 481 . . . . . . 7 ((𝜑 ∧ (lim sup‘𝐹) = -∞) → 𝐹:𝑍⟶ℝ*)
9189, 3, 90xlimmnflimsup2 43781 . . . . . 6 ((𝜑 ∧ (lim sup‘𝐹) = -∞) → (𝐹~~>*-∞ ↔ (lim sup‘𝐹) = -∞))
9288, 91mpbird 256 . . . . 5 ((𝜑 ∧ (lim sup‘𝐹) = -∞) → 𝐹~~>*-∞)
9385, 87, 92breldmd 5855 . . . 4 ((𝜑 ∧ (lim sup‘𝐹) = -∞) → 𝐹 ∈ dom ~~>*)
9493adantlr 712 . . 3 (((𝜑 ∧ (lim inf‘𝐹) = (lim sup‘𝐹)) ∧ (lim sup‘𝐹) = -∞) → 𝐹 ∈ dom ~~>*)
951ad2antrr 723 . . . . . . 7 (((𝜑 ∧ (lim inf‘𝐹) = (lim sup‘𝐹)) ∧ (lim sup‘𝐹) ∈ ℝ) → 𝑀 ∈ ℤ)
964ad2antrr 723 . . . . . . 7 (((𝜑 ∧ (lim inf‘𝐹) = (lim sup‘𝐹)) ∧ (lim sup‘𝐹) ∈ ℝ) → 𝐹:𝑍⟶ℝ*)
97 simpr 485 . . . . . . . 8 (((𝜑 ∧ (lim inf‘𝐹) = (lim sup‘𝐹)) ∧ (lim sup‘𝐹) ∈ ℝ) → (lim sup‘𝐹) ∈ ℝ)
9897renepnfd 11128 . . . . . . 7 (((𝜑 ∧ (lim inf‘𝐹) = (lim sup‘𝐹)) ∧ (lim sup‘𝐹) ∈ ℝ) → (lim sup‘𝐹) ≠ +∞)
99 simplr 766 . . . . . . . . 9 (((𝜑 ∧ (lim inf‘𝐹) = (lim sup‘𝐹)) ∧ (lim sup‘𝐹) ∈ ℝ) → (lim inf‘𝐹) = (lim sup‘𝐹))
10099, 97eqeltrd 2837 . . . . . . . 8 (((𝜑 ∧ (lim inf‘𝐹) = (lim sup‘𝐹)) ∧ (lim sup‘𝐹) ∈ ℝ) → (lim inf‘𝐹) ∈ ℝ)
101100renemnfd 11129 . . . . . . 7 (((𝜑 ∧ (lim inf‘𝐹) = (lim sup‘𝐹)) ∧ (lim sup‘𝐹) ∈ ℝ) → (lim inf‘𝐹) ≠ -∞)
10295, 3, 96, 98, 101liminflimsupxrre 43746 . . . . . 6 (((𝜑 ∧ (lim inf‘𝐹) = (lim sup‘𝐹)) ∧ (lim sup‘𝐹) ∈ ℝ) → ∃𝑚𝑍 (𝐹 ↾ (ℤ𝑚)):(ℤ𝑚)⟶ℝ)
1033eluzelz2 43330 . . . . . . . . 9 (𝑚𝑍𝑚 ∈ ℤ)
104103ad2antlr 724 . . . . . . . 8 (((((𝜑 ∧ (lim inf‘𝐹) = (lim sup‘𝐹)) ∧ (lim sup‘𝐹) ∈ ℝ) ∧ 𝑚𝑍) ∧ (𝐹 ↾ (ℤ𝑚)):(ℤ𝑚)⟶ℝ) → 𝑚 ∈ ℤ)
105 eqid 2736 . . . . . . . 8 (ℤ𝑚) = (ℤ𝑚)
106 simpr 485 . . . . . . . 8 (((((𝜑 ∧ (lim inf‘𝐹) = (lim sup‘𝐹)) ∧ (lim sup‘𝐹) ∈ ℝ) ∧ 𝑚𝑍) ∧ (𝐹 ↾ (ℤ𝑚)):(ℤ𝑚)⟶ℝ) → (𝐹 ↾ (ℤ𝑚)):(ℤ𝑚)⟶ℝ)
107 simplll 772 . . . . . . . . . . 11 ((((𝜑 ∧ (lim inf‘𝐹) = (lim sup‘𝐹)) ∧ (lim sup‘𝐹) ∈ ℝ) ∧ 𝑚𝑍) → 𝜑)
108 simpl 483 . . . . . . . . . . . . 13 (((lim inf‘𝐹) = (lim sup‘𝐹) ∧ (lim sup‘𝐹) ∈ ℝ) → (lim inf‘𝐹) = (lim sup‘𝐹))
109 simpr 485 . . . . . . . . . . . . 13 (((lim inf‘𝐹) = (lim sup‘𝐹) ∧ (lim sup‘𝐹) ∈ ℝ) → (lim sup‘𝐹) ∈ ℝ)
110108, 109eqeltrd 2837 . . . . . . . . . . . 12 (((lim inf‘𝐹) = (lim sup‘𝐹) ∧ (lim sup‘𝐹) ∈ ℝ) → (lim inf‘𝐹) ∈ ℝ)
111110ad4ant23 750 . . . . . . . . . . 11 ((((𝜑 ∧ (lim inf‘𝐹) = (lim sup‘𝐹)) ∧ (lim sup‘𝐹) ∈ ℝ) ∧ 𝑚𝑍) → (lim inf‘𝐹) ∈ ℝ)
112 simpr 485 . . . . . . . . . . 11 ((((𝜑 ∧ (lim inf‘𝐹) = (lim sup‘𝐹)) ∧ (lim sup‘𝐹) ∈ ℝ) ∧ 𝑚𝑍) → 𝑚𝑍)
1131033ad2ant3 1134 . . . . . . . . . . . . 13 ((𝜑 ∧ (lim inf‘𝐹) ∈ ℝ ∧ 𝑚𝑍) → 𝑚 ∈ ℤ)
114273ad2ant1 1132 . . . . . . . . . . . . 13 ((𝜑 ∧ (lim inf‘𝐹) ∈ ℝ ∧ 𝑚𝑍) → 𝐹 ∈ V)
115313ad2ant1 1132 . . . . . . . . . . . . 13 ((𝜑 ∧ (lim inf‘𝐹) ∈ ℝ ∧ 𝑚𝑍) → dom 𝐹 ⊆ ℤ)
116113, 105, 114, 115liminfresuz2 43716 . . . . . . . . . . . 12 ((𝜑 ∧ (lim inf‘𝐹) ∈ ℝ ∧ 𝑚𝑍) → (lim inf‘(𝐹 ↾ (ℤ𝑚))) = (lim inf‘𝐹))
117 simp2 1136 . . . . . . . . . . . 12 ((𝜑 ∧ (lim inf‘𝐹) ∈ ℝ ∧ 𝑚𝑍) → (lim inf‘𝐹) ∈ ℝ)
118116, 117eqeltrd 2837 . . . . . . . . . . 11 ((𝜑 ∧ (lim inf‘𝐹) ∈ ℝ ∧ 𝑚𝑍) → (lim inf‘(𝐹 ↾ (ℤ𝑚))) ∈ ℝ)
119107, 111, 112, 118syl3anc 1370 . . . . . . . . . 10 ((((𝜑 ∧ (lim inf‘𝐹) = (lim sup‘𝐹)) ∧ (lim sup‘𝐹) ∈ ℝ) ∧ 𝑚𝑍) → (lim inf‘(𝐹 ↾ (ℤ𝑚))) ∈ ℝ)
120119adantr 481 . . . . . . . . 9 (((((𝜑 ∧ (lim inf‘𝐹) = (lim sup‘𝐹)) ∧ (lim sup‘𝐹) ∈ ℝ) ∧ 𝑚𝑍) ∧ (𝐹 ↾ (ℤ𝑚)):(ℤ𝑚)⟶ℝ) → (lim inf‘(𝐹 ↾ (ℤ𝑚))) ∈ ℝ)
121 simp2 1136 . . . . . . . . . . 11 ((𝜑 ∧ (lim inf‘𝐹) = (lim sup‘𝐹) ∧ 𝑚𝑍) → (lim inf‘𝐹) = (lim sup‘𝐹))
122103adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑚𝑍) → 𝑚 ∈ ℤ)
12327adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑚𝑍) → 𝐹 ∈ V)
12431adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑚𝑍) → dom 𝐹 ⊆ ℤ)
125122, 105, 123, 124liminfresuz2 43716 . . . . . . . . . . . 12 ((𝜑𝑚𝑍) → (lim inf‘(𝐹 ↾ (ℤ𝑚))) = (lim inf‘𝐹))
1261253adant2 1130 . . . . . . . . . . 11 ((𝜑 ∧ (lim inf‘𝐹) = (lim sup‘𝐹) ∧ 𝑚𝑍) → (lim inf‘(𝐹 ↾ (ℤ𝑚))) = (lim inf‘𝐹))
127122, 105, 123, 124limsupresuz2 43638 . . . . . . . . . . . 12 ((𝜑𝑚𝑍) → (lim sup‘(𝐹 ↾ (ℤ𝑚))) = (lim sup‘𝐹))
1281273adant2 1130 . . . . . . . . . . 11 ((𝜑 ∧ (lim inf‘𝐹) = (lim sup‘𝐹) ∧ 𝑚𝑍) → (lim sup‘(𝐹 ↾ (ℤ𝑚))) = (lim sup‘𝐹))
129121, 126, 1283eqtr4d 2786 . . . . . . . . . 10 ((𝜑 ∧ (lim inf‘𝐹) = (lim sup‘𝐹) ∧ 𝑚𝑍) → (lim inf‘(𝐹 ↾ (ℤ𝑚))) = (lim sup‘(𝐹 ↾ (ℤ𝑚))))
130129ad5ant124 1364 . . . . . . . . 9 (((((𝜑 ∧ (lim inf‘𝐹) = (lim sup‘𝐹)) ∧ (lim sup‘𝐹) ∈ ℝ) ∧ 𝑚𝑍) ∧ (𝐹 ↾ (ℤ𝑚)):(ℤ𝑚)⟶ℝ) → (lim inf‘(𝐹 ↾ (ℤ𝑚))) = (lim sup‘(𝐹 ↾ (ℤ𝑚))))
131104, 105, 106climliminflimsup3 43739 . . . . . . . . 9 (((((𝜑 ∧ (lim inf‘𝐹) = (lim sup‘𝐹)) ∧ (lim sup‘𝐹) ∈ ℝ) ∧ 𝑚𝑍) ∧ (𝐹 ↾ (ℤ𝑚)):(ℤ𝑚)⟶ℝ) → ((𝐹 ↾ (ℤ𝑚)) ∈ dom ⇝ ↔ ((lim inf‘(𝐹 ↾ (ℤ𝑚))) ∈ ℝ ∧ (lim inf‘(𝐹 ↾ (ℤ𝑚))) = (lim sup‘(𝐹 ↾ (ℤ𝑚))))))
132120, 130, 131mpbir2and 710 . . . . . . . 8 (((((𝜑 ∧ (lim inf‘𝐹) = (lim sup‘𝐹)) ∧ (lim sup‘𝐹) ∈ ℝ) ∧ 𝑚𝑍) ∧ (𝐹 ↾ (ℤ𝑚)):(ℤ𝑚)⟶ℝ) → (𝐹 ↾ (ℤ𝑚)) ∈ dom ⇝ )
133104, 105, 106, 132dmclimxlim 43780 . . . . . . 7 (((((𝜑 ∧ (lim inf‘𝐹) = (lim sup‘𝐹)) ∧ (lim sup‘𝐹) ∈ ℝ) ∧ 𝑚𝑍) ∧ (𝐹 ↾ (ℤ𝑚)):(ℤ𝑚)⟶ℝ) → (𝐹 ↾ (ℤ𝑚)) ∈ dom ~~>*)
13417ad4antr 729 . . . . . . . 8 (((((𝜑 ∧ (lim inf‘𝐹) = (lim sup‘𝐹)) ∧ (lim sup‘𝐹) ∈ ℝ) ∧ 𝑚𝑍) ∧ (𝐹 ↾ (ℤ𝑚)):(ℤ𝑚)⟶ℝ) → 𝐹 ∈ (ℝ*pm ℂ))
135134, 104xlimresdm 43788 . . . . . . 7 (((((𝜑 ∧ (lim inf‘𝐹) = (lim sup‘𝐹)) ∧ (lim sup‘𝐹) ∈ ℝ) ∧ 𝑚𝑍) ∧ (𝐹 ↾ (ℤ𝑚)):(ℤ𝑚)⟶ℝ) → (𝐹 ∈ dom ~~>* ↔ (𝐹 ↾ (ℤ𝑚)) ∈ dom ~~>*))
136133, 135mpbird 256 . . . . . 6 (((((𝜑 ∧ (lim inf‘𝐹) = (lim sup‘𝐹)) ∧ (lim sup‘𝐹) ∈ ℝ) ∧ 𝑚𝑍) ∧ (𝐹 ↾ (ℤ𝑚)):(ℤ𝑚)⟶ℝ) → 𝐹 ∈ dom ~~>*)
137102, 136rexlimddv2 43752 . . . . 5 (((𝜑 ∧ (lim inf‘𝐹) = (lim sup‘𝐹)) ∧ (lim sup‘𝐹) ∈ ℝ) → 𝐹 ∈ dom ~~>*)
138137adantlr 712 . . . 4 ((((𝜑 ∧ (lim inf‘𝐹) = (lim sup‘𝐹)) ∧ (lim sup‘𝐹) ≠ -∞) ∧ (lim sup‘𝐹) ∈ ℝ) → 𝐹 ∈ dom ~~>*)
139 simpll 764 . . . . 5 ((((𝜑 ∧ (lim inf‘𝐹) = (lim sup‘𝐹)) ∧ (lim sup‘𝐹) ≠ -∞) ∧ ¬ (lim sup‘𝐹) ∈ ℝ) → (𝜑 ∧ (lim inf‘𝐹) = (lim sup‘𝐹)))
140 simpllr 773 . . . . . 6 ((((𝜑 ∧ (lim inf‘𝐹) = (lim sup‘𝐹)) ∧ (lim sup‘𝐹) ≠ -∞) ∧ ¬ (lim sup‘𝐹) ∈ ℝ) → (lim inf‘𝐹) = (lim sup‘𝐹))
14148ad2antrr 723 . . . . . . . 8 (((𝜑 ∧ (lim sup‘𝐹) ≠ -∞) ∧ ¬ (lim sup‘𝐹) ∈ ℝ) → (lim sup‘𝐹) ∈ ℝ*)
142 simpr 485 . . . . . . . 8 (((𝜑 ∧ (lim sup‘𝐹) ≠ -∞) ∧ ¬ (lim sup‘𝐹) ∈ ℝ) → ¬ (lim sup‘𝐹) ∈ ℝ)
143 simplr 766 . . . . . . . 8 (((𝜑 ∧ (lim sup‘𝐹) ≠ -∞) ∧ ¬ (lim sup‘𝐹) ∈ ℝ) → (lim sup‘𝐹) ≠ -∞)
144141, 142, 143xrnmnfpnf 43005 . . . . . . 7 (((𝜑 ∧ (lim sup‘𝐹) ≠ -∞) ∧ ¬ (lim sup‘𝐹) ∈ ℝ) → (lim sup‘𝐹) = +∞)
145144adantllr 716 . . . . . 6 ((((𝜑 ∧ (lim inf‘𝐹) = (lim sup‘𝐹)) ∧ (lim sup‘𝐹) ≠ -∞) ∧ ¬ (lim sup‘𝐹) ∈ ℝ) → (lim sup‘𝐹) = +∞)
146140, 145eqtrd 2776 . . . . 5 ((((𝜑 ∧ (lim inf‘𝐹) = (lim sup‘𝐹)) ∧ (lim sup‘𝐹) ≠ -∞) ∧ ¬ (lim sup‘𝐹) ∈ ℝ) → (lim inf‘𝐹) = +∞)
14727adantr 481 . . . . . . 7 ((𝜑 ∧ (lim inf‘𝐹) = +∞) → 𝐹 ∈ V)
148 pnfxr 11131 . . . . . . . 8 +∞ ∈ ℝ*
149148a1i 11 . . . . . . 7 ((𝜑 ∧ (lim inf‘𝐹) = +∞) → +∞ ∈ ℝ*)
1501, 3, 4xlimpnfliminf2 43790 . . . . . . . 8 (𝜑 → (𝐹~~>*+∞ ↔ (lim inf‘𝐹) = +∞))
151150biimpar 478 . . . . . . 7 ((𝜑 ∧ (lim inf‘𝐹) = +∞) → 𝐹~~>*+∞)
152147, 149, 151breldmd 5855 . . . . . 6 ((𝜑 ∧ (lim inf‘𝐹) = +∞) → 𝐹 ∈ dom ~~>*)
153152adantlr 712 . . . . 5 (((𝜑 ∧ (lim inf‘𝐹) = (lim sup‘𝐹)) ∧ (lim inf‘𝐹) = +∞) → 𝐹 ∈ dom ~~>*)
154139, 146, 153syl2anc 584 . . . 4 ((((𝜑 ∧ (lim inf‘𝐹) = (lim sup‘𝐹)) ∧ (lim sup‘𝐹) ≠ -∞) ∧ ¬ (lim sup‘𝐹) ∈ ℝ) → 𝐹 ∈ dom ~~>*)
155138, 154pm2.61dan 810 . . 3 (((𝜑 ∧ (lim inf‘𝐹) = (lim sup‘𝐹)) ∧ (lim sup‘𝐹) ≠ -∞) → 𝐹 ∈ dom ~~>*)
15694, 155pm2.61dane 3029 . 2 ((𝜑 ∧ (lim inf‘𝐹) = (lim sup‘𝐹)) → 𝐹 ∈ dom ~~>*)
15784, 156impbida 798 1 (𝜑 → (𝐹 ∈ dom ~~>* ↔ (lim inf‘𝐹) = (lim sup‘𝐹)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1086   = wceq 1540  wcel 2105  wne 2940  Vcvv 3441  wss 3898   class class class wbr 5093  dom cdm 5621  cres 5623  wf 6476  cfv 6480  (class class class)co 7338  pm cpm 8688  cc 10971  cr 10972  +∞cpnf 11108  -∞cmnf 11109  *cxr 11110  cle 11112  cz 12421  cuz 12684  lim supclsp 15279  cli 15293  lim infclsi 43680  ~~>*clsxlim 43747
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5230  ax-sep 5244  ax-nul 5251  ax-pow 5309  ax-pr 5373  ax-un 7651  ax-cnex 11029  ax-resscn 11030  ax-1cn 11031  ax-icn 11032  ax-addcl 11033  ax-addrcl 11034  ax-mulcl 11035  ax-mulrcl 11036  ax-mulcom 11037  ax-addass 11038  ax-mulass 11039  ax-distr 11040  ax-i2m1 11041  ax-1ne0 11042  ax-1rid 11043  ax-rnegex 11044  ax-rrecex 11045  ax-cnre 11046  ax-pre-lttri 11047  ax-pre-lttrn 11048  ax-pre-ltadd 11049  ax-pre-mulgt0 11050  ax-pre-sup 11051
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3917  df-nul 4271  df-if 4475  df-pw 4550  df-sn 4575  df-pr 4577  df-tp 4579  df-op 4581  df-uni 4854  df-int 4896  df-iun 4944  df-br 5094  df-opab 5156  df-mpt 5177  df-tr 5211  df-id 5519  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5576  df-we 5578  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6239  df-ord 6306  df-on 6307  df-lim 6308  df-suc 6309  df-iota 6432  df-fun 6482  df-fn 6483  df-f 6484  df-f1 6485  df-fo 6486  df-f1o 6487  df-fv 6488  df-isom 6489  df-riota 7294  df-ov 7341  df-oprab 7342  df-mpo 7343  df-om 7782  df-1st 7900  df-2nd 7901  df-frecs 8168  df-wrecs 8199  df-recs 8273  df-rdg 8312  df-1o 8368  df-er 8570  df-map 8689  df-pm 8690  df-en 8806  df-dom 8807  df-sdom 8808  df-fin 8809  df-fi 9269  df-sup 9300  df-inf 9301  df-pnf 11113  df-mnf 11114  df-xr 11115  df-ltxr 11116  df-le 11117  df-sub 11309  df-neg 11310  df-div 11735  df-nn 12076  df-2 12138  df-3 12139  df-4 12140  df-5 12141  df-6 12142  df-7 12143  df-8 12144  df-9 12145  df-n0 12336  df-z 12422  df-dec 12540  df-uz 12685  df-q 12791  df-rp 12833  df-xneg 12950  df-xadd 12951  df-xmul 12952  df-ioo 13185  df-ioc 13186  df-ico 13187  df-icc 13188  df-fz 13342  df-fzo 13485  df-fl 13614  df-ceil 13615  df-seq 13824  df-exp 13885  df-cj 14910  df-re 14911  df-im 14912  df-sqrt 15046  df-abs 15047  df-limsup 15280  df-clim 15297  df-rlim 15298  df-struct 16946  df-slot 16981  df-ndx 16993  df-base 17011  df-plusg 17073  df-mulr 17074  df-starv 17075  df-tset 17079  df-ple 17080  df-ds 17082  df-unif 17083  df-rest 17231  df-topn 17232  df-topgen 17252  df-ordt 17310  df-ps 18382  df-tsr 18383  df-psmet 20696  df-xmet 20697  df-met 20698  df-bl 20699  df-mopn 20700  df-cnfld 20705  df-top 22150  df-topon 22167  df-topsp 22189  df-bases 22203  df-lm 22487  df-haus 22573  df-xms 23580  df-ms 23581  df-liminf 43681  df-xlim 43748
This theorem is referenced by:  xlimlimsupleliminf  43792
  Copyright terms: Public domain W3C validator