4sqlem14

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	4sqlem14	$⊢ φ \to R \in ℕ_{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	6	ssrab3	$⊢ T \subseteq ℕ$
20		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
21	19 20	sseqtri	$⊢ T \subseteq ℤ_{\geq 1}$
22	1 2 3 4 5 6 7	4sqlem13	$⊢ φ \to (T \neq \emptyset \land M < P)$
23	22	simpld	$⊢ φ \to T \neq \emptyset$
24		infssuzcl	$⊢ (T \subseteq ℤ_{\geq 1} \land T \neq \emptyset) \to sup (T ℝ <) \in T$
25	21 23 24	sylancr	$⊢ φ \to sup (T ℝ <) \in T$
26	7 25	eqeltrid	$⊢ φ \to M \in T$
27	19 26	sseldi	$⊢ φ \to M \in ℕ$
28	27	nnzd	$⊢ φ \to M \in ℤ$
29		prmz	$⊢ P \in ℙ \to P \in ℤ$
30	4 29	syl	$⊢ φ \to P \in ℤ$
31		dvdsmul1	$⊢ (M \in ℤ \land P \in ℤ) \to M ∥ M P$
32	28 30 31	syl2anc	$⊢ φ \to M ∥ M P$
33	9 27 13	4sqlem8	$⊢ φ \to M ∥ (A^{2} - E^{2})$
34	10 27 14	4sqlem8	$⊢ φ \to M ∥ (B^{2} - F^{2})$
35		zsqcl	$⊢ A \in ℤ \to A^{2} \in ℤ$
36	9 35	syl	$⊢ φ \to A^{2} \in ℤ$
37	9 27 13	4sqlem5	$⊢ φ \to (E \in ℤ \land \frac{A - E}{M} \in ℤ)$
38	37	simpld	$⊢ φ \to E \in ℤ$
39		zsqcl2	$⊢ E \in ℤ \to E^{2} \in ℕ_{0}$
40	38 39	syl	$⊢ φ \to E^{2} \in ℕ_{0}$
41	40	nn0zd	$⊢ φ \to E^{2} \in ℤ$
42	36 41	zsubcld	$⊢ φ \to A^{2} - E^{2} \in ℤ$
43		zsqcl	$⊢ B \in ℤ \to B^{2} \in ℤ$
44	10 43	syl	$⊢ φ \to B^{2} \in ℤ$
45	10 27 14	4sqlem5	$⊢ φ \to (F \in ℤ \land \frac{B - F}{M} \in ℤ)$
46	45	simpld	$⊢ φ \to F \in ℤ$
47		zsqcl2	$⊢ F \in ℤ \to F^{2} \in ℕ_{0}$
48	46 47	syl	$⊢ φ \to F^{2} \in ℕ_{0}$
49	48	nn0zd	$⊢ φ \to F^{2} \in ℤ$
50	44 49	zsubcld	$⊢ φ \to B^{2} - F^{2} \in ℤ$
51		dvds2add	$⊢ (M \in ℤ \land A^{2} - E^{2} \in ℤ \land B^{2} - F^{2} \in ℤ) \to ((M ∥ (A^{2} - E^{2}) \land M ∥ (B^{2} - F^{2})) \to M ∥ ((A^{2} - E^{2}) + B^{2} - F^{2}))$
52	28 42 50 51	syl3anc	$⊢ φ \to ((M ∥ (A^{2} - E^{2}) \land M ∥ (B^{2} - F^{2})) \to M ∥ ((A^{2} - E^{2}) + B^{2} - F^{2}))$
53	33 34 52	mp2and	$⊢ φ \to M ∥ ((A^{2} - E^{2}) + B^{2} - F^{2})$
54	9	zcnd	$⊢ φ \to A \in ℂ$
55	54	sqcld	$⊢ φ \to A^{2} \in ℂ$
56	10	zcnd	$⊢ φ \to B \in ℂ$
57	56	sqcld	$⊢ φ \to B^{2} \in ℂ$
58	38	zcnd	$⊢ φ \to E \in ℂ$
59	58	sqcld	$⊢ φ \to E^{2} \in ℂ$
60	46	zcnd	$⊢ φ \to F \in ℂ$
61	60	sqcld	$⊢ φ \to F^{2} \in ℂ$
62	55 57 59 61	addsub4d	$⊢ φ \to A^{2} + B^{2} - (E^{2} + F^{2}) = (A^{2} - E^{2}) + B^{2} - F^{2}$
63	53 62	breqtrrd	$⊢ φ \to M ∥ (A^{2} + B^{2} - (E^{2} + F^{2}))$
64	11 27 15	4sqlem8	$⊢ φ \to M ∥ (C^{2} - G^{2})$
65	12 27 16	4sqlem8	$⊢ φ \to M ∥ (D^{2} - H^{2})$
66		zsqcl	$⊢ C \in ℤ \to C^{2} \in ℤ$
67	11 66	syl	$⊢ φ \to C^{2} \in ℤ$
68	11 27 15	4sqlem5	$⊢ φ \to (G \in ℤ \land \frac{C - G}{M} \in ℤ)$
69	68	simpld	$⊢ φ \to G \in ℤ$
70		zsqcl2	$⊢ G \in ℤ \to G^{2} \in ℕ_{0}$
71	69 70	syl	$⊢ φ \to G^{2} \in ℕ_{0}$
72	71	nn0zd	$⊢ φ \to G^{2} \in ℤ$
73	67 72	zsubcld	$⊢ φ \to C^{2} - G^{2} \in ℤ$
74		zsqcl	$⊢ D \in ℤ \to D^{2} \in ℤ$
75	12 74	syl	$⊢ φ \to D^{2} \in ℤ$
76	12 27 16	4sqlem5	$⊢ φ \to (H \in ℤ \land \frac{D - H}{M} \in ℤ)$
77	76	simpld	$⊢ φ \to H \in ℤ$
78		zsqcl2	$⊢ H \in ℤ \to H^{2} \in ℕ_{0}$
79	77 78	syl	$⊢ φ \to H^{2} \in ℕ_{0}$
80	79	nn0zd	$⊢ φ \to H^{2} \in ℤ$
81	75 80	zsubcld	$⊢ φ \to D^{2} - H^{2} \in ℤ$
82		dvds2add	$⊢ (M \in ℤ \land C^{2} - G^{2} \in ℤ \land D^{2} - H^{2} \in ℤ) \to ((M ∥ (C^{2} - G^{2}) \land M ∥ (D^{2} - H^{2})) \to M ∥ ((C^{2} - G^{2}) + D^{2} - H^{2}))$
83	28 73 81 82	syl3anc	$⊢ φ \to ((M ∥ (C^{2} - G^{2}) \land M ∥ (D^{2} - H^{2})) \to M ∥ ((C^{2} - G^{2}) + D^{2} - H^{2}))$
84	64 65 83	mp2and	$⊢ φ \to M ∥ ((C^{2} - G^{2}) + D^{2} - H^{2})$
85	11	zcnd	$⊢ φ \to C \in ℂ$
86	85	sqcld	$⊢ φ \to C^{2} \in ℂ$
87	12	zcnd	$⊢ φ \to D \in ℂ$
88	87	sqcld	$⊢ φ \to D^{2} \in ℂ$
89	69	zcnd	$⊢ φ \to G \in ℂ$
90	89	sqcld	$⊢ φ \to G^{2} \in ℂ$
91	77	zcnd	$⊢ φ \to H \in ℂ$
92	91	sqcld	$⊢ φ \to H^{2} \in ℂ$
93	86 88 90 92	addsub4d	$⊢ φ \to C^{2} + D^{2} - (G^{2} + H^{2}) = (C^{2} - G^{2}) + D^{2} - H^{2}$
94	84 93	breqtrrd	$⊢ φ \to M ∥ (C^{2} + D^{2} - (G^{2} + H^{2}))$
95	36 44	zaddcld	$⊢ φ \to A^{2} + B^{2} \in ℤ$
96	40 48	nn0addcld	$⊢ φ \to E^{2} + F^{2} \in ℕ_{0}$
97	96	nn0zd	$⊢ φ \to E^{2} + F^{2} \in ℤ$
98	95 97	zsubcld	$⊢ φ \to A^{2} + B^{2} - (E^{2} + F^{2}) \in ℤ$
99	67 75	zaddcld	$⊢ φ \to C^{2} + D^{2} \in ℤ$
100	71 79	nn0addcld	$⊢ φ \to G^{2} + H^{2} \in ℕ_{0}$
101	100	nn0zd	$⊢ φ \to G^{2} + H^{2} \in ℤ$
102	99 101	zsubcld	$⊢ φ \to C^{2} + D^{2} - (G^{2} + H^{2}) \in ℤ$
103		dvds2add	$⊢ (M \in ℤ \land A^{2} + B^{2} - (E^{2} + F^{2}) \in ℤ \land C^{2} + D^{2} - (G^{2} + H^{2}) \in ℤ) \to ((M ∥ (A^{2} + B^{2} - (E^{2} + F^{2})) \land M ∥ (C^{2} + D^{2} - (G^{2} + H^{2}))) \to M ∥ ((A^{2} + B^{2} - (E^{2} + F^{2})) + (C^{2} + D^{2}) - (G^{2} + H^{2})))$
104	28 98 102 103	syl3anc	$⊢ φ \to ((M ∥ (A^{2} + B^{2} - (E^{2} + F^{2})) \land M ∥ (C^{2} + D^{2} - (G^{2} + H^{2}))) \to M ∥ ((A^{2} + B^{2} - (E^{2} + F^{2})) + (C^{2} + D^{2}) - (G^{2} + H^{2})))$
105	63 94 104	mp2and	$⊢ φ \to M ∥ ((A^{2} + B^{2} - (E^{2} + F^{2})) + (C^{2} + D^{2}) - (G^{2} + H^{2}))$
106	18	oveq1d	$⊢ φ \to M P - (E^{2} + F^{2} + G^{2} + H^{2}) = (A^{2} + B^{2}) + (C^{2} + D^{2}) - (E^{2} + F^{2} + G^{2} + H^{2})$
107	55 57	addcld	$⊢ φ \to A^{2} + B^{2} \in ℂ$
108	86 88	addcld	$⊢ φ \to C^{2} + D^{2} \in ℂ$
109	59 61	addcld	$⊢ φ \to E^{2} + F^{2} \in ℂ$
110	90 92	addcld	$⊢ φ \to G^{2} + H^{2} \in ℂ$
111	107 108 109 110	addsub4d	$⊢ φ \to (A^{2} + B^{2}) + (C^{2} + D^{2}) - (E^{2} + F^{2} + G^{2} + H^{2}) = (A^{2} + B^{2} - (E^{2} + F^{2})) + (C^{2} + D^{2}) - (G^{2} + H^{2})$
112	106 111	eqtrd	$⊢ φ \to M P - (E^{2} + F^{2} + G^{2} + H^{2}) = (A^{2} + B^{2} - (E^{2} + F^{2})) + (C^{2} + D^{2}) - (G^{2} + H^{2})$
113	105 112	breqtrrd	$⊢ φ \to M ∥ (M P - (E^{2} + F^{2} + G^{2} + H^{2}))$
114	28 30	zmulcld	$⊢ φ \to M P \in ℤ$
115	97 101	zaddcld	$⊢ φ \to E^{2} + F^{2} + G^{2} + H^{2} \in ℤ$
116	114 115	zsubcld	$⊢ φ \to M P - (E^{2} + F^{2} + G^{2} + H^{2}) \in ℤ$
117	28 32 113 114 116	dvds2subd	$⊢ φ \to M ∥ (M P - (M P - (E^{2} + F^{2} + G^{2} + H^{2})))$
118	27	nncnd	$⊢ φ \to M \in ℂ$
119		prmnn	$⊢ P \in ℙ \to P \in ℕ$
120	4 119	syl	$⊢ φ \to P \in ℕ$
121	120	nncnd	$⊢ φ \to P \in ℂ$
122	118 121	mulcld	$⊢ φ \to M P \in ℂ$
123	109 110	addcld	$⊢ φ \to E^{2} + F^{2} + G^{2} + H^{2} \in ℂ$
124	122 123	nncand	$⊢ φ \to M P - (M P - (E^{2} + F^{2} + G^{2} + H^{2})) = E^{2} + F^{2} + G^{2} + H^{2}$
125	117 124	breqtrd	$⊢ φ \to M ∥ (E^{2} + F^{2} + G^{2} + H^{2})$
126	27	nnne0d	$⊢ φ \to M \neq 0$
127	96 100	nn0addcld	$⊢ φ \to E^{2} + F^{2} + G^{2} + H^{2} \in ℕ_{0}$
128	127	nn0zd	$⊢ φ \to E^{2} + F^{2} + G^{2} + H^{2} \in ℤ$
129		dvdsval2	$⊢ (M \in ℤ \land M \neq 0 \land E^{2} + F^{2} + G^{2} + H^{2} \in ℤ) \to (M ∥ (E^{2} + F^{2} + G^{2} + H^{2}) \leftrightarrow \frac{E^{2} + F^{2} + G^{2} + H^{2}}{M} \in ℤ)$
130	28 126 128 129	syl3anc	$⊢ φ \to (M ∥ (E^{2} + F^{2} + G^{2} + H^{2}) \leftrightarrow \frac{E^{2} + F^{2} + G^{2} + H^{2}}{M} \in ℤ)$
131	125 130	mpbid	$⊢ φ \to \frac{E^{2} + F^{2} + G^{2} + H^{2}}{M} \in ℤ$
132	127	nn0red	$⊢ φ \to E^{2} + F^{2} + G^{2} + H^{2} \in ℝ$
133	127	nn0ge0d	$⊢ φ \to 0 \leq E^{2} + F^{2} + G^{2} + H^{2}$
134	27	nnred	$⊢ φ \to M \in ℝ$
135	27	nngt0d	$⊢ φ \to 0 < M$
136		divge0	$⊢ ((E^{2} + F^{2} + G^{2} + H^{2} \in ℝ \land 0 \leq E^{2} + F^{2} + G^{2} + H^{2}) \land (M \in ℝ \land 0 < M)) \to 0 \leq \frac{E^{2} + F^{2} + G^{2} + H^{2}}{M}$
137	132 133 134 135 136	syl22anc	$⊢ φ \to 0 \leq \frac{E^{2} + F^{2} + G^{2} + H^{2}}{M}$
138		elnn0z	$⊢ \frac{E^{2} + F^{2} + G^{2} + H^{2}}{M} \in ℕ_{0} \leftrightarrow (\frac{E^{2} + F^{2} + G^{2} + H^{2}}{M} \in ℤ \land 0 \leq \frac{E^{2} + F^{2} + G^{2} + H^{2}}{M})$
139	131 137 138	sylanbrc	$⊢ φ \to \frac{E^{2} + F^{2} + G^{2} + H^{2}}{M} \in ℕ_{0}$
140	17 139	eqeltrid	$⊢ φ \to R \in ℕ_{0}$

Metamath Proof Explorer

Theorem 4sqlem14

Proof