Metamath Proof Explorer

Theorem imo72b2lem0

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

Ref Expression
Hypotheses imo72b2lem0.1 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
imo72b2lem0.2 ⊢ ( 𝜑 → 𝐺 : ℝ ⟶ ℝ )
imo72b2lem0.3 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
imo72b2lem0.4 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
imo72b2lem0.5 ⊢ ( 𝜑 → ( ( 𝐹 ‘ ( 𝐴 + 𝐵 ) ) + ( 𝐹 ‘ ( 𝐴 − 𝐵 ) ) ) = ( 2 · ( ( 𝐹 ‘ 𝐴 ) · ( 𝐺 ‘ 𝐵 ) ) ) )
imo72b2lem0.6 ⊢ ( 𝜑 → ∀ 𝑦 ∈ ℝ ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 1 )
Assertion imo72b2lem0 ( 𝜑 → ( ( abs ‘ ( 𝐹 ‘ 𝐴 ) ) · ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) ≤ sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) )

Proof

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