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	eqtr3id	$⊢ (φ \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	104	adantr	$⊢ (φ \land R = M) \to M^{2} \in ℤ$
139	132	adantr	$⊢ (φ \land R = M) \to A^{2} + B^{2} \in ℤ$
140	51	adantr	$⊢ (φ \land R = M) \to (\frac{\frac{M^{2}}{2}}{2}) + (\frac{\frac{M^{2}}{2}}{2}) = \frac{M^{2}}{2}$
141	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))$
142	141	simpld	$⊢ (φ \land R = M) \to ((\frac{\frac{M^{2}}{2}}{2}) - E^{2} = 0 \land (\frac{\frac{M^{2}}{2}}{2}) - F^{2} = 0)$
143	142	simpld	$⊢ (φ \land R = M) \to (\frac{\frac{M^{2}}{2}}{2}) - E^{2} = 0$
144	46	recnd	$⊢ φ \to \frac{\frac{M^{2}}{2}}{2} \in ℂ$
145	24	zcnd	$⊢ φ \to E^{2} \in ℂ$
146	144 145	subeq0ad	$⊢ φ \to ((\frac{\frac{M^{2}}{2}}{2}) - E^{2} = 0 \leftrightarrow \frac{\frac{M^{2}}{2}}{2} = E^{2})$
147	146	adantr	$⊢ (φ \land R = M) \to ((\frac{\frac{M^{2}}{2}}{2}) - E^{2} = 0 \leftrightarrow \frac{\frac{M^{2}}{2}}{2} = E^{2})$
148	143 147	mpbid	$⊢ (φ \land R = M) \to \frac{\frac{M^{2}}{2}}{2} = E^{2}$
149	24	adantr	$⊢ (φ \land R = M) \to E^{2} \in ℤ$
150	148 149	eqeltrd	$⊢ (φ \land R = M) \to \frac{\frac{M^{2}}{2}}{2} \in ℤ$
151	150 150	zaddcld	$⊢ (φ \land R = M) \to (\frac{\frac{M^{2}}{2}}{2}) + (\frac{\frac{M^{2}}{2}}{2}) \in ℤ$
152	140 151	eqeltrrd	$⊢ (φ \land R = M) \to \frac{M^{2}}{2} \in ℤ$
153	139 152	zsubcld	$⊢ (φ \land R = M) \to A^{2} + B^{2} - (\frac{M^{2}}{2}) \in ℤ$
154	133	adantr	$⊢ (φ \land R = M) \to C^{2} + D^{2} \in ℤ$
155	154 152	zsubcld	$⊢ (φ \land R = M) \to C^{2} + D^{2} - (\frac{M^{2}}{2}) \in ℤ$
156	106	adantr	$⊢ (φ \land R = M) \to A^{2} \in ℤ$
157	156 150	zsubcld	$⊢ (φ \land R = M) \to A^{2} - (\frac{\frac{M^{2}}{2}}{2}) \in ℤ$
158	108	adantr	$⊢ (φ \land R = M) \to B^{2} \in ℤ$
159	158 150	zsubcld	$⊢ (φ \land R = M) \to B^{2} - (\frac{\frac{M^{2}}{2}}{2}) \in ℤ$
160	9 20 13 143	4sqlem10	$⊢ (φ \land R = M) \to M^{2} ∥ (A^{2} - (\frac{\frac{M^{2}}{2}}{2}))$
161	142	simprd	$⊢ (φ \land R = M) \to (\frac{\frac{M^{2}}{2}}{2}) - F^{2} = 0$
162	10 20 14 161	4sqlem10	$⊢ (φ \land R = M) \to M^{2} ∥ (B^{2} - (\frac{\frac{M^{2}}{2}}{2}))$
163	138 157 159 160 162	dvds2addd	$⊢ (φ \land R = M) \to M^{2} ∥ ((A^{2} - (\frac{\frac{M^{2}}{2}}{2})) + B^{2} - (\frac{\frac{M^{2}}{2}}{2}))$
164	106	zcnd	$⊢ φ \to A^{2} \in ℂ$
165	108	zcnd	$⊢ φ \to B^{2} \in ℂ$
166	164 165 144 144	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})$
167	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})$
168	166 167	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})$
169	168	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})$
170	163 169	breqtrd	$⊢ (φ \land R = M) \to M^{2} ∥ (A^{2} + B^{2} - (\frac{M^{2}}{2}))$
171	125	adantr	$⊢ (φ \land R = M) \to C^{2} \in ℤ$
172	171 150	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 150	zsubcld	$⊢ (φ \land R = M) \to D^{2} - (\frac{\frac{M^{2}}{2}}{2}) \in ℤ$
175	141	simprd	$⊢ (φ \land R = M) \to ((\frac{\frac{M^{2}}{2}}{2}) - G^{2} = 0 \land (\frac{\frac{M^{2}}{2}}{2}) - H^{2} = 0)$
176	175	simpld	$⊢ (φ \land R = M) \to (\frac{\frac{M^{2}}{2}}{2}) - G^{2} = 0$
177	11 20 15 176	4sqlem10	$⊢ (φ \land R = M) \to M^{2} ∥ (C^{2} - (\frac{\frac{M^{2}}{2}}{2}))$
178	175	simprd	$⊢ (φ \land R = M) \to (\frac{\frac{M^{2}}{2}}{2}) - H^{2} = 0$
179	12 20 16 178	4sqlem10	$⊢ (φ \land R = M) \to M^{2} ∥ (D^{2} - (\frac{\frac{M^{2}}{2}}{2}))$
180	138 172 174 177 179	dvds2addd	$⊢ (φ \land R = M) \to M^{2} ∥ ((C^{2} - (\frac{\frac{M^{2}}{2}}{2})) + D^{2} - (\frac{\frac{M^{2}}{2}}{2}))$
181	125	zcnd	$⊢ φ \to C^{2} \in ℂ$
182	127	zcnd	$⊢ φ \to D^{2} \in ℂ$
183	181 182 144 144	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})$
184	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})$
185	183 184	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})$
186	185	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})$
187	180 186	breqtrd	$⊢ (φ \land R = M) \to M^{2} ∥ (C^{2} + D^{2} - (\frac{M^{2}}{2}))$
188	138 153 155 170 187	dvds2addd	$⊢ (φ \land R = M) \to M^{2} ∥ ((A^{2} + B^{2} - (\frac{M^{2}}{2})) + (C^{2} + D^{2}) - (\frac{M^{2}}{2}))$
189	132	zcnd	$⊢ φ \to A^{2} + B^{2} \in ℂ$
190	133	zcnd	$⊢ φ \to C^{2} + D^{2} \in ℂ$
191	189 190 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})$
192	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}$
193	191 192	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}$
194	193	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}$
195	188 194	breqtrd	$⊢ (φ \land R = M) \to M^{2} ∥ ((A^{2} + B^{2}) + (C^{2} + D^{2}) - M^{2})$
196	132 133	zaddcld	$⊢ φ \to A^{2} + B^{2} + C^{2} + D^{2} \in ℤ$
197	196	adantr	$⊢ (φ \land R = M) \to A^{2} + B^{2} + C^{2} + D^{2} \in ℤ$
198		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}))$
199	138 197 198	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}))$
200	195 199	mpbird	$⊢ (φ \land R = M) \to M^{2} ∥ (A^{2} + B^{2} + C^{2} + D^{2})$
201	137 200	jaodan	$⊢ (φ \land (R = 0 \lor R = M)) \to M^{2} ∥ (A^{2} + B^{2} + C^{2} + D^{2})$
202	18	adantr	$⊢ (φ \land (R = 0 \lor R = M)) \to M P = A^{2} + B^{2} + C^{2} + D^{2}$
203	201 202	breqtrrd	$⊢ (φ \land (R = 0 \lor R = M)) \to M^{2} ∥ M P$
204	203	ex	$⊢ φ \to ((R = 0 \lor R = M) \to M^{2} ∥ M P)$
205	69 204	jca	$⊢ φ \to (R \leq M \land ((R = 0 \lor R = M) \to M^{2} ∥ M P))$

Metamath Proof Explorer

Theorem 4sqlem16

Proof