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

Metamath Proof Explorer

Theorem 4sqlem14

Proof