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	biimpi	$⊢ \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	72	a1i	$⊢ φ \to (\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))$
74	73	imp	$⊢ (φ \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)$
75	4 74	mpdan	$⊢ φ \to \forall v \in ℝ \forall u \in ℝ F (u + v) + F (u - v) = 2 F (u) G (v)$
76	70 3 75	rspcdv2	$⊢ φ \to \forall u \in ℝ F (u + B) + F (u - B) = 2 F (u) G (B)$
77	76	r19.21bi	$⊢ (φ \land u \in ℝ) \to F (u + B) + F (u - B) = 2 F (u) G (B)$
78	77	adantlr	$⊢ ((φ \land 1 < \|G (B)\|) \land u \in ℝ) \to F (u + B) + F (u - B) = 2 F (u) G (B)$
79	5	ad2antrr	$⊢ ((φ \land 1 < \|G (B)\|) \land u \in ℝ) \to \forall y \in ℝ \|F (y)\| \leq 1$
80	56 57 58 59 78 79	imo72b2lem0	$⊢ ((φ \land 1 < \|G (B)\|) \land u \in ℝ) \to \|F (u)\| \|G (B)\| \leq sup (abs [F [ℝ]] ℝ <)$
81		0xr	$⊢ 0 \in ℝ^{*}$
82	81	a1i	$⊢ ((φ \land 1 < \|G (B)\|) \land u \in ℝ) \to 0 \in ℝ^{*}$
83		1xr	$⊢ 1 \in ℝ^{*}$
84	83	a1i	$⊢ ((φ \land 1 < \|G (B)\|) \land u \in ℝ) \to 1 \in ℝ^{*}$
85	16	adantr	$⊢ ((φ \land 1 < \|G (B)\|) \land u \in ℝ) \to \|G (B)\| \in ℝ$
86	85	rexrd	$⊢ ((φ \land 1 < \|G (B)\|) \land u \in ℝ) \to \|G (B)\| \in ℝ^{*}$
87	51	a1i	$⊢ ((φ \land 1 < \|G (B)\|) \land u \in ℝ) \to 0 < 1$
88		simplr	$⊢ ((φ \land 1 < \|G (B)\|) \land u \in ℝ) \to 1 < \|G (B)\|$
89	82 84 86 87 88	xrlttrd	$⊢ ((φ \land 1 < \|G (B)\|) \land u \in ℝ) \to 0 < \|G (B)\|$
90	23	ffvelcdmda	$⊢ ((φ \land 1 < \|G (B)\|) \land u \in ℝ) \to F (u) \in ℝ$
91	90	recnd	$⊢ ((φ \land 1 < \|G (B)\|) \land u \in ℝ) \to F (u) \in ℂ$
92	91	abscld	$⊢ ((φ \land 1 < \|G (B)\|) \land u \in ℝ) \to \|F (u)\| \in ℝ$
93	46	adantr	$⊢ ((φ \land 1 < \|G (B)\|) \land u \in ℝ) \to sup (abs [F [ℝ]] ℝ <) \in ℝ$
94	80 89 85 92 93	lemuldiv3d	$⊢ ((φ \land 1 < \|G (B)\|) \land u \in ℝ) \to \|F (u)\| \leq \frac{sup (abs [F [ℝ]] ℝ <)}{\|G (B)\|}$
95	94	ralrimiva	$⊢ (φ \land 1 < \|G (B)\|) \to \forall u \in ℝ \|F (u)\| \leq \frac{sup (abs [F [ℝ]] ℝ <)}{\|G (B)\|}$
96	23 55 95	imo72b2lem2	$⊢ (φ \land 1 < \|G (B)\|) \to sup (abs [F [ℝ]] ℝ <) \leq \frac{sup (abs [F [ℝ]] ℝ <)}{\|G (B)\|}$
97	96 53 16 46 46	lemuldiv4d	$⊢ (φ \land 1 < \|G (B)\|) \to sup (abs [F [ℝ]] ℝ <) \|G (B)\| \leq sup (abs [F [ℝ]] ℝ <)$
98	49 97	eqbrtrrd	$⊢ (φ \land 1 < \|G (B)\|) \to \|G (B)\| sup (abs [F [ℝ]] ℝ <) \leq sup (abs [F [ℝ]] ℝ <)$
99	6	adantr	$⊢ (φ \land 1 < \|G (B)\|) \to \exists x \in ℝ F (x) \neq 0$
100	5	adantr	$⊢ (φ \land 1 < \|G (B)\|) \to \forall y \in ℝ \|F (y)\| \leq 1$
101	23 99 100	imo72b2lem1	$⊢ (φ \land 1 < \|G (B)\|) \to 0 < sup (abs [F [ℝ]] ℝ <)$
102	98 101 46 16 46	lemuldiv3d	$⊢ (φ \land 1 < \|G (B)\|) \to \|G (B)\| \leq \frac{sup (abs [F [ℝ]] ℝ <)}{sup (abs [F [ℝ]] ℝ <)}$
103	26 46	sseldd	$⊢ (φ \land 1 < \|G (B)\|) \to sup (abs [F [ℝ]] ℝ <) \in ℂ$
104	101	gt0ne0d	$⊢ (φ \land 1 < \|G (B)\|) \to sup (abs [F [ℝ]] ℝ <) \neq 0$
105	103 104	dividd	$⊢ (φ \land 1 < \|G (B)\|) \to \frac{sup (abs [F [ℝ]] ℝ <)}{sup (abs [F [ℝ]] ℝ <)} = 1$
106	105	eqcomd	$⊢ (φ \land 1 < \|G (B)\|) \to 1 = \frac{sup (abs [F [ℝ]] ℝ <)}{sup (abs [F [ℝ]] ℝ <)}$
107	102 106	breqtrrd	$⊢ (φ \land 1 < \|G (B)\|) \to \|G (B)\| \leq 1$
108	16 17 107	lensymd	$⊢ (φ \land 1 < \|G (B)\|) \to \neg 1 < \|G (B)\|$
109	11 108	pm2.65da	$⊢ φ \to \neg 1 < \|G (B)\|$
110	9 10 109	nltled	$⊢ φ \to \|G (B)\| \leq 1$

Metamath Proof Explorer

Theorem imo72b2

Proof