Theorem imo72b2lem0

Description: Lemma for imo72b2 . (Contributed by Stanislas Polu, 9-Mar-2020)

	Ref	Expression
Hypotheses	imo72b2lem0.1	$$⊢\phi \to F:ℝ⟶ℝ$$
	imo72b2lem0.2	$$⊢\phi \to G:ℝ⟶ℝ$$
	imo72b2lem0.3	$$⊢\phi \to A\in ℝ$$
	imo72b2lem0.4	$$⊢\phi \to B\in ℝ$$
	imo72b2lem0.5	$$⊢\phi \to F\left(A+B\right)+F\left(A-B\right)=2F\left(A\right)G\left(B\right)$$
	imo72b2lem0.6	$$⊢\phi \to \forall y\in ℝ\left|F\left(y\right)\right|\le 1$$
Assertion	imo72b2lem0	$$⊢\phi \to \left|F\left(A\right)\right|\left|G\left(B\right)\right|\le sup\left(\mathrm{abs}\left[F\left[ℝ\right]\right],ℝ,<\right)$$

Proof

Step	Hyp	Ref	Expression
1		imo72b2lem0.1	$$⊢\phi \to F:ℝ⟶ℝ$$
2		imo72b2lem0.2	$$⊢\phi \to G:ℝ⟶ℝ$$
3		imo72b2lem0.3	$$⊢\phi \to A\in ℝ$$
4		imo72b2lem0.4	$$⊢\phi \to B\in ℝ$$
5		imo72b2lem0.5	$$⊢\phi \to F\left(A+B\right)+F\left(A-B\right)=2F\left(A\right)G\left(B\right)$$
6		imo72b2lem0.6	$$⊢\phi \to \forall y\in ℝ\left|F\left(y\right)\right|\le 1$$
7	1 3	ffvelcdmd	$$⊢\phi \to F\left(A\right)\in ℝ$$
8	7	recnd	$$⊢\phi \to F\left(A\right)\in ℂ$$
9	8	idi	$$⊢\phi \to F\left(A\right)\in ℂ$$
10	2 4	ffvelcdmd	$$⊢\phi \to G\left(B\right)\in ℝ$$
11	10	recnd	$$⊢\phi \to G\left(B\right)\in ℂ$$
12	11	idi	$$⊢\phi \to G\left(B\right)\in ℂ$$
13	9 12	mulcld	$$⊢\phi \to F\left(A\right)G\left(B\right)\in ℂ$$
14	13	abscld	$$⊢\phi \to \left|F\left(A\right)G\left(B\right)\right|\in ℝ$$
15		imaco	$$⊢\left(\mathrm{abs}\circ F\right)\left[ℝ\right]=\mathrm{abs}\left[F\left[ℝ\right]\right]$$
16	15	eqcomi	$$⊢\mathrm{abs}\left[F\left[ℝ\right]\right]=\left(\mathrm{abs}\circ F\right)\left[ℝ\right]$$
17		imassrn	$$⊢\left(\mathrm{abs}\circ F\right)\left[ℝ\right]\subseteq \mathrm{ran}\left(\mathrm{abs}\circ F\right)$$
18	17	a1i	$$⊢\phi \to \left(\mathrm{abs}\circ F\right)\left[ℝ\right]\subseteq \mathrm{ran}\left(\mathrm{abs}\circ F\right)$$
19		absf	$$⊢\mathrm{abs}:ℂ⟶ℝ$$
20	19	a1i	$$⊢\phi \to \mathrm{abs}:ℂ⟶ℝ$$
21		ax-resscn	$$⊢ℝ\subseteq ℂ$$
22	21	a1i	$$⊢\phi \to ℝ\subseteq ℂ$$
23	20 22	fssresd	$$⊢\phi \to \left({\mathrm{abs}\upharpoonright }_{ℝ}\right):ℝ⟶ℝ$$
24	1 23	fco2d	$$⊢\phi \to \left(\mathrm{abs}\circ F\right):ℝ⟶ℝ$$
25	24	frnd	$$⊢\phi \to \mathrm{ran}\left(\mathrm{abs}\circ F\right)\subseteq ℝ$$
26	18 25	sstrd	$$⊢\phi \to \left(\mathrm{abs}\circ F\right)\left[ℝ\right]\subseteq ℝ$$
27	16 26	eqsstrid	$$⊢\phi \to \mathrm{abs}\left[F\left[ℝ\right]\right]\subseteq ℝ$$
28		0re	$$⊢0\in ℝ$$
29	28	ne0ii	$$⊢ℝ\ne \varnothing$$
30	29	a1i	$$⊢\phi \to ℝ\ne \varnothing$$
31	30 24	wnefimgd	$$⊢\phi \to \left(\mathrm{abs}\circ F\right)\left[ℝ\right]\ne \varnothing$$
32	31	necomd	$$⊢\phi \to \varnothing \ne \left(\mathrm{abs}\circ F\right)\left[ℝ\right]$$
33	16	a1i	$$⊢\phi \to \mathrm{abs}\left[F\left[ℝ\right]\right]=\left(\mathrm{abs}\circ F\right)\left[ℝ\right]$$
34	32 33	neeqtrrd	$$⊢\phi \to \varnothing \ne \mathrm{abs}\left[F\left[ℝ\right]\right]$$
35	34	necomd	$$⊢\phi \to \mathrm{abs}\left[F\left[ℝ\right]\right]\ne \varnothing$$
36		1red	$$⊢\phi \to 1\in ℝ$$
37		simpr	$$⊢\left(\phi \wedge c=1\right)\to c=1$$
38	37	breq2d	$$⊢\left(\phi \wedge c=1\right)\to \left(x\le c\leftrightarrow x\le 1\right)$$
39	38	ralbidv	$$⊢\left(\phi \wedge c=1\right)\to \left(\forall x\in \mathrm{abs}\left[F\left[ℝ\right]\right]x\le c\leftrightarrow \forall x\in \mathrm{abs}\left[F\left[ℝ\right]\right]x\le 1\right)$$
40	1 6	extoimad	$$⊢\phi \to \forall x\in \mathrm{abs}\left[F\left[ℝ\right]\right]x\le 1$$
41	36 39 40	rspcedvd	$$⊢\phi \to \exists c\in ℝ\forall x\in \mathrm{abs}\left[F\left[ℝ\right]\right]x\le c$$
42	27 35 41	suprcld	$$⊢\phi \to sup\left(\mathrm{abs}\left[F\left[ℝ\right]\right],ℝ,<\right)\in ℝ$$
43		2re	$$⊢2\in ℝ$$
44	43	a1i	$$⊢\phi \to 2\in ℝ$$
45	5	idi	$$⊢\phi \to F\left(A+B\right)+F\left(A-B\right)=2F\left(A\right)G\left(B\right)$$
46	45	fveq2d	$$⊢\phi \to \left|F\left(A+B\right)+F\left(A-B\right)\right|=\left|2F\left(A\right)G\left(B\right)\right|$$
47		2cnd	$$⊢\phi \to 2\in ℂ$$
48	47 13	mulcld	$$⊢\phi \to 2F\left(A\right)G\left(B\right)\in ℂ$$
49	48	abscld	$$⊢\phi \to \left|2F\left(A\right)G\left(B\right)\right|\in ℝ$$
50	46 49	eqeltrd	$$⊢\phi \to \left|F\left(A+B\right)+F\left(A-B\right)\right|\in ℝ$$
51	1	idi	$$⊢\phi \to F:ℝ⟶ℝ$$
52	3	idi	$$⊢\phi \to A\in ℝ$$
53	4	idi	$$⊢\phi \to B\in ℝ$$
54	52 53	readdcld	$$⊢\phi \to A+B\in ℝ$$
55	51 54	ffvelcdmd	$$⊢\phi \to F\left(A+B\right)\in ℝ$$
56	55	recnd	$$⊢\phi \to F\left(A+B\right)\in ℂ$$
57	56	abscld	$$⊢\phi \to \left|F\left(A+B\right)\right|\in ℝ$$
58	52 53	resubcld	$$⊢\phi \to A-B\in ℝ$$
59	51 58	ffvelcdmd	$$⊢\phi \to F\left(A-B\right)\in ℝ$$
60	59	recnd	$$⊢\phi \to F\left(A-B\right)\in ℂ$$
61	60	abscld	$$⊢\phi \to \left|F\left(A-B\right)\right|\in ℝ$$
62	57 61	readdcld	$$⊢\phi \to \left|F\left(A+B\right)\right|+\left|F\left(A-B\right)\right|\in ℝ$$
63	44 42	remulcld	$$⊢\phi \to 2sup\left(\mathrm{abs}\left[F\left[ℝ\right]\right],ℝ,<\right)\in ℝ$$
64	56 60	abstrid	$$⊢\phi \to \left|F\left(A+B\right)+F\left(A-B\right)\right|\le \left|F\left(A+B\right)\right|+\left|F\left(A-B\right)\right|$$
65	1 54	fvco3d	$$⊢\phi \to \left(\mathrm{abs}\circ F\right)\left(A+B\right)=\left|F\left(A+B\right)\right|$$
66	54 24	wfximgfd	$$⊢\phi \to \left(\mathrm{abs}\circ F\right)\left(A+B\right)\in \left(\mathrm{abs}\circ F\right)\left[ℝ\right]$$
67	33	idi	$$⊢\phi \to \mathrm{abs}\left[F\left[ℝ\right]\right]=\left(\mathrm{abs}\circ F\right)\left[ℝ\right]$$
68	66 67	eleqtrrd	$$⊢\phi \to \left(\mathrm{abs}\circ F\right)\left(A+B\right)\in \mathrm{abs}\left[F\left[ℝ\right]\right]$$
69	65 68	eqeltrrd	$$⊢\phi \to \left|F\left(A+B\right)\right|\in \mathrm{abs}\left[F\left[ℝ\right]\right]$$
70	27 35 41 69	suprubd	$$⊢\phi \to \left|F\left(A+B\right)\right|\le sup\left(\mathrm{abs}\left[F\left[ℝ\right]\right],ℝ,<\right)$$
71	1 58	fvco3d	$$⊢\phi \to \left(\mathrm{abs}\circ F\right)\left(A-B\right)=\left|F\left(A-B\right)\right|$$
72	58 24	wfximgfd	$$⊢\phi \to \left(\mathrm{abs}\circ F\right)\left(A-B\right)\in \left(\mathrm{abs}\circ F\right)\left[ℝ\right]$$
73	72 33	eleqtrrd	$$⊢\phi \to \left(\mathrm{abs}\circ F\right)\left(A-B\right)\in \mathrm{abs}\left[F\left[ℝ\right]\right]$$
74	71 73	eqeltrrd	$$⊢\phi \to \left|F\left(A-B\right)\right|\in \mathrm{abs}\left[F\left[ℝ\right]\right]$$
75	27 35 41 74	suprubd	$$⊢\phi \to \left|F\left(A-B\right)\right|\le sup\left(\mathrm{abs}\left[F\left[ℝ\right]\right],ℝ,<\right)$$
76	57 61 42 42 70 75	le2addd	$$⊢\phi \to \left|F\left(A+B\right)\right|+\left|F\left(A-B\right)\right|\le sup\left(\mathrm{abs}\left[F\left[ℝ\right]\right],ℝ,<\right)+sup\left(\mathrm{abs}\left[F\left[ℝ\right]\right],ℝ,<\right)$$
77	42	recnd	$$⊢\phi \to sup\left(\mathrm{abs}\left[F\left[ℝ\right]\right],ℝ,<\right)\in ℂ$$
78	77	2timesd	$$⊢\phi \to 2sup\left(\mathrm{abs}\left[F\left[ℝ\right]\right],ℝ,<\right)=sup\left(\mathrm{abs}\left[F\left[ℝ\right]\right],ℝ,<\right)+sup\left(\mathrm{abs}\left[F\left[ℝ\right]\right],ℝ,<\right)$$
79	78	eqcomd	$$⊢\phi \to sup\left(\mathrm{abs}\left[F\left[ℝ\right]\right],ℝ,<\right)+sup\left(\mathrm{abs}\left[F\left[ℝ\right]\right],ℝ,<\right)=2sup\left(\mathrm{abs}\left[F\left[ℝ\right]\right],ℝ,<\right)$$
80	79 63	eqeltrd	$$⊢\phi \to sup\left(\mathrm{abs}\left[F\left[ℝ\right]\right],ℝ,<\right)+sup\left(\mathrm{abs}\left[F\left[ℝ\right]\right],ℝ,<\right)\in ℝ$$
81	76 79 62 80	leeq2d	$$⊢\phi \to \left|F\left(A+B\right)\right|+\left|F\left(A-B\right)\right|\le 2sup\left(\mathrm{abs}\left[F\left[ℝ\right]\right],ℝ,<\right)$$
82	50 62 63 64 81	letrd	$$⊢\phi \to \left|F\left(A+B\right)+F\left(A-B\right)\right|\le 2sup\left(\mathrm{abs}\left[F\left[ℝ\right]\right],ℝ,<\right)$$
83	82 46 50 63	leeq1d	$$⊢\phi \to \left|2F\left(A\right)G\left(B\right)\right|\le 2sup\left(\mathrm{abs}\left[F\left[ℝ\right]\right],ℝ,<\right)$$
84		0le2	$$⊢0\le 2$$
85	84	a1i	$$⊢\phi \to 0\le 2$$
86	7	idi	$$⊢\phi \to F\left(A\right)\in ℝ$$
87	10	idi	$$⊢\phi \to G\left(B\right)\in ℝ$$
88	86 87	remulcld	$$⊢\phi \to F\left(A\right)G\left(B\right)\in ℝ$$
89	85 44 88	absmulrposd	$$⊢\phi \to \left|2F\left(A\right)G\left(B\right)\right|=2\left|F\left(A\right)G\left(B\right)\right|$$
90	83 89 49 63	leeq1d	$$⊢\phi \to 2\left|F\left(A\right)G\left(B\right)\right|\le 2sup\left(\mathrm{abs}\left[F\left[ℝ\right]\right],ℝ,<\right)$$
91		2pos	$$⊢0<2$$
92	91	a1i	$$⊢\phi \to 0<2$$
93	14 42 44 90 92	wwlemuld	$$⊢\phi \to \left|F\left(A\right)G\left(B\right)\right|\le sup\left(\mathrm{abs}\left[F\left[ℝ\right]\right],ℝ,<\right)$$
94	8 11	absmuld	$$⊢\phi \to \left|F\left(A\right)G\left(B\right)\right|=\left|F\left(A\right)\right|\left|G\left(B\right)\right|$$
95	94	idi	$$⊢\phi \to \left|F\left(A\right)G\left(B\right)\right|=\left|F\left(A\right)\right|\left|G\left(B\right)\right|$$
96	93 95 14 42	leeq1d	$$⊢\phi \to \left|F\left(A\right)\right|\left|G\left(B\right)\right|\le sup\left(\mathrm{abs}\left[F\left[ℝ\right]\right],ℝ,<\right)$$