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	ffvelrnd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ ℝ )
8	7	recnd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ ℂ )
9	8	idi	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ ℂ )
10	2 4	ffvelrnd	⊢ ( 𝜑 → ( 𝐺 ‘ 𝐵 ) ∈ ℝ )
11	10	recnd	⊢ ( 𝜑 → ( 𝐺 ‘ 𝐵 ) ∈ ℂ )
12	11	idi	⊢ ( 𝜑 → ( 𝐺 ‘ 𝐵 ) ∈ ℂ )
13	9 12	mulcld	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) · ( 𝐺 ‘ 𝐵 ) ) ∈ ℂ )
14	13	abscld	⊢ ( 𝜑 → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) · ( 𝐺 ‘ 𝐵 ) ) ) ∈ ℝ )
15		imaco	⊢ ( ( abs ∘ 𝐹 ) “ ℝ ) = ( abs “ ( 𝐹 “ ℝ ) )
16	15	eqcomi	⊢ ( abs “ ( 𝐹 “ ℝ ) ) = ( ( abs ∘ 𝐹 ) “ ℝ )
17		imassrn	⊢ ( ( abs ∘ 𝐹 ) “ ℝ ) ⊆ ran ( abs ∘ 𝐹 )
18	17	a1i	⊢ ( 𝜑 → ( ( abs ∘ 𝐹 ) “ ℝ ) ⊆ ran ( abs ∘ 𝐹 ) )
19		absf	⊢ abs : ℂ ⟶ ℝ
20	19	a1i	⊢ ( 𝜑 → abs : ℂ ⟶ ℝ )
21		ax-resscn	⊢ ℝ ⊆ ℂ
22	21	a1i	⊢ ( 𝜑 → ℝ ⊆ ℂ )
23	20 22	fssresd	⊢ ( 𝜑 → ( abs ↾ ℝ ) : ℝ ⟶ ℝ )
24	1 23	fco2d	⊢ ( 𝜑 → ( abs ∘ 𝐹 ) : ℝ ⟶ ℝ )
25	24	frnd	⊢ ( 𝜑 → ran ( abs ∘ 𝐹 ) ⊆ ℝ )
26	18 25	sstrd	⊢ ( 𝜑 → ( ( abs ∘ 𝐹 ) “ ℝ ) ⊆ ℝ )
27	16 26	eqsstrid	⊢ ( 𝜑 → ( abs “ ( 𝐹 “ ℝ ) ) ⊆ ℝ )
28		0re	⊢ 0 ∈ ℝ
29	28	ne0ii	⊢ ℝ ≠ ∅
30	29	a1i	⊢ ( 𝜑 → ℝ ≠ ∅ )
31	30 24	wnefimgd	⊢ ( 𝜑 → ( ( abs ∘ 𝐹 ) “ ℝ ) ≠ ∅ )
32	31	necomd	⊢ ( 𝜑 → ∅ ≠ ( ( abs ∘ 𝐹 ) “ ℝ ) )
33	16	a1i	⊢ ( 𝜑 → ( abs “ ( 𝐹 “ ℝ ) ) = ( ( abs ∘ 𝐹 ) “ ℝ ) )
34	32 33	neeqtrrd	⊢ ( 𝜑 → ∅ ≠ ( abs “ ( 𝐹 “ ℝ ) ) )
35	34	necomd	⊢ ( 𝜑 → ( abs “ ( 𝐹 “ ℝ ) ) ≠ ∅ )
36		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
37		simpr	⊢ ( ( 𝜑 ∧ 𝑐 = 1 ) → 𝑐 = 1 )
38	37	breq2d	⊢ ( ( 𝜑 ∧ 𝑐 = 1 ) → ( 𝑥 ≤ 𝑐 ↔ 𝑥 ≤ 1 ) )
39	38	ralbidv	⊢ ( ( 𝜑 ∧ 𝑐 = 1 ) → ( ∀ 𝑥 ∈ ( abs “ ( 𝐹 “ ℝ ) ) 𝑥 ≤ 𝑐 ↔ ∀ 𝑥 ∈ ( abs “ ( 𝐹 “ ℝ ) ) 𝑥 ≤ 1 ) )
40	1 6	extoimad	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( abs “ ( 𝐹 “ ℝ ) ) 𝑥 ≤ 1 )
41	36 39 40	rspcedvd	⊢ ( 𝜑 → ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ ( abs “ ( 𝐹 “ ℝ ) ) 𝑥 ≤ 𝑐 )
42	27 35 41	suprcld	⊢ ( 𝜑 → sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) ∈ ℝ )
43		2re	⊢ 2 ∈ ℝ
44	43	a1i	⊢ ( 𝜑 → 2 ∈ ℝ )
45	5	idi	⊢ ( 𝜑 → ( ( 𝐹 ‘ ( 𝐴 + 𝐵 ) ) + ( 𝐹 ‘ ( 𝐴 − 𝐵 ) ) ) = ( 2 · ( ( 𝐹 ‘ 𝐴 ) · ( 𝐺 ‘ 𝐵 ) ) ) )
46	45	fveq2d	⊢ ( 𝜑 → ( abs ‘ ( ( 𝐹 ‘ ( 𝐴 + 𝐵 ) ) + ( 𝐹 ‘ ( 𝐴 − 𝐵 ) ) ) ) = ( abs ‘ ( 2 · ( ( 𝐹 ‘ 𝐴 ) · ( 𝐺 ‘ 𝐵 ) ) ) ) )
47		2cnd	⊢ ( 𝜑 → 2 ∈ ℂ )
48	47 13	mulcld	⊢ ( 𝜑 → ( 2 · ( ( 𝐹 ‘ 𝐴 ) · ( 𝐺 ‘ 𝐵 ) ) ) ∈ ℂ )
49	48	abscld	⊢ ( 𝜑 → ( abs ‘ ( 2 · ( ( 𝐹 ‘ 𝐴 ) · ( 𝐺 ‘ 𝐵 ) ) ) ) ∈ ℝ )
50	46 49	eqeltrd	⊢ ( 𝜑 → ( abs ‘ ( ( 𝐹 ‘ ( 𝐴 + 𝐵 ) ) + ( 𝐹 ‘ ( 𝐴 − 𝐵 ) ) ) ) ∈ ℝ )
51	1	idi	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
52	3	idi	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
53	4	idi	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
54	52 53	readdcld	⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) ∈ ℝ )
55	51 54	ffvelrnd	⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐴 + 𝐵 ) ) ∈ ℝ )
56	55	recnd	⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐴 + 𝐵 ) ) ∈ ℂ )
57	56	abscld	⊢ ( 𝜑 → ( abs ‘ ( 𝐹 ‘ ( 𝐴 + 𝐵 ) ) ) ∈ ℝ )
58	52 53	resubcld	⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ∈ ℝ )
59	51 58	ffvelrnd	⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐴 − 𝐵 ) ) ∈ ℝ )
60	59	recnd	⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐴 − 𝐵 ) ) ∈ ℂ )
61	60	abscld	⊢ ( 𝜑 → ( abs ‘ ( 𝐹 ‘ ( 𝐴 − 𝐵 ) ) ) ∈ ℝ )
62	57 61	readdcld	⊢ ( 𝜑 → ( ( abs ‘ ( 𝐹 ‘ ( 𝐴 + 𝐵 ) ) ) + ( abs ‘ ( 𝐹 ‘ ( 𝐴 − 𝐵 ) ) ) ) ∈ ℝ )
63	44 42	remulcld	⊢ ( 𝜑 → ( 2 · sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) ) ∈ ℝ )
64	56 60	abstrid	⊢ ( 𝜑 → ( abs ‘ ( ( 𝐹 ‘ ( 𝐴 + 𝐵 ) ) + ( 𝐹 ‘ ( 𝐴 − 𝐵 ) ) ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ ( 𝐴 + 𝐵 ) ) ) + ( abs ‘ ( 𝐹 ‘ ( 𝐴 − 𝐵 ) ) ) ) )
65	1 54	fvco3d	⊢ ( 𝜑 → ( ( abs ∘ 𝐹 ) ‘ ( 𝐴 + 𝐵 ) ) = ( abs ‘ ( 𝐹 ‘ ( 𝐴 + 𝐵 ) ) ) )
66	54 24	wfximgfd	⊢ ( 𝜑 → ( ( abs ∘ 𝐹 ) ‘ ( 𝐴 + 𝐵 ) ) ∈ ( ( abs ∘ 𝐹 ) “ ℝ ) )
67	33	idi	⊢ ( 𝜑 → ( abs “ ( 𝐹 “ ℝ ) ) = ( ( abs ∘ 𝐹 ) “ ℝ ) )
68	66 67	eleqtrrd	⊢ ( 𝜑 → ( ( abs ∘ 𝐹 ) ‘ ( 𝐴 + 𝐵 ) ) ∈ ( abs “ ( 𝐹 “ ℝ ) ) )
69	65 68	eqeltrrd	⊢ ( 𝜑 → ( abs ‘ ( 𝐹 ‘ ( 𝐴 + 𝐵 ) ) ) ∈ ( abs “ ( 𝐹 “ ℝ ) ) )
70	27 35 41 69	suprubd	⊢ ( 𝜑 → ( abs ‘ ( 𝐹 ‘ ( 𝐴 + 𝐵 ) ) ) ≤ sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) )
71	1 58	fvco3d	⊢ ( 𝜑 → ( ( abs ∘ 𝐹 ) ‘ ( 𝐴 − 𝐵 ) ) = ( abs ‘ ( 𝐹 ‘ ( 𝐴 − 𝐵 ) ) ) )
72	58 24	wfximgfd	⊢ ( 𝜑 → ( ( abs ∘ 𝐹 ) ‘ ( 𝐴 − 𝐵 ) ) ∈ ( ( abs ∘ 𝐹 ) “ ℝ ) )
73	72 33	eleqtrrd	⊢ ( 𝜑 → ( ( abs ∘ 𝐹 ) ‘ ( 𝐴 − 𝐵 ) ) ∈ ( abs “ ( 𝐹 “ ℝ ) ) )
74	71 73	eqeltrrd	⊢ ( 𝜑 → ( abs ‘ ( 𝐹 ‘ ( 𝐴 − 𝐵 ) ) ) ∈ ( abs “ ( 𝐹 “ ℝ ) ) )
75	27 35 41 74	suprubd	⊢ ( 𝜑 → ( abs ‘ ( 𝐹 ‘ ( 𝐴 − 𝐵 ) ) ) ≤ sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) )
76	57 61 42 42 70 75	le2addd	⊢ ( 𝜑 → ( ( abs ‘ ( 𝐹 ‘ ( 𝐴 + 𝐵 ) ) ) + ( abs ‘ ( 𝐹 ‘ ( 𝐴 − 𝐵 ) ) ) ) ≤ ( sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) + sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) ) )
77	42	recnd	⊢ ( 𝜑 → sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) ∈ ℂ )
78	77	2timesd	⊢ ( 𝜑 → ( 2 · sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) ) = ( sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) + sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) ) )
79	78	eqcomd	⊢ ( 𝜑 → ( sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) + sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) ) = ( 2 · sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) ) )
80	79 63	eqeltrd	⊢ ( 𝜑 → ( sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) + sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) ) ∈ ℝ )
81	76 79 62 80	leeq2d	⊢ ( 𝜑 → ( ( abs ‘ ( 𝐹 ‘ ( 𝐴 + 𝐵 ) ) ) + ( abs ‘ ( 𝐹 ‘ ( 𝐴 − 𝐵 ) ) ) ) ≤ ( 2 · sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) ) )
82	50 62 63 64 81	letrd	⊢ ( 𝜑 → ( abs ‘ ( ( 𝐹 ‘ ( 𝐴 + 𝐵 ) ) + ( 𝐹 ‘ ( 𝐴 − 𝐵 ) ) ) ) ≤ ( 2 · sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) ) )
83	82 46 50 63	leeq1d	⊢ ( 𝜑 → ( abs ‘ ( 2 · ( ( 𝐹 ‘ 𝐴 ) · ( 𝐺 ‘ 𝐵 ) ) ) ) ≤ ( 2 · sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) ) )
84		0le2	⊢ 0 ≤ 2
85	84	a1i	⊢ ( 𝜑 → 0 ≤ 2 )
86	7	idi	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ ℝ )
87	10	idi	⊢ ( 𝜑 → ( 𝐺 ‘ 𝐵 ) ∈ ℝ )
88	86 87	remulcld	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) · ( 𝐺 ‘ 𝐵 ) ) ∈ ℝ )
89	85 44 88	absmulrposd	⊢ ( 𝜑 → ( abs ‘ ( 2 · ( ( 𝐹 ‘ 𝐴 ) · ( 𝐺 ‘ 𝐵 ) ) ) ) = ( 2 · ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) · ( 𝐺 ‘ 𝐵 ) ) ) ) )
90	83 89 49 63	leeq1d	⊢ ( 𝜑 → ( 2 · ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) · ( 𝐺 ‘ 𝐵 ) ) ) ) ≤ ( 2 · sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) ) )
91		2pos	⊢ 0 < 2
92	91	a1i	⊢ ( 𝜑 → 0 < 2 )
93	14 42 44 90 92	wwlemuld	⊢ ( 𝜑 → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) · ( 𝐺 ‘ 𝐵 ) ) ) ≤ sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) )
94	8 11	absmuld	⊢ ( 𝜑 → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) · ( 𝐺 ‘ 𝐵 ) ) ) = ( ( abs ‘ ( 𝐹 ‘ 𝐴 ) ) · ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) )
95	94	idi	⊢ ( 𝜑 → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) · ( 𝐺 ‘ 𝐵 ) ) ) = ( ( abs ‘ ( 𝐹 ‘ 𝐴 ) ) · ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) )
96	93 95 14 42	leeq1d	⊢ ( 𝜑 → ( ( abs ‘ ( 𝐹 ‘ 𝐴 ) ) · ( abs ‘ ( 𝐺 ‘ 𝐵 ) ) ) ≤ sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) )