2sqlem8

	Ref	Expression
Hypotheses	2sq.1	$⊢ S = ran (w \in ℤ [i] ⟼ {\|w\|}^{2})$
	2sqlem7.2	$⊢ Y = \{z \| \exists x \in ℤ \exists y \in ℤ (x \gcd y = 1 \land z = x^{2} + y^{2})\}$
	2sqlem9.5	$⊢ φ \to \forall b \in (1 \dots M - 1) \forall a \in Y (b ∥ a \to b \in S)$
	2sqlem9.7	$⊢ φ \to M ∥ N$
	2sqlem8.n	$⊢ φ \to N \in ℕ$
	2sqlem8.m	$⊢ φ \to M \in ℤ_{\geq 2}$
	2sqlem8.1	$⊢ φ \to A \in ℤ$
	2sqlem8.2	$⊢ φ \to B \in ℤ$
	2sqlem8.3	$⊢ φ \to A \gcd B = 1$
	2sqlem8.4	$⊢ φ \to N = A^{2} + B^{2}$
	2sqlem8.c	$⊢ C = ((A + (\frac{M}{2})) \mod M) - (\frac{M}{2})$
	2sqlem8.d	$⊢ D = ((B + (\frac{M}{2})) \mod M) - (\frac{M}{2})$
	2sqlem8.e	$⊢ E = \frac{C}{C \gcd D}$
	2sqlem8.f	$⊢ F = \frac{D}{C \gcd D}$
Assertion	2sqlem8	$⊢ φ \to M \in S$

Proof

