Metamath Proof Explorer

Theorem imo72b2lem0

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

Ref Expression
Hypotheses imo72b2lem0.1 ⊢ φ → F : ℝ ⟶ ℝ
imo72b2lem0.2 ⊢ φ → G : ℝ ⟶ ℝ
imo72b2lem0.3 ⊢ φ → A ∈ ℝ
imo72b2lem0.4 ⊢ φ → B ∈ ℝ
imo72b2lem0.5 ⊢ φ → F ⁡ A + B + F ⁡ A − B = 2 ⁢ F ⁡ A ⁢ G ⁡ B
imo72b2lem0.6 ⊢ φ → ∀ y ∈ ℝ F ⁡ y ≤ 1
Assertion imo72b2lem0 ⊢ φ → F ⁡ A ⁢ G ⁡ B ≤ sup abs F ℝ ℝ <

Proof

Step Hyp Ref Expression
1 imo72b2lem0.1 ⊢ φ → F : ℝ ⟶ ℝ
2 imo72b2lem0.2 ⊢ φ → G : ℝ ⟶ ℝ
3 imo72b2lem0.3 ⊢ φ → A ∈ ℝ
4 imo72b2lem0.4 ⊢ φ → B ∈ ℝ
5 imo72b2lem0.5 ⊢ φ → F ⁡ A + B + F ⁡ A − B = 2 ⁢ F ⁡ A ⁢ G ⁡ B
6 imo72b2lem0.6 ⊢ φ → ∀ y ∈ ℝ F ⁡ y ≤ 1
7 1 3 ffvelcdmd ⊢ φ → F ⁡ A ∈ ℝ
8 7 recnd ⊢ φ → F ⁡ A ∈ ℂ
9 2 4 ffvelcdmd ⊢ φ → G ⁡ B ∈ ℝ
10 9 recnd ⊢ φ → G ⁡ B ∈ ℂ
11 8 10 absmuld ⊢ φ → F ⁡ A ⁢ G ⁡ B = F ⁡ A ⁢ G ⁡ B
12 8 10 mulcld ⊢ φ → F ⁡ A ⁢ G ⁡ B ∈ ℂ
13 12 abscld ⊢ φ → F ⁡ A ⁢ G ⁡ B ∈ ℝ
14 absf ⊢ abs : ℂ ⟶ ℝ
15 14 a1i ⊢ φ → abs : ℂ ⟶ ℝ
16 15 fimassd ⊢ φ → abs F ℝ ⊆ ℝ
17 imaco ⊢ abs ∘ F ℝ = abs F ℝ
18 3 ne0d ⊢ φ → ℝ ≠ ∅
19 ax-resscn ⊢ ℝ ⊆ ℂ
20 19 a1i ⊢ φ → ℝ ⊆ ℂ
21 15 20 fssresd ⊢ φ → abs ↾ ℝ : ℝ ⟶ ℝ
22 1 21 fco2d ⊢ φ → abs ∘ F : ℝ ⟶ ℝ
23 18 22 wnefimgd ⊢ φ → abs ∘ F ℝ ≠ ∅
24 17 23 eqnetrrid ⊢ φ → abs F ℝ ≠ ∅
25 1red ⊢ φ → 1 ∈ ℝ
26 simpr ⊢ φ ∧ c = 1 → c = 1
27 26 breq2d ⊢ φ ∧ c = 1 → x ≤ c ↔ x ≤ 1
28 27 ralbidv ⊢ φ ∧ c = 1 → ∀ x ∈ abs F ℝ x ≤ c ↔ ∀ x ∈ abs F ℝ x ≤ 1
29 1 6 extoimad ⊢ φ → ∀ x ∈ abs F ℝ x ≤ 1
30 25 28 29 rspcedvd ⊢ φ → ∃ c ∈ ℝ ∀ x ∈ abs F ℝ x ≤ c
31 16 24 30 suprcld ⊢ φ → sup abs F ℝ ℝ < ∈ ℝ
32 2re ⊢ 2 ∈ ℝ
33 32 a1i ⊢ φ → 2 ∈ ℝ
34 0le2 ⊢ 0 ≤ 2
35 34 a1i ⊢ φ → 0 ≤ 2
36 7 9 remulcld ⊢ φ → F ⁡ A ⁢ G ⁡ B ∈ ℝ
37 35 33 36 absmulrposd ⊢ φ → 2 ⁢ F ⁡ A ⁢ G ⁡ B = 2 ⁢ F ⁡ A ⁢ G ⁡ B
38 5 fveq2d ⊢ φ → F ⁡ A + B + F ⁡ A − B = 2 ⁢ F ⁡ A ⁢ G ⁡ B
39 2cnd ⊢ φ → 2 ∈ ℂ
40 39 12 mulcld ⊢ φ → 2 ⁢ F ⁡ A ⁢ G ⁡ B ∈ ℂ
41 40 abscld ⊢ φ → 2 ⁢ F ⁡ A ⁢ G ⁡ B ∈ ℝ
42 38 41 eqeltrd ⊢ φ → F ⁡ A + B + F ⁡ A − B ∈ ℝ
43 3 4 readdcld ⊢ φ → A + B ∈ ℝ
44 1 43 ffvelcdmd ⊢ φ → F ⁡ A + B ∈ ℝ
45 44 recnd ⊢ φ → F ⁡ A + B ∈ ℂ
46 45 abscld ⊢ φ → F ⁡ A + B ∈ ℝ
47 3 4 resubcld ⊢ φ → A − B ∈ ℝ
48 1 47 ffvelcdmd ⊢ φ → F ⁡ A − B ∈ ℝ
49 48 recnd ⊢ φ → F ⁡ A − B ∈ ℂ
50 49 abscld ⊢ φ → F ⁡ A − B ∈ ℝ
51 46 50 readdcld ⊢ φ → F ⁡ A + B + F ⁡ A − B ∈ ℝ
52 33 31 remulcld ⊢ φ → 2 ⁢ sup abs F ℝ ℝ < ∈ ℝ
53 45 49 abstrid ⊢ φ → F ⁡ A + B + F ⁡ A − B ≤ F ⁡ A + B + F ⁡ A − B
54 1 43 fvco3d ⊢ φ → abs ∘ F ⁡ A + B = F ⁡ A + B
55 43 22 wfximgfd ⊢ φ → abs ∘ F ⁡ A + B ∈ abs ∘ F ℝ
56 55 17 eleqtrdi ⊢ φ → abs ∘ F ⁡ A + B ∈ abs F ℝ
57 54 56 eqeltrrd ⊢ φ → F ⁡ A + B ∈ abs F ℝ
58 16 24 30 57 suprubd ⊢ φ → F ⁡ A + B ≤ sup abs F ℝ ℝ <
59 1 47 fvco3d ⊢ φ → abs ∘ F ⁡ A − B = F ⁡ A − B
60 47 22 wfximgfd ⊢ φ → abs ∘ F ⁡ A − B ∈ abs ∘ F ℝ
61 60 17 eleqtrdi ⊢ φ → abs ∘ F ⁡ A − B ∈ abs F ℝ
62 59 61 eqeltrrd ⊢ φ → F ⁡ A − B ∈ abs F ℝ
63 16 24 30 62 suprubd ⊢ φ → F ⁡ A − B ≤ sup abs F ℝ ℝ <
64 46 50 31 31 58 63 le2addd ⊢ φ → F ⁡ A + B + F ⁡ A − B ≤ sup abs F ℝ ℝ < + sup abs F ℝ ℝ <
65 31 recnd ⊢ φ → sup abs F ℝ ℝ < ∈ ℂ
66 65 2timesd ⊢ φ → 2 ⁢ sup abs F ℝ ℝ < = sup abs F ℝ ℝ < + sup abs F ℝ ℝ <
67 64 66 breqtrrd ⊢ φ → F ⁡ A + B + F ⁡ A − B ≤ 2 ⁢ sup abs F ℝ ℝ <
68 42 51 52 53 67 letrd ⊢ φ → F ⁡ A + B + F ⁡ A − B ≤ 2 ⁢ sup abs F ℝ ℝ <
69 38 68 eqbrtrrd ⊢ φ → 2 ⁢ F ⁡ A ⁢ G ⁡ B ≤ 2 ⁢ sup abs F ℝ ℝ <
70 37 69 eqbrtrrd ⊢ φ → 2 ⁢ F ⁡ A ⁢ G ⁡ B ≤ 2 ⁢ sup abs F ℝ ℝ <
71 2pos ⊢ 0 < 2
72 71 a1i ⊢ φ → 0 < 2
73 13 31 33 70 72 wwlemuld ⊢ φ → F ⁡ A ⁢ G ⁡ B ≤ sup abs F ℝ ℝ <
74 11 73 eqbrtrrd ⊢ φ → F ⁡ A ⁢ G ⁡ B ≤ sup abs F ℝ ℝ <