4sqlem15

Description: Lemma for 4sq . (Contributed by Mario Carneiro, 16-Jul-2014) (Revised by AV, 14-Sep-2020)

	Ref	Expression
Hypotheses	4sq.1	$⊢ S = \{n \| \exists x \in ℤ \exists y \in ℤ \exists z \in ℤ \exists w \in ℤ n = x^{2} + y^{2} + z^{2} + w^{2}\}$
	4sq.2	$⊢ φ \to N \in ℕ$
	4sq.3	$⊢ φ \to P = 2 \cdot N + 1$
	4sq.4	$⊢ φ \to P \in ℙ$
	4sq.5	$⊢ φ \to (0 \dots 2 \cdot N) \subseteq S$
	4sq.6	$⊢ T = \{i \in ℕ \| i P \in S\}$
	4sq.7	$⊢ M = sup (T ℝ <)$
	4sq.m	$⊢ φ \to M \in ℤ_{\geq 2}$
	4sq.a	$⊢ φ \to A \in ℤ$
	4sq.b	$⊢ φ \to B \in ℤ$
	4sq.c	$⊢ φ \to C \in ℤ$
	4sq.d	$⊢ φ \to D \in ℤ$
	4sq.e	$⊢ E = ((A + (\frac{M}{2})) \mod M) - (\frac{M}{2})$
	4sq.f	$⊢ F = ((B + (\frac{M}{2})) \mod M) - (\frac{M}{2})$
	4sq.g	$⊢ G = ((C + (\frac{M}{2})) \mod M) - (\frac{M}{2})$
	4sq.h	$⊢ H = ((D + (\frac{M}{2})) \mod M) - (\frac{M}{2})$
	4sq.r	$⊢ R = \frac{E^{2} + F^{2} + G^{2} + H^{2}}{M}$
	4sq.p	$⊢ φ \to M P = A^{2} + B^{2} + C^{2} + D^{2}$
Assertion	4sqlem15	$⊢ (φ \land R = M) \to (((\frac{\frac{M^{2}}{2}}{2}) - E^{2} = 0 \land (\frac{\frac{M^{2}}{2}}{2}) - F^{2} = 0) \land ((\frac{\frac{M^{2}}{2}}{2}) - G^{2} = 0 \land (\frac{\frac{M^{2}}{2}}{2}) - H^{2} = 0))$

Proof

