Metamath Proof Explorer

Theorem liminfreuzlem

Description: Given a function on the reals, its inferior limit is real if and only if two condition holds: 1. there is a real number that is greater than or equal to the function, infinitely often; 2. there is a real number that is smaller than or equal to the function. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses liminfreuzlem.1 ⊢ Ⅎ 𝑗 𝐹
liminfreuzlem.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
liminfreuzlem.3 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
liminfreuzlem.4 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
Assertion liminfreuzlem ( 𝜑 → ( ( lim inf ‘ 𝐹 ) ∈ ℝ ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )

Proof

Step Hyp Ref Expression
1 liminfreuzlem.1 ⊢ Ⅎ 𝑗 𝐹
2 liminfreuzlem.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 liminfreuzlem.3 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4 liminfreuzlem.4 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
5 nfv ⊢ Ⅎ 𝑗 𝜑
6 5 1 2 3 4 liminfvaluz4 ⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) = -𝑒 ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑗 ) ) ) )
7 6 eleq1d ⊢ ( 𝜑 → ( ( lim inf ‘ 𝐹 ) ∈ ℝ ↔ -𝑒 ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ ) )
8 3 fvexi ⊢ 𝑍 ∈ V
9 8 mptex ⊢ ( 𝑗 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑗 ) ) ∈ V
10 limsupcl ⊢ ( ( 𝑗 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑗 ) ) ∈ V → ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ* )
11 9 10 ax-mp ⊢ ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ*
12 11 a1i ⊢ ( 𝜑 → ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ* )
13 12 xnegred ⊢ ( 𝜑 → ( ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ ↔ -𝑒 ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ ) )
14 7 13 bitr4d ⊢ ( 𝜑 → ( ( lim inf ‘ 𝐹 ) ∈ ℝ ↔ ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ ) )
15 4 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ )
16 15 renegcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → - ( 𝐹 ‘ 𝑗 ) ∈ ℝ )
17 5 2 3 16 limsupreuzmpt ⊢ ( 𝜑 → ( ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ ↔ ( ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑦 ≤ - ( 𝐹 ‘ 𝑗 ) ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑗 ∈ 𝑍 - ( 𝐹 ‘ 𝑗 ) ≤ 𝑦 ) ) )
18 renegcl ⊢ ( 𝑦 ∈ ℝ → - 𝑦 ∈ ℝ )
19 18 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑦 ≤ - ( 𝐹 ‘ 𝑗 ) ) → - 𝑦 ∈ ℝ )
20 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → 𝑦 ∈ ℝ )
21 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → 𝐹 : 𝑍 ⟶ ℝ )
22 3 uztrn2 ⊢ ( ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → 𝑗 ∈ 𝑍 )
23 22 adantll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → 𝑗 ∈ 𝑍 )
24 21 23 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ )
25 24 adantllr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ )
26 20 25 leneg2d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( 𝑦 ≤ - ( 𝐹 ‘ 𝑗 ) ↔ ( 𝐹 ‘ 𝑗 ) ≤ - 𝑦 ) )
27 26 rexbidva ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑘 ∈ 𝑍 ) → ( ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑦 ≤ - ( 𝐹 ‘ 𝑗 ) ↔ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ - 𝑦 ) )
28 27 ralbidva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑦 ≤ - ( 𝐹 ‘ 𝑗 ) ↔ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ - 𝑦 ) )
29 28 biimpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑦 ≤ - ( 𝐹 ‘ 𝑗 ) → ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ - 𝑦 ) )
30 29 imp ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑦 ≤ - ( 𝐹 ‘ 𝑗 ) ) → ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ - 𝑦 )
31 breq2 ⊢ ( 𝑥 = - 𝑦 → ( ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑗 ) ≤ - 𝑦 ) )
32 31 rexbidv ⊢ ( 𝑥 = - 𝑦 → ( ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ - 𝑦 ) )
33 32 ralbidv ⊢ ( 𝑥 = - 𝑦 → ( ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ - 𝑦 ) )
34 33 rspcev ⊢ ( ( - 𝑦 ∈ ℝ ∧ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ - 𝑦 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
35 19 30 34 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑦 ≤ - ( 𝐹 ‘ 𝑗 ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
36 35 rexlimdva2 ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑦 ≤ - ( 𝐹 ‘ 𝑗 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
37 renegcl ⊢ ( 𝑥 ∈ ℝ → - 𝑥 ∈ ℝ )
38 37 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → - 𝑥 ∈ ℝ )
39 24 adantllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ )
40 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → 𝑥 ∈ ℝ )
41 39 40 lenegd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ - 𝑥 ≤ - ( 𝐹 ‘ 𝑗 ) ) )
42 41 rexbidva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑘 ∈ 𝑍 ) → ( ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) - 𝑥 ≤ - ( 𝐹 ‘ 𝑗 ) ) )
43 42 ralbidva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) - 𝑥 ≤ - ( 𝐹 ‘ 𝑗 ) ) )
44 43 biimpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 → ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) - 𝑥 ≤ - ( 𝐹 ‘ 𝑗 ) ) )
45 44 imp ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) - 𝑥 ≤ - ( 𝐹 ‘ 𝑗 ) )
46 breq1 ⊢ ( 𝑦 = - 𝑥 → ( 𝑦 ≤ - ( 𝐹 ‘ 𝑗 ) ↔ - 𝑥 ≤ - ( 𝐹 ‘ 𝑗 ) ) )
47 46 rexbidv ⊢ ( 𝑦 = - 𝑥 → ( ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑦 ≤ - ( 𝐹 ‘ 𝑗 ) ↔ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) - 𝑥 ≤ - ( 𝐹 ‘ 𝑗 ) ) )
48 47 ralbidv ⊢ ( 𝑦 = - 𝑥 → ( ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑦 ≤ - ( 𝐹 ‘ 𝑗 ) ↔ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) - 𝑥 ≤ - ( 𝐹 ‘ 𝑗 ) ) )
49 48 rspcev ⊢ ( ( - 𝑥 ∈ ℝ ∧ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) - 𝑥 ≤ - ( 𝐹 ‘ 𝑗 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑦 ≤ - ( 𝐹 ‘ 𝑗 ) )
50 38 45 49 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑦 ≤ - ( 𝐹 ‘ 𝑗 ) )
51 50 rexlimdva2 ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 → ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑦 ≤ - ( 𝐹 ‘ 𝑗 ) ) )
52 36 51 impbid ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑦 ≤ - ( 𝐹 ‘ 𝑗 ) ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
53 18 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑗 ∈ 𝑍 - ( 𝐹 ‘ 𝑗 ) ≤ 𝑦 ) → - 𝑦 ∈ ℝ )
54 15 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ )
55 simplr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) → 𝑦 ∈ ℝ )
56 54 55 leneg3d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) → ( - ( 𝐹 ‘ 𝑗 ) ≤ 𝑦 ↔ - 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) )
57 56 ralbidva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ∀ 𝑗 ∈ 𝑍 - ( 𝐹 ‘ 𝑗 ) ≤ 𝑦 ↔ ∀ 𝑗 ∈ 𝑍 - 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) )
58 57 biimpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ∀ 𝑗 ∈ 𝑍 - ( 𝐹 ‘ 𝑗 ) ≤ 𝑦 → ∀ 𝑗 ∈ 𝑍 - 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) )
59 58 imp ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑗 ∈ 𝑍 - ( 𝐹 ‘ 𝑗 ) ≤ 𝑦 ) → ∀ 𝑗 ∈ 𝑍 - 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) )
60 breq1 ⊢ ( 𝑥 = - 𝑦 → ( 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ↔ - 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) )
61 60 ralbidv ⊢ ( 𝑥 = - 𝑦 → ( ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ↔ ∀ 𝑗 ∈ 𝑍 - 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) )
62 61 rspcev ⊢ ( ( - 𝑦 ∈ ℝ ∧ ∀ 𝑗 ∈ 𝑍 - 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
63 53 59 62 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∀ 𝑗 ∈ 𝑍 - ( 𝐹 ‘ 𝑗 ) ≤ 𝑦 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
64 63 rexlimdva2 ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑗 ∈ 𝑍 - ( 𝐹 ‘ 𝑗 ) ≤ 𝑦 → ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
65 37 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → - 𝑥 ∈ ℝ )
66 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) → 𝑥 ∈ ℝ )
67 15 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ )
68 66 67 lenegd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) → ( 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ↔ - ( 𝐹 ‘ 𝑗 ) ≤ - 𝑥 ) )
69 68 ralbidva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ↔ ∀ 𝑗 ∈ 𝑍 - ( 𝐹 ‘ 𝑗 ) ≤ - 𝑥 ) )
70 69 biimpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) → ∀ 𝑗 ∈ 𝑍 - ( 𝐹 ‘ 𝑗 ) ≤ - 𝑥 ) )
71 70 imp ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → ∀ 𝑗 ∈ 𝑍 - ( 𝐹 ‘ 𝑗 ) ≤ - 𝑥 )
72 brralrspcev ⊢ ( ( - 𝑥 ∈ ℝ ∧ ∀ 𝑗 ∈ 𝑍 - ( 𝐹 ‘ 𝑗 ) ≤ - 𝑥 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑗 ∈ 𝑍 - ( 𝐹 ‘ 𝑗 ) ≤ 𝑦 )
73 65 71 72 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑗 ∈ 𝑍 - ( 𝐹 ‘ 𝑗 ) ≤ 𝑦 )
74 73 rexlimdva2 ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑗 ∈ 𝑍 - ( 𝐹 ‘ 𝑗 ) ≤ 𝑦 ) )
75 64 74 impbid ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑗 ∈ 𝑍 - ( 𝐹 ‘ 𝑗 ) ≤ 𝑦 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
76 52 75 anbi12d ⊢ ( 𝜑 → ( ( ∃ 𝑦 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑦 ≤ - ( 𝐹 ‘ 𝑗 ) ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑗 ∈ 𝑍 - ( 𝐹 ‘ 𝑗 ) ≤ 𝑦 ) ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
77 17 76 bitrd ⊢ ( 𝜑 → ( ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ - ( 𝐹 ‘ 𝑗 ) ) ) ∈ ℝ ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
78 14 77 bitrd ⊢ ( 𝜑 → ( ( lim inf ‘ 𝐹 ) ∈ ℝ ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )