Theorem 2sqblem

Description: Lemma for 2sqb . (Contributed by Mario Carneiro, 20-Jun-2015)

	Ref	Expression
Hypotheses	2sqb.1	$$⊢\phi \to \left(P\in \mathbb{P}\wedge P\ne 2\right)$$
	2sqb.2	$$⊢\phi \to \left(X\in \mathbb{Z}\wedge Y\in \mathbb{Z}\right)$$
	2sqb.3	$$⊢\phi \to P=X^2+Y^2$$
	2sqb.4	$$⊢\phi \to A\in \mathbb{Z}$$
	2sqb.5	$$⊢\phi \to B\in \mathbb{Z}$$
	2sqb.6	$$⊢\phi \to P\gcd Y=PA+YB$$
Assertion	2sqblem	$$⊢\phi \to P\mathrm{mod}4=1$$

Proof

Step	Hyp	Ref	Expression
1		2sqb.1	$$⊢\phi \to \left(P\in \mathbb{P}\wedge P\ne 2\right)$$
2		2sqb.2	$$⊢\phi \to \left(X\in \mathbb{Z}\wedge Y\in \mathbb{Z}\right)$$
3		2sqb.3	$$⊢\phi \to P=X^2+Y^2$$
4		2sqb.4	$$⊢\phi \to A\in \mathbb{Z}$$
5		2sqb.5	$$⊢\phi \to B\in \mathbb{Z}$$
6		2sqb.6	$$⊢\phi \to P\gcd Y=PA+YB$$
7	1	simpld	$$⊢\phi \to P\in \mathbb{P}$$
8		nprmdvds1	$$⊢P\in \mathbb{P}\to \neg P\parallel 1$$
9	7 8	syl	$$⊢\phi \to \neg P\parallel 1$$
10		prmz	$$⊢P\in \mathbb{P}\to P\in \mathbb{Z}$$
11	7 10	syl	$$⊢\phi \to P\in \mathbb{Z}$$
12		1z	$$⊢1\in \mathbb{Z}$$
13		dvdsnegb	$$⊢\left(P\in \mathbb{Z}\wedge 1\in \mathbb{Z}\right)\to \left(P\parallel 1\leftrightarrow P\parallel -1\right)$$
14	11 12 13	sylancl	$$⊢\phi \to \left(P\parallel 1\leftrightarrow P\parallel -1\right)$$
15	9 14	mtbid	$$⊢\phi \to \neg P\parallel -1$$
16	2	simpld	$$⊢\phi \to X\in \mathbb{Z}$$
17	16 5	zmulcld	$$⊢\phi \to XB\in \mathbb{Z}$$
18		zsqcl	$$⊢B\in \mathbb{Z}\to B^2\in \mathbb{Z}$$
19	5 18	syl	$$⊢\phi \to B^2\in \mathbb{Z}$$
20		dvdsmul1	$$⊢\left(P\in \mathbb{Z}\wedge B^2\in \mathbb{Z}\right)\to P\parallel P{B}^2$$
21	11 19 20	syl2anc	$$⊢\phi \to P\parallel P{B}^2$$
22	2	simprd	$$⊢\phi \to Y\in \mathbb{Z}$$
23	22 5	zmulcld	$$⊢\phi \to YB\in \mathbb{Z}$$
24		zsqcl	$$⊢YB\in \mathbb{Z}\to {YB}^2\in \mathbb{Z}$$
25	23 24	syl	$$⊢\phi \to {YB}^2\in \mathbb{Z}$$
26		peano2zm	$$⊢{YB}^2\in \mathbb{Z}\to {YB}^2-1\in \mathbb{Z}$$
27	25 26	syl	$$⊢\phi \to {YB}^2-1\in \mathbb{Z}$$
28	27	zcnd	$$⊢\phi \to {YB}^2-1\in ℂ$$
29		zsqcl	$$⊢XB\in \mathbb{Z}\to {XB}^2\in \mathbb{Z}$$
30	17 29	syl	$$⊢\phi \to {XB}^2\in \mathbb{Z}$$
31	30	peano2zd	$$⊢\phi \to {XB}^2+1\in \mathbb{Z}$$
32	31	zcnd	$$⊢\phi \to {XB}^2+1\in ℂ$$
33	28 32	addcomd	$$⊢\phi \to \left({YB}^2-1\right)+{XB}^2+1={XB}^2+1+\left({YB}^2-1\right)$$
34	30	zcnd	$$⊢\phi \to {XB}^2\in ℂ$$
35		ax-1cn	$$⊢1\in ℂ$$
36	35	a1i	$$⊢\phi \to 1\in ℂ$$
37	25	zcnd	$$⊢\phi \to {YB}^2\in ℂ$$
38	34 36 37	ppncand	$$⊢\phi \to {XB}^2+1+\left({YB}^2-1\right)={XB}^2+{YB}^2$$
39		zsqcl	$$⊢X\in \mathbb{Z}\to X^2\in \mathbb{Z}$$
40	16 39	syl	$$⊢\phi \to X^2\in \mathbb{Z}$$
41	40	zcnd	$$⊢\phi \to X^2\in ℂ$$
42		zsqcl	$$⊢Y\in \mathbb{Z}\to Y^2\in \mathbb{Z}$$
43	22 42	syl	$$⊢\phi \to Y^2\in \mathbb{Z}$$
44	43	zcnd	$$⊢\phi \to Y^2\in ℂ$$
45	19	zcnd	$$⊢\phi \to B^2\in ℂ$$
46	41 44 45	adddird	$$⊢\phi \to \left(X^2+Y^2\right)B^2=X^2{B}^2+Y^2{B}^2$$
47	3	oveq1d	$$⊢\phi \to P{B}^2=\left(X^2+Y^2\right)B^2$$
48	16	zcnd	$$⊢\phi \to X\in ℂ$$
49	5	zcnd	$$⊢\phi \to B\in ℂ$$
50	48 49	sqmuld	$$⊢\phi \to {XB}^2=X^2{B}^2$$
51	22	zcnd	$$⊢\phi \to Y\in ℂ$$
52	51 49	sqmuld	$$⊢\phi \to {YB}^2=Y^2{B}^2$$
53	50 52	oveq12d	$$⊢\phi \to {XB}^2+{YB}^2=X^2{B}^2+Y^2{B}^2$$
54	46 47 53	3eqtr4rd	$$⊢\phi \to {XB}^2+{YB}^2=P{B}^2$$
55	33 38 54	3eqtrd	$$⊢\phi \to \left({YB}^2-1\right)+{XB}^2+1=P{B}^2$$
56	21 55	breqtrrd	$$⊢\phi \to P\parallel \left(\left({YB}^2-1\right)+{XB}^2+1\right)$$
57		dvdsmul1	$$⊢\left(P\in \mathbb{Z}\wedge A\in \mathbb{Z}\right)\to P\parallel PA$$
58	11 4 57	syl2anc	$$⊢\phi \to P\parallel PA$$
59	11 4	zmulcld	$$⊢\phi \to PA\in \mathbb{Z}$$
60		dvdsnegb	$$⊢\left(P\in \mathbb{Z}\wedge PA\in \mathbb{Z}\right)\to \left(P\parallel PA\leftrightarrow P\parallel \left(-PA\right)\right)$$
61	11 59 60	syl2anc	$$⊢\phi \to \left(P\parallel PA\leftrightarrow P\parallel \left(-PA\right)\right)$$
62	58 61	mpbid	$$⊢\phi \to P\parallel \left(-PA\right)$$
63	23	zcnd	$$⊢\phi \to YB\in ℂ$$
64		negsubdi2	$$⊢\left(1\in ℂ\wedge YB\in ℂ\right)\to -\left(1-YB\right)=YB-1$$
65	35 63 64	sylancr	$$⊢\phi \to -\left(1-YB\right)=YB-1$$
66	59	zcnd	$$⊢\phi \to PA\in ℂ$$
67	22	zred	$$⊢\phi \to Y\in ℝ$$
68		absresq	$$⊢Y\in ℝ\to {\left|Y\right|}^2=Y^2$$
69	67 68	syl	$$⊢\phi \to {\left|Y\right|}^2=Y^2$$
70	67	resqcld	$$⊢\phi \to Y^2\in ℝ$$
71		prmnn	$$⊢P\in \mathbb{P}\to P\in \mathbb{N}$$
72	7 71	syl	$$⊢\phi \to P\in \mathbb{N}$$
73	72	nnred	$$⊢\phi \to P\in ℝ$$
74	73	resqcld	$$⊢\phi \to P^2\in ℝ$$
75		zsqcl2	$$⊢X\in \mathbb{Z}\to X^2\in {\mathbb{N}}_0$$
76	16 75	syl	$$⊢\phi \to X^2\in {\mathbb{N}}_0$$
77		nn0addge2	$$⊢\left(Y^2\in ℝ\wedge X^2\in {\mathbb{N}}_0\right)\to Y^2\le X^2+Y^2$$
78	70 76 77	syl2anc	$$⊢\phi \to Y^2\le X^2+Y^2$$
79	78 3	breqtrrd	$$⊢\phi \to Y^2\le P$$
80	11	zcnd	$$⊢\phi \to P\in ℂ$$
81	80	exp1d	$$⊢\phi \to P^1=P$$
82	12	a1i	$$⊢\phi \to 1\in \mathbb{Z}$$
83		2z	$$⊢2\in \mathbb{Z}$$
84	83	a1i	$$⊢\phi \to 2\in \mathbb{Z}$$
85		prmuz2	$$⊢P\in \mathbb{P}\to P\in {\mathbb{Z}}_{\ge 2}$$
86	7 85	syl	$$⊢\phi \to P\in {\mathbb{Z}}_{\ge 2}$$
87		eluz2gt1	$$⊢P\in {\mathbb{Z}}_{\ge 2}\to 1<P$$
88	86 87	syl	$$⊢\phi \to 1<P$$
89		1lt2	$$⊢1<2$$
90	89	a1i	$$⊢\phi \to 1<2$$
91		ltexp2a	$$⊢\left(\left(P\in ℝ\wedge 1\in \mathbb{Z}\wedge 2\in \mathbb{Z}\right)\wedge \left(1<P\wedge 1<2\right)\right)\to P^1<P^2$$
92	73 82 84 88 90 91	syl32anc	$$⊢\phi \to P^1<P^2$$
93	81 92	eqbrtrrd	$$⊢\phi \to P<P^2$$
94	70 73 74 79 93	lelttrd	$$⊢\phi \to Y^2<P^2$$
95	69 94	eqbrtrd	$$⊢\phi \to {\left|Y\right|}^2<P^2$$
96	51	abscld	$$⊢\phi \to \left|Y\right|\in ℝ$$
97	51	absge0d	$$⊢\phi \to 0\le \left|Y\right|$$
98	72	nnnn0d	$$⊢\phi \to P\in {\mathbb{N}}_0$$
99	98	nn0ge0d	$$⊢\phi \to 0\le P$$
100	96 73 97 99	lt2sqd	$$⊢\phi \to \left(\left|Y\right|<P\leftrightarrow {\left|Y\right|}^2<P^2\right)$$
101	95 100	mpbird	$$⊢\phi \to \left|Y\right|<P$$
102	11	zred	$$⊢\phi \to P\in ℝ$$
103	96 102	ltnled	$$⊢\phi \to \left(\left|Y\right|<P\leftrightarrow \neg P\le \left|Y\right|\right)$$
104	101 103	mpbid	$$⊢\phi \to \neg P\le \left|Y\right|$$
105		sqnprm	$$⊢X\in \mathbb{Z}\to \neg X^2\in \mathbb{P}$$
106	16 105	syl	$$⊢\phi \to \neg X^2\in \mathbb{P}$$
107	51	abs00ad	$$⊢\phi \to \left(\left|Y\right|=0\leftrightarrow Y=0\right)$$
108	3 7	eqeltrrd	$$⊢\phi \to X^2+Y^2\in \mathbb{P}$$
109		sq0i	$$⊢Y=0\to Y^2=0$$
110	109	oveq2d	$$⊢Y=0\to X^2+Y^2=X^2+0$$
111	110	eleq1d	$$⊢Y=0\to \left(X^2+Y^2\in \mathbb{P}\leftrightarrow X^2+0\in \mathbb{P}\right)$$
112	108 111	syl5ibcom	$$⊢\phi \to \left(Y=0\to X^2+0\in \mathbb{P}\right)$$
113	41	addridd	$$⊢\phi \to X^2+0=X^2$$
114	113	eleq1d	$$⊢\phi \to \left(X^2+0\in \mathbb{P}\leftrightarrow X^2\in \mathbb{P}\right)$$
115	112 114	sylibd	$$⊢\phi \to \left(Y=0\to X^2\in \mathbb{P}\right)$$
116	107 115	sylbid	$$⊢\phi \to \left(\left|Y\right|=0\to X^2\in \mathbb{P}\right)$$
117	106 116	mtod	$$⊢\phi \to \neg \left|Y\right|=0$$
118		nn0abscl	$$⊢Y\in \mathbb{Z}\to \left|Y\right|\in {\mathbb{N}}_0$$
119	22 118	syl	$$⊢\phi \to \left|Y\right|\in {\mathbb{N}}_0$$
120		elnn0	$$⊢\left|Y\right|\in {\mathbb{N}}_0\leftrightarrow \left(\left|Y\right|\in \mathbb{N}\vee \left|Y\right|=0\right)$$
121	119 120	sylib	$$⊢\phi \to \left(\left|Y\right|\in \mathbb{N}\vee \left|Y\right|=0\right)$$
122	121	ord	$$⊢\phi \to \left(\neg \left|Y\right|\in \mathbb{N}\to \left|Y\right|=0\right)$$
123	117 122	mt3d	$$⊢\phi \to \left|Y\right|\in \mathbb{N}$$
124		dvdsle	$$⊢\left(P\in \mathbb{Z}\wedge \left|Y\right|\in \mathbb{N}\right)\to \left(P\parallel \left|Y\right|\to P\le \left|Y\right|\right)$$
125	11 123 124	syl2anc	$$⊢\phi \to \left(P\parallel \left|Y\right|\to P\le \left|Y\right|\right)$$
126	104 125	mtod	$$⊢\phi \to \neg P\parallel \left|Y\right|$$
127		dvdsabsb	$$⊢\left(P\in \mathbb{Z}\wedge Y\in \mathbb{Z}\right)\to \left(P\parallel Y\leftrightarrow P\parallel \left|Y\right|\right)$$
128	11 22 127	syl2anc	$$⊢\phi \to \left(P\parallel Y\leftrightarrow P\parallel \left|Y\right|\right)$$
129	126 128	mtbird	$$⊢\phi \to \neg P\parallel Y$$
130		coprm	$$⊢\left(P\in \mathbb{P}\wedge Y\in \mathbb{Z}\right)\to \left(\neg P\parallel Y\leftrightarrow P\gcd Y=1\right)$$
131	7 22 130	syl2anc	$$⊢\phi \to \left(\neg P\parallel Y\leftrightarrow P\gcd Y=1\right)$$
132	129 131	mpbid	$$⊢\phi \to P\gcd Y=1$$
133	132 6	eqtr3d	$$⊢\phi \to 1=PA+YB$$
134	66 63 133	mvrraddd	$$⊢\phi \to 1-YB=PA$$
135	134	negeqd	$$⊢\phi \to -\left(1-YB\right)=-PA$$
136	65 135	eqtr3d	$$⊢\phi \to YB-1=-PA$$
137	62 136	breqtrrd	$$⊢\phi \to P\parallel \left(YB-1\right)$$
138	23	peano2zd	$$⊢\phi \to YB+1\in \mathbb{Z}$$
139		peano2zm	$$⊢YB\in \mathbb{Z}\to YB-1\in \mathbb{Z}$$
140	23 139	syl	$$⊢\phi \to YB-1\in \mathbb{Z}$$
141		dvdsmultr2	$$⊢\left(P\in \mathbb{Z}\wedge YB+1\in \mathbb{Z}\wedge YB-1\in \mathbb{Z}\right)\to \left(P\parallel \left(YB-1\right)\to P\parallel \left(YB+1\right)\left(YB-1\right)\right)$$
142	11 138 140 141	syl3anc	$$⊢\phi \to \left(P\parallel \left(YB-1\right)\to P\parallel \left(YB+1\right)\left(YB-1\right)\right)$$
143	137 142	mpd	$$⊢\phi \to P\parallel \left(YB+1\right)\left(YB-1\right)$$
144		sq1	$$⊢1^2=1$$
145	144	oveq2i	$$⊢{YB}^2-1^2={YB}^2-1$$
146		subsq	$$⊢\left(YB\in ℂ\wedge 1\in ℂ\right)\to {YB}^2-1^2=\left(YB+1\right)\left(YB-1\right)$$
147	63 35 146	sylancl	$$⊢\phi \to {YB}^2-1^2=\left(YB+1\right)\left(YB-1\right)$$
148	145 147	eqtr3id	$$⊢\phi \to {YB}^2-1=\left(YB+1\right)\left(YB-1\right)$$
149	143 148	breqtrrd	$$⊢\phi \to P\parallel \left({YB}^2-1\right)$$
150		dvdsadd2b	$$⊢\left(P\in \mathbb{Z}\wedge {XB}^2+1\in \mathbb{Z}\wedge \left({YB}^2-1\in \mathbb{Z}\wedge P\parallel \left({YB}^2-1\right)\right)\right)\to \left(P\parallel \left({XB}^2+1\right)\leftrightarrow P\parallel \left(\left({YB}^2-1\right)+{XB}^2+1\right)\right)$$
151	11 31 27 149 150	syl112anc	$$⊢\phi \to \left(P\parallel \left({XB}^2+1\right)\leftrightarrow P\parallel \left(\left({YB}^2-1\right)+{XB}^2+1\right)\right)$$
152	56 151	mpbird	$$⊢\phi \to P\parallel \left({XB}^2+1\right)$$
153		subneg	$$⊢\left({XB}^2\in ℂ\wedge 1\in ℂ\right)\to {XB}^2--1={XB}^2+1$$
154	34 35 153	sylancl	$$⊢\phi \to {XB}^2--1={XB}^2+1$$
155	152 154	breqtrrd	$$⊢\phi \to P\parallel \left({XB}^2--1\right)$$
156		oveq1	$$⊢x=XB\to x^2={XB}^2$$
157	156	oveq1d	$$⊢x=XB\to x^2--1={XB}^2--1$$
158	157	breq2d	$$⊢x=XB\to \left(P\parallel \left(x^2--1\right)\leftrightarrow P\parallel \left({XB}^2--1\right)\right)$$
159	158	rspcev	$$⊢\left(XB\in \mathbb{Z}\wedge P\parallel \left({XB}^2--1\right)\right)\to \exists x\in \mathbb{Z}P\parallel \left(x^2--1\right)$$
160	17 155 159	syl2anc	$$⊢\phi \to \exists x\in \mathbb{Z}P\parallel \left(x^2--1\right)$$
161		neg1z	$$⊢-1\in \mathbb{Z}$$
162		eldifsn	$$⊢P\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\leftrightarrow \left(P\in \mathbb{P}\wedge P\ne 2\right)$$
163	1 162	sylibr	$$⊢\phi \to P\in \left(\mathbb{P}\setminus \left\{2\right\}\right)$$
164		lgsqr	$$⊢\left(-1\in \mathbb{Z}\wedge P\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\right)\to \left(-1{/}_{L}P=1\leftrightarrow \left(\neg P\parallel -1\wedge \exists x\in \mathbb{Z}P\parallel \left(x^2--1\right)\right)\right)$$
165	161 163 164	sylancr	$$⊢\phi \to \left(-1{/}_{L}P=1\leftrightarrow \left(\neg P\parallel -1\wedge \exists x\in \mathbb{Z}P\parallel \left(x^2--1\right)\right)\right)$$
166	15 160 165	mpbir2and	$$⊢\phi \to -1{/}_{L}P=1$$
167		m1lgs	$$⊢P\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\to \left(-1{/}_{L}P=1\leftrightarrow P\mathrm{mod}4=1\right)$$
168	163 167	syl	$$⊢\phi \to \left(-1{/}_{L}P=1\leftrightarrow P\mathrm{mod}4=1\right)$$
169	166 168	mpbid	$$⊢\phi \to P\mathrm{mod}4=1$$