Metamath Proof Explorer


Theorem limsupre3uz

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, infinitely often; 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 limsupre3uz.1 𝑗 𝐹
limsupre3uz.2 ( 𝜑𝑀 ∈ ℤ )
limsupre3uz.3 𝑍 = ( ℤ𝑀 )
limsupre3uz.4 ( 𝜑𝐹 : 𝑍 ⟶ ℝ* )
Assertion limsupre3uz ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ∈ ℝ ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) 𝑥 ≤ ( 𝐹𝑗 ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) ( 𝐹𝑗 ) ≤ 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 limsupre3uz.1 𝑗 𝐹
2 limsupre3uz.2 ( 𝜑𝑀 ∈ ℤ )
3 limsupre3uz.3 𝑍 = ( ℤ𝑀 )
4 limsupre3uz.4 ( 𝜑𝐹 : 𝑍 ⟶ ℝ* )
5 nfcv 𝑙 𝐹
6 5 2 3 4 limsupre3uzlem ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ∈ ℝ ↔ ( ∃ 𝑦 ∈ ℝ ∀ 𝑖𝑍𝑙 ∈ ( ℤ𝑖 ) 𝑦 ≤ ( 𝐹𝑙 ) ∧ ∃ 𝑦 ∈ ℝ ∃ 𝑖𝑍𝑙 ∈ ( ℤ𝑖 ) ( 𝐹𝑙 ) ≤ 𝑦 ) ) )
7 breq1 ( 𝑦 = 𝑥 → ( 𝑦 ≤ ( 𝐹𝑙 ) ↔ 𝑥 ≤ ( 𝐹𝑙 ) ) )
8 7 rexbidv ( 𝑦 = 𝑥 → ( ∃ 𝑙 ∈ ( ℤ𝑖 ) 𝑦 ≤ ( 𝐹𝑙 ) ↔ ∃ 𝑙 ∈ ( ℤ𝑖 ) 𝑥 ≤ ( 𝐹𝑙 ) ) )
9 8 ralbidv ( 𝑦 = 𝑥 → ( ∀ 𝑖𝑍𝑙 ∈ ( ℤ𝑖 ) 𝑦 ≤ ( 𝐹𝑙 ) ↔ ∀ 𝑖𝑍𝑙 ∈ ( ℤ𝑖 ) 𝑥 ≤ ( 𝐹𝑙 ) ) )
10 fveq2 ( 𝑖 = 𝑘 → ( ℤ𝑖 ) = ( ℤ𝑘 ) )
11 10 rexeqdv ( 𝑖 = 𝑘 → ( ∃ 𝑙 ∈ ( ℤ𝑖 ) 𝑥 ≤ ( 𝐹𝑙 ) ↔ ∃ 𝑙 ∈ ( ℤ𝑘 ) 𝑥 ≤ ( 𝐹𝑙 ) ) )
12 nfcv 𝑗 𝑥
13 nfcv 𝑗
14 nfcv 𝑗 𝑙
15 1 14 nffv 𝑗 ( 𝐹𝑙 )
16 12 13 15 nfbr 𝑗 𝑥 ≤ ( 𝐹𝑙 )
17 nfv 𝑙 𝑥 ≤ ( 𝐹𝑗 )
18 fveq2 ( 𝑙 = 𝑗 → ( 𝐹𝑙 ) = ( 𝐹𝑗 ) )
19 18 breq2d ( 𝑙 = 𝑗 → ( 𝑥 ≤ ( 𝐹𝑙 ) ↔ 𝑥 ≤ ( 𝐹𝑗 ) ) )
20 16 17 19 cbvrexw ( ∃ 𝑙 ∈ ( ℤ𝑘 ) 𝑥 ≤ ( 𝐹𝑙 ) ↔ ∃ 𝑗 ∈ ( ℤ𝑘 ) 𝑥 ≤ ( 𝐹𝑗 ) )
21 20 a1i ( 𝑖 = 𝑘 → ( ∃ 𝑙 ∈ ( ℤ𝑘 ) 𝑥 ≤ ( 𝐹𝑙 ) ↔ ∃ 𝑗 ∈ ( ℤ𝑘 ) 𝑥 ≤ ( 𝐹𝑗 ) ) )
22 11 21 bitrd ( 𝑖 = 𝑘 → ( ∃ 𝑙 ∈ ( ℤ𝑖 ) 𝑥 ≤ ( 𝐹𝑙 ) ↔ ∃ 𝑗 ∈ ( ℤ𝑘 ) 𝑥 ≤ ( 𝐹𝑗 ) ) )
23 22 cbvralvw ( ∀ 𝑖𝑍𝑙 ∈ ( ℤ𝑖 ) 𝑥 ≤ ( 𝐹𝑙 ) ↔ ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) 𝑥 ≤ ( 𝐹𝑗 ) )
24 23 a1i ( 𝑦 = 𝑥 → ( ∀ 𝑖𝑍𝑙 ∈ ( ℤ𝑖 ) 𝑥 ≤ ( 𝐹𝑙 ) ↔ ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) 𝑥 ≤ ( 𝐹𝑗 ) ) )
25 9 24 bitrd ( 𝑦 = 𝑥 → ( ∀ 𝑖𝑍𝑙 ∈ ( ℤ𝑖 ) 𝑦 ≤ ( 𝐹𝑙 ) ↔ ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) 𝑥 ≤ ( 𝐹𝑗 ) ) )
26 25 cbvrexvw ( ∃ 𝑦 ∈ ℝ ∀ 𝑖𝑍𝑙 ∈ ( ℤ𝑖 ) 𝑦 ≤ ( 𝐹𝑙 ) ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) 𝑥 ≤ ( 𝐹𝑗 ) )
27 breq2 ( 𝑦 = 𝑥 → ( ( 𝐹𝑙 ) ≤ 𝑦 ↔ ( 𝐹𝑙 ) ≤ 𝑥 ) )
28 27 ralbidv ( 𝑦 = 𝑥 → ( ∀ 𝑙 ∈ ( ℤ𝑖 ) ( 𝐹𝑙 ) ≤ 𝑦 ↔ ∀ 𝑙 ∈ ( ℤ𝑖 ) ( 𝐹𝑙 ) ≤ 𝑥 ) )
29 28 rexbidv ( 𝑦 = 𝑥 → ( ∃ 𝑖𝑍𝑙 ∈ ( ℤ𝑖 ) ( 𝐹𝑙 ) ≤ 𝑦 ↔ ∃ 𝑖𝑍𝑙 ∈ ( ℤ𝑖 ) ( 𝐹𝑙 ) ≤ 𝑥 ) )
30 10 raleqdv ( 𝑖 = 𝑘 → ( ∀ 𝑙 ∈ ( ℤ𝑖 ) ( 𝐹𝑙 ) ≤ 𝑥 ↔ ∀ 𝑙 ∈ ( ℤ𝑘 ) ( 𝐹𝑙 ) ≤ 𝑥 ) )
31 15 13 12 nfbr 𝑗 ( 𝐹𝑙 ) ≤ 𝑥
32 nfv 𝑙 ( 𝐹𝑗 ) ≤ 𝑥
33 18 breq1d ( 𝑙 = 𝑗 → ( ( 𝐹𝑙 ) ≤ 𝑥 ↔ ( 𝐹𝑗 ) ≤ 𝑥 ) )
34 31 32 33 cbvralw ( ∀ 𝑙 ∈ ( ℤ𝑘 ) ( 𝐹𝑙 ) ≤ 𝑥 ↔ ∀ 𝑗 ∈ ( ℤ𝑘 ) ( 𝐹𝑗 ) ≤ 𝑥 )
35 34 a1i ( 𝑖 = 𝑘 → ( ∀ 𝑙 ∈ ( ℤ𝑘 ) ( 𝐹𝑙 ) ≤ 𝑥 ↔ ∀ 𝑗 ∈ ( ℤ𝑘 ) ( 𝐹𝑗 ) ≤ 𝑥 ) )
36 30 35 bitrd ( 𝑖 = 𝑘 → ( ∀ 𝑙 ∈ ( ℤ𝑖 ) ( 𝐹𝑙 ) ≤ 𝑥 ↔ ∀ 𝑗 ∈ ( ℤ𝑘 ) ( 𝐹𝑗 ) ≤ 𝑥 ) )
37 36 cbvrexvw ( ∃ 𝑖𝑍𝑙 ∈ ( ℤ𝑖 ) ( 𝐹𝑙 ) ≤ 𝑥 ↔ ∃ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) ( 𝐹𝑗 ) ≤ 𝑥 )
38 37 a1i ( 𝑦 = 𝑥 → ( ∃ 𝑖𝑍𝑙 ∈ ( ℤ𝑖 ) ( 𝐹𝑙 ) ≤ 𝑥 ↔ ∃ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) ( 𝐹𝑗 ) ≤ 𝑥 ) )
39 29 38 bitrd ( 𝑦 = 𝑥 → ( ∃ 𝑖𝑍𝑙 ∈ ( ℤ𝑖 ) ( 𝐹𝑙 ) ≤ 𝑦 ↔ ∃ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) ( 𝐹𝑗 ) ≤ 𝑥 ) )
40 39 cbvrexvw ( ∃ 𝑦 ∈ ℝ ∃ 𝑖𝑍𝑙 ∈ ( ℤ𝑖 ) ( 𝐹𝑙 ) ≤ 𝑦 ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) ( 𝐹𝑗 ) ≤ 𝑥 )
41 26 40 anbi12i ( ( ∃ 𝑦 ∈ ℝ ∀ 𝑖𝑍𝑙 ∈ ( ℤ𝑖 ) 𝑦 ≤ ( 𝐹𝑙 ) ∧ ∃ 𝑦 ∈ ℝ ∃ 𝑖𝑍𝑙 ∈ ( ℤ𝑖 ) ( 𝐹𝑙 ) ≤ 𝑦 ) ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) 𝑥 ≤ ( 𝐹𝑗 ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) ( 𝐹𝑗 ) ≤ 𝑥 ) )
42 41 a1i ( 𝜑 → ( ( ∃ 𝑦 ∈ ℝ ∀ 𝑖𝑍𝑙 ∈ ( ℤ𝑖 ) 𝑦 ≤ ( 𝐹𝑙 ) ∧ ∃ 𝑦 ∈ ℝ ∃ 𝑖𝑍𝑙 ∈ ( ℤ𝑖 ) ( 𝐹𝑙 ) ≤ 𝑦 ) ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) 𝑥 ≤ ( 𝐹𝑗 ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) ( 𝐹𝑗 ) ≤ 𝑥 ) ) )
43 6 42 bitrd ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ∈ ℝ ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) 𝑥 ≤ ( 𝐹𝑗 ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) ( 𝐹𝑗 ) ≤ 𝑥 ) ) )