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 ffvelrnd ( ( 𝜑𝑖𝑍 ) → ( 𝐹𝑖 ) ∈ ℝ )
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 ‘ 𝐹 ) ∈ ℝ ↔ ( ∃ 𝑥 ∈ ℝ ∀ 𝑘𝑍𝑗 ∈ ( ℤ𝑘 ) 𝑥 ≤ ( 𝐹𝑗 ) ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑗𝑍 ( 𝐹𝑗 ) ≤ 𝑥 ) ) )