4sqlem17

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 = inf (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	4sqlem17	$⊢ \neg φ$

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 = inf (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	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18	4sqlem16	$⊢ φ \to (R \leq M \land ((R = 0 \lor R = M) \to M^{2} ∥ M P))$
20	19	simpld	$⊢ φ \to R \leq M$
21	6	ssrab3	$⊢ T \subseteq ℕ$
22		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
23	21 22	sseqtri	$⊢ T \subseteq ℤ_{\geq 1}$
24	1 2 3 4 5 6 7	4sqlem13	$⊢ φ \to (T \neq \emptyset \land M < P)$
25	24	simpld	$⊢ φ \to T \neq \emptyset$
26		infssuzcl	$⊢ (T \subseteq ℤ_{\geq 1} \land T \neq \emptyset) \to inf (T ℝ <) \in T$
27	23 25 26	sylancr	$⊢ φ \to inf (T ℝ <) \in T$
28	7 27	eqeltrid	$⊢ φ \to M \in T$
29	21 28	sselid	$⊢ φ \to M \in ℕ$
30	29	nnred	$⊢ φ \to M \in ℝ$
31	24	simprd	$⊢ φ \to M < P$
32	30 31	ltned	$⊢ φ \to M \neq P$
33	29	nncnd	$⊢ φ \to M \in ℂ$
34	33	sqvald	$⊢ φ \to M^{2} = M \cdot M$
35	34	breq1d	$⊢ φ \to (M^{2} ∥ M P \leftrightarrow M \cdot M ∥ M P)$
36	29	nnzd	$⊢ φ \to M \in ℤ$
37		prmz	$⊢ P \in ℙ \to P \in ℤ$
38	4 37	syl	$⊢ φ \to P \in ℤ$
39	29	nnne0d	$⊢ φ \to M \neq 0$
40		dvdscmulr	$⊢ (M \in ℤ \land P \in ℤ \land (M \in ℤ \land M \neq 0)) \to (M \cdot M ∥ M P \leftrightarrow M ∥ P)$
41	36 38 36 39 40	syl112anc	$⊢ φ \to (M \cdot M ∥ M P \leftrightarrow M ∥ P)$
42		dvdsprm	$⊢ (M \in ℤ_{\geq 2} \land P \in ℙ) \to (M ∥ P \leftrightarrow M = P)$
43	8 4 42	syl2anc	$⊢ φ \to (M ∥ P \leftrightarrow M = P)$
44	35 41 43	3bitrd	$⊢ φ \to (M^{2} ∥ M P \leftrightarrow M = P)$
45	44	necon3bbid	$⊢ φ \to (\neg M^{2} ∥ M P \leftrightarrow M \neq P)$
46	32 45	mpbird	$⊢ φ \to \neg M^{2} ∥ M P$
47	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18	4sqlem14	$⊢ φ \to R \in ℕ_{0}$
48		elnn0	$⊢ R \in ℕ_{0} \leftrightarrow (R \in ℕ \lor R = 0)$
49	47 48	sylib	$⊢ φ \to (R \in ℕ \lor R = 0)$
50	49	ord	$⊢ φ \to (\neg R \in ℕ \to R = 0)$
51		orc	$⊢ R = 0 \to (R = 0 \lor R = M)$
52	19	simprd	$⊢ φ \to ((R = 0 \lor R = M) \to M^{2} ∥ M P)$
53	51 52	syl5	$⊢ φ \to (R = 0 \to M^{2} ∥ M P)$
54	50 53	syld	$⊢ φ \to (\neg R \in ℕ \to M^{2} ∥ M P)$
55	46 54	mt3d	$⊢ φ \to R \in ℕ$
56		gzreim	$⊢ (A \in ℤ \land B \in ℤ) \to A + i B \in ℤ [i]$
57	9 10 56	syl2anc	$⊢ φ \to A + i B \in ℤ [i]$
58		gzcn	$⊢ A + i B \in ℤ [i] \to A + i B \in ℂ$
59	57 58	syl	$⊢ φ \to A + i B \in ℂ$
60	59	absvalsq2d	$⊢ φ \to {\|A + i B\|}^{2} = {ℜ (A + i B)}^{2} + {ℑ (A + i B)}^{2}$
61	9	zred	$⊢ φ \to A \in ℝ$
62	10	zred	$⊢ φ \to B \in ℝ$
63	61 62	crred	$⊢ φ \to ℜ (A + i B) = A$
64	63	oveq1d	$⊢ φ \to {ℜ (A + i B)}^{2} = A^{2}$
65	61 62	crimd	$⊢ φ \to ℑ (A + i B) = B$
66	65	oveq1d	$⊢ φ \to {ℑ (A + i B)}^{2} = B^{2}$
67	64 66	oveq12d	$⊢ φ \to {ℜ (A + i B)}^{2} + {ℑ (A + i B)}^{2} = A^{2} + B^{2}$
68	60 67	eqtrd	$⊢ φ \to {\|A + i B\|}^{2} = A^{2} + B^{2}$
69		gzreim	$⊢ (C \in ℤ \land D \in ℤ) \to C + i D \in ℤ [i]$
70	11 12 69	syl2anc	$⊢ φ \to C + i D \in ℤ [i]$
71		gzcn	$⊢ C + i D \in ℤ [i] \to C + i D \in ℂ$
72	70 71	syl	$⊢ φ \to C + i D \in ℂ$
73	72	absvalsq2d	$⊢ φ \to {\|C + i D\|}^{2} = {ℜ (C + i D)}^{2} + {ℑ (C + i D)}^{2}$
74	11	zred	$⊢ φ \to C \in ℝ$
75	12	zred	$⊢ φ \to D \in ℝ$
76	74 75	crred	$⊢ φ \to ℜ (C + i D) = C$
77	76	oveq1d	$⊢ φ \to {ℜ (C + i D)}^{2} = C^{2}$
78	74 75	crimd	$⊢ φ \to ℑ (C + i D) = D$
79	78	oveq1d	$⊢ φ \to {ℑ (C + i D)}^{2} = D^{2}$
80	77 79	oveq12d	$⊢ φ \to {ℜ (C + i D)}^{2} + {ℑ (C + i D)}^{2} = C^{2} + D^{2}$
81	73 80	eqtrd	$⊢ φ \to {\|C + i D\|}^{2} = C^{2} + D^{2}$
82	68 81	oveq12d	$⊢ φ \to {\|A + i B\|}^{2} + {\|C + i D\|}^{2} = A^{2} + B^{2} + C^{2} + D^{2}$
83	18 82	eqtr4d	$⊢ φ \to M P = {\|A + i B\|}^{2} + {\|C + i D\|}^{2}$
84	83	oveq1d	$⊢ φ \to \frac{M P}{M} = \frac{{\|A + i B\|}^{2} + {\|C + i D\|}^{2}}{M}$
85		prmnn	$⊢ P \in ℙ \to P \in ℕ$
86	4 85	syl	$⊢ φ \to P \in ℕ$
87	86	nncnd	$⊢ φ \to P \in ℂ$
88	87 33 39	divcan3d	$⊢ φ \to \frac{M P}{M} = P$
89	84 88	eqtr3d	$⊢ φ \to \frac{{\|A + i B\|}^{2} + {\|C + i D\|}^{2}}{M} = P$
90	9 29 13	4sqlem5	$⊢ φ \to (E \in ℤ \land \frac{A - E}{M} \in ℤ)$
91	90	simpld	$⊢ φ \to E \in ℤ$
92	10 29 14	4sqlem5	$⊢ φ \to (F \in ℤ \land \frac{B - F}{M} \in ℤ)$
93	92	simpld	$⊢ φ \to F \in ℤ$
94		gzreim	$⊢ (E \in ℤ \land F \in ℤ) \to E + i F \in ℤ [i]$
95	91 93 94	syl2anc	$⊢ φ \to E + i F \in ℤ [i]$
96		gzcn	$⊢ E + i F \in ℤ [i] \to E + i F \in ℂ$
97	95 96	syl	$⊢ φ \to E + i F \in ℂ$
98	97	absvalsq2d	$⊢ φ \to {\|E + i F\|}^{2} = {ℜ (E + i F)}^{2} + {ℑ (E + i F)}^{2}$
99	91	zred	$⊢ φ \to E \in ℝ$
100	93	zred	$⊢ φ \to F \in ℝ$
101	99 100	crred	$⊢ φ \to ℜ (E + i F) = E$
102	101	oveq1d	$⊢ φ \to {ℜ (E + i F)}^{2} = E^{2}$
103	99 100	crimd	$⊢ φ \to ℑ (E + i F) = F$
104	103	oveq1d	$⊢ φ \to {ℑ (E + i F)}^{2} = F^{2}$
105	102 104	oveq12d	$⊢ φ \to {ℜ (E + i F)}^{2} + {ℑ (E + i F)}^{2} = E^{2} + F^{2}$
106	98 105	eqtrd	$⊢ φ \to {\|E + i F\|}^{2} = E^{2} + F^{2}$
107	11 29 15	4sqlem5	$⊢ φ \to (G \in ℤ \land \frac{C - G}{M} \in ℤ)$
108	107	simpld	$⊢ φ \to G \in ℤ$
109	12 29 16	4sqlem5	$⊢ φ \to (H \in ℤ \land \frac{D - H}{M} \in ℤ)$
110	109	simpld	$⊢ φ \to H \in ℤ$
111		gzreim	$⊢ (G \in ℤ \land H \in ℤ) \to G + i H \in ℤ [i]$
112	108 110 111	syl2anc	$⊢ φ \to G + i H \in ℤ [i]$
113		gzcn	$⊢ G + i H \in ℤ [i] \to G + i H \in ℂ$
114	112 113	syl	$⊢ φ \to G + i H \in ℂ$
115	114	absvalsq2d	$⊢ φ \to {\|G + i H\|}^{2} = {ℜ (G + i H)}^{2} + {ℑ (G + i H)}^{2}$
116	108	zred	$⊢ φ \to G \in ℝ$
117	110	zred	$⊢ φ \to H \in ℝ$
118	116 117	crred	$⊢ φ \to ℜ (G + i H) = G$
119	118	oveq1d	$⊢ φ \to {ℜ (G + i H)}^{2} = G^{2}$
120	116 117	crimd	$⊢ φ \to ℑ (G + i H) = H$
121	120	oveq1d	$⊢ φ \to {ℑ (G + i H)}^{2} = H^{2}$
122	119 121	oveq12d	$⊢ φ \to {ℜ (G + i H)}^{2} + {ℑ (G + i H)}^{2} = G^{2} + H^{2}$
123	115 122	eqtrd	$⊢ φ \to {\|G + i H\|}^{2} = G^{2} + H^{2}$
124	106 123	oveq12d	$⊢ φ \to {\|E + i F\|}^{2} + {\|G + i H\|}^{2} = E^{2} + F^{2} + G^{2} + H^{2}$
125	124	oveq1d	$⊢ φ \to \frac{{\|E + i F\|}^{2} + {\|G + i H\|}^{2}}{M} = \frac{E^{2} + F^{2} + G^{2} + H^{2}}{M}$
126	125 17	eqtr4di	$⊢ φ \to \frac{{\|E + i F\|}^{2} + {\|G + i H\|}^{2}}{M} = R$
127	89 126	oveq12d	$⊢ φ \to (\frac{{\|A + i B\|}^{2} + {\|C + i D\|}^{2}}{M}) (\frac{{\|E + i F\|}^{2} + {\|G + i H\|}^{2}}{M}) = P R$
128	55	nncnd	$⊢ φ \to R \in ℂ$
129	87 128	mulcomd	$⊢ φ \to P R = R P$
130	127 129	eqtrd	$⊢ φ \to (\frac{{\|A + i B\|}^{2} + {\|C + i D\|}^{2}}{M}) (\frac{{\|E + i F\|}^{2} + {\|G + i H\|}^{2}}{M}) = R P$
131		eqid	$⊢ {\|A + i B\|}^{2} + {\|C + i D\|}^{2} = {\|A + i B\|}^{2} + {\|C + i D\|}^{2}$
132		eqid	$⊢ {\|E + i F\|}^{2} + {\|G + i H\|}^{2} = {\|E + i F\|}^{2} + {\|G + i H\|}^{2}$
133	9	zcnd	$⊢ φ \to A \in ℂ$
134		ax-icn	$⊢ i \in ℂ$
135	10	zcnd	$⊢ φ \to B \in ℂ$
136		mulcl	$⊢ (i \in ℂ \land B \in ℂ) \to i B \in ℂ$
137	134 135 136	sylancr	$⊢ φ \to i B \in ℂ$
138	91	zcnd	$⊢ φ \to E \in ℂ$
139	93	zcnd	$⊢ φ \to F \in ℂ$
140		mulcl	$⊢ (i \in ℂ \land F \in ℂ) \to i F \in ℂ$
141	134 139 140	sylancr	$⊢ φ \to i F \in ℂ$
142	133 137 138 141	addsub4d	$⊢ φ \to A + i B - (E + i F) = (A - E) + i B - i F$
143	134	a1i	$⊢ φ \to i \in ℂ$
144	143 135 139	subdid	$⊢ φ \to i (B - F) = i B - i F$
145	144	oveq2d	$⊢ φ \to A - E + i (B - F) = (A - E) + i B - i F$
146	142 145	eqtr4d	$⊢ φ \to A + i B - (E + i F) = A - E + i (B - F)$
147	146	oveq1d	$⊢ φ \to \frac{A + i B - (E + i F)}{M} = \frac{A - E + i (B - F)}{M}$
148	133 138	subcld	$⊢ φ \to A - E \in ℂ$
149	135 139	subcld	$⊢ φ \to B - F \in ℂ$
150		mulcl	$⊢ (i \in ℂ \land B - F \in ℂ) \to i (B - F) \in ℂ$
151	134 149 150	sylancr	$⊢ φ \to i (B - F) \in ℂ$
152	148 151 33 39	divdird	$⊢ φ \to \frac{A - E + i (B - F)}{M} = (\frac{A - E}{M}) + (\frac{i (B - F)}{M})$
153	143 149 33 39	divassd	$⊢ φ \to \frac{i (B - F)}{M} = i (\frac{B - F}{M})$
154	153	oveq2d	$⊢ φ \to (\frac{A - E}{M}) + (\frac{i (B - F)}{M}) = (\frac{A - E}{M}) + i (\frac{B - F}{M})$
155	147 152 154	3eqtrd	$⊢ φ \to \frac{A + i B - (E + i F)}{M} = (\frac{A - E}{M}) + i (\frac{B - F}{M})$
156	90	simprd	$⊢ φ \to \frac{A - E}{M} \in ℤ$
157	92	simprd	$⊢ φ \to \frac{B - F}{M} \in ℤ$
158		gzreim	$⊢ (\frac{A - E}{M} \in ℤ \land \frac{B - F}{M} \in ℤ) \to (\frac{A - E}{M}) + i (\frac{B - F}{M}) \in ℤ [i]$
159	156 157 158	syl2anc	$⊢ φ \to (\frac{A - E}{M}) + i (\frac{B - F}{M}) \in ℤ [i]$
160	155 159	eqeltrd	$⊢ φ \to \frac{A + i B - (E + i F)}{M} \in ℤ [i]$
161	11	zcnd	$⊢ φ \to C \in ℂ$
162	12	zcnd	$⊢ φ \to D \in ℂ$
163		mulcl	$⊢ (i \in ℂ \land D \in ℂ) \to i D \in ℂ$
164	134 162 163	sylancr	$⊢ φ \to i D \in ℂ$
165	108	zcnd	$⊢ φ \to G \in ℂ$
166	110	zcnd	$⊢ φ \to H \in ℂ$
167		mulcl	$⊢ (i \in ℂ \land H \in ℂ) \to i H \in ℂ$
168	134 166 167	sylancr	$⊢ φ \to i H \in ℂ$
169	161 164 165 168	addsub4d	$⊢ φ \to C + i D - (G + i H) = (C - G) + i D - i H$
170	143 162 166	subdid	$⊢ φ \to i (D - H) = i D - i H$
171	170	oveq2d	$⊢ φ \to C - G + i (D - H) = (C - G) + i D - i H$
172	169 171	eqtr4d	$⊢ φ \to C + i D - (G + i H) = C - G + i (D - H)$
173	172	oveq1d	$⊢ φ \to \frac{C + i D - (G + i H)}{M} = \frac{C - G + i (D - H)}{M}$
174	161 165	subcld	$⊢ φ \to C - G \in ℂ$
175	162 166	subcld	$⊢ φ \to D - H \in ℂ$
176		mulcl	$⊢ (i \in ℂ \land D - H \in ℂ) \to i (D - H) \in ℂ$
177	134 175 176	sylancr	$⊢ φ \to i (D - H) \in ℂ$
178	174 177 33 39	divdird	$⊢ φ \to \frac{C - G + i (D - H)}{M} = (\frac{C - G}{M}) + (\frac{i (D - H)}{M})$
179	143 175 33 39	divassd	$⊢ φ \to \frac{i (D - H)}{M} = i (\frac{D - H}{M})$
180	179	oveq2d	$⊢ φ \to (\frac{C - G}{M}) + (\frac{i (D - H)}{M}) = (\frac{C - G}{M}) + i (\frac{D - H}{M})$
181	173 178 180	3eqtrd	$⊢ φ \to \frac{C + i D - (G + i H)}{M} = (\frac{C - G}{M}) + i (\frac{D - H}{M})$
182	107	simprd	$⊢ φ \to \frac{C - G}{M} \in ℤ$
183	109	simprd	$⊢ φ \to \frac{D - H}{M} \in ℤ$
184		gzreim	$⊢ (\frac{C - G}{M} \in ℤ \land \frac{D - H}{M} \in ℤ) \to (\frac{C - G}{M}) + i (\frac{D - H}{M}) \in ℤ [i]$
185	182 183 184	syl2anc	$⊢ φ \to (\frac{C - G}{M}) + i (\frac{D - H}{M}) \in ℤ [i]$
186	181 185	eqeltrd	$⊢ φ \to \frac{C + i D - (G + i H)}{M} \in ℤ [i]$
187	86	nnnn0d	$⊢ φ \to P \in ℕ_{0}$
188	89 187	eqeltrd	$⊢ φ \to \frac{{\|A + i B\|}^{2} + {\|C + i D\|}^{2}}{M} \in ℕ_{0}$
189	1 57 70 95 112 131 132 29 160 186 188	mul4sqlem	$⊢ φ \to (\frac{{\|A + i B\|}^{2} + {\|C + i D\|}^{2}}{M}) (\frac{{\|E + i F\|}^{2} + {\|G + i H\|}^{2}}{M}) \in S$
190	130 189	eqeltrrd	$⊢ φ \to R P \in S$
191		oveq1	$⊢ i = R \to i P = R P$
192	191	eleq1d	$⊢ i = R \to (i P \in S \leftrightarrow R P \in S)$
193	192 6	elrab2	$⊢ R \in T \leftrightarrow (R \in ℕ \land R P \in S)$
194	55 190 193	sylanbrc	$⊢ φ \to R \in T$
195		infssuzle	$⊢ (T \subseteq ℤ_{\geq 1} \land R \in T) \to inf (T ℝ <) \leq R$
196	23 194 195	sylancr	$⊢ φ \to inf (T ℝ <) \leq R$
197	7 196	eqbrtrid	$⊢ φ \to M \leq R$
198	55	nnred	$⊢ φ \to R \in ℝ$
199	198 30	letri3d	$⊢ φ \to (R = M \leftrightarrow (R \leq M \land M \leq R))$
200	20 197 199	mpbir2and	$⊢ φ \to R = M$
201	200	olcd	$⊢ φ \to (R = 0 \lor R = M)$
202	201 52	mpd	$⊢ φ \to M^{2} ∥ M P$
203	202 46	pm2.65i	$⊢ \neg φ$

Metamath Proof Explorer

Theorem 4sqlem17

Proof