Step	Hyp	Ref	Expression
1		2sq.1	$⊢ S = ran (w \in ℤ [i] ⟼ {\|w\|}^{2})$
2		2sqlem7.2	$⊢ Y = \{z \| \exists x \in ℤ \exists y \in ℤ (x \gcd y = 1 \land z = x^{2} + y^{2})\}$
3		2sqlem9.5	$⊢ φ \to \forall b \in (1 \dots M - 1) \forall a \in Y (b ∥ a \to b \in S)$
4		2sqlem9.7	$⊢ φ \to M ∥ N$
5		2sqlem8.n	$⊢ φ \to N \in ℕ$
6		2sqlem8.m	$⊢ φ \to M \in ℤ_{\geq 2}$
7		2sqlem8.1	$⊢ φ \to A \in ℤ$
8		2sqlem8.2	$⊢ φ \to B \in ℤ$
9		2sqlem8.3	$⊢ φ \to A \gcd B = 1$
10		2sqlem8.4	$⊢ φ \to N = A^{2} + B^{2}$
11		2sqlem8.c	$⊢ C = ((A + (\frac{M}{2})) \mod M) - (\frac{M}{2})$
12		2sqlem8.d	$⊢ D = ((B + (\frac{M}{2})) \mod M) - (\frac{M}{2})$
13		2sqlem8.e	$⊢ E = \frac{C}{C \gcd D}$
14		2sqlem8.f	$⊢ F = \frac{D}{C \gcd D}$
15		eluz2b3	$⊢ M \in ℤ_{\geq 2} \leftrightarrow (M \in ℕ \land M \neq 1)$
16	6 15	sylib	$⊢ φ \to (M \in ℕ \land M \neq 1)$
17	16	simpld	$⊢ φ \to M \in ℕ$
18		eluzelz	$⊢ M \in ℤ_{\geq 2} \to M \in ℤ$
19	6 18	syl	$⊢ φ \to M \in ℤ$
20	5	nnzd	$⊢ φ \to N \in ℤ$
21	7 17 11	4sqlem5	$⊢ φ \to (C \in ℤ \land \frac{A - C}{M} \in ℤ)$
22	21	simpld	$⊢ φ \to C \in ℤ$
23		zsqcl	$⊢ C \in ℤ \to C^{2} \in ℤ$
24	22 23	syl	$⊢ φ \to C^{2} \in ℤ$
25	8 17 12	4sqlem5	$⊢ φ \to (D \in ℤ \land \frac{B - D}{M} \in ℤ)$
26	25	simpld	$⊢ φ \to D \in ℤ$
27		zsqcl	$⊢ D \in ℤ \to D^{2} \in ℤ$
28	26 27	syl	$⊢ φ \to D^{2} \in ℤ$
29	24 28	zaddcld	$⊢ φ \to C^{2} + D^{2} \in ℤ$
30		zsqcl	$⊢ A \in ℤ \to A^{2} \in ℤ$
31	7 30	syl	$⊢ φ \to A^{2} \in ℤ$
32	31 24	zsubcld	$⊢ φ \to A^{2} - C^{2} \in ℤ$
33		zsqcl	$⊢ B \in ℤ \to B^{2} \in ℤ$
34	8 33	syl	$⊢ φ \to B^{2} \in ℤ$
35	34 28	zsubcld	$⊢ φ \to B^{2} - D^{2} \in ℤ$
36	7 17 11	4sqlem8	$⊢ φ \to M ∥ (A^{2} - C^{2})$
37	8 17 12	4sqlem8	$⊢ φ \to M ∥ (B^{2} - D^{2})$
38	19 32 35 36 37	dvds2addd	$⊢ φ \to M ∥ ((A^{2} - C^{2}) + B^{2} - D^{2})$
39	10	oveq1d	$⊢ φ \to N - (C^{2} + D^{2}) = A^{2} + B^{2} - (C^{2} + D^{2})$
40	31	zcnd	$⊢ φ \to A^{2} \in ℂ$
41	34	zcnd	$⊢ φ \to B^{2} \in ℂ$
42	24	zcnd	$⊢ φ \to C^{2} \in ℂ$
43	28	zcnd	$⊢ φ \to D^{2} \in ℂ$
44	40 41 42 43	addsub4d	$⊢ φ \to A^{2} + B^{2} - (C^{2} + D^{2}) = (A^{2} - C^{2}) + B^{2} - D^{2}$
45	39 44	eqtrd	$⊢ φ \to N - (C^{2} + D^{2}) = (A^{2} - C^{2}) + B^{2} - D^{2}$
46	38 45	breqtrrd	$⊢ φ \to M ∥ (N - (C^{2} + D^{2}))$
47		dvdssub2	$⊢ ((M \in ℤ \land N \in ℤ \land C^{2} + D^{2} \in ℤ) \land M ∥ (N - (C^{2} + D^{2}))) \to (M ∥ N \leftrightarrow M ∥ (C^{2} + D^{2}))$
48	19 20 29 46 47	syl31anc	$⊢ φ \to (M ∥ N \leftrightarrow M ∥ (C^{2} + D^{2}))$
49	4 48	mpbid	$⊢ φ \to M ∥ (C^{2} + D^{2})$
50	1 2 3 4 5 6 7 8 9 10 11 12	2sqlem8a	$⊢ φ \to C \gcd D \in ℕ$
51	50	nnzd	$⊢ φ \to C \gcd D \in ℤ$
52		zsqcl2	$⊢ C \gcd D \in ℤ \to {(C \gcd D)}^{2} \in ℕ_{0}$
53	51 52	syl	$⊢ φ \to {(C \gcd D)}^{2} \in ℕ_{0}$
54	53	nn0cnd	$⊢ φ \to {(C \gcd D)}^{2} \in ℂ$
55		gcddvds	$⊢ (C \in ℤ \land D \in ℤ) \to ((C \gcd D) ∥ C \land (C \gcd D) ∥ D)$
56	22 26 55	syl2anc	$⊢ φ \to ((C \gcd D) ∥ C \land (C \gcd D) ∥ D)$
57	56	simpld	$⊢ φ \to (C \gcd D) ∥ C$
58	50	nnne0d	$⊢ φ \to C \gcd D \neq 0$
59		dvdsval2	$⊢ (C \gcd D \in ℤ \land C \gcd D \neq 0 \land C \in ℤ) \to ((C \gcd D) ∥ C \leftrightarrow \frac{C}{C \gcd D} \in ℤ)$
60	51 58 22 59	syl3anc	$⊢ φ \to ((C \gcd D) ∥ C \leftrightarrow \frac{C}{C \gcd D} \in ℤ)$
61	57 60	mpbid	$⊢ φ \to \frac{C}{C \gcd D} \in ℤ$
62	13 61	eqeltrid	$⊢ φ \to E \in ℤ$
63		zsqcl2	$⊢ E \in ℤ \to E^{2} \in ℕ_{0}$
64	62 63	syl	$⊢ φ \to E^{2} \in ℕ_{0}$
65	64	nn0cnd	$⊢ φ \to E^{2} \in ℂ$
66	56	simprd	$⊢ φ \to (C \gcd D) ∥ D$
67		dvdsval2	$⊢ (C \gcd D \in ℤ \land C \gcd D \neq 0 \land D \in ℤ) \to ((C \gcd D) ∥ D \leftrightarrow \frac{D}{C \gcd D} \in ℤ)$
68	51 58 26 67	syl3anc	$⊢ φ \to ((C \gcd D) ∥ D \leftrightarrow \frac{D}{C \gcd D} \in ℤ)$
69	66 68	mpbid	$⊢ φ \to \frac{D}{C \gcd D} \in ℤ$
70	14 69	eqeltrid	$⊢ φ \to F \in ℤ$
71		zsqcl2	$⊢ F \in ℤ \to F^{2} \in ℕ_{0}$
72	70 71	syl	$⊢ φ \to F^{2} \in ℕ_{0}$
73	72	nn0cnd	$⊢ φ \to F^{2} \in ℂ$
74	54 65 73	adddid	$⊢ φ \to {(C \gcd D)}^{2} (E^{2} + F^{2}) = {(C \gcd D)}^{2} E^{2} + {(C \gcd D)}^{2} F^{2}$
75	51	zcnd	$⊢ φ \to C \gcd D \in ℂ$
76	62	zcnd	$⊢ φ \to E \in ℂ$
77	75 76	sqmuld	$⊢ φ \to {(C \gcd D) E}^{2} = {(C \gcd D)}^{2} E^{2}$
78	13	oveq2i	$⊢ (C \gcd D) E = (C \gcd D) (\frac{C}{C \gcd D})$
79	22	zcnd	$⊢ φ \to C \in ℂ$
80	79 75 58	divcan2d	$⊢ φ \to (C \gcd D) (\frac{C}{C \gcd D}) = C$
81	78 80	eqtrid	$⊢ φ \to (C \gcd D) E = C$
82	81	oveq1d	$⊢ φ \to {(C \gcd D) E}^{2} = C^{2}$
83	77 82	eqtr3d	$⊢ φ \to {(C \gcd D)}^{2} E^{2} = C^{2}$
84	70	zcnd	$⊢ φ \to F \in ℂ$
85	75 84	sqmuld	$⊢ φ \to {(C \gcd D) F}^{2} = {(C \gcd D)}^{2} F^{2}$
86	14	oveq2i	$⊢ (C \gcd D) F = (C \gcd D) (\frac{D}{C \gcd D})$
87	26	zcnd	$⊢ φ \to D \in ℂ$
88	87 75 58	divcan2d	$⊢ φ \to (C \gcd D) (\frac{D}{C \gcd D}) = D$
89	86 88	eqtrid	$⊢ φ \to (C \gcd D) F = D$
90	89	oveq1d	$⊢ φ \to {(C \gcd D) F}^{2} = D^{2}$
91	85 90	eqtr3d	$⊢ φ \to {(C \gcd D)}^{2} F^{2} = D^{2}$
92	83 91	oveq12d	$⊢ φ \to {(C \gcd D)}^{2} E^{2} + {(C \gcd D)}^{2} F^{2} = C^{2} + D^{2}$
93	74 92	eqtrd	$⊢ φ \to {(C \gcd D)}^{2} (E^{2} + F^{2}) = C^{2} + D^{2}$
94	49 93	breqtrrd	$⊢ φ \to M ∥ {(C \gcd D)}^{2} (E^{2} + F^{2})$
95		zsqcl	$⊢ C \gcd D \in ℤ \to {(C \gcd D)}^{2} \in ℤ$
96	51 95	syl	$⊢ φ \to {(C \gcd D)}^{2} \in ℤ$
97	19 96	gcdcomd	$⊢ φ \to M \gcd {(C \gcd D)}^{2} = {(C \gcd D)}^{2} \gcd M$
98	51 19	gcdcld	$⊢ φ \to (C \gcd D) \gcd M \in ℕ_{0}$
99	98	nn0zd	$⊢ φ \to (C \gcd D) \gcd M \in ℤ$
100		gcddvds	$⊢ (C \gcd D \in ℤ \land M \in ℤ) \to (((C \gcd D) \gcd M) ∥ (C \gcd D) \land ((C \gcd D) \gcd M) ∥ M)$
101	51 19 100	syl2anc	$⊢ φ \to (((C \gcd D) \gcd M) ∥ (C \gcd D) \land ((C \gcd D) \gcd M) ∥ M)$
102	101	simpld	$⊢ φ \to ((C \gcd D) \gcd M) ∥ (C \gcd D)$
103	99 51 22 102 57	dvdstrd	$⊢ φ \to ((C \gcd D) \gcd M) ∥ C$
104	7 22	zsubcld	$⊢ φ \to A - C \in ℤ$
105	101	simprd	$⊢ φ \to ((C \gcd D) \gcd M) ∥ M$
106	21	simprd	$⊢ φ \to \frac{A - C}{M} \in ℤ$
107	17	nnne0d	$⊢ φ \to M \neq 0$
108		dvdsval2	$⊢ (M \in ℤ \land M \neq 0 \land A - C \in ℤ) \to (M ∥ (A - C) \leftrightarrow \frac{A - C}{M} \in ℤ)$
109	19 107 104 108	syl3anc	$⊢ φ \to (M ∥ (A - C) \leftrightarrow \frac{A - C}{M} \in ℤ)$
110	106 109	mpbird	$⊢ φ \to M ∥ (A - C)$
111	99 19 104 105 110	dvdstrd	$⊢ φ \to ((C \gcd D) \gcd M) ∥ (A - C)$
112		dvdssub2	$⊢ (((C \gcd D) \gcd M \in ℤ \land A \in ℤ \land C \in ℤ) \land ((C \gcd D) \gcd M) ∥ (A - C)) \to (((C \gcd D) \gcd M) ∥ A \leftrightarrow ((C \gcd D) \gcd M) ∥ C)$
113	99 7 22 111 112	syl31anc	$⊢ φ \to (((C \gcd D) \gcd M) ∥ A \leftrightarrow ((C \gcd D) \gcd M) ∥ C)$
114	103 113	mpbird	$⊢ φ \to ((C \gcd D) \gcd M) ∥ A$
115	99 51 26 102 66	dvdstrd	$⊢ φ \to ((C \gcd D) \gcd M) ∥ D$
116	8 26	zsubcld	$⊢ φ \to B - D \in ℤ$
117	25	simprd	$⊢ φ \to \frac{B - D}{M} \in ℤ$
118		dvdsval2	$⊢ (M \in ℤ \land M \neq 0 \land B - D \in ℤ) \to (M ∥ (B - D) \leftrightarrow \frac{B - D}{M} \in ℤ)$
119	19 107 116 118	syl3anc	$⊢ φ \to (M ∥ (B - D) \leftrightarrow \frac{B - D}{M} \in ℤ)$
120	117 119	mpbird	$⊢ φ \to M ∥ (B - D)$
121	99 19 116 105 120	dvdstrd	$⊢ φ \to ((C \gcd D) \gcd M) ∥ (B - D)$
122		dvdssub2	$⊢ (((C \gcd D) \gcd M \in ℤ \land B \in ℤ \land D \in ℤ) \land ((C \gcd D) \gcd M) ∥ (B - D)) \to (((C \gcd D) \gcd M) ∥ B \leftrightarrow ((C \gcd D) \gcd M) ∥ D)$
123	99 8 26 121 122	syl31anc	$⊢ φ \to (((C \gcd D) \gcd M) ∥ B \leftrightarrow ((C \gcd D) \gcd M) ∥ D)$
124	115 123	mpbird	$⊢ φ \to ((C \gcd D) \gcd M) ∥ B$
125		ax-1ne0	$⊢ 1 \neq 0$
126	125	a1i	$⊢ φ \to 1 \neq 0$
127	9 126	eqnetrd	$⊢ φ \to A \gcd B \neq 0$
128	127	neneqd	$⊢ φ \to \neg A \gcd B = 0$
129		gcdeq0	$⊢ (A \in ℤ \land B \in ℤ) \to (A \gcd B = 0 \leftrightarrow (A = 0 \land B = 0))$
130	7 8 129	syl2anc	$⊢ φ \to (A \gcd B = 0 \leftrightarrow (A = 0 \land B = 0))$
131	128 130	mtbid	$⊢ φ \to \neg (A = 0 \land B = 0)$
132		dvdslegcd	$⊢ (((C \gcd D) \gcd M \in ℤ \land A \in ℤ \land B \in ℤ) \land \neg (A = 0 \land B = 0)) \to ((((C \gcd D) \gcd M) ∥ A \land ((C \gcd D) \gcd M) ∥ B) \to (C \gcd D) \gcd M \leq A \gcd B)$
133	99 7 8 131 132	syl31anc	$⊢ φ \to ((((C \gcd D) \gcd M) ∥ A \land ((C \gcd D) \gcd M) ∥ B) \to (C \gcd D) \gcd M \leq A \gcd B)$
134	114 124 133	mp2and	$⊢ φ \to (C \gcd D) \gcd M \leq A \gcd B$
135	134 9	breqtrd	$⊢ φ \to (C \gcd D) \gcd M \leq 1$
136		simpr	$⊢ (C \gcd D = 0 \land M = 0) \to M = 0$
137	136	necon3ai	$⊢ M \neq 0 \to \neg (C \gcd D = 0 \land M = 0)$
138	107 137	syl	$⊢ φ \to \neg (C \gcd D = 0 \land M = 0)$
139		gcdn0cl	$⊢ ((C \gcd D \in ℤ \land M \in ℤ) \land \neg (C \gcd D = 0 \land M = 0)) \to (C \gcd D) \gcd M \in ℕ$
140	51 19 138 139	syl21anc	$⊢ φ \to (C \gcd D) \gcd M \in ℕ$
141		nnle1eq1	$⊢ (C \gcd D) \gcd M \in ℕ \to ((C \gcd D) \gcd M \leq 1 \leftrightarrow (C \gcd D) \gcd M = 1)$
142	140 141	syl	$⊢ φ \to ((C \gcd D) \gcd M \leq 1 \leftrightarrow (C \gcd D) \gcd M = 1)$
143	135 142	mpbid	$⊢ φ \to (C \gcd D) \gcd M = 1$
144		2nn	$⊢ 2 \in ℕ$
145	144	a1i	$⊢ φ \to 2 \in ℕ$
146		rplpwr	$⊢ (C \gcd D \in ℕ \land M \in ℕ \land 2 \in ℕ) \to ((C \gcd D) \gcd M = 1 \to {(C \gcd D)}^{2} \gcd M = 1)$
147	50 17 145 146	syl3anc	$⊢ φ \to ((C \gcd D) \gcd M = 1 \to {(C \gcd D)}^{2} \gcd M = 1)$
148	143 147	mpd	$⊢ φ \to {(C \gcd D)}^{2} \gcd M = 1$
149	97 148	eqtrd	$⊢ φ \to M \gcd {(C \gcd D)}^{2} = 1$
150	64 72	nn0addcld	$⊢ φ \to E^{2} + F^{2} \in ℕ_{0}$
151	150	nn0zd	$⊢ φ \to E^{2} + F^{2} \in ℤ$
152		coprmdvds	$⊢ (M \in ℤ \land {(C \gcd D)}^{2} \in ℤ \land E^{2} + F^{2} \in ℤ) \to ((M ∥ {(C \gcd D)}^{2} (E^{2} + F^{2}) \land M \gcd {(C \gcd D)}^{2} = 1) \to M ∥ (E^{2} + F^{2}))$
153	19 96 151 152	syl3anc	$⊢ φ \to ((M ∥ {(C \gcd D)}^{2} (E^{2} + F^{2}) \land M \gcd {(C \gcd D)}^{2} = 1) \to M ∥ (E^{2} + F^{2}))$
154	94 149 153	mp2and	$⊢ φ \to M ∥ (E^{2} + F^{2})$
155		dvdsval2	$⊢ (M \in ℤ \land M \neq 0 \land E^{2} + F^{2} \in ℤ) \to (M ∥ (E^{2} + F^{2}) \leftrightarrow \frac{E^{2} + F^{2}}{M} \in ℤ)$
156	19 107 151 155	syl3anc	$⊢ φ \to (M ∥ (E^{2} + F^{2}) \leftrightarrow \frac{E^{2} + F^{2}}{M} \in ℤ)$
157	154 156	mpbid	$⊢ φ \to \frac{E^{2} + F^{2}}{M} \in ℤ$
158	64	nn0red	$⊢ φ \to E^{2} \in ℝ$
159	72	nn0red	$⊢ φ \to F^{2} \in ℝ$
160	158 159	readdcld	$⊢ φ \to E^{2} + F^{2} \in ℝ$
161	17	nnred	$⊢ φ \to M \in ℝ$
162	1 2	2sqlem7	$⊢ Y \subseteq S \cap ℕ$
163		inss2	$⊢ S \cap ℕ \subseteq ℕ$
164	162 163	sstri	$⊢ Y \subseteq ℕ$
165	62 70	gcdcld	$⊢ φ \to E \gcd F \in ℕ_{0}$
166	165	nn0cnd	$⊢ φ \to E \gcd F \in ℂ$
167		1cnd	$⊢ φ \to 1 \in ℂ$
168	75	mulridd	$⊢ φ \to (C \gcd D) \cdot 1 = C \gcd D$
169	81 89	oveq12d	$⊢ φ \to (C \gcd D) E \gcd (C \gcd D) F = C \gcd D$
170	22 26	gcdcld	$⊢ φ \to C \gcd D \in ℕ_{0}$
171		mulgcd	$⊢ (C \gcd D \in ℕ_{0} \land E \in ℤ \land F \in ℤ) \to (C \gcd D) E \gcd (C \gcd D) F = (C \gcd D) (E \gcd F)$
172	170 62 70 171	syl3anc	$⊢ φ \to (C \gcd D) E \gcd (C \gcd D) F = (C \gcd D) (E \gcd F)$
173	168 169 172	3eqtr2rd	$⊢ φ \to (C \gcd D) (E \gcd F) = (C \gcd D) \cdot 1$
174	166 167 75 58 173	mulcanad	$⊢ φ \to E \gcd F = 1$
175		eqidd	$⊢ φ \to E^{2} + F^{2} = E^{2} + F^{2}$
176		oveq1	$⊢ x = E \to x \gcd y = E \gcd y$
177	176	eqeq1d	$⊢ x = E \to (x \gcd y = 1 \leftrightarrow E \gcd y = 1)$
178		oveq1	$⊢ x = E \to x^{2} = E^{2}$
179	178	oveq1d	$⊢ x = E \to x^{2} + y^{2} = E^{2} + y^{2}$
180	179	eqeq2d	$⊢ x = E \to (E^{2} + F^{2} = x^{2} + y^{2} \leftrightarrow E^{2} + F^{2} = E^{2} + y^{2})$
181	177 180	anbi12d	$⊢ x = E \to ((x \gcd y = 1 \land E^{2} + F^{2} = x^{2} + y^{2}) \leftrightarrow (E \gcd y = 1 \land E^{2} + F^{2} = E^{2} + y^{2}))$
182		oveq2	$⊢ y = F \to E \gcd y = E \gcd F$
183	182	eqeq1d	$⊢ y = F \to (E \gcd y = 1 \leftrightarrow E \gcd F = 1)$
184		oveq1	$⊢ y = F \to y^{2} = F^{2}$
185	184	oveq2d	$⊢ y = F \to E^{2} + y^{2} = E^{2} + F^{2}$
186	185	eqeq2d	$⊢ y = F \to (E^{2} + F^{2} = E^{2} + y^{2} \leftrightarrow E^{2} + F^{2} = E^{2} + F^{2})$
187	183 186	anbi12d	$⊢ y = F \to ((E \gcd y = 1 \land E^{2} + F^{2} = E^{2} + y^{2}) \leftrightarrow (E \gcd F = 1 \land E^{2} + F^{2} = E^{2} + F^{2}))$
188	181 187	rspc2ev	$⊢ (E \in ℤ \land F \in ℤ \land (E \gcd F = 1 \land E^{2} + F^{2} = E^{2} + F^{2})) \to \exists x \in ℤ \exists y \in ℤ (x \gcd y = 1 \land E^{2} + F^{2} = x^{2} + y^{2})$
189	62 70 174 175 188	syl112anc	$⊢ φ \to \exists x \in ℤ \exists y \in ℤ (x \gcd y = 1 \land E^{2} + F^{2} = x^{2} + y^{2})$
190		ovex	$⊢ E^{2} + F^{2} \in V$
191		eqeq1	$⊢ z = E^{2} + F^{2} \to (z = x^{2} + y^{2} \leftrightarrow E^{2} + F^{2} = x^{2} + y^{2})$
192	191	anbi2d	$⊢ z = E^{2} + F^{2} \to ((x \gcd y = 1 \land z = x^{2} + y^{2}) \leftrightarrow (x \gcd y = 1 \land E^{2} + F^{2} = x^{2} + y^{2}))$
193	192	2rexbidv	$⊢ z = E^{2} + F^{2} \to (\exists x \in ℤ \exists y \in ℤ (x \gcd y = 1 \land z = x^{2} + y^{2}) \leftrightarrow \exists x \in ℤ \exists y \in ℤ (x \gcd y = 1 \land E^{2} + F^{2} = x^{2} + y^{2}))$
194	190 193 2	elab2	$⊢ E^{2} + F^{2} \in Y \leftrightarrow \exists x \in ℤ \exists y \in ℤ (x \gcd y = 1 \land E^{2} + F^{2} = x^{2} + y^{2})$
195	189 194	sylibr	$⊢ φ \to E^{2} + F^{2} \in Y$
196	164 195	sselid	$⊢ φ \to E^{2} + F^{2} \in ℕ$
197	196	nngt0d	$⊢ φ \to 0 < E^{2} + F^{2}$
198	17	nngt0d	$⊢ φ \to 0 < M$
199	160 161 197 198	divgt0d	$⊢ φ \to 0 < \frac{E^{2} + F^{2}}{M}$
200		elnnz	$⊢ \frac{E^{2} + F^{2}}{M} \in ℕ \leftrightarrow (\frac{E^{2} + F^{2}}{M} \in ℤ \land 0 < \frac{E^{2} + F^{2}}{M})$
201	157 199 200	sylanbrc	$⊢ φ \to \frac{E^{2} + F^{2}}{M} \in ℕ$
202		prmnn	$⊢ p \in ℙ \to p \in ℕ$
203	202	ad2antrl	$⊢ (φ \land (p \in ℙ \land p ∥ (\frac{E^{2} + F^{2}}{M}))) \to p \in ℕ$
204	203	nnred	$⊢ (φ \land (p \in ℙ \land p ∥ (\frac{E^{2} + F^{2}}{M}))) \to p \in ℝ$
205	157	adantr	$⊢ (φ \land (p \in ℙ \land p ∥ (\frac{E^{2} + F^{2}}{M}))) \to \frac{E^{2} + F^{2}}{M} \in ℤ$
206	205	zred	$⊢ (φ \land (p \in ℙ \land p ∥ (\frac{E^{2} + F^{2}}{M}))) \to \frac{E^{2} + F^{2}}{M} \in ℝ$
207		peano2zm	$⊢ M \in ℤ \to M - 1 \in ℤ$
208	19 207	syl	$⊢ φ \to M - 1 \in ℤ$
209	208	zred	$⊢ φ \to M - 1 \in ℝ$
210	209	adantr	$⊢ (φ \land (p \in ℙ \land p ∥ (\frac{E^{2} + F^{2}}{M}))) \to M - 1 \in ℝ$
211		simprr	$⊢ (φ \land (p \in ℙ \land p ∥ (\frac{E^{2} + F^{2}}{M}))) \to p ∥ (\frac{E^{2} + F^{2}}{M})$
212		prmz	$⊢ p \in ℙ \to p \in ℤ$
213	212	ad2antrl	$⊢ (φ \land (p \in ℙ \land p ∥ (\frac{E^{2} + F^{2}}{M}))) \to p \in ℤ$
214	201	adantr	$⊢ (φ \land (p \in ℙ \land p ∥ (\frac{E^{2} + F^{2}}{M}))) \to \frac{E^{2} + F^{2}}{M} \in ℕ$
215		dvdsle	$⊢ (p \in ℤ \land \frac{E^{2} + F^{2}}{M} \in ℕ) \to (p ∥ (\frac{E^{2} + F^{2}}{M}) \to p \leq \frac{E^{2} + F^{2}}{M})$
216	213 214 215	syl2anc	$⊢ (φ \land (p \in ℙ \land p ∥ (\frac{E^{2} + F^{2}}{M}))) \to (p ∥ (\frac{E^{2} + F^{2}}{M}) \to p \leq \frac{E^{2} + F^{2}}{M})$
217	211 216	mpd	$⊢ (φ \land (p \in ℙ \land p ∥ (\frac{E^{2} + F^{2}}{M}))) \to p \leq \frac{E^{2} + F^{2}}{M}$
218		zsqcl	$⊢ M \in ℤ \to M^{2} \in ℤ$
219	19 218	syl	$⊢ φ \to M^{2} \in ℤ$
220	219	zred	$⊢ φ \to M^{2} \in ℝ$
221	220	rehalfcld	$⊢ φ \to \frac{M^{2}}{2} \in ℝ$
222	24	zred	$⊢ φ \to C^{2} \in ℝ$
223	28	zred	$⊢ φ \to D^{2} \in ℝ$
224	222 223	readdcld	$⊢ φ \to C^{2} + D^{2} \in ℝ$
225		1red	$⊢ φ \to 1 \in ℝ$
226	50	nnsqcld	$⊢ φ \to {(C \gcd D)}^{2} \in ℕ$
227	226	nnred	$⊢ φ \to {(C \gcd D)}^{2} \in ℝ$
228	150	nn0ge0d	$⊢ φ \to 0 \leq E^{2} + F^{2}$
229	226	nnge1d	$⊢ φ \to 1 \leq {(C \gcd D)}^{2}$
230	225 227 160 228 229	lemul1ad	$⊢ φ \to 1 (E^{2} + F^{2}) \leq {(C \gcd D)}^{2} (E^{2} + F^{2})$
231	150	nn0cnd	$⊢ φ \to E^{2} + F^{2} \in ℂ$
232	231	mullidd	$⊢ φ \to 1 (E^{2} + F^{2}) = E^{2} + F^{2}$
233	230 232 93	3brtr3d	$⊢ φ \to E^{2} + F^{2} \leq C^{2} + D^{2}$
234	221	rehalfcld	$⊢ φ \to \frac{\frac{M^{2}}{2}}{2} \in ℝ$
235	7 17 11	4sqlem7	$⊢ φ \to C^{2} \leq \frac{\frac{M^{2}}{2}}{2}$
236	8 17 12	4sqlem7	$⊢ φ \to D^{2} \leq \frac{\frac{M^{2}}{2}}{2}$
237	222 223 234 234 235 236	le2addd	$⊢ φ \to C^{2} + D^{2} \leq (\frac{\frac{M^{2}}{2}}{2}) + (\frac{\frac{M^{2}}{2}}{2})$
238	221	recnd	$⊢ φ \to \frac{M^{2}}{2} \in ℂ$
239	238	2halvesd	$⊢ φ \to (\frac{\frac{M^{2}}{2}}{2}) + (\frac{\frac{M^{2}}{2}}{2}) = \frac{M^{2}}{2}$
240	237 239	breqtrd	$⊢ φ \to C^{2} + D^{2} \leq \frac{M^{2}}{2}$
241	160 224 221 233 240	letrd	$⊢ φ \to E^{2} + F^{2} \leq \frac{M^{2}}{2}$
242	17	nnsqcld	$⊢ φ \to M^{2} \in ℕ$
243	242	nnrpd	$⊢ φ \to M^{2} \in ℝ^{+}$
244		rphalflt	$⊢ M^{2} \in ℝ^{+} \to \frac{M^{2}}{2} < M^{2}$
245	243 244	syl	$⊢ φ \to \frac{M^{2}}{2} < M^{2}$
246	160 221 220 241 245	lelttrd	$⊢ φ \to E^{2} + F^{2} < M^{2}$
247	19	zcnd	$⊢ φ \to M \in ℂ$
248	247	sqvald	$⊢ φ \to M^{2} = M \cdot M$
249	246 248	breqtrd	$⊢ φ \to E^{2} + F^{2} < M \cdot M$
250		ltdivmul	$⊢ (E^{2} + F^{2} \in ℝ \land M \in ℝ \land (M \in ℝ \land 0 < M)) \to (\frac{E^{2} + F^{2}}{M} < M \leftrightarrow E^{2} + F^{2} < M \cdot M)$
251	160 161 161 198 250	syl112anc	$⊢ φ \to (\frac{E^{2} + F^{2}}{M} < M \leftrightarrow E^{2} + F^{2} < M \cdot M)$
252	249 251	mpbird	$⊢ φ \to \frac{E^{2} + F^{2}}{M} < M$
253		zltlem1	$⊢ (\frac{E^{2} + F^{2}}{M} \in ℤ \land M \in ℤ) \to (\frac{E^{2} + F^{2}}{M} < M \leftrightarrow \frac{E^{2} + F^{2}}{M} \leq M - 1)$
254	157 19 253	syl2anc	$⊢ φ \to (\frac{E^{2} + F^{2}}{M} < M \leftrightarrow \frac{E^{2} + F^{2}}{M} \leq M - 1)$
255	252 254	mpbid	$⊢ φ \to \frac{E^{2} + F^{2}}{M} \leq M - 1$
256	255	adantr	$⊢ (φ \land (p \in ℙ \land p ∥ (\frac{E^{2} + F^{2}}{M}))) \to \frac{E^{2} + F^{2}}{M} \leq M - 1$
257	204 206 210 217 256	letrd	$⊢ (φ \land (p \in ℙ \land p ∥ (\frac{E^{2} + F^{2}}{M}))) \to p \leq M - 1$
258	208	adantr	$⊢ (φ \land (p \in ℙ \land p ∥ (\frac{E^{2} + F^{2}}{M}))) \to M - 1 \in ℤ$
259		fznn	$⊢ M - 1 \in ℤ \to (p \in (1 \dots M - 1) \leftrightarrow (p \in ℕ \land p \leq M - 1))$
260	258 259	syl	$⊢ (φ \land (p \in ℙ \land p ∥ (\frac{E^{2} + F^{2}}{M}))) \to (p \in (1 \dots M - 1) \leftrightarrow (p \in ℕ \land p \leq M - 1))$
261	203 257 260	mpbir2and	$⊢ (φ \land (p \in ℙ \land p ∥ (\frac{E^{2} + F^{2}}{M}))) \to p \in (1 \dots M - 1)$
262	195	adantr	$⊢ (φ \land (p \in ℙ \land p ∥ (\frac{E^{2} + F^{2}}{M}))) \to E^{2} + F^{2} \in Y$
263	261 262	jca	$⊢ (φ \land (p \in ℙ \land p ∥ (\frac{E^{2} + F^{2}}{M}))) \to (p \in (1 \dots M - 1) \land E^{2} + F^{2} \in Y)$
264	3	adantr	$⊢ (φ \land (p \in ℙ \land p ∥ (\frac{E^{2} + F^{2}}{M}))) \to \forall b \in (1 \dots M - 1) \forall a \in Y (b ∥ a \to b \in S)$
265	151	adantr	$⊢ (φ \land (p \in ℙ \land p ∥ (\frac{E^{2} + F^{2}}{M}))) \to E^{2} + F^{2} \in ℤ$
266		dvdsmul2	$⊢ (M \in ℤ \land \frac{E^{2} + F^{2}}{M} \in ℤ) \to (\frac{E^{2} + F^{2}}{M}) ∥ M (\frac{E^{2} + F^{2}}{M})$
267	19 157 266	syl2anc	$⊢ φ \to (\frac{E^{2} + F^{2}}{M}) ∥ M (\frac{E^{2} + F^{2}}{M})$
268	231 247 107	divcan2d	$⊢ φ \to M (\frac{E^{2} + F^{2}}{M}) = E^{2} + F^{2}$
269	267 268	breqtrd	$⊢ φ \to (\frac{E^{2} + F^{2}}{M}) ∥ (E^{2} + F^{2})$
270	269	adantr	$⊢ (φ \land (p \in ℙ \land p ∥ (\frac{E^{2} + F^{2}}{M}))) \to (\frac{E^{2} + F^{2}}{M}) ∥ (E^{2} + F^{2})$
271	213 205 265 211 270	dvdstrd	$⊢ (φ \land (p \in ℙ \land p ∥ (\frac{E^{2} + F^{2}}{M}))) \to p ∥ (E^{2} + F^{2})$
272		breq1	$⊢ b = p \to (b ∥ a \leftrightarrow p ∥ a)$
273		eleq1w	$⊢ b = p \to (b \in S \leftrightarrow p \in S)$
274	272 273	imbi12d	$⊢ b = p \to ((b ∥ a \to b \in S) \leftrightarrow (p ∥ a \to p \in S))$
275		breq2	$⊢ a = E^{2} + F^{2} \to (p ∥ a \leftrightarrow p ∥ (E^{2} + F^{2}))$
276	275	imbi1d	$⊢ a = E^{2} + F^{2} \to ((p ∥ a \to p \in S) \leftrightarrow (p ∥ (E^{2} + F^{2}) \to p \in S))$
277	274 276	rspc2v	$⊢ (p \in (1 \dots M - 1) \land E^{2} + F^{2} \in Y) \to (\forall b \in (1 \dots M - 1) \forall a \in Y (b ∥ a \to b \in S) \to (p ∥ (E^{2} + F^{2}) \to p \in S))$
278	263 264 271 277	syl3c	$⊢ (φ \land (p \in ℙ \land p ∥ (\frac{E^{2} + F^{2}}{M}))) \to p \in S$
279	278	expr	$⊢ (φ \land p \in ℙ) \to (p ∥ (\frac{E^{2} + F^{2}}{M}) \to p \in S)$
280	279	ralrimiva	$⊢ φ \to \forall p \in ℙ (p ∥ (\frac{E^{2} + F^{2}}{M}) \to p \in S)$
281		inss1	$⊢ S \cap ℕ \subseteq S$
282	162 281	sstri	$⊢ Y \subseteq S$
283	282 195	sselid	$⊢ φ \to E^{2} + F^{2} \in S$
284	268 283	eqeltrd	$⊢ φ \to M (\frac{E^{2} + F^{2}}{M}) \in S$
285	1 17 201 280 284	2sqlem6	$⊢ φ \to M \in S$

Metamath Proof Explorer

Theorem 2sqlem8

Proof