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 )