Metamath Proof Explorer

Theorem imo72b2

Description: IMO 1972 B2. (14th International Mathematical Olympiad in Poland, problem B2). (Contributed by Stanislas Polu, 9-Mar-2020)

Ref Expression
Hypotheses imo72b2.1 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
imo72b2.2 ⊢ ( 𝜑 → 𝐺 : ℝ ⟶ ℝ )
imo72b2.4 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
imo72b2.5 ⊢ ( 𝜑 → ∀ 𝑢 ∈ ℝ ∀ 𝑣 ∈ ℝ ( ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) + ( 𝐹 ‘ ( 𝑢 − 𝑣 ) ) ) = ( 2 · ( ( 𝐹 ‘ 𝑢 ) · ( 𝐺 ‘ 𝑣 ) ) ) )
imo72b2.6 ⊢ ( 𝜑 → ∀ 𝑦 ∈ ℝ ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 1 )
imo72b2.7 ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ( 𝐹 ‘ 𝑥 ) ≠ 0 )
Assertion imo72b2 ( 𝜑 → ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ≤ 1 )

Proof

Step Hyp Ref Expression
1 imo72b2.1 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
2 imo72b2.2 ⊢ ( 𝜑 → 𝐺 : ℝ ⟶ ℝ )
3 imo72b2.4 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
4 imo72b2.5 ⊢ ( 𝜑 → ∀ 𝑢 ∈ ℝ ∀ 𝑣 ∈ ℝ ( ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) + ( 𝐹 ‘ ( 𝑢 − 𝑣 ) ) ) = ( 2 · ( ( 𝐹 ‘ 𝑢 ) · ( 𝐺 ‘ 𝑣 ) ) ) )
5 imo72b2.6 ⊢ ( 𝜑 → ∀ 𝑦 ∈ ℝ ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 1 )
6 imo72b2.7 ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ( 𝐹 ‘ 𝑥 ) ≠ 0 )
7 2 3 ffvelcdmd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐵 ) ∈ ℝ )
8 7 recnd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐵 ) ∈ ℂ )
9 8 abscld ⊢ ( 𝜑 → ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ∈ ℝ )
10 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
11 simpr ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) )
12 2 adantr ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → 𝐺 : ℝ ⟶ ℝ )
13 3 adantr ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → 𝐵 ∈ ℝ )
14 12 13 ffvelcdmd ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → ( 𝐺 ‘ 𝐵 ) ∈ ℝ )
15 14 recnd ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → ( 𝐺 ‘ 𝐵 ) ∈ ℂ )
16 15 abscld ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ∈ ℝ )
17 10 adantr ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → 1 ∈ ℝ )
18 ax-resscn ⊢ ℝ ⊆ ℂ
19 imaco ⊢ ( ( abs ∘ 𝐹 ) “ ℝ ) = ( abs “ ( 𝐹 “ ℝ ) )
20 19 eqcomi ⊢ ( abs “ ( 𝐹 “ ℝ ) ) = ( ( abs ∘ 𝐹 ) “ ℝ )
21 imassrn ⊢ ( ( abs ∘ 𝐹 ) “ ℝ ) ⊆ ran ( abs ∘ 𝐹 )
22 21 a1i ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → ( ( abs ∘ 𝐹 ) “ ℝ ) ⊆ ran ( abs ∘ 𝐹 ) )
23 1 adantr ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → 𝐹 : ℝ ⟶ ℝ )
24 absf ⊢ abs : ℂ ⟶ ℝ
25 24 a1i ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → abs : ℂ ⟶ ℝ )
26 18 a1i ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → ℝ ⊆ ℂ )
27 25 26 fssresd ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → ( abs ↾ ℝ ) : ℝ ⟶ ℝ )
28 23 27 fco2d ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → ( abs ∘ 𝐹 ) : ℝ ⟶ ℝ )
29 28 frnd ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → ran ( abs ∘ 𝐹 ) ⊆ ℝ )
30 22 29 sstrd ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → ( ( abs ∘ 𝐹 ) “ ℝ ) ⊆ ℝ )
31 20 30 eqsstrid ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → ( abs “ ( 𝐹 “ ℝ ) ) ⊆ ℝ )
32 0re ⊢ 0 ∈ ℝ
33 32 ne0ii ⊢ ℝ ≠ ∅
34 33 a1i ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → ℝ ≠ ∅ )
35 34 28 wnefimgd ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → ( ( abs ∘ 𝐹 ) “ ℝ ) ≠ ∅ )
36 35 necomd ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → ∅ ≠ ( ( abs ∘ 𝐹 ) “ ℝ ) )
37 20 a1i ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → ( abs “ ( 𝐹 “ ℝ ) ) = ( ( abs ∘ 𝐹 ) “ ℝ ) )
38 36 37 neeqtrrd ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → ∅ ≠ ( abs “ ( 𝐹 “ ℝ ) ) )
39 38 necomd ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → ( abs “ ( 𝐹 “ ℝ ) ) ≠ ∅ )
40 simpr ⊢ ( ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) ∧ 𝑐 = 1 ) → 𝑐 = 1 )
41 40 breq2d ⊢ ( ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) ∧ 𝑐 = 1 ) → ( 𝑡 ≤ 𝑐 ↔ 𝑡 ≤ 1 ) )
42 41 ralbidv ⊢ ( ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) ∧ 𝑐 = 1 ) → ( ∀ 𝑡 ∈ ( abs “ ( 𝐹 “ ℝ ) ) 𝑡 ≤ 𝑐 ↔ ∀ 𝑡 ∈ ( abs “ ( 𝐹 “ ℝ ) ) 𝑡 ≤ 1 ) )
43 1 5 extoimad ⊢ ( 𝜑 → ∀ 𝑡 ∈ ( abs “ ( 𝐹 “ ℝ ) ) 𝑡 ≤ 1 )
44 43 adantr ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → ∀ 𝑡 ∈ ( abs “ ( 𝐹 “ ℝ ) ) 𝑡 ≤ 1 )
45 17 42 44 rspcedvd ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ ( abs “ ( 𝐹 “ ℝ ) ) 𝑡 ≤ 𝑐 )
46 31 39 45 suprcld ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) ∈ ℝ )
47 18 46 sselid ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) ∈ ℂ )
48 18 16 sselid ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ∈ ℂ )
49 47 48 mulcomd ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → ( sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) · ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) = ( ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) · sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) ) )
50 32 a1i ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → 0 ∈ ℝ )
51 0lt1 ⊢ 0 < 1
52 51 a1i ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → 0 < 1 )
53 50 17 16 52 11 lttrd ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → 0 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) )
54 53 gt0ne0d ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ≠ 0 )
55 46 16 54 redivcld ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → ( sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) / ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) ∈ ℝ )
56 23 adantr ⊢ ( ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) ∧ 𝑢 ∈ ℝ ) → 𝐹 : ℝ ⟶ ℝ )
57 12 adantr ⊢ ( ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) ∧ 𝑢 ∈ ℝ ) → 𝐺 : ℝ ⟶ ℝ )
58 simpr ⊢ ( ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) ∧ 𝑢 ∈ ℝ ) → 𝑢 ∈ ℝ )
59 13 adantr ⊢ ( ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) ∧ 𝑢 ∈ ℝ ) → 𝐵 ∈ ℝ )
60 simpr ⊢ ( ( 𝜑 ∧ 𝑣 = 𝐵 ) → 𝑣 = 𝐵 )
61 60 oveq2d ⊢ ( ( 𝜑 ∧ 𝑣 = 𝐵 ) → ( 𝑢 + 𝑣 ) = ( 𝑢 + 𝐵 ) )
62 61 fveq2d ⊢ ( ( 𝜑 ∧ 𝑣 = 𝐵 ) → ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) = ( 𝐹 ‘ ( 𝑢 + 𝐵 ) ) )
63 60 oveq2d ⊢ ( ( 𝜑 ∧ 𝑣 = 𝐵 ) → ( 𝑢 − 𝑣 ) = ( 𝑢 − 𝐵 ) )
64 63 fveq2d ⊢ ( ( 𝜑 ∧ 𝑣 = 𝐵 ) → ( 𝐹 ‘ ( 𝑢 − 𝑣 ) ) = ( 𝐹 ‘ ( 𝑢 − 𝐵 ) ) )
65 62 64 oveq12d ⊢ ( ( 𝜑 ∧ 𝑣 = 𝐵 ) → ( ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) + ( 𝐹 ‘ ( 𝑢 − 𝑣 ) ) ) = ( ( 𝐹 ‘ ( 𝑢 + 𝐵 ) ) + ( 𝐹 ‘ ( 𝑢 − 𝐵 ) ) ) )
66 60 fveq2d ⊢ ( ( 𝜑 ∧ 𝑣 = 𝐵 ) → ( 𝐺 ‘ 𝑣 ) = ( 𝐺 ‘ 𝐵 ) )
67 66 oveq2d ⊢ ( ( 𝜑 ∧ 𝑣 = 𝐵 ) → ( ( 𝐹 ‘ 𝑢 ) · ( 𝐺 ‘ 𝑣 ) ) = ( ( 𝐹 ‘ 𝑢 ) · ( 𝐺 ‘ 𝐵 ) ) )
68 67 oveq2d ⊢ ( ( 𝜑 ∧ 𝑣 = 𝐵 ) → ( 2 · ( ( 𝐹 ‘ 𝑢 ) · ( 𝐺 ‘ 𝑣 ) ) ) = ( 2 · ( ( 𝐹 ‘ 𝑢 ) · ( 𝐺 ‘ 𝐵 ) ) ) )
69 65 68 eqeq12d ⊢ ( ( 𝜑 ∧ 𝑣 = 𝐵 ) → ( ( ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) + ( 𝐹 ‘ ( 𝑢 − 𝑣 ) ) ) = ( 2 · ( ( 𝐹 ‘ 𝑢 ) · ( 𝐺 ‘ 𝑣 ) ) ) ↔ ( ( 𝐹 ‘ ( 𝑢 + 𝐵 ) ) + ( 𝐹 ‘ ( 𝑢 − 𝐵 ) ) ) = ( 2 · ( ( 𝐹 ‘ 𝑢 ) · ( 𝐺 ‘ 𝐵 ) ) ) ) )
70 69 ralbidv ⊢ ( ( 𝜑 ∧ 𝑣 = 𝐵 ) → ( ∀ 𝑢 ∈ ℝ ( ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) + ( 𝐹 ‘ ( 𝑢 − 𝑣 ) ) ) = ( 2 · ( ( 𝐹 ‘ 𝑢 ) · ( 𝐺 ‘ 𝑣 ) ) ) ↔ ∀ 𝑢 ∈ ℝ ( ( 𝐹 ‘ ( 𝑢 + 𝐵 ) ) + ( 𝐹 ‘ ( 𝑢 − 𝐵 ) ) ) = ( 2 · ( ( 𝐹 ‘ 𝑢 ) · ( 𝐺 ‘ 𝐵 ) ) ) ) )
71 ralcom ⊢ ( ∀ 𝑢 ∈ ℝ ∀ 𝑣 ∈ ℝ ( ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) + ( 𝐹 ‘ ( 𝑢 − 𝑣 ) ) ) = ( 2 · ( ( 𝐹 ‘ 𝑢 ) · ( 𝐺 ‘ 𝑣 ) ) ) ↔ ∀ 𝑣 ∈ ℝ ∀ 𝑢 ∈ ℝ ( ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) + ( 𝐹 ‘ ( 𝑢 − 𝑣 ) ) ) = ( 2 · ( ( 𝐹 ‘ 𝑢 ) · ( 𝐺 ‘ 𝑣 ) ) ) )
72 71 biimpi ⊢ ( ∀ 𝑢 ∈ ℝ ∀ 𝑣 ∈ ℝ ( ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) + ( 𝐹 ‘ ( 𝑢 − 𝑣 ) ) ) = ( 2 · ( ( 𝐹 ‘ 𝑢 ) · ( 𝐺 ‘ 𝑣 ) ) ) → ∀ 𝑣 ∈ ℝ ∀ 𝑢 ∈ ℝ ( ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) + ( 𝐹 ‘ ( 𝑢 − 𝑣 ) ) ) = ( 2 · ( ( 𝐹 ‘ 𝑢 ) · ( 𝐺 ‘ 𝑣 ) ) ) )
73 72 a1i ⊢ ( 𝜑 → ( ∀ 𝑢 ∈ ℝ ∀ 𝑣 ∈ ℝ ( ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) + ( 𝐹 ‘ ( 𝑢 − 𝑣 ) ) ) = ( 2 · ( ( 𝐹 ‘ 𝑢 ) · ( 𝐺 ‘ 𝑣 ) ) ) → ∀ 𝑣 ∈ ℝ ∀ 𝑢 ∈ ℝ ( ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) + ( 𝐹 ‘ ( 𝑢 − 𝑣 ) ) ) = ( 2 · ( ( 𝐹 ‘ 𝑢 ) · ( 𝐺 ‘ 𝑣 ) ) ) ) )
74 73 imp ⊢ ( ( 𝜑 ∧ ∀ 𝑢 ∈ ℝ ∀ 𝑣 ∈ ℝ ( ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) + ( 𝐹 ‘ ( 𝑢 − 𝑣 ) ) ) = ( 2 · ( ( 𝐹 ‘ 𝑢 ) · ( 𝐺 ‘ 𝑣 ) ) ) ) → ∀ 𝑣 ∈ ℝ ∀ 𝑢 ∈ ℝ ( ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) + ( 𝐹 ‘ ( 𝑢 − 𝑣 ) ) ) = ( 2 · ( ( 𝐹 ‘ 𝑢 ) · ( 𝐺 ‘ 𝑣 ) ) ) )
75 4 74 mpdan ⊢ ( 𝜑 → ∀ 𝑣 ∈ ℝ ∀ 𝑢 ∈ ℝ ( ( 𝐹 ‘ ( 𝑢 + 𝑣 ) ) + ( 𝐹 ‘ ( 𝑢 − 𝑣 ) ) ) = ( 2 · ( ( 𝐹 ‘ 𝑢 ) · ( 𝐺 ‘ 𝑣 ) ) ) )
76 70 3 75 rspcdv2 ⊢ ( 𝜑 → ∀ 𝑢 ∈ ℝ ( ( 𝐹 ‘ ( 𝑢 + 𝐵 ) ) + ( 𝐹 ‘ ( 𝑢 − 𝐵 ) ) ) = ( 2 · ( ( 𝐹 ‘ 𝑢 ) · ( 𝐺 ‘ 𝐵 ) ) ) )
77 76 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ℝ ) → ( ( 𝐹 ‘ ( 𝑢 + 𝐵 ) ) + ( 𝐹 ‘ ( 𝑢 − 𝐵 ) ) ) = ( 2 · ( ( 𝐹 ‘ 𝑢 ) · ( 𝐺 ‘ 𝐵 ) ) ) )
78 77 adantlr ⊢ ( ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) ∧ 𝑢 ∈ ℝ ) → ( ( 𝐹 ‘ ( 𝑢 + 𝐵 ) ) + ( 𝐹 ‘ ( 𝑢 − 𝐵 ) ) ) = ( 2 · ( ( 𝐹 ‘ 𝑢 ) · ( 𝐺 ‘ 𝐵 ) ) ) )
79 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) ∧ 𝑢 ∈ ℝ ) → ∀ 𝑦 ∈ ℝ ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 1 )
80 56 57 58 59 78 79 imo72b2lem0 ⊢ ( ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) ∧ 𝑢 ∈ ℝ ) → ( ( abs ‘ ( 𝐹 ‘ 𝑢 ) ) · ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) ≤ sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) )
81 0xr ⊢ 0 ∈ ℝ*
82 81 a1i ⊢ ( ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) ∧ 𝑢 ∈ ℝ ) → 0 ∈ ℝ* )
83 1xr ⊢ 1 ∈ ℝ*
84 83 a1i ⊢ ( ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) ∧ 𝑢 ∈ ℝ ) → 1 ∈ ℝ* )
85 16 adantr ⊢ ( ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) ∧ 𝑢 ∈ ℝ ) → ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ∈ ℝ )
86 85 rexrd ⊢ ( ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) ∧ 𝑢 ∈ ℝ ) → ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ∈ ℝ* )
87 51 a1i ⊢ ( ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) ∧ 𝑢 ∈ ℝ ) → 0 < 1 )
88 simplr ⊢ ( ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) ∧ 𝑢 ∈ ℝ ) → 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) )
89 82 84 86 87 88 xrlttrd ⊢ ( ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) ∧ 𝑢 ∈ ℝ ) → 0 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) )
90 23 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) ∧ 𝑢 ∈ ℝ ) → ( 𝐹 ‘ 𝑢 ) ∈ ℝ )
91 90 recnd ⊢ ( ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) ∧ 𝑢 ∈ ℝ ) → ( 𝐹 ‘ 𝑢 ) ∈ ℂ )
92 91 abscld ⊢ ( ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) ∧ 𝑢 ∈ ℝ ) → ( abs ‘ ( 𝐹 ‘ 𝑢 ) ) ∈ ℝ )
93 46 adantr ⊢ ( ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) ∧ 𝑢 ∈ ℝ ) → sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) ∈ ℝ )
94 80 89 85 92 93 lemuldiv3d ⊢ ( ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) ∧ 𝑢 ∈ ℝ ) → ( abs ‘ ( 𝐹 ‘ 𝑢 ) ) ≤ ( sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) / ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) )
95 94 ralrimiva ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → ∀ 𝑢 ∈ ℝ ( abs ‘ ( 𝐹 ‘ 𝑢 ) ) ≤ ( sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) / ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) )
96 23 55 95 imo72b2lem2 ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) ≤ ( sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) / ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) )
97 96 53 16 46 46 lemuldiv4d ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → ( sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) · ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) ≤ sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) )
98 49 97 eqbrtrrd ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → ( ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) · sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) ) ≤ sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) )
99 6 adantr ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → ∃ 𝑥 ∈ ℝ ( 𝐹 ‘ 𝑥 ) ≠ 0 )
100 5 adantr ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → ∀ 𝑦 ∈ ℝ ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 1 )
101 23 99 100 imo72b2lem1 ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → 0 < sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) )
102 98 101 46 16 46 lemuldiv3d ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ≤ ( sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) / sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) ) )
103 26 46 sseldd ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) ∈ ℂ )
104 101 gt0ne0d ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) ≠ 0 )
105 103 104 dividd ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → ( sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) / sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) ) = 1 )
106 105 eqcomd ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → 1 = ( sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) / sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) ) )
107 102 106 breqtrrd ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ≤ 1 )
108 16 17 107 lensymd ⊢ ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) → ¬ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) )
109 11 108 pm2.65da ⊢ ( 𝜑 → ¬ 1 < ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) )
110 9 10 109 nltled ⊢ ( 𝜑 → ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ≤ 1 )