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 ⊢ Ⅎ _ j F
limsupre3.2 ⊢ φ → A ⊆ ℝ
limsupre3.3 ⊢ φ → F : A ⟶ ℝ *
Assertion limsupre3 ⊢ φ → lim sup ⁡ F ∈ ℝ ↔ ∃ x ∈ ℝ ∀ k ∈ ℝ ∃ j ∈ A k ≤ j ∧ x ≤ F ⁡ j ∧ ∃ x ∈ ℝ ∃ k ∈ ℝ ∀ j ∈ A k ≤ j → F ⁡ j ≤ x

Proof

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