Metamath Proof Explorer

Theorem climliminflimsupd

Description: If a sequence of real numbers converges, its inferior limit and its superior limit are equal. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses climliminflimsupd.1 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
climliminflimsupd.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
climliminflimsupd.3 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
climliminflimsupd.4 ⊢ ( 𝜑 → 𝐹 ∈ dom ⇝ )
Assertion climliminflimsupd ( 𝜑 → ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 climliminflimsupd.1 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2 climliminflimsupd.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 climliminflimsupd.3 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
4 climliminflimsupd.4 ⊢ ( 𝜑 → 𝐹 ∈ dom ⇝ )
5 3 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) )
6 5 fveq2d ⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) = ( lim inf ‘ ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) ) )
7 2 fvexi ⊢ 𝑍 ∈ V
8 7 mptex ⊢ ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) ∈ V
9 liminfcl ⊢ ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) ∈ V → ( lim inf ‘ ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) ) ∈ ℝ* )
10 8 9 ax-mp ⊢ ( lim inf ‘ ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) ) ∈ ℝ*
11 10 a1i ⊢ ( 𝜑 → ( lim inf ‘ ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) ) ∈ ℝ* )
12 6 11 eqeltrd ⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) ∈ ℝ* )
13 nfv ⊢ Ⅎ 𝑘 𝜑
14 3 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
15 14 renegcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → - ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
16 13 1 2 15 limsupvaluz4 ⊢ ( 𝜑 → ( lim sup ‘ ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ) = -𝑒 ( lim inf ‘ ( 𝑘 ∈ 𝑍 ↦ - - ( 𝐹 ‘ 𝑘 ) ) ) )
17 climrel ⊢ Rel ⇝
18 17 a1i ⊢ ( 𝜑 → Rel ⇝ )
19 nfcv ⊢ Ⅎ 𝑘 𝐹
20 1 2 3 climlimsup ⊢ ( 𝜑 → ( 𝐹 ∈ dom ⇝ ↔ 𝐹 ⇝ ( lim sup ‘ 𝐹 ) ) )
21 4 20 mpbid ⊢ ( 𝜑 → 𝐹 ⇝ ( lim sup ‘ 𝐹 ) )
22 14 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
23 13 19 2 1 21 22 climneg ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ⇝ - ( lim sup ‘ 𝐹 ) )
24 releldm ⊢ ( ( Rel ⇝ ∧ ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ⇝ - ( lim sup ‘ 𝐹 ) ) → ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ∈ dom ⇝ )
25 18 23 24 syl2anc ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ∈ dom ⇝ )
26 15 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) : 𝑍 ⟶ ℝ )
27 1 2 26 climlimsup ⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ∈ dom ⇝ ↔ ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ⇝ ( lim sup ‘ ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ) ) )
28 25 27 mpbid ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ⇝ ( lim sup ‘ ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ) )
29 climuni ⊢ ( ( ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ⇝ ( lim sup ‘ ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ) ∧ ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ⇝ - ( lim sup ‘ 𝐹 ) ) → ( lim sup ‘ ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ) = - ( lim sup ‘ 𝐹 ) )
30 28 23 29 syl2anc ⊢ ( 𝜑 → ( lim sup ‘ ( 𝑘 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑘 ) ) ) = - ( lim sup ‘ 𝐹 ) )
31 22 negnegd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → - - ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
32 31 mpteq2dva ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ - - ( 𝐹 ‘ 𝑘 ) ) = ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) )
33 32 5 eqtr4d ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ - - ( 𝐹 ‘ 𝑘 ) ) = 𝐹 )
34 33 fveq2d ⊢ ( 𝜑 → ( lim inf ‘ ( 𝑘 ∈ 𝑍 ↦ - - ( 𝐹 ‘ 𝑘 ) ) ) = ( lim inf ‘ 𝐹 ) )
35 34 xnegeqd ⊢ ( 𝜑 → -𝑒 ( lim inf ‘ ( 𝑘 ∈ 𝑍 ↦ - - ( 𝐹 ‘ 𝑘 ) ) ) = -𝑒 ( lim inf ‘ 𝐹 ) )
36 16 30 35 3eqtr3d ⊢ ( 𝜑 → - ( lim sup ‘ 𝐹 ) = -𝑒 ( lim inf ‘ 𝐹 ) )
37 2 1 21 14 climrecl ⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ∈ ℝ )
38 37 renegcld ⊢ ( 𝜑 → - ( lim sup ‘ 𝐹 ) ∈ ℝ )
39 36 38 eqeltrrd ⊢ ( 𝜑 → -𝑒 ( lim inf ‘ 𝐹 ) ∈ ℝ )
40 xnegrecl2 ⊢ ( ( ( lim inf ‘ 𝐹 ) ∈ ℝ* ∧ -𝑒 ( lim inf ‘ 𝐹 ) ∈ ℝ ) → ( lim inf ‘ 𝐹 ) ∈ ℝ )
41 12 39 40 syl2anc ⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) ∈ ℝ )
42 41 recnd ⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) ∈ ℂ )
43 37 recnd ⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ∈ ℂ )
44 41 rexnegd ⊢ ( 𝜑 → -𝑒 ( lim inf ‘ 𝐹 ) = - ( lim inf ‘ 𝐹 ) )
45 36 44 eqtr2d ⊢ ( 𝜑 → - ( lim inf ‘ 𝐹 ) = - ( lim sup ‘ 𝐹 ) )
46 42 43 45 neg11d ⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) )