Metamath Proof Explorer

Theorem limsupre3

Description: Given a function on the extended 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, at some point, in any upper part of the reals; 2. there is a real number that is eventually greater than or equal to the function. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses limsupre3.1 ⊢ Ⅎ 𝑗 𝐹
limsupre3.2 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
limsupre3.3 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* )
Assertion limsupre3 ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ∈ ℝ ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 limsupre3.1 ⊢ Ⅎ 𝑗 𝐹
2 limsupre3.2 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
3 limsupre3.3 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* )
4 nfcv ⊢ Ⅎ 𝑙 𝐹
5 4 2 3 limsupre3lem ⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ∈ ℝ ↔ ( ∃ 𝑦 ∈ ℝ ∀ 𝑖 ∈ ℝ ∃ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) ∧ ∃ 𝑦 ∈ ℝ ∃ 𝑖 ∈ ℝ ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ) ) )
6 breq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ↔ 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ) )
7 6 anbi2d ⊢ ( 𝑦 = 𝑥 → ( ( 𝑖 ≤ 𝑙 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) ↔ ( 𝑖 ≤ 𝑙 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ) ) )
8 7 rexbidv ⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) ↔ ∃ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ) ) )
9 8 ralbidv ⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑖 ∈ ℝ ∃ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) ↔ ∀ 𝑖 ∈ ℝ ∃ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ) ) )
10 breq1 ⊢ ( 𝑖 = 𝑘 → ( 𝑖 ≤ 𝑙 ↔ 𝑘 ≤ 𝑙 ) )
11 10 anbi1d ⊢ ( 𝑖 = 𝑘 → ( ( 𝑖 ≤ 𝑙 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ) ↔ ( 𝑘 ≤ 𝑙 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ) ) )
12 11 rexbidv ⊢ ( 𝑖 = 𝑘 → ( ∃ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ) ↔ ∃ 𝑙 ∈ 𝐴 ( 𝑘 ≤ 𝑙 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ) ) )
13 nfv ⊢ Ⅎ 𝑗 𝑘 ≤ 𝑙
14 nfcv ⊢ Ⅎ 𝑗 𝑥
15 nfcv ⊢ Ⅎ 𝑗 ≤
16 nfcv ⊢ Ⅎ 𝑗 𝑙
17 1 16 nffv ⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑙 )
18 14 15 17 nfbr ⊢ Ⅎ 𝑗 𝑥 ≤ ( 𝐹 ‘ 𝑙 )
19 13 18 nfan ⊢ Ⅎ 𝑗 ( 𝑘 ≤ 𝑙 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) )
20 nfv ⊢ Ⅎ 𝑙 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) )
21 breq2 ⊢ ( 𝑙 = 𝑗 → ( 𝑘 ≤ 𝑙 ↔ 𝑘 ≤ 𝑗 ) )
22 fveq2 ⊢ ( 𝑙 = 𝑗 → ( 𝐹 ‘ 𝑙 ) = ( 𝐹 ‘ 𝑗 ) )
23 22 breq2d ⊢ ( 𝑙 = 𝑗 → ( 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ↔ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
24 21 23 anbi12d ⊢ ( 𝑙 = 𝑗 → ( ( 𝑘 ≤ 𝑙 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ) ↔ ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
25 19 20 24 cbvrexw ⊢ ( ∃ 𝑙 ∈ 𝐴 ( 𝑘 ≤ 𝑙 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ) ↔ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
26 25 a1i ⊢ ( 𝑖 = 𝑘 → ( ∃ 𝑙 ∈ 𝐴 ( 𝑘 ≤ 𝑙 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ) ↔ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
27 12 26 bitrd ⊢ ( 𝑖 = 𝑘 → ( ∃ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ) ↔ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
28 27 cbvralvw ⊢ ( ∀ 𝑖 ∈ ℝ ∃ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ) ↔ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
29 28 a1i ⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑖 ∈ ℝ ∃ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ) ↔ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
30 9 29 bitrd ⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑖 ∈ ℝ ∃ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) ↔ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
31 30 cbvrexvw ⊢ ( ∃ 𝑦 ∈ ℝ ∀ 𝑖 ∈ ℝ ∃ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
32 breq2 ⊢ ( 𝑦 = 𝑥 → ( ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ↔ ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) )
33 32 imbi2d ⊢ ( 𝑦 = 𝑥 → ( ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ↔ ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) ) )
34 33 ralbidv ⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ↔ ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) ) )
35 34 rexbidv ⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ ℝ ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ↔ ∃ 𝑖 ∈ ℝ ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) ) )
36 10 imbi1d ⊢ ( 𝑖 = 𝑘 → ( ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) ↔ ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) ) )
37 36 ralbidv ⊢ ( 𝑖 = 𝑘 → ( ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) ↔ ∀ 𝑙 ∈ 𝐴 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) ) )
38 17 15 14 nfbr ⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥
39 13 38 nfim ⊢ Ⅎ 𝑗 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 )
40 nfv ⊢ Ⅎ 𝑙 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
41 22 breq1d ⊢ ( 𝑙 = 𝑗 → ( ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
42 21 41 imbi12d ⊢ ( 𝑙 = 𝑗 → ( ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) ↔ ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
43 39 40 42 cbvralw ⊢ ( ∀ 𝑙 ∈ 𝐴 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) ↔ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
44 43 a1i ⊢ ( 𝑖 = 𝑘 → ( ∀ 𝑙 ∈ 𝐴 ( 𝑘 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) ↔ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
45 37 44 bitrd ⊢ ( 𝑖 = 𝑘 → ( ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) ↔ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
46 45 cbvrexvw ⊢ ( ∃ 𝑖 ∈ ℝ ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) ↔ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
47 46 a1i ⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ ℝ ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) ↔ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
48 35 47 bitrd ⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ ℝ ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ↔ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
49 48 cbvrexvw ⊢ ( ∃ 𝑦 ∈ ℝ ∃ 𝑖 ∈ ℝ ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
50 31 49 anbi12i ⊢ ( ( ∃ 𝑦 ∈ ℝ ∀ 𝑖 ∈ ℝ ∃ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) ∧ ∃ 𝑦 ∈ ℝ ∃ 𝑖 ∈ ℝ ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ) ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) )
51 50 a1i ⊢ ( 𝜑 → ( ( ∃ 𝑦 ∈ ℝ ∀ 𝑖 ∈ ℝ ∃ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 ∧ 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) ∧ ∃ 𝑦 ∈ ℝ ∃ 𝑖 ∈ ℝ ∀ 𝑙 ∈ 𝐴 ( 𝑖 ≤ 𝑙 → ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ) ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) ) )
52 5 51 bitrd ⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ∈ ℝ ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℝ ∃ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 ∧ 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝐴 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) ) ) )