Metamath Proof Explorer

Theorem imo72b2lem2

Description: Lemma for imo72b2 . (Contributed by Stanislas Polu, 9-Mar-2020)

Ref Expression
Hypotheses imo72b2lem2.1 ⊢ φ → F : ℝ ⟶ ℝ
imo72b2lem2.2 ⊢ φ → C ∈ ℝ
imo72b2lem2.3 ⊢ φ → ∀ z ∈ ℝ F ⁡ z ≤ C
Assertion imo72b2lem2 ⊢ φ → sup abs F ℝ ℝ < ≤ C

Proof

Step Hyp Ref Expression
1 imo72b2lem2.1 ⊢ φ → F : ℝ ⟶ ℝ
2 imo72b2lem2.2 ⊢ φ → C ∈ ℝ
3 imo72b2lem2.3 ⊢ φ → ∀ z ∈ ℝ F ⁡ z ≤ C
4 imaco ⊢ abs ∘ F ℝ = abs F ℝ
5 4 eqcomi ⊢ abs F ℝ = abs ∘ F ℝ
6 imassrn ⊢ abs ∘ F ℝ ⊆ ran ⁡ abs ∘ F
7 6 a1i ⊢ φ → abs ∘ F ℝ ⊆ ran ⁡ abs ∘ F
8 absf ⊢ abs : ℂ ⟶ ℝ
9 8 a1i ⊢ φ → abs : ℂ ⟶ ℝ
10 ax-resscn ⊢ ℝ ⊆ ℂ
11 10 a1i ⊢ φ → ℝ ⊆ ℂ
12 9 11 fssresd ⊢ φ → abs ↾ ℝ : ℝ ⟶ ℝ
13 1 12 fco2d ⊢ φ → abs ∘ F : ℝ ⟶ ℝ
14 13 frnd ⊢ φ → ran ⁡ abs ∘ F ⊆ ℝ
15 7 14 sstrd ⊢ φ → abs ∘ F ℝ ⊆ ℝ
16 5 15 eqsstrid ⊢ φ → abs F ℝ ⊆ ℝ
17 0re ⊢ 0 ∈ ℝ
18 17 ne0ii ⊢ ℝ ≠ ∅
19 18 a1i ⊢ φ → ℝ ≠ ∅
20 19 13 wnefimgd ⊢ φ → abs ∘ F ℝ ≠ ∅
21 20 necomd ⊢ φ → ∅ ≠ abs ∘ F ℝ
22 5 a1i ⊢ φ → abs F ℝ = abs ∘ F ℝ
23 21 22 neeqtrrd ⊢ φ → ∅ ≠ abs F ℝ
24 23 necomd ⊢ φ → abs F ℝ ≠ ∅
25 simpr ⊢ φ ∧ c = C → c = C
26 25 breq2d ⊢ φ ∧ c = C → v ≤ c ↔ v ≤ C
27 26 ralbidv ⊢ φ ∧ c = C → ∀ v ∈ abs F ℝ v ≤ c ↔ ∀ v ∈ abs F ℝ v ≤ C
28 1 3 extoimad ⊢ φ → ∀ v ∈ abs F ℝ v ≤ C
29 2 27 28 rspcedvd ⊢ φ → ∃ c ∈ ℝ ∀ v ∈ abs F ℝ v ≤ c
30 1 3 extoimad ⊢ φ → ∀ t ∈ abs F ℝ t ≤ C
31 16 24 29 2 30 suprleubrd ⊢ φ → sup abs F ℝ ℝ < ≤ C