4sqlem16

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	4sqlem16	$⊢ φ \to (R \leq M \land ((R = 0 \lor R = M) \to M^{2} ∥ M P))$

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	9 20 13	4sqlem5	$⊢ φ \to (E \in ℤ \land \frac{A - E}{M} \in ℤ)$
22	21	simpld	$⊢ φ \to E \in ℤ$
23		zsqcl	$⊢ E \in ℤ \to E^{2} \in ℤ$
24	22 23	syl	$⊢ φ \to E^{2} \in ℤ$
25	24	zred	$⊢ φ \to E^{2} \in ℝ$
26	10 20 14	4sqlem5	$⊢ φ \to (F \in ℤ \land \frac{B - F}{M} \in ℤ)$
27	26	simpld	$⊢ φ \to F \in ℤ$
28		zsqcl	$⊢ F \in ℤ \to F^{2} \in ℤ$
29	27 28	syl	$⊢ φ \to F^{2} \in ℤ$
30	29	zred	$⊢ φ \to F^{2} \in ℝ$
31	25 30	readdcld	$⊢ φ \to E^{2} + F^{2} \in ℝ$
32	11 20 15	4sqlem5	$⊢ φ \to (G \in ℤ \land \frac{C - G}{M} \in ℤ)$
33	32	simpld	$⊢ φ \to G \in ℤ$
34		zsqcl	$⊢ G \in ℤ \to G^{2} \in ℤ$
35	33 34	syl	$⊢ φ \to G^{2} \in ℤ$
36	35	zred	$⊢ φ \to G^{2} \in ℝ$
37	12 20 16	4sqlem5	$⊢ φ \to (H \in ℤ \land \frac{D - H}{M} \in ℤ)$
38	37	simpld	$⊢ φ \to H \in ℤ$
39		zsqcl	$⊢ H \in ℤ \to H^{2} \in ℤ$
40	38 39	syl	$⊢ φ \to H^{2} \in ℤ$
41	40	zred	$⊢ φ \to H^{2} \in ℝ$
42	36 41	readdcld	$⊢ φ \to G^{2} + H^{2} \in ℝ$
43	20	nnred	$⊢ φ \to M \in ℝ$
44	43	resqcld	$⊢ φ \to M^{2} \in ℝ$
45	44	rehalfcld	$⊢ φ \to \frac{M^{2}}{2} \in ℝ$
46	45	rehalfcld	$⊢ φ \to \frac{\frac{M^{2}}{2}}{2} \in ℝ$
47	9 20 13	4sqlem7	$⊢ φ \to E^{2} \leq \frac{\frac{M^{2}}{2}}{2}$
48	10 20 14	4sqlem7	$⊢ φ \to F^{2} \leq \frac{\frac{M^{2}}{2}}{2}$
49	25 30 46 46 47 48	le2addd	$⊢ φ \to E^{2} + F^{2} \leq (\frac{\frac{M^{2}}{2}}{2}) + (\frac{\frac{M^{2}}{2}}{2})$
50	45	recnd	$⊢ φ \to \frac{M^{2}}{2} \in ℂ$
51	50	2halvesd	$⊢ φ \to (\frac{\frac{M^{2}}{2}}{2}) + (\frac{\frac{M^{2}}{2}}{2}) = \frac{M^{2}}{2}$
52	49 51	breqtrd	$⊢ φ \to E^{2} + F^{2} \leq \frac{M^{2}}{2}$
53	11 20 15	4sqlem7	$⊢ φ \to G^{2} \leq \frac{\frac{M^{2}}{2}}{2}$
54	12 20 16	4sqlem7	$⊢ φ \to H^{2} \leq \frac{\frac{M^{2}}{2}}{2}$
55	36 41 46 46 53 54	le2addd	$⊢ φ \to G^{2} + H^{2} \leq (\frac{\frac{M^{2}}{2}}{2}) + (\frac{\frac{M^{2}}{2}}{2})$
56	55 51	breqtrd	$⊢ φ \to G^{2} + H^{2} \leq \frac{M^{2}}{2}$
57	31 42 45 45 52 56	le2addd	$⊢ φ \to E^{2} + F^{2} + G^{2} + H^{2} \leq (\frac{M^{2}}{2}) + (\frac{M^{2}}{2})$
58	44	recnd	$⊢ φ \to M^{2} \in ℂ$
59	58	2halvesd	$⊢ φ \to (\frac{M^{2}}{2}) + (\frac{M^{2}}{2}) = M^{2}$
60	57 59	breqtrd	$⊢ φ \to E^{2} + F^{2} + G^{2} + H^{2} \leq M^{2}$
61	43	recnd	$⊢ φ \to M \in ℂ$
62	61	sqvald	$⊢ φ \to M^{2} = M \cdot M$
63	60 62	breqtrd	$⊢ φ \to E^{2} + F^{2} + G^{2} + H^{2} \leq M \cdot M$
64	31 42	readdcld	$⊢ φ \to E^{2} + F^{2} + G^{2} + H^{2} \in ℝ$
65	20	nngt0d	$⊢ φ \to 0 < M$
66		ledivmul	$⊢ (E^{2} + F^{2} + G^{2} + H^{2} \in ℝ \land M \in ℝ \land (M \in ℝ \land 0 < M)) \to (\frac{E^{2} + F^{2} + G^{2} + H^{2}}{M} \leq M \leftrightarrow E^{2} + F^{2} + G^{2} + H^{2} \leq M \cdot M)$
67	64 43 43 65 66	syl112anc	$⊢ φ \to (\frac{E^{2} + F^{2} + G^{2} + H^{2}}{M} \leq M \leftrightarrow E^{2} + F^{2} + G^{2} + H^{2} \leq M \cdot M)$
68	63 67	mpbird	$⊢ φ \to \frac{E^{2} + F^{2} + G^{2} + H^{2}}{M} \leq M$
69	17 68	eqbrtrid	$⊢ φ \to R \leq M$
70		simpr	$⊢ (φ \land R = 0) \to R = 0$
71	17 70	syl5eqr	$⊢ (φ \land R = 0) \to \frac{E^{2} + F^{2} + G^{2} + H^{2}}{M} = 0$
72	64	recnd	$⊢ φ \to E^{2} + F^{2} + G^{2} + H^{2} \in ℂ$
73	20	nnne0d	$⊢ φ \to M \neq 0$
74	72 61 73	diveq0ad	$⊢ φ \to (\frac{E^{2} + F^{2} + G^{2} + H^{2}}{M} = 0 \leftrightarrow E^{2} + F^{2} + G^{2} + H^{2} = 0)$
75		zsqcl2	$⊢ E \in ℤ \to E^{2} \in ℕ_{0}$
76	22 75	syl	$⊢ φ \to E^{2} \in ℕ_{0}$
77		zsqcl2	$⊢ F \in ℤ \to F^{2} \in ℕ_{0}$
78	27 77	syl	$⊢ φ \to F^{2} \in ℕ_{0}$
79	76 78	nn0addcld	$⊢ φ \to E^{2} + F^{2} \in ℕ_{0}$
80	79	nn0ge0d	$⊢ φ \to 0 \leq E^{2} + F^{2}$
81		zsqcl2	$⊢ G \in ℤ \to G^{2} \in ℕ_{0}$
82	33 81	syl	$⊢ φ \to G^{2} \in ℕ_{0}$
83		zsqcl2	$⊢ H \in ℤ \to H^{2} \in ℕ_{0}$
84	38 83	syl	$⊢ φ \to H^{2} \in ℕ_{0}$
85	82 84	nn0addcld	$⊢ φ \to G^{2} + H^{2} \in ℕ_{0}$
86	85	nn0ge0d	$⊢ φ \to 0 \leq G^{2} + H^{2}$
87		add20	$⊢ ((E^{2} + F^{2} \in ℝ \land 0 \leq E^{2} + F^{2}) \land (G^{2} + H^{2} \in ℝ \land 0 \leq G^{2} + H^{2})) \to (E^{2} + F^{2} + G^{2} + H^{2} = 0 \leftrightarrow (E^{2} + F^{2} = 0 \land G^{2} + H^{2} = 0))$
88	31 80 42 86 87	syl22anc	$⊢ φ \to (E^{2} + F^{2} + G^{2} + H^{2} = 0 \leftrightarrow (E^{2} + F^{2} = 0 \land G^{2} + H^{2} = 0))$
89	74 88	bitrd	$⊢ φ \to (\frac{E^{2} + F^{2} + G^{2} + H^{2}}{M} = 0 \leftrightarrow (E^{2} + F^{2} = 0 \land G^{2} + H^{2} = 0))$
90	89	biimpa	$⊢ (φ \land \frac{E^{2} + F^{2} + G^{2} + H^{2}}{M} = 0) \to (E^{2} + F^{2} = 0 \land G^{2} + H^{2} = 0)$
91	71 90	syldan	$⊢ (φ \land R = 0) \to (E^{2} + F^{2} = 0 \land G^{2} + H^{2} = 0)$
92	91	simpld	$⊢ (φ \land R = 0) \to E^{2} + F^{2} = 0$
93	76	nn0ge0d	$⊢ φ \to 0 \leq E^{2}$
94	78	nn0ge0d	$⊢ φ \to 0 \leq F^{2}$
95		add20	$⊢ ((E^{2} \in ℝ \land 0 \leq E^{2}) \land (F^{2} \in ℝ \land 0 \leq F^{2})) \to (E^{2} + F^{2} = 0 \leftrightarrow (E^{2} = 0 \land F^{2} = 0))$
96	25 93 30 94 95	syl22anc	$⊢ φ \to (E^{2} + F^{2} = 0 \leftrightarrow (E^{2} = 0 \land F^{2} = 0))$
97	96	biimpa	$⊢ (φ \land E^{2} + F^{2} = 0) \to (E^{2} = 0 \land F^{2} = 0)$
98	92 97	syldan	$⊢ (φ \land R = 0) \to (E^{2} = 0 \land F^{2} = 0)$
99	98	simpld	$⊢ (φ \land R = 0) \to E^{2} = 0$
100	9 20 13 99	4sqlem9	$⊢ (φ \land R = 0) \to M^{2} ∥ A^{2}$
101	98	simprd	$⊢ (φ \land R = 0) \to F^{2} = 0$
102	10 20 14 101	4sqlem9	$⊢ (φ \land R = 0) \to M^{2} ∥ B^{2}$
103	20	nnsqcld	$⊢ φ \to M^{2} \in ℕ$
104	103	nnzd	$⊢ φ \to M^{2} \in ℤ$
105		zsqcl	$⊢ A \in ℤ \to A^{2} \in ℤ$
106	9 105	syl	$⊢ φ \to A^{2} \in ℤ$
107		zsqcl	$⊢ B \in ℤ \to B^{2} \in ℤ$
108	10 107	syl	$⊢ φ \to B^{2} \in ℤ$
109		dvds2add	$⊢ (M^{2} \in ℤ \land A^{2} \in ℤ \land B^{2} \in ℤ) \to ((M^{2} ∥ A^{2} \land M^{2} ∥ B^{2}) \to M^{2} ∥ (A^{2} + B^{2}))$
110	104 106 108 109	syl3anc	$⊢ φ \to ((M^{2} ∥ A^{2} \land M^{2} ∥ B^{2}) \to M^{2} ∥ (A^{2} + B^{2}))$
111	110	adantr	$⊢ (φ \land R = 0) \to ((M^{2} ∥ A^{2} \land M^{2} ∥ B^{2}) \to M^{2} ∥ (A^{2} + B^{2}))$
112	100 102 111	mp2and	$⊢ (φ \land R = 0) \to M^{2} ∥ (A^{2} + B^{2})$
113	91	simprd	$⊢ (φ \land R = 0) \to G^{2} + H^{2} = 0$
114	82	nn0ge0d	$⊢ φ \to 0 \leq G^{2}$
115	84	nn0ge0d	$⊢ φ \to 0 \leq H^{2}$
116		add20	$⊢ ((G^{2} \in ℝ \land 0 \leq G^{2}) \land (H^{2} \in ℝ \land 0 \leq H^{2})) \to (G^{2} + H^{2} = 0 \leftrightarrow (G^{2} = 0 \land H^{2} = 0))$
117	36 114 41 115 116	syl22anc	$⊢ φ \to (G^{2} + H^{2} = 0 \leftrightarrow (G^{2} = 0 \land H^{2} = 0))$
118	117	biimpa	$⊢ (φ \land G^{2} + H^{2} = 0) \to (G^{2} = 0 \land H^{2} = 0)$
119	113 118	syldan	$⊢ (φ \land R = 0) \to (G^{2} = 0 \land H^{2} = 0)$
120	119	simpld	$⊢ (φ \land R = 0) \to G^{2} = 0$
121	11 20 15 120	4sqlem9	$⊢ (φ \land R = 0) \to M^{2} ∥ C^{2}$
122	119	simprd	$⊢ (φ \land R = 0) \to H^{2} = 0$
123	12 20 16 122	4sqlem9	$⊢ (φ \land R = 0) \to M^{2} ∥ D^{2}$
124		zsqcl	$⊢ C \in ℤ \to C^{2} \in ℤ$
125	11 124	syl	$⊢ φ \to C^{2} \in ℤ$
126		zsqcl	$⊢ D \in ℤ \to D^{2} \in ℤ$
127	12 126	syl	$⊢ φ \to D^{2} \in ℤ$
128		dvds2add	$⊢ (M^{2} \in ℤ \land C^{2} \in ℤ \land D^{2} \in ℤ) \to ((M^{2} ∥ C^{2} \land M^{2} ∥ D^{2}) \to M^{2} ∥ (C^{2} + D^{2}))$
129	104 125 127 128	syl3anc	$⊢ φ \to ((M^{2} ∥ C^{2} \land M^{2} ∥ D^{2}) \to M^{2} ∥ (C^{2} + D^{2}))$
130	129	adantr	$⊢ (φ \land R = 0) \to ((M^{2} ∥ C^{2} \land M^{2} ∥ D^{2}) \to M^{2} ∥ (C^{2} + D^{2}))$
131	121 123 130	mp2and	$⊢ (φ \land R = 0) \to M^{2} ∥ (C^{2} + D^{2})$
132	106 108	zaddcld	$⊢ φ \to A^{2} + B^{2} \in ℤ$
133	125 127	zaddcld	$⊢ φ \to C^{2} + D^{2} \in ℤ$
134		dvds2add	$⊢ (M^{2} \in ℤ \land A^{2} + B^{2} \in ℤ \land C^{2} + D^{2} \in ℤ) \to ((M^{2} ∥ (A^{2} + B^{2}) \land M^{2} ∥ (C^{2} + D^{2})) \to M^{2} ∥ (A^{2} + B^{2} + C^{2} + D^{2}))$
135	104 132 133 134	syl3anc	$⊢ φ \to ((M^{2} ∥ (A^{2} + B^{2}) \land M^{2} ∥ (C^{2} + D^{2})) \to M^{2} ∥ (A^{2} + B^{2} + C^{2} + D^{2}))$
136	135	adantr	$⊢ (φ \land R = 0) \to ((M^{2} ∥ (A^{2} + B^{2}) \land M^{2} ∥ (C^{2} + D^{2})) \to M^{2} ∥ (A^{2} + B^{2} + C^{2} + D^{2}))$
137	112 131 136	mp2and	$⊢ (φ \land R = 0) \to M^{2} ∥ (A^{2} + B^{2} + C^{2} + D^{2})$
138	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18	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))$
139	138	simpld	$⊢ (φ \land R = M) \to ((\frac{\frac{M^{2}}{2}}{2}) - E^{2} = 0 \land (\frac{\frac{M^{2}}{2}}{2}) - F^{2} = 0)$
140	139	simpld	$⊢ (φ \land R = M) \to (\frac{\frac{M^{2}}{2}}{2}) - E^{2} = 0$
141	9 20 13 140	4sqlem10	$⊢ (φ \land R = M) \to M^{2} ∥ (A^{2} - (\frac{\frac{M^{2}}{2}}{2}))$
142	139	simprd	$⊢ (φ \land R = M) \to (\frac{\frac{M^{2}}{2}}{2}) - F^{2} = 0$
143	10 20 14 142	4sqlem10	$⊢ (φ \land R = M) \to M^{2} ∥ (B^{2} - (\frac{\frac{M^{2}}{2}}{2}))$
144	104	adantr	$⊢ (φ \land R = M) \to M^{2} \in ℤ$
145	106	adantr	$⊢ (φ \land R = M) \to A^{2} \in ℤ$
146	46	recnd	$⊢ φ \to \frac{\frac{M^{2}}{2}}{2} \in ℂ$
147	24	zcnd	$⊢ φ \to E^{2} \in ℂ$
148	146 147	subeq0ad	$⊢ φ \to ((\frac{\frac{M^{2}}{2}}{2}) - E^{2} = 0 \leftrightarrow \frac{\frac{M^{2}}{2}}{2} = E^{2})$
149	148	adantr	$⊢ (φ \land R = M) \to ((\frac{\frac{M^{2}}{2}}{2}) - E^{2} = 0 \leftrightarrow \frac{\frac{M^{2}}{2}}{2} = E^{2})$
150	140 149	mpbid	$⊢ (φ \land R = M) \to \frac{\frac{M^{2}}{2}}{2} = E^{2}$
151	24	adantr	$⊢ (φ \land R = M) \to E^{2} \in ℤ$
152	150 151	eqeltrd	$⊢ (φ \land R = M) \to \frac{\frac{M^{2}}{2}}{2} \in ℤ$
153	145 152	zsubcld	$⊢ (φ \land R = M) \to A^{2} - (\frac{\frac{M^{2}}{2}}{2}) \in ℤ$
154	108	adantr	$⊢ (φ \land R = M) \to B^{2} \in ℤ$
155	154 152	zsubcld	$⊢ (φ \land R = M) \to B^{2} - (\frac{\frac{M^{2}}{2}}{2}) \in ℤ$
156		dvds2add	$⊢ (M^{2} \in ℤ \land A^{2} - (\frac{\frac{M^{2}}{2}}{2}) \in ℤ \land B^{2} - (\frac{\frac{M^{2}}{2}}{2}) \in ℤ) \to ((M^{2} ∥ (A^{2} - (\frac{\frac{M^{2}}{2}}{2})) \land M^{2} ∥ (B^{2} - (\frac{\frac{M^{2}}{2}}{2}))) \to M^{2} ∥ ((A^{2} - (\frac{\frac{M^{2}}{2}}{2})) + B^{2} - (\frac{\frac{M^{2}}{2}}{2})))$
157	144 153 155 156	syl3anc	$⊢ (φ \land R = M) \to ((M^{2} ∥ (A^{2} - (\frac{\frac{M^{2}}{2}}{2})) \land M^{2} ∥ (B^{2} - (\frac{\frac{M^{2}}{2}}{2}))) \to M^{2} ∥ ((A^{2} - (\frac{\frac{M^{2}}{2}}{2})) + B^{2} - (\frac{\frac{M^{2}}{2}}{2})))$
158	141 143 157	mp2and	$⊢ (φ \land R = M) \to M^{2} ∥ ((A^{2} - (\frac{\frac{M^{2}}{2}}{2})) + B^{2} - (\frac{\frac{M^{2}}{2}}{2}))$
159	106	zcnd	$⊢ φ \to A^{2} \in ℂ$
160	108	zcnd	$⊢ φ \to B^{2} \in ℂ$
161	159 160 146 146	addsub4d	$⊢ φ \to A^{2} + B^{2} - ((\frac{\frac{M^{2}}{2}}{2}) + (\frac{\frac{M^{2}}{2}}{2})) = (A^{2} - (\frac{\frac{M^{2}}{2}}{2})) + B^{2} - (\frac{\frac{M^{2}}{2}}{2})$
162	51	oveq2d	$⊢ φ \to A^{2} + B^{2} - ((\frac{\frac{M^{2}}{2}}{2}) + (\frac{\frac{M^{2}}{2}}{2})) = A^{2} + B^{2} - (\frac{M^{2}}{2})$
163	161 162	eqtr3d	$⊢ φ \to (A^{2} - (\frac{\frac{M^{2}}{2}}{2})) + B^{2} - (\frac{\frac{M^{2}}{2}}{2}) = A^{2} + B^{2} - (\frac{M^{2}}{2})$
164	163	adantr	$⊢ (φ \land R = M) \to (A^{2} - (\frac{\frac{M^{2}}{2}}{2})) + B^{2} - (\frac{\frac{M^{2}}{2}}{2}) = A^{2} + B^{2} - (\frac{M^{2}}{2})$
165	158 164	breqtrd	$⊢ (φ \land R = M) \to M^{2} ∥ (A^{2} + B^{2} - (\frac{M^{2}}{2}))$
166	138	simprd	$⊢ (φ \land R = M) \to ((\frac{\frac{M^{2}}{2}}{2}) - G^{2} = 0 \land (\frac{\frac{M^{2}}{2}}{2}) - H^{2} = 0)$
167	166	simpld	$⊢ (φ \land R = M) \to (\frac{\frac{M^{2}}{2}}{2}) - G^{2} = 0$
168	11 20 15 167	4sqlem10	$⊢ (φ \land R = M) \to M^{2} ∥ (C^{2} - (\frac{\frac{M^{2}}{2}}{2}))$
169	166	simprd	$⊢ (φ \land R = M) \to (\frac{\frac{M^{2}}{2}}{2}) - H^{2} = 0$
170	12 20 16 169	4sqlem10	$⊢ (φ \land R = M) \to M^{2} ∥ (D^{2} - (\frac{\frac{M^{2}}{2}}{2}))$
171	125	adantr	$⊢ (φ \land R = M) \to C^{2} \in ℤ$
172	171 152	zsubcld	$⊢ (φ \land R = M) \to C^{2} - (\frac{\frac{M^{2}}{2}}{2}) \in ℤ$
173	127	adantr	$⊢ (φ \land R = M) \to D^{2} \in ℤ$
174	173 152	zsubcld	$⊢ (φ \land R = M) \to D^{2} - (\frac{\frac{M^{2}}{2}}{2}) \in ℤ$
175		dvds2add	$⊢ (M^{2} \in ℤ \land C^{2} - (\frac{\frac{M^{2}}{2}}{2}) \in ℤ \land D^{2} - (\frac{\frac{M^{2}}{2}}{2}) \in ℤ) \to ((M^{2} ∥ (C^{2} - (\frac{\frac{M^{2}}{2}}{2})) \land M^{2} ∥ (D^{2} - (\frac{\frac{M^{2}}{2}}{2}))) \to M^{2} ∥ ((C^{2} - (\frac{\frac{M^{2}}{2}}{2})) + D^{2} - (\frac{\frac{M^{2}}{2}}{2})))$
176	144 172 174 175	syl3anc	$⊢ (φ \land R = M) \to ((M^{2} ∥ (C^{2} - (\frac{\frac{M^{2}}{2}}{2})) \land M^{2} ∥ (D^{2} - (\frac{\frac{M^{2}}{2}}{2}))) \to M^{2} ∥ ((C^{2} - (\frac{\frac{M^{2}}{2}}{2})) + D^{2} - (\frac{\frac{M^{2}}{2}}{2})))$
177	168 170 176	mp2and	$⊢ (φ \land R = M) \to M^{2} ∥ ((C^{2} - (\frac{\frac{M^{2}}{2}}{2})) + D^{2} - (\frac{\frac{M^{2}}{2}}{2}))$
178	125	zcnd	$⊢ φ \to C^{2} \in ℂ$
179	127	zcnd	$⊢ φ \to D^{2} \in ℂ$
180	178 179 146 146	addsub4d	$⊢ φ \to C^{2} + D^{2} - ((\frac{\frac{M^{2}}{2}}{2}) + (\frac{\frac{M^{2}}{2}}{2})) = (C^{2} - (\frac{\frac{M^{2}}{2}}{2})) + D^{2} - (\frac{\frac{M^{2}}{2}}{2})$
181	51	oveq2d	$⊢ φ \to C^{2} + D^{2} - ((\frac{\frac{M^{2}}{2}}{2}) + (\frac{\frac{M^{2}}{2}}{2})) = C^{2} + D^{2} - (\frac{M^{2}}{2})$
182	180 181	eqtr3d	$⊢ φ \to (C^{2} - (\frac{\frac{M^{2}}{2}}{2})) + D^{2} - (\frac{\frac{M^{2}}{2}}{2}) = C^{2} + D^{2} - (\frac{M^{2}}{2})$
183	182	adantr	$⊢ (φ \land R = M) \to (C^{2} - (\frac{\frac{M^{2}}{2}}{2})) + D^{2} - (\frac{\frac{M^{2}}{2}}{2}) = C^{2} + D^{2} - (\frac{M^{2}}{2})$
184	177 183	breqtrd	$⊢ (φ \land R = M) \to M^{2} ∥ (C^{2} + D^{2} - (\frac{M^{2}}{2}))$
185	132	adantr	$⊢ (φ \land R = M) \to A^{2} + B^{2} \in ℤ$
186	51	adantr	$⊢ (φ \land R = M) \to (\frac{\frac{M^{2}}{2}}{2}) + (\frac{\frac{M^{2}}{2}}{2}) = \frac{M^{2}}{2}$
187	152 152	zaddcld	$⊢ (φ \land R = M) \to (\frac{\frac{M^{2}}{2}}{2}) + (\frac{\frac{M^{2}}{2}}{2}) \in ℤ$
188	186 187	eqeltrrd	$⊢ (φ \land R = M) \to \frac{M^{2}}{2} \in ℤ$
189	185 188	zsubcld	$⊢ (φ \land R = M) \to A^{2} + B^{2} - (\frac{M^{2}}{2}) \in ℤ$
190	133	adantr	$⊢ (φ \land R = M) \to C^{2} + D^{2} \in ℤ$
191	190 188	zsubcld	$⊢ (φ \land R = M) \to C^{2} + D^{2} - (\frac{M^{2}}{2}) \in ℤ$
192		dvds2add	$⊢ (M^{2} \in ℤ \land A^{2} + B^{2} - (\frac{M^{2}}{2}) \in ℤ \land C^{2} + D^{2} - (\frac{M^{2}}{2}) \in ℤ) \to ((M^{2} ∥ (A^{2} + B^{2} - (\frac{M^{2}}{2})) \land M^{2} ∥ (C^{2} + D^{2} - (\frac{M^{2}}{2}))) \to M^{2} ∥ ((A^{2} + B^{2} - (\frac{M^{2}}{2})) + (C^{2} + D^{2}) - (\frac{M^{2}}{2})))$
193	144 189 191 192	syl3anc	$⊢ (φ \land R = M) \to ((M^{2} ∥ (A^{2} + B^{2} - (\frac{M^{2}}{2})) \land M^{2} ∥ (C^{2} + D^{2} - (\frac{M^{2}}{2}))) \to M^{2} ∥ ((A^{2} + B^{2} - (\frac{M^{2}}{2})) + (C^{2} + D^{2}) - (\frac{M^{2}}{2})))$
194	165 184 193	mp2and	$⊢ (φ \land R = M) \to M^{2} ∥ ((A^{2} + B^{2} - (\frac{M^{2}}{2})) + (C^{2} + D^{2}) - (\frac{M^{2}}{2}))$
195	132	zcnd	$⊢ φ \to A^{2} + B^{2} \in ℂ$
196	133	zcnd	$⊢ φ \to C^{2} + D^{2} \in ℂ$
197	195 196 50 50	addsub4d	$⊢ φ \to (A^{2} + B^{2}) + (C^{2} + D^{2}) - ((\frac{M^{2}}{2}) + (\frac{M^{2}}{2})) = (A^{2} + B^{2} - (\frac{M^{2}}{2})) + (C^{2} + D^{2}) - (\frac{M^{2}}{2})$
198	59	oveq2d	$⊢ φ \to (A^{2} + B^{2}) + (C^{2} + D^{2}) - ((\frac{M^{2}}{2}) + (\frac{M^{2}}{2})) = (A^{2} + B^{2}) + (C^{2} + D^{2}) - M^{2}$
199	197 198	eqtr3d	$⊢ φ \to (A^{2} + B^{2} - (\frac{M^{2}}{2})) + (C^{2} + D^{2}) - (\frac{M^{2}}{2}) = (A^{2} + B^{2}) + (C^{2} + D^{2}) - M^{2}$
200	199	adantr	$⊢ (φ \land R = M) \to (A^{2} + B^{2} - (\frac{M^{2}}{2})) + (C^{2} + D^{2}) - (\frac{M^{2}}{2}) = (A^{2} + B^{2}) + (C^{2} + D^{2}) - M^{2}$
201	194 200	breqtrd	$⊢ (φ \land R = M) \to M^{2} ∥ ((A^{2} + B^{2}) + (C^{2} + D^{2}) - M^{2})$
202	132 133	zaddcld	$⊢ φ \to A^{2} + B^{2} + C^{2} + D^{2} \in ℤ$
203	202	adantr	$⊢ (φ \land R = M) \to A^{2} + B^{2} + C^{2} + D^{2} \in ℤ$
204		dvdssubr	$⊢ (M^{2} \in ℤ \land A^{2} + B^{2} + C^{2} + D^{2} \in ℤ) \to (M^{2} ∥ (A^{2} + B^{2} + C^{2} + D^{2}) \leftrightarrow M^{2} ∥ ((A^{2} + B^{2}) + (C^{2} + D^{2}) - M^{2}))$
205	144 203 204	syl2anc	$⊢ (φ \land R = M) \to (M^{2} ∥ (A^{2} + B^{2} + C^{2} + D^{2}) \leftrightarrow M^{2} ∥ ((A^{2} + B^{2}) + (C^{2} + D^{2}) - M^{2}))$
206	201 205	mpbird	$⊢ (φ \land R = M) \to M^{2} ∥ (A^{2} + B^{2} + C^{2} + D^{2})$
207	137 206	jaodan	$⊢ (φ \land (R = 0 \lor R = M)) \to M^{2} ∥ (A^{2} + B^{2} + C^{2} + D^{2})$
208	18	adantr	$⊢ (φ \land (R = 0 \lor R = M)) \to M P = A^{2} + B^{2} + C^{2} + D^{2}$
209	207 208	breqtrrd	$⊢ (φ \land (R = 0 \lor R = M)) \to M^{2} ∥ M P$
210	209	ex	$⊢ φ \to ((R = 0 \lor R = M) \to M^{2} ∥ M P)$
211	69 210	jca	$⊢ φ \to (R \leq M \land ((R = 0 \lor R = M) \to M^{2} ∥ M P))$

Metamath Proof Explorer

Theorem 4sqlem16

Proof