Step	Hyp	Ref	Expression
1		4sq.1	$⊢ S = \{n \| \exists x \in ℤ \exists y \in ℤ \exists z \in ℤ \exists w \in ℤ n = x^{2} + y^{2} + z^{2} + w^{2}\}$
2		4sq.2	$⊢ φ \to N \in ℕ$
3		4sq.3	$⊢ φ \to P = 2 \cdot N + 1$
4		4sq.4	$⊢ φ \to P \in ℙ$
5		4sq.5	$⊢ φ \to (0 \dots 2 \cdot N) \subseteq S$
6		4sq.6	$⊢ T = \{i \in ℕ \| i P \in S\}$
7		4sq.7	$⊢ M = sup (T ℝ <)$
8		4sq.m	$⊢ φ \to M \in ℤ_{\geq 2}$
9		4sq.a	$⊢ φ \to A \in ℤ$
10		4sq.b	$⊢ φ \to B \in ℤ$
11		4sq.c	$⊢ φ \to C \in ℤ$
12		4sq.d	$⊢ φ \to D \in ℤ$
13		4sq.e	$⊢ E = ((A + (\frac{M}{2})) \mod M) - (\frac{M}{2})$
14		4sq.f	$⊢ F = ((B + (\frac{M}{2})) \mod M) - (\frac{M}{2})$
15		4sq.g	$⊢ G = ((C + (\frac{M}{2})) \mod M) - (\frac{M}{2})$
16		4sq.h	$⊢ H = ((D + (\frac{M}{2})) \mod M) - (\frac{M}{2})$
17		4sq.r	$⊢ R = \frac{E^{2} + F^{2} + G^{2} + H^{2}}{M}$
18		4sq.p	$⊢ φ \to M P = A^{2} + B^{2} + C^{2} + D^{2}$
19		eluz2nn	$⊢ M \in ℤ_{\geq 2} \to M \in ℕ$
20	8 19	syl	$⊢ φ \to M \in ℕ$
21	20	nnred	$⊢ φ \to M \in ℝ$
22	21	resqcld	$⊢ φ \to M^{2} \in ℝ$
23	22	rehalfcld	$⊢ φ \to \frac{M^{2}}{2} \in ℝ$
24	23	rehalfcld	$⊢ φ \to \frac{\frac{M^{2}}{2}}{2} \in ℝ$
25	24	recnd	$⊢ φ \to \frac{\frac{M^{2}}{2}}{2} \in ℂ$
26	9 20 13	4sqlem5	$⊢ φ \to (E \in ℤ \land \frac{A - E}{M} \in ℤ)$
27	26	simpld	$⊢ φ \to E \in ℤ$
28		zsqcl	$⊢ E \in ℤ \to E^{2} \in ℤ$
29	27 28	syl	$⊢ φ \to E^{2} \in ℤ$
30	29	zred	$⊢ φ \to E^{2} \in ℝ$
31	30	recnd	$⊢ φ \to E^{2} \in ℂ$
32	10 20 14	4sqlem5	$⊢ φ \to (F \in ℤ \land \frac{B - F}{M} \in ℤ)$
33	32	simpld	$⊢ φ \to F \in ℤ$
34		zsqcl	$⊢ F \in ℤ \to F^{2} \in ℤ$
35	33 34	syl	$⊢ φ \to F^{2} \in ℤ$
36	35	zred	$⊢ φ \to F^{2} \in ℝ$
37	36	recnd	$⊢ φ \to F^{2} \in ℂ$
38	25 25 31 37	addsub4d	$⊢ φ \to (\frac{\frac{M^{2}}{2}}{2}) + (\frac{\frac{M^{2}}{2}}{2}) - (E^{2} + F^{2}) = ((\frac{\frac{M^{2}}{2}}{2}) - E^{2}) + (\frac{\frac{M^{2}}{2}}{2}) - F^{2}$
39	23	recnd	$⊢ φ \to \frac{M^{2}}{2} \in ℂ$
40	39	2halvesd	$⊢ φ \to (\frac{\frac{M^{2}}{2}}{2}) + (\frac{\frac{M^{2}}{2}}{2}) = \frac{M^{2}}{2}$
41	40	oveq1d	$⊢ φ \to (\frac{\frac{M^{2}}{2}}{2}) + (\frac{\frac{M^{2}}{2}}{2}) - (E^{2} + F^{2}) = (\frac{M^{2}}{2}) - (E^{2} + F^{2})$
42	38 41	eqtr3d	$⊢ φ \to ((\frac{\frac{M^{2}}{2}}{2}) - E^{2}) + (\frac{\frac{M^{2}}{2}}{2}) - F^{2} = (\frac{M^{2}}{2}) - (E^{2} + F^{2})$
43	42	adantr	$⊢ (φ \land R = M) \to ((\frac{\frac{M^{2}}{2}}{2}) - E^{2}) + (\frac{\frac{M^{2}}{2}}{2}) - F^{2} = (\frac{M^{2}}{2}) - (E^{2} + F^{2})$
44	22	recnd	$⊢ φ \to M^{2} \in ℂ$
45	44	2halvesd	$⊢ φ \to (\frac{M^{2}}{2}) + (\frac{M^{2}}{2}) = M^{2}$
46	45	adantr	$⊢ (φ \land R = M) \to (\frac{M^{2}}{2}) + (\frac{M^{2}}{2}) = M^{2}$
47	21	recnd	$⊢ φ \to M \in ℂ$
48	47	sqvald	$⊢ φ \to M^{2} = M \cdot M$
49	48	adantr	$⊢ (φ \land R = M) \to M^{2} = M \cdot M$
50		simpr	$⊢ (φ \land R = M) \to R = M$
51	17 50	eqtr3id	$⊢ (φ \land R = M) \to \frac{E^{2} + F^{2} + G^{2} + H^{2}}{M} = M$
52	51	oveq1d	$⊢ (φ \land R = M) \to (\frac{E^{2} + F^{2} + G^{2} + H^{2}}{M}) \cdot M = M \cdot M$
53	30 36	readdcld	$⊢ φ \to E^{2} + F^{2} \in ℝ$
54	11 20 15	4sqlem5	$⊢ φ \to (G \in ℤ \land \frac{C - G}{M} \in ℤ)$
55	54	simpld	$⊢ φ \to G \in ℤ$
56		zsqcl	$⊢ G \in ℤ \to G^{2} \in ℤ$
57	55 56	syl	$⊢ φ \to G^{2} \in ℤ$
58	57	zred	$⊢ φ \to G^{2} \in ℝ$
59	12 20 16	4sqlem5	$⊢ φ \to (H \in ℤ \land \frac{D - H}{M} \in ℤ)$
60	59	simpld	$⊢ φ \to H \in ℤ$
61		zsqcl	$⊢ H \in ℤ \to H^{2} \in ℤ$
62	60 61	syl	$⊢ φ \to H^{2} \in ℤ$
63	62	zred	$⊢ φ \to H^{2} \in ℝ$
64	58 63	readdcld	$⊢ φ \to G^{2} + H^{2} \in ℝ$
65	53 64	readdcld	$⊢ φ \to E^{2} + F^{2} + G^{2} + H^{2} \in ℝ$
66	65	recnd	$⊢ φ \to E^{2} + F^{2} + G^{2} + H^{2} \in ℂ$
67	20	nnne0d	$⊢ φ \to M \neq 0$
68	66 47 67	divcan1d	$⊢ φ \to (\frac{E^{2} + F^{2} + G^{2} + H^{2}}{M}) \cdot M = E^{2} + F^{2} + G^{2} + H^{2}$
69	68	adantr	$⊢ (φ \land R = M) \to (\frac{E^{2} + F^{2} + G^{2} + H^{2}}{M}) \cdot M = E^{2} + F^{2} + G^{2} + H^{2}$
70	49 52 69	3eqtr2rd	$⊢ (φ \land R = M) \to E^{2} + F^{2} + G^{2} + H^{2} = M^{2}$
71	46 70	oveq12d	$⊢ (φ \land R = M) \to (\frac{M^{2}}{2}) + (\frac{M^{2}}{2}) - (E^{2} + F^{2} + G^{2} + H^{2}) = M^{2} - M^{2}$
72	53	recnd	$⊢ φ \to E^{2} + F^{2} \in ℂ$
73	64	recnd	$⊢ φ \to G^{2} + H^{2} \in ℂ$
74	39 39 72 73	addsub4d	$⊢ φ \to (\frac{M^{2}}{2}) + (\frac{M^{2}}{2}) - (E^{2} + F^{2} + G^{2} + H^{2}) = ((\frac{M^{2}}{2}) - (E^{2} + F^{2})) + (\frac{M^{2}}{2}) - (G^{2} + H^{2})$
75	74	adantr	$⊢ (φ \land R = M) \to (\frac{M^{2}}{2}) + (\frac{M^{2}}{2}) - (E^{2} + F^{2} + G^{2} + H^{2}) = ((\frac{M^{2}}{2}) - (E^{2} + F^{2})) + (\frac{M^{2}}{2}) - (G^{2} + H^{2})$
76	44	subidd	$⊢ φ \to M^{2} - M^{2} = 0$
77	76	adantr	$⊢ (φ \land R = M) \to M^{2} - M^{2} = 0$
78	71 75 77	3eqtr3d	$⊢ (φ \land R = M) \to ((\frac{M^{2}}{2}) - (E^{2} + F^{2})) + (\frac{M^{2}}{2}) - (G^{2} + H^{2}) = 0$
79	23 53	resubcld	$⊢ φ \to (\frac{M^{2}}{2}) - (E^{2} + F^{2}) \in ℝ$
80	9 20 13	4sqlem7	$⊢ φ \to E^{2} \leq \frac{\frac{M^{2}}{2}}{2}$
81	10 20 14	4sqlem7	$⊢ φ \to F^{2} \leq \frac{\frac{M^{2}}{2}}{2}$
82	30 36 24 24 80 81	le2addd	$⊢ φ \to E^{2} + F^{2} \leq (\frac{\frac{M^{2}}{2}}{2}) + (\frac{\frac{M^{2}}{2}}{2})$
83	82 40	breqtrd	$⊢ φ \to E^{2} + F^{2} \leq \frac{M^{2}}{2}$
84	23 53	subge0d	$⊢ φ \to (0 \leq (\frac{M^{2}}{2}) - (E^{2} + F^{2}) \leftrightarrow E^{2} + F^{2} \leq \frac{M^{2}}{2})$
85	83 84	mpbird	$⊢ φ \to 0 \leq (\frac{M^{2}}{2}) - (E^{2} + F^{2})$
86	23 64	resubcld	$⊢ φ \to (\frac{M^{2}}{2}) - (G^{2} + H^{2}) \in ℝ$
87	11 20 15	4sqlem7	$⊢ φ \to G^{2} \leq \frac{\frac{M^{2}}{2}}{2}$
88	12 20 16	4sqlem7	$⊢ φ \to H^{2} \leq \frac{\frac{M^{2}}{2}}{2}$
89	58 63 24 24 87 88	le2addd	$⊢ φ \to G^{2} + H^{2} \leq (\frac{\frac{M^{2}}{2}}{2}) + (\frac{\frac{M^{2}}{2}}{2})$
90	89 40	breqtrd	$⊢ φ \to G^{2} + H^{2} \leq \frac{M^{2}}{2}$
91	23 64	subge0d	$⊢ φ \to (0 \leq (\frac{M^{2}}{2}) - (G^{2} + H^{2}) \leftrightarrow G^{2} + H^{2} \leq \frac{M^{2}}{2})$
92	90 91	mpbird	$⊢ φ \to 0 \leq (\frac{M^{2}}{2}) - (G^{2} + H^{2})$
93		add20	$⊢ (((\frac{M^{2}}{2}) - (E^{2} + F^{2}) \in ℝ \land 0 \leq (\frac{M^{2}}{2}) - (E^{2} + F^{2})) \land ((\frac{M^{2}}{2}) - (G^{2} + H^{2}) \in ℝ \land 0 \leq (\frac{M^{2}}{2}) - (G^{2} + H^{2}))) \to (((\frac{M^{2}}{2}) - (E^{2} + F^{2})) + (\frac{M^{2}}{2}) - (G^{2} + H^{2}) = 0 \leftrightarrow ((\frac{M^{2}}{2}) - (E^{2} + F^{2}) = 0 \land (\frac{M^{2}}{2}) - (G^{2} + H^{2}) = 0))$
94	79 85 86 92 93	syl22anc	$⊢ φ \to (((\frac{M^{2}}{2}) - (E^{2} + F^{2})) + (\frac{M^{2}}{2}) - (G^{2} + H^{2}) = 0 \leftrightarrow ((\frac{M^{2}}{2}) - (E^{2} + F^{2}) = 0 \land (\frac{M^{2}}{2}) - (G^{2} + H^{2}) = 0))$
95	94	biimpa	$⊢ (φ \land ((\frac{M^{2}}{2}) - (E^{2} + F^{2})) + (\frac{M^{2}}{2}) - (G^{2} + H^{2}) = 0) \to ((\frac{M^{2}}{2}) - (E^{2} + F^{2}) = 0 \land (\frac{M^{2}}{2}) - (G^{2} + H^{2}) = 0)$
96	78 95	syldan	$⊢ (φ \land R = M) \to ((\frac{M^{2}}{2}) - (E^{2} + F^{2}) = 0 \land (\frac{M^{2}}{2}) - (G^{2} + H^{2}) = 0)$
97	96	simpld	$⊢ (φ \land R = M) \to (\frac{M^{2}}{2}) - (E^{2} + F^{2}) = 0$
98	43 97	eqtrd	$⊢ (φ \land R = M) \to ((\frac{\frac{M^{2}}{2}}{2}) - E^{2}) + (\frac{\frac{M^{2}}{2}}{2}) - F^{2} = 0$
99	24 30	resubcld	$⊢ φ \to (\frac{\frac{M^{2}}{2}}{2}) - E^{2} \in ℝ$
100	24 30	subge0d	$⊢ φ \to (0 \leq (\frac{\frac{M^{2}}{2}}{2}) - E^{2} \leftrightarrow E^{2} \leq \frac{\frac{M^{2}}{2}}{2})$
101	80 100	mpbird	$⊢ φ \to 0 \leq (\frac{\frac{M^{2}}{2}}{2}) - E^{2}$
102	24 36	resubcld	$⊢ φ \to (\frac{\frac{M^{2}}{2}}{2}) - F^{2} \in ℝ$
103	24 36	subge0d	$⊢ φ \to (0 \leq (\frac{\frac{M^{2}}{2}}{2}) - F^{2} \leftrightarrow F^{2} \leq \frac{\frac{M^{2}}{2}}{2})$
104	81 103	mpbird	$⊢ φ \to 0 \leq (\frac{\frac{M^{2}}{2}}{2}) - F^{2}$
105		add20	$⊢ (((\frac{\frac{M^{2}}{2}}{2}) - E^{2} \in ℝ \land 0 \leq (\frac{\frac{M^{2}}{2}}{2}) - E^{2}) \land ((\frac{\frac{M^{2}}{2}}{2}) - F^{2} \in ℝ \land 0 \leq (\frac{\frac{M^{2}}{2}}{2}) - F^{2})) \to (((\frac{\frac{M^{2}}{2}}{2}) - E^{2}) + (\frac{\frac{M^{2}}{2}}{2}) - F^{2} = 0 \leftrightarrow ((\frac{\frac{M^{2}}{2}}{2}) - E^{2} = 0 \land (\frac{\frac{M^{2}}{2}}{2}) - F^{2} = 0))$
106	99 101 102 104 105	syl22anc	$⊢ φ \to (((\frac{\frac{M^{2}}{2}}{2}) - E^{2}) + (\frac{\frac{M^{2}}{2}}{2}) - F^{2} = 0 \leftrightarrow ((\frac{\frac{M^{2}}{2}}{2}) - E^{2} = 0 \land (\frac{\frac{M^{2}}{2}}{2}) - F^{2} = 0))$
107	106	biimpa	$⊢ (φ \land ((\frac{\frac{M^{2}}{2}}{2}) - E^{2}) + (\frac{\frac{M^{2}}{2}}{2}) - F^{2} = 0) \to ((\frac{\frac{M^{2}}{2}}{2}) - E^{2} = 0 \land (\frac{\frac{M^{2}}{2}}{2}) - F^{2} = 0)$
108	98 107	syldan	$⊢ (φ \land R = M) \to ((\frac{\frac{M^{2}}{2}}{2}) - E^{2} = 0 \land (\frac{\frac{M^{2}}{2}}{2}) - F^{2} = 0)$
109	58	recnd	$⊢ φ \to G^{2} \in ℂ$
110	63	recnd	$⊢ φ \to H^{2} \in ℂ$
111	25 25 109 110	addsub4d	$⊢ φ \to (\frac{\frac{M^{2}}{2}}{2}) + (\frac{\frac{M^{2}}{2}}{2}) - (G^{2} + H^{2}) = ((\frac{\frac{M^{2}}{2}}{2}) - G^{2}) + (\frac{\frac{M^{2}}{2}}{2}) - H^{2}$
112	40	oveq1d	$⊢ φ \to (\frac{\frac{M^{2}}{2}}{2}) + (\frac{\frac{M^{2}}{2}}{2}) - (G^{2} + H^{2}) = (\frac{M^{2}}{2}) - (G^{2} + H^{2})$
113	111 112	eqtr3d	$⊢ φ \to ((\frac{\frac{M^{2}}{2}}{2}) - G^{2}) + (\frac{\frac{M^{2}}{2}}{2}) - H^{2} = (\frac{M^{2}}{2}) - (G^{2} + H^{2})$
114	113	adantr	$⊢ (φ \land R = M) \to ((\frac{\frac{M^{2}}{2}}{2}) - G^{2}) + (\frac{\frac{M^{2}}{2}}{2}) - H^{2} = (\frac{M^{2}}{2}) - (G^{2} + H^{2})$
115	96	simprd	$⊢ (φ \land R = M) \to (\frac{M^{2}}{2}) - (G^{2} + H^{2}) = 0$
116	114 115	eqtrd	$⊢ (φ \land R = M) \to ((\frac{\frac{M^{2}}{2}}{2}) - G^{2}) + (\frac{\frac{M^{2}}{2}}{2}) - H^{2} = 0$
117	24 58	resubcld	$⊢ φ \to (\frac{\frac{M^{2}}{2}}{2}) - G^{2} \in ℝ$
118	24 58	subge0d	$⊢ φ \to (0 \leq (\frac{\frac{M^{2}}{2}}{2}) - G^{2} \leftrightarrow G^{2} \leq \frac{\frac{M^{2}}{2}}{2})$
119	87 118	mpbird	$⊢ φ \to 0 \leq (\frac{\frac{M^{2}}{2}}{2}) - G^{2}$
120	24 63	resubcld	$⊢ φ \to (\frac{\frac{M^{2}}{2}}{2}) - H^{2} \in ℝ$
121	24 63	subge0d	$⊢ φ \to (0 \leq (\frac{\frac{M^{2}}{2}}{2}) - H^{2} \leftrightarrow H^{2} \leq \frac{\frac{M^{2}}{2}}{2})$
122	88 121	mpbird	$⊢ φ \to 0 \leq (\frac{\frac{M^{2}}{2}}{2}) - H^{2}$
123		add20	$⊢ (((\frac{\frac{M^{2}}{2}}{2}) - G^{2} \in ℝ \land 0 \leq (\frac{\frac{M^{2}}{2}}{2}) - G^{2}) \land ((\frac{\frac{M^{2}}{2}}{2}) - H^{2} \in ℝ \land 0 \leq (\frac{\frac{M^{2}}{2}}{2}) - H^{2})) \to (((\frac{\frac{M^{2}}{2}}{2}) - G^{2}) + (\frac{\frac{M^{2}}{2}}{2}) - H^{2} = 0 \leftrightarrow ((\frac{\frac{M^{2}}{2}}{2}) - G^{2} = 0 \land (\frac{\frac{M^{2}}{2}}{2}) - H^{2} = 0))$
124	117 119 120 122 123	syl22anc	$⊢ φ \to (((\frac{\frac{M^{2}}{2}}{2}) - G^{2}) + (\frac{\frac{M^{2}}{2}}{2}) - H^{2} = 0 \leftrightarrow ((\frac{\frac{M^{2}}{2}}{2}) - G^{2} = 0 \land (\frac{\frac{M^{2}}{2}}{2}) - H^{2} = 0))$
125	124	biimpa	$⊢ (φ \land ((\frac{\frac{M^{2}}{2}}{2}) - G^{2}) + (\frac{\frac{M^{2}}{2}}{2}) - H^{2} = 0) \to ((\frac{\frac{M^{2}}{2}}{2}) - G^{2} = 0 \land (\frac{\frac{M^{2}}{2}}{2}) - H^{2} = 0)$
126	116 125	syldan	$⊢ (φ \land R = M) \to ((\frac{\frac{M^{2}}{2}}{2}) - G^{2} = 0 \land (\frac{\frac{M^{2}}{2}}{2}) - H^{2} = 0)$
127	108 126	jca	$⊢ (φ \land R = M) \to (((\frac{\frac{M^{2}}{2}}{2}) - E^{2} = 0 \land (\frac{\frac{M^{2}}{2}}{2}) - F^{2} = 0) \land ((\frac{\frac{M^{2}}{2}}{2}) - G^{2} = 0 \land (\frac{\frac{M^{2}}{2}}{2}) - H^{2} = 0))$

Metamath Proof Explorer

Theorem 4sqlem15

Proof