| 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  “  ( 𝐹  “  ℝ ) ) ,  ℝ ,   <  ) ) |