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	$⊢ φ \to F : ℝ ⟶ ℝ$
	imo72b2.2	$⊢ φ \to G : ℝ ⟶ ℝ$
	imo72b2.4	$⊢ φ \to B \in ℝ$
	imo72b2.5	$⊢ φ \to \forall u \in ℝ \forall v \in ℝ F (u + v) + F (u - v) = 2 F (u) G (v)$
	imo72b2.6	$⊢ φ \to \forall y \in ℝ \|F (y)\| \leq 1$
	imo72b2.7	$⊢ φ \to \exists x \in ℝ F (x) \neq 0$
Assertion	imo72b2	$⊢ φ \to \|G (B)\| \leq 1$

Proof

Step	Hyp	Ref	Expression
1		imo72b2.1	$⊢ φ \to F : ℝ ⟶ ℝ$
2		imo72b2.2	$⊢ φ \to G : ℝ ⟶ ℝ$
3		imo72b2.4	$⊢ φ \to B \in ℝ$
4		imo72b2.5	$⊢ φ \to \forall u \in ℝ \forall v \in ℝ F (u + v) + F (u - v) = 2 F (u) G (v)$
5		imo72b2.6	$⊢ φ \to \forall y \in ℝ \|F (y)\| \leq 1$
6		imo72b2.7	$⊢ φ \to \exists x \in ℝ F (x) \neq 0$
7	2 3	ffvelcdmd	$⊢ φ \to G (B) \in ℝ$
8	7	recnd	$⊢ φ \to G (B) \in ℂ$
9	8	abscld	$⊢ φ \to \|G (B)\| \in ℝ$
10		1red	$⊢ φ \to 1 \in ℝ$
11		simpr	$⊢ (φ \land 1 < \|G (B)\|) \to 1 < \|G (B)\|$
12	2	adantr	$⊢ (φ \land 1 < \|G (B)\|) \to G : ℝ ⟶ ℝ$
13	3	adantr	$⊢ (φ \land 1 < \|G (B)\|) \to B \in ℝ$
14	12 13	ffvelcdmd	$⊢ (φ \land 1 < \|G (B)\|) \to G (B) \in ℝ$
15	14	recnd	$⊢ (φ \land 1 < \|G (B)\|) \to G (B) \in ℂ$
16	15	abscld	$⊢ (φ \land 1 < \|G (B)\|) \to \|G (B)\| \in ℝ$
17	10	adantr	$⊢ (φ \land 1 < \|G (B)\|) \to 1 \in ℝ$
18		ax-resscn	$⊢ ℝ \subseteq ℂ$
19		imaco	$⊢ (abs \circ F) [ℝ] = abs [F [ℝ]]$
20	19	eqcomi	$⊢ abs [F [ℝ]] = (abs \circ F) [ℝ]$
21		imassrn	$⊢ (abs \circ F) [ℝ] \subseteq ran (abs \circ F)$
22	21	a1i	$⊢ (φ \land 1 < \|G (B)\|) \to (abs \circ F) [ℝ] \subseteq ran (abs \circ F)$
23	1	adantr	$⊢ (φ \land 1 < \|G (B)\|) \to F : ℝ ⟶ ℝ$
24		absf	$⊢ abs : ℂ ⟶ ℝ$
25	24	a1i	$⊢ (φ \land 1 < \|G (B)\|) \to abs : ℂ ⟶ ℝ$
26	18	a1i	$⊢ (φ \land 1 < \|G (B)\|) \to ℝ \subseteq ℂ$
27	25 26	fssresd	$⊢ (φ \land 1 < \|G (B)\|) \to ({abs ↾}_{ℝ}) : ℝ ⟶ ℝ$
28	23 27	fco2d	$⊢ (φ \land 1 < \|G (B)\|) \to (abs \circ F) : ℝ ⟶ ℝ$
29	28	frnd	$⊢ (φ \land 1 < \|G (B)\|) \to ran (abs \circ F) \subseteq ℝ$
30	22 29	sstrd	$⊢ (φ \land 1 < \|G (B)\|) \to (abs \circ F) [ℝ] \subseteq ℝ$
31	20 30	eqsstrid	$⊢ (φ \land 1 < \|G (B)\|) \to abs [F [ℝ]] \subseteq ℝ$
32		0re	$⊢ 0 \in ℝ$
33	32	ne0ii	$⊢ ℝ \neq \emptyset$
34	33	a1i	$⊢ (φ \land 1 < \|G (B)\|) \to ℝ \neq \emptyset$
35	34 28	wnefimgd	$⊢ (φ \land 1 < \|G (B)\|) \to (abs \circ F) [ℝ] \neq \emptyset$
36	35	necomd	$⊢ (φ \land 1 < \|G (B)\|) \to \emptyset \neq (abs \circ F) [ℝ]$
37	20	a1i	$⊢ (φ \land 1 < \|G (B)\|) \to abs [F [ℝ]] = (abs \circ F) [ℝ]$
38	36 37	neeqtrrd	$⊢ (φ \land 1 < \|G (B)\|) \to \emptyset \neq abs [F [ℝ]]$
39	38	necomd	$⊢ (φ \land 1 < \|G (B)\|) \to abs [F [ℝ]] \neq \emptyset$
40		simpr	$⊢ ((φ \land 1 < \|G (B)\|) \land c = 1) \to c = 1$
41	40	breq2d	$⊢ ((φ \land 1 < \|G (B)\|) \land c = 1) \to (t \leq c \leftrightarrow t \leq 1)$
42	41	ralbidv	$⊢ ((φ \land 1 < \|G (B)\|) \land c = 1) \to (\forall t \in abs [F [ℝ]] t \leq c \leftrightarrow \forall t \in abs [F [ℝ]] t \leq 1)$
43	1 5	extoimad	$⊢ φ \to \forall t \in abs [F [ℝ]] t \leq 1$
44	43	adantr	$⊢ (φ \land 1 < \|G (B)\|) \to \forall t \in abs [F [ℝ]] t \leq 1$
45	17 42 44	rspcedvd	$⊢ (φ \land 1 < \|G (B)\|) \to \exists c \in ℝ \forall t \in abs [F [ℝ]] t \leq c$
46	31 39 45	suprcld	$⊢ (φ \land 1 < \|G (B)\|) \to sup (abs [F [ℝ]] ℝ <) \in ℝ$
47	18 46	sselid	$⊢ (φ \land 1 < \|G (B)\|) \to sup (abs [F [ℝ]] ℝ <) \in ℂ$
48	18 16	sselid	$⊢ (φ \land 1 < \|G (B)\|) \to \|G (B)\| \in ℂ$
49	47 48	mulcomd	$⊢ (φ \land 1 < \|G (B)\|) \to sup (abs [F [ℝ]] ℝ <) \|G (B)\| = \|G (B)\| sup (abs [F [ℝ]] ℝ <)$
50	32	a1i	$⊢ (φ \land 1 < \|G (B)\|) \to 0 \in ℝ$
51		0lt1	$⊢ 0 < 1$
52	51	a1i	$⊢ (φ \land 1 < \|G (B)\|) \to 0 < 1$
53	50 17 16 52 11	lttrd	$⊢ (φ \land 1 < \|G (B)\|) \to 0 < \|G (B)\|$
54	53	gt0ne0d	$⊢ (φ \land 1 < \|G (B)\|) \to \|G (B)\| \neq 0$
55	46 16 54	redivcld	$⊢ (φ \land 1 < \|G (B)\|) \to \frac{sup (abs [F [ℝ]] ℝ <)}{\|G (B)\|} \in ℝ$
56	23	adantr	$⊢ ((φ \land 1 < \|G (B)\|) \land u \in ℝ) \to F : ℝ ⟶ ℝ$
57	12	adantr	$⊢ ((φ \land 1 < \|G (B)\|) \land u \in ℝ) \to G : ℝ ⟶ ℝ$
58		simpr	$⊢ ((φ \land 1 < \|G (B)\|) \land u \in ℝ) \to u \in ℝ$
59	13	adantr	$⊢ ((φ \land 1 < \|G (B)\|) \land u \in ℝ) \to B \in ℝ$
60		simpr	$⊢ (φ \land v = B) \to v = B$
61	60	oveq2d	$⊢ (φ \land v = B) \to u + v = u + B$
62	61	fveq2d	$⊢ (φ \land v = B) \to F (u + v) = F (u + B)$
63	60	oveq2d	$⊢ (φ \land v = B) \to u - v = u - B$
64	63	fveq2d	$⊢ (φ \land v = B) \to F (u - v) = F (u - B)$
65	62 64	oveq12d	$⊢ (φ \land v = B) \to F (u + v) + F (u - v) = F (u + B) + F (u - B)$
66	60	fveq2d	$⊢ (φ \land v = B) \to G (v) = G (B)$
67	66	oveq2d	$⊢ (φ \land v = B) \to F (u) G (v) = F (u) G (B)$
68	67	oveq2d	$⊢ (φ \land v = B) \to 2 F (u) G (v) = 2 F (u) G (B)$
69	65 68	eqeq12d	$⊢ (φ \land v = B) \to (F (u + v) + F (u - v) = 2 F (u) G (v) \leftrightarrow F (u + B) + F (u - B) = 2 F (u) G (B))$
70	69	ralbidv	$⊢ (φ \land v = B) \to (\forall u \in ℝ F (u + v) + F (u - v) = 2 F (u) G (v) \leftrightarrow \forall u \in ℝ F (u + B) + F (u - B) = 2 F (u) G (B))$
71		ralcom	$⊢ \forall u \in ℝ \forall v \in ℝ F (u + v) + F (u - v) = 2 F (u) G (v) \leftrightarrow \forall v \in ℝ \forall u \in ℝ F (u + v) + F (u - v) = 2 F (u) G (v)$
72	71	bilani	$⊢ (φ \land \forall u \in ℝ \forall v \in ℝ F (u + v) + F (u - v) = 2 F (u) G (v)) \to \forall v \in ℝ \forall u \in ℝ F (u + v) + F (u - v) = 2 F (u) G (v)$
73	4 72	mpdan	$⊢ φ \to \forall v \in ℝ \forall u \in ℝ F (u + v) + F (u - v) = 2 F (u) G (v)$
74	70 3 73	rspcdv2	$⊢ φ \to \forall u \in ℝ F (u + B) + F (u - B) = 2 F (u) G (B)$
75	74	r19.21bi	$⊢ (φ \land u \in ℝ) \to F (u + B) + F (u - B) = 2 F (u) G (B)$
76	75	adantlr	$⊢ ((φ \land 1 < \|G (B)\|) \land u \in ℝ) \to F (u + B) + F (u - B) = 2 F (u) G (B)$
77	5	ad2antrr	$⊢ ((φ \land 1 < \|G (B)\|) \land u \in ℝ) \to \forall y \in ℝ \|F (y)\| \leq 1$
78	56 57 58 59 76 77	imo72b2lem0	$⊢ ((φ \land 1 < \|G (B)\|) \land u \in ℝ) \to \|F (u)\| \|G (B)\| \leq sup (abs [F [ℝ]] ℝ <)$
79		0xr	$⊢ 0 \in ℝ^{*}$
80	79	a1i	$⊢ ((φ \land 1 < \|G (B)\|) \land u \in ℝ) \to 0 \in ℝ^{*}$
81		1xr	$⊢ 1 \in ℝ^{*}$
82	81	a1i	$⊢ ((φ \land 1 < \|G (B)\|) \land u \in ℝ) \to 1 \in ℝ^{*}$
83	16	adantr	$⊢ ((φ \land 1 < \|G (B)\|) \land u \in ℝ) \to \|G (B)\| \in ℝ$
84	83	rexrd	$⊢ ((φ \land 1 < \|G (B)\|) \land u \in ℝ) \to \|G (B)\| \in ℝ^{*}$
85	51	a1i	$⊢ ((φ \land 1 < \|G (B)\|) \land u \in ℝ) \to 0 < 1$
86		simplr	$⊢ ((φ \land 1 < \|G (B)\|) \land u \in ℝ) \to 1 < \|G (B)\|$
87	80 82 84 85 86	xrlttrd	$⊢ ((φ \land 1 < \|G (B)\|) \land u \in ℝ) \to 0 < \|G (B)\|$
88	23	ffvelcdmda	$⊢ ((φ \land 1 < \|G (B)\|) \land u \in ℝ) \to F (u) \in ℝ$
89	88	recnd	$⊢ ((φ \land 1 < \|G (B)\|) \land u \in ℝ) \to F (u) \in ℂ$
90	89	abscld	$⊢ ((φ \land 1 < \|G (B)\|) \land u \in ℝ) \to \|F (u)\| \in ℝ$
91	46	adantr	$⊢ ((φ \land 1 < \|G (B)\|) \land u \in ℝ) \to sup (abs [F [ℝ]] ℝ <) \in ℝ$
92	78 87 83 90 91	lemuldiv3d	$⊢ ((φ \land 1 < \|G (B)\|) \land u \in ℝ) \to \|F (u)\| \leq \frac{sup (abs [F [ℝ]] ℝ <)}{\|G (B)\|}$
93	92	ralrimiva	$⊢ (φ \land 1 < \|G (B)\|) \to \forall u \in ℝ \|F (u)\| \leq \frac{sup (abs [F [ℝ]] ℝ <)}{\|G (B)\|}$
94	23 55 93	imo72b2lem2	$⊢ (φ \land 1 < \|G (B)\|) \to sup (abs [F [ℝ]] ℝ <) \leq \frac{sup (abs [F [ℝ]] ℝ <)}{\|G (B)\|}$
95	94 53 16 46 46	lemuldiv4d	$⊢ (φ \land 1 < \|G (B)\|) \to sup (abs [F [ℝ]] ℝ <) \|G (B)\| \leq sup (abs [F [ℝ]] ℝ <)$
96	49 95	eqbrtrrd	$⊢ (φ \land 1 < \|G (B)\|) \to \|G (B)\| sup (abs [F [ℝ]] ℝ <) \leq sup (abs [F [ℝ]] ℝ <)$
97	6	adantr	$⊢ (φ \land 1 < \|G (B)\|) \to \exists x \in ℝ F (x) \neq 0$
98	5	adantr	$⊢ (φ \land 1 < \|G (B)\|) \to \forall y \in ℝ \|F (y)\| \leq 1$
99	23 97 98	imo72b2lem1	$⊢ (φ \land 1 < \|G (B)\|) \to 0 < sup (abs [F [ℝ]] ℝ <)$
100	96 99 46 16 46	lemuldiv3d	$⊢ (φ \land 1 < \|G (B)\|) \to \|G (B)\| \leq \frac{sup (abs [F [ℝ]] ℝ <)}{sup (abs [F [ℝ]] ℝ <)}$
101	26 46	sseldd	$⊢ (φ \land 1 < \|G (B)\|) \to sup (abs [F [ℝ]] ℝ <) \in ℂ$
102	99	gt0ne0d	$⊢ (φ \land 1 < \|G (B)\|) \to sup (abs [F [ℝ]] ℝ <) \neq 0$
103	101 102	dividd	$⊢ (φ \land 1 < \|G (B)\|) \to \frac{sup (abs [F [ℝ]] ℝ <)}{sup (abs [F [ℝ]] ℝ <)} = 1$
104	103	eqcomd	$⊢ (φ \land 1 < \|G (B)\|) \to 1 = \frac{sup (abs [F [ℝ]] ℝ <)}{sup (abs [F [ℝ]] ℝ <)}$
105	100 104	breqtrrd	$⊢ (φ \land 1 < \|G (B)\|) \to \|G (B)\| \leq 1$
106	16 17 105	lensymd	$⊢ (φ \land 1 < \|G (B)\|) \to \neg 1 < \|G (B)\|$
107	11 106	pm2.65da	$⊢ φ \to \neg 1 < \|G (B)\|$
108	9 10 107	nltled	$⊢ φ \to \|G (B)\| \leq 1$

Metamath Proof Explorer

Theorem imo72b2

Proof