# Metamath Proof Explorer

## Theorem 2sqblem

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

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

### Proof

Step Hyp Ref Expression
1 2sqb.1 ${⊢}{\phi }\to \left({P}\in ℙ\wedge {P}\ne 2\right)$
2 2sqb.2 ${⊢}{\phi }\to \left({X}\in ℤ\wedge {Y}\in ℤ\right)$
3 2sqb.3 ${⊢}{\phi }\to {P}={{X}}^{2}+{{Y}}^{2}$
4 2sqb.4 ${⊢}{\phi }\to {A}\in ℤ$
5 2sqb.5 ${⊢}{\phi }\to {B}\in ℤ$
6 2sqb.6 ${⊢}{\phi }\to {P}\mathrm{gcd}{Y}={P}{A}+{Y}{B}$
7 1 simpld ${⊢}{\phi }\to {P}\in ℙ$
8 nprmdvds1 ${⊢}{P}\in ℙ\to ¬{P}\parallel 1$
9 7 8 syl ${⊢}{\phi }\to ¬{P}\parallel 1$
10 prmz ${⊢}{P}\in ℙ\to {P}\in ℤ$
11 7 10 syl ${⊢}{\phi }\to {P}\in ℤ$
12 1z ${⊢}1\in ℤ$
13 dvdsnegb ${⊢}\left({P}\in ℤ\wedge 1\in ℤ\right)\to \left({P}\parallel 1↔{P}\parallel -1\right)$
14 11 12 13 sylancl ${⊢}{\phi }\to \left({P}\parallel 1↔{P}\parallel -1\right)$
15 9 14 mtbid ${⊢}{\phi }\to ¬{P}\parallel -1$
16 2 simpld ${⊢}{\phi }\to {X}\in ℤ$
17 16 5 zmulcld ${⊢}{\phi }\to {X}{B}\in ℤ$
18 zsqcl ${⊢}{B}\in ℤ\to {{B}}^{2}\in ℤ$
19 5 18 syl ${⊢}{\phi }\to {{B}}^{2}\in ℤ$
20 dvdsmul1 ${⊢}\left({P}\in ℤ\wedge {{B}}^{2}\in ℤ\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 ℤ$
23 22 5 zmulcld ${⊢}{\phi }\to {Y}{B}\in ℤ$
24 zsqcl ${⊢}{Y}{B}\in ℤ\to {{Y}{B}}^{2}\in ℤ$
25 23 24 syl ${⊢}{\phi }\to {{Y}{B}}^{2}\in ℤ$
26 peano2zm ${⊢}{{Y}{B}}^{2}\in ℤ\to {{Y}{B}}^{2}-1\in ℤ$
27 25 26 syl ${⊢}{\phi }\to {{Y}{B}}^{2}-1\in ℤ$
28 27 zcnd ${⊢}{\phi }\to {{Y}{B}}^{2}-1\in ℂ$
29 zsqcl ${⊢}{X}{B}\in ℤ\to {{X}{B}}^{2}\in ℤ$
30 17 29 syl ${⊢}{\phi }\to {{X}{B}}^{2}\in ℤ$
31 30 peano2zd ${⊢}{\phi }\to {{X}{B}}^{2}+1\in ℤ$
32 31 zcnd ${⊢}{\phi }\to {{X}{B}}^{2}+1\in ℂ$
33 28 32 addcomd ${⊢}{\phi }\to \left({{Y}{B}}^{2}-1\right)+{{X}{B}}^{2}+1={{X}{B}}^{2}+1+\left({{Y}{B}}^{2}-1\right)$
34 30 zcnd ${⊢}{\phi }\to {{X}{B}}^{2}\in ℂ$
35 ax-1cn ${⊢}1\in ℂ$
36 35 a1i ${⊢}{\phi }\to 1\in ℂ$
37 25 zcnd ${⊢}{\phi }\to {{Y}{B}}^{2}\in ℂ$
38 34 36 37 ppncand ${⊢}{\phi }\to {{X}{B}}^{2}+1+\left({{Y}{B}}^{2}-1\right)={{X}{B}}^{2}+{{Y}{B}}^{2}$
39 zsqcl ${⊢}{X}\in ℤ\to {{X}}^{2}\in ℤ$
40 16 39 syl ${⊢}{\phi }\to {{X}}^{2}\in ℤ$
41 40 zcnd ${⊢}{\phi }\to {{X}}^{2}\in ℂ$
42 zsqcl ${⊢}{Y}\in ℤ\to {{Y}}^{2}\in ℤ$
43 22 42 syl ${⊢}{\phi }\to {{Y}}^{2}\in ℤ$
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 {{X}{B}}^{2}={{X}}^{2}{{B}}^{2}$
51 22 zcnd ${⊢}{\phi }\to {Y}\in ℂ$
52 51 49 sqmuld ${⊢}{\phi }\to {{Y}{B}}^{2}={{Y}}^{2}{{B}}^{2}$
53 50 52 oveq12d ${⊢}{\phi }\to {{X}{B}}^{2}+{{Y}{B}}^{2}={{X}}^{2}{{B}}^{2}+{{Y}}^{2}{{B}}^{2}$
54 46 47 53 3eqtr4rd ${⊢}{\phi }\to {{X}{B}}^{2}+{{Y}{B}}^{2}={P}{{B}}^{2}$
55 33 38 54 3eqtrd ${⊢}{\phi }\to \left({{Y}{B}}^{2}-1\right)+{{X}{B}}^{2}+1={P}{{B}}^{2}$
56 21 55 breqtrrd ${⊢}{\phi }\to {P}\parallel \left(\left({{Y}{B}}^{2}-1\right)+{{X}{B}}^{2}+1\right)$
57 dvdsmul1 ${⊢}\left({P}\in ℤ\wedge {A}\in ℤ\right)\to {P}\parallel {P}{A}$
58 11 4 57 syl2anc ${⊢}{\phi }\to {P}\parallel {P}{A}$
59 11 4 zmulcld ${⊢}{\phi }\to {P}{A}\in ℤ$
60 dvdsnegb ${⊢}\left({P}\in ℤ\wedge {P}{A}\in ℤ\right)\to \left({P}\parallel {P}{A}↔{P}\parallel \left(-{P}{A}\right)\right)$
61 11 59 60 syl2anc ${⊢}{\phi }\to \left({P}\parallel {P}{A}↔{P}\parallel \left(-{P}{A}\right)\right)$
62 58 61 mpbid ${⊢}{\phi }\to {P}\parallel \left(-{P}{A}\right)$
63 23 zcnd ${⊢}{\phi }\to {Y}{B}\in ℂ$
64 negsubdi2 ${⊢}\left(1\in ℂ\wedge {Y}{B}\in ℂ\right)\to -\left(1-{Y}{B}\right)={Y}{B}-1$
65 35 63 64 sylancr ${⊢}{\phi }\to -\left(1-{Y}{B}\right)={Y}{B}-1$
66 59 zcnd ${⊢}{\phi }\to {P}{A}\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 ℙ\to {P}\in ℕ$
72 7 71 syl ${⊢}{\phi }\to {P}\in ℕ$
73 72 nnred ${⊢}{\phi }\to {P}\in ℝ$
74 73 resqcld ${⊢}{\phi }\to {{P}}^{2}\in ℝ$
75 zsqcl2 ${⊢}{X}\in ℤ\to {{X}}^{2}\in {ℕ}_{0}$
76 16 75 syl ${⊢}{\phi }\to {{X}}^{2}\in {ℕ}_{0}$
77 nn0addge2 ${⊢}\left({{Y}}^{2}\in ℝ\wedge {{X}}^{2}\in {ℕ}_{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 ℤ$
83 2z ${⊢}2\in ℤ$
84 83 a1i ${⊢}{\phi }\to 2\in ℤ$
85 prmuz2 ${⊢}{P}\in ℙ\to {P}\in {ℤ}_{\ge 2}$
86 7 85 syl ${⊢}{\phi }\to {P}\in {ℤ}_{\ge 2}$
87 eluz2gt1 ${⊢}{P}\in {ℤ}_{\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 ℤ\wedge 2\in ℤ\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 {ℕ}_{0}$
99 98 nn0ge0d ${⊢}{\phi }\to 0\le {P}$
100 96 73 97 99 lt2sqd ${⊢}{\phi }\to \left(\left|{Y}\right|<{P}↔{\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}↔¬{P}\le \left|{Y}\right|\right)$
104 101 103 mpbid ${⊢}{\phi }\to ¬{P}\le \left|{Y}\right|$
105 sqnprm ${⊢}{X}\in ℤ\to ¬{{X}}^{2}\in ℙ$
106 16 105 syl ${⊢}{\phi }\to ¬{{X}}^{2}\in ℙ$
107 51 abs00ad ${⊢}{\phi }\to \left(\left|{Y}\right|=0↔{Y}=0\right)$
108 3 7 eqeltrrd ${⊢}{\phi }\to {{X}}^{2}+{{Y}}^{2}\in ℙ$
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 ℙ↔{{X}}^{2}+0\in ℙ\right)$
112 108 111 syl5ibcom ${⊢}{\phi }\to \left({Y}=0\to {{X}}^{2}+0\in ℙ\right)$
113 41 addid1d ${⊢}{\phi }\to {{X}}^{2}+0={{X}}^{2}$
114 113 eleq1d ${⊢}{\phi }\to \left({{X}}^{2}+0\in ℙ↔{{X}}^{2}\in ℙ\right)$
115 112 114 sylibd ${⊢}{\phi }\to \left({Y}=0\to {{X}}^{2}\in ℙ\right)$
116 107 115 sylbid ${⊢}{\phi }\to \left(\left|{Y}\right|=0\to {{X}}^{2}\in ℙ\right)$
117 106 116 mtod ${⊢}{\phi }\to ¬\left|{Y}\right|=0$
118 nn0abscl ${⊢}{Y}\in ℤ\to \left|{Y}\right|\in {ℕ}_{0}$
119 22 118 syl ${⊢}{\phi }\to \left|{Y}\right|\in {ℕ}_{0}$
120 elnn0 ${⊢}\left|{Y}\right|\in {ℕ}_{0}↔\left(\left|{Y}\right|\in ℕ\vee \left|{Y}\right|=0\right)$
121 119 120 sylib ${⊢}{\phi }\to \left(\left|{Y}\right|\in ℕ\vee \left|{Y}\right|=0\right)$
122 121 ord ${⊢}{\phi }\to \left(¬\left|{Y}\right|\in ℕ\to \left|{Y}\right|=0\right)$
123 117 122 mt3d ${⊢}{\phi }\to \left|{Y}\right|\in ℕ$
124 dvdsle ${⊢}\left({P}\in ℤ\wedge \left|{Y}\right|\in ℕ\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 ¬{P}\parallel \left|{Y}\right|$
127 dvdsabsb ${⊢}\left({P}\in ℤ\wedge {Y}\in ℤ\right)\to \left({P}\parallel {Y}↔{P}\parallel \left|{Y}\right|\right)$
128 11 22 127 syl2anc ${⊢}{\phi }\to \left({P}\parallel {Y}↔{P}\parallel \left|{Y}\right|\right)$
129 126 128 mtbird ${⊢}{\phi }\to ¬{P}\parallel {Y}$
130 coprm ${⊢}\left({P}\in ℙ\wedge {Y}\in ℤ\right)\to \left(¬{P}\parallel {Y}↔{P}\mathrm{gcd}{Y}=1\right)$
131 7 22 130 syl2anc ${⊢}{\phi }\to \left(¬{P}\parallel {Y}↔{P}\mathrm{gcd}{Y}=1\right)$
132 129 131 mpbid ${⊢}{\phi }\to {P}\mathrm{gcd}{Y}=1$
133 132 6 eqtr3d ${⊢}{\phi }\to 1={P}{A}+{Y}{B}$
134 66 63 133 mvrraddd ${⊢}{\phi }\to 1-{Y}{B}={P}{A}$
135 134 negeqd ${⊢}{\phi }\to -\left(1-{Y}{B}\right)=-{P}{A}$
136 65 135 eqtr3d ${⊢}{\phi }\to {Y}{B}-1=-{P}{A}$
137 62 136 breqtrrd ${⊢}{\phi }\to {P}\parallel \left({Y}{B}-1\right)$
138 23 peano2zd ${⊢}{\phi }\to {Y}{B}+1\in ℤ$
139 peano2zm ${⊢}{Y}{B}\in ℤ\to {Y}{B}-1\in ℤ$
140 23 139 syl ${⊢}{\phi }\to {Y}{B}-1\in ℤ$
141 dvdsmultr2 ${⊢}\left({P}\in ℤ\wedge {Y}{B}+1\in ℤ\wedge {Y}{B}-1\in ℤ\right)\to \left({P}\parallel \left({Y}{B}-1\right)\to {P}\parallel \left({Y}{B}+1\right)\left({Y}{B}-1\right)\right)$
142 11 138 140 141 syl3anc ${⊢}{\phi }\to \left({P}\parallel \left({Y}{B}-1\right)\to {P}\parallel \left({Y}{B}+1\right)\left({Y}{B}-1\right)\right)$
143 137 142 mpd ${⊢}{\phi }\to {P}\parallel \left({Y}{B}+1\right)\left({Y}{B}-1\right)$
144 sq1 ${⊢}{1}^{2}=1$
145 144 oveq2i ${⊢}{{Y}{B}}^{2}-{1}^{2}={{Y}{B}}^{2}-1$
146 subsq ${⊢}\left({Y}{B}\in ℂ\wedge 1\in ℂ\right)\to {{Y}{B}}^{2}-{1}^{2}=\left({Y}{B}+1\right)\left({Y}{B}-1\right)$
147 63 35 146 sylancl ${⊢}{\phi }\to {{Y}{B}}^{2}-{1}^{2}=\left({Y}{B}+1\right)\left({Y}{B}-1\right)$
148 145 147 syl5eqr ${⊢}{\phi }\to {{Y}{B}}^{2}-1=\left({Y}{B}+1\right)\left({Y}{B}-1\right)$
149 143 148 breqtrrd ${⊢}{\phi }\to {P}\parallel \left({{Y}{B}}^{2}-1\right)$
150 dvdsadd2b ${⊢}\left({P}\in ℤ\wedge {{X}{B}}^{2}+1\in ℤ\wedge \left({{Y}{B}}^{2}-1\in ℤ\wedge {P}\parallel \left({{Y}{B}}^{2}-1\right)\right)\right)\to \left({P}\parallel \left({{X}{B}}^{2}+1\right)↔{P}\parallel \left(\left({{Y}{B}}^{2}-1\right)+{{X}{B}}^{2}+1\right)\right)$
151 11 31 27 149 150 syl112anc ${⊢}{\phi }\to \left({P}\parallel \left({{X}{B}}^{2}+1\right)↔{P}\parallel \left(\left({{Y}{B}}^{2}-1\right)+{{X}{B}}^{2}+1\right)\right)$
152 56 151 mpbird ${⊢}{\phi }\to {P}\parallel \left({{X}{B}}^{2}+1\right)$
153 subneg ${⊢}\left({{X}{B}}^{2}\in ℂ\wedge 1\in ℂ\right)\to {{X}{B}}^{2}--1={{X}{B}}^{2}+1$
154 34 35 153 sylancl ${⊢}{\phi }\to {{X}{B}}^{2}--1={{X}{B}}^{2}+1$
155 152 154 breqtrrd ${⊢}{\phi }\to {P}\parallel \left({{X}{B}}^{2}--1\right)$
156 oveq1 ${⊢}{x}={X}{B}\to {{x}}^{2}={{X}{B}}^{2}$
157 156 oveq1d ${⊢}{x}={X}{B}\to {{x}}^{2}--1={{X}{B}}^{2}--1$
158 157 breq2d ${⊢}{x}={X}{B}\to \left({P}\parallel \left({{x}}^{2}--1\right)↔{P}\parallel \left({{X}{B}}^{2}--1\right)\right)$
159 158 rspcev ${⊢}\left({X}{B}\in ℤ\wedge {P}\parallel \left({{X}{B}}^{2}--1\right)\right)\to \exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}{P}\parallel \left({{x}}^{2}--1\right)$
160 17 155 159 syl2anc ${⊢}{\phi }\to \exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}{P}\parallel \left({{x}}^{2}--1\right)$
161 neg1z ${⊢}-1\in ℤ$
162 eldifsn ${⊢}{P}\in \left(ℙ\setminus \left\{2\right\}\right)↔\left({P}\in ℙ\wedge {P}\ne 2\right)$
163 1 162 sylibr ${⊢}{\phi }\to {P}\in \left(ℙ\setminus \left\{2\right\}\right)$
164 lgsqr ${⊢}\left(-1\in ℤ\wedge {P}\in \left(ℙ\setminus \left\{2\right\}\right)\right)\to \left(-1{/}_{L}{P}=1↔\left(¬{P}\parallel -1\wedge \exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}{P}\parallel \left({{x}}^{2}--1\right)\right)\right)$
165 161 163 164 sylancr ${⊢}{\phi }\to \left(-1{/}_{L}{P}=1↔\left(¬{P}\parallel -1\wedge \exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}{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(ℙ\setminus \left\{2\right\}\right)\to \left(-1{/}_{L}{P}=1↔{P}\mathrm{mod}4=1\right)$
168 163 167 syl ${⊢}{\phi }\to \left(-1{/}_{L}{P}=1↔{P}\mathrm{mod}4=1\right)$
169 166 168 mpbid ${⊢}{\phi }\to {P}\mathrm{mod}4=1$