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 ‘ 𝐹 ) )