Metamath Proof Explorer


Theorem imo72b2

Description: IMO 1972 B2. (14th International Mathemahics 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 ffvelrnd ( 𝜑 → ( 𝐺𝐵 ) ∈ ℝ )
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 ffvelrnd ( ( 𝜑 ∧ 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 sseldi ( ( 𝜑 ∧ 1 < ( abs ‘ ( 𝐺𝐵 ) ) ) → sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) ∈ ℂ )
48 18 16 sseldi ( ( 𝜑 ∧ 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 rspcdvinvd ( 𝜑 → ∀ 𝑢 ∈ ℝ ( ( 𝐹 ‘ ( 𝑢 + 𝐵 ) ) + ( 𝐹 ‘ ( 𝑢𝐵 ) ) ) = ( 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 ffvelrnda ( ( ( 𝜑 ∧ 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 )