This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem limsupreuz

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

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

Proof

Step Hyp Ref Expression
1 limsupreuz.1 ⊢ Ⅎ 𝑗 𝐹
2 limsupreuz.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 limsupreuz.3 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4 limsupreuz.4 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
5 nfcv ⊢ Ⅎ 𝑙 𝐹
6 4 frexr ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
7 5 2 3 6 limsupre3uzlem ⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ∈ ℝ ↔ ( ∃ 𝑦 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ∧ ∃ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ) )
8 breq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ↔ 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ) )
9 8 rexbidv ⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ) )
10 9 ralbidv ⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑖 ∈ 𝑍 ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∀ 𝑖 ∈ 𝑍 ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ) )
11 fveq2 ⊢ ( 𝑖 = 𝑘 → ( ℤ≥ ‘ 𝑖 ) = ( ℤ≥ ‘ 𝑘 ) )
12 11 rexeqdv ⊢ ( 𝑖 = 𝑘 → ( ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ) )
13 nfcv ⊢ Ⅎ 𝑗 𝑥
14 nfcv ⊢ Ⅎ 𝑗 ≤
15 nfcv ⊢ Ⅎ 𝑗 𝑙
16 1 15 nffv ⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑙 )
17 13 14 16 nfbr ⊢ Ⅎ 𝑗 𝑥 ≤ ( 𝐹 ‘ 𝑙 )
18 nfv ⊢ Ⅎ 𝑙 𝑥 ≤ ( 𝐹 ‘ 𝑗 )
19 fveq2 ⊢ ( 𝑙 = 𝑗 → ( 𝐹 ‘ 𝑙 ) = ( 𝐹 ‘ 𝑗 ) )
20 19 breq2d ⊢ ( 𝑙 = 𝑗 → ( 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ↔ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
21 17 18 20 cbvrexw ⊢ ( ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
22 21 a1i ⊢ ( 𝑖 = 𝑘 → ( ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
23 12 22 bitrd ⊢ ( 𝑖 = 𝑘 → ( ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
24 23 cbvralvw ⊢ ( ∀ 𝑖 ∈ 𝑍 ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
25 24 a1i ⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑖 ∈ 𝑍 ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
26 10 25 bitrd ⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑖 ∈ 𝑍 ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
27 26 cbvrexvw ⊢ ( ∃ 𝑦 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
28 breq2 ⊢ ( 𝑦 = 𝑥 → ( ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ↔ ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) )
29 28 ralbidv ⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ↔ ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) )
30 29 rexbidv ⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ↔ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) )
31 11 raleqdv ⊢ ( 𝑖 = 𝑘 → ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) )
32 16 14 13 nfbr ⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥
33 nfv ⊢ Ⅎ 𝑙 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥
34 19 breq1d ⊢ ( 𝑙 = 𝑗 → ( ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
35 32 33 34 cbvralw ⊢ ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
36 35 a1i ⊢ ( 𝑖 = 𝑘 → ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
37 31 36 bitrd ⊢ ( 𝑖 = 𝑘 → ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
38 37 cbvrexvw ⊢ ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
39 38 a1i ⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
40 30 39 bitrd ⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ↔ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
41 40 cbvrexvw ⊢ ( ∃ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
42 27 41 anbi12i ⊢ ( ( ∃ 𝑦 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ∧ ∃ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
43 42 a1i ⊢ ( 𝜑 → ( ( ∃ 𝑦 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ∃ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ∧ ∃ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
44 7 43 bitrd ⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ∈ ℝ ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
45 nfv ⊢ Ⅎ 𝑖 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥
46 nfcv ⊢ Ⅎ 𝑗 𝑖
47 1 46 nffv ⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑖 )
48 47 14 13 nfbr ⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑖 ) ≤ 𝑥
49 fveq2 ⊢ ( 𝑗 = 𝑖 → ( 𝐹 ‘ 𝑗 ) = ( 𝐹 ‘ 𝑖 ) )
50 49 breq1d ⊢ ( 𝑗 = 𝑖 → ( ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑖 ) ≤ 𝑥 ) )
51 45 48 50 cbvralw ⊢ ( ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑖 ) ≤ 𝑥 )
52 51 rexbii ⊢ ( ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ∃ 𝑘 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑖 ) ≤ 𝑥 )
53 52 rexbii ⊢ ( ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑖 ) ≤ 𝑥 )
54 53 a1i ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑖 ) ≤ 𝑥 ) )
55 nfv ⊢ Ⅎ 𝑖 𝜑
56 4 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → 𝐹 : 𝑍 ⟶ ℝ )
57 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → 𝑖 ∈ 𝑍 )
58 56 57 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑖 ) ∈ ℝ )
59 55 2 3 58 uzub ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑖 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑖 ) ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ( 𝐹 ‘ 𝑖 ) ≤ 𝑥 ) )
60 eqcom ⊢ ( 𝑗 = 𝑖 ↔ 𝑖 = 𝑗 )
61 60 imbi1i ⊢ ( ( 𝑗 = 𝑖 → ( ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑖 ) ≤ 𝑥 ) ) ↔ ( 𝑖 = 𝑗 → ( ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑖 ) ≤ 𝑥 ) ) )
62 bicom ⊢ ( ( ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑖 ) ≤ 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑖 ) ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
63 62 imbi2i ⊢ ( ( 𝑖 = 𝑗 → ( ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑖 ) ≤ 𝑥 ) ) ↔ ( 𝑖 = 𝑗 → ( ( 𝐹 ‘ 𝑖 ) ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
64 61 63 bitri ⊢ ( ( 𝑗 = 𝑖 → ( ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑖 ) ≤ 𝑥 ) ) ↔ ( 𝑖 = 𝑗 → ( ( 𝐹 ‘ 𝑖 ) ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
65 50 64 mpbi ⊢ ( 𝑖 = 𝑗 → ( ( 𝐹 ‘ 𝑖 ) ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
66 48 45 65 cbvralw ⊢ ( ∀ 𝑖 ∈ 𝑍 ( 𝐹 ‘ 𝑖 ) ≤ 𝑥 ↔ ∀ 𝑗 ∈ 𝑍 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
67 66 rexbii ⊢ ( ∃ 𝑥 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ( 𝐹 ‘ 𝑖 ) ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
68 67 a1i ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑖 ∈ 𝑍 ( 𝐹 ‘ 𝑖 ) ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
69 54 59 68 3bitrd ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
70 69 anbi2d ⊢ ( 𝜑 → ( ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
71 44 70 bitrd ⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ∈ ℝ ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ 𝑍 ∃ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )