Metamath Proof Explorer


Theorem 2sqblem

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

Ref Expression
Hypotheses 2sqb.1 φ P P 2
2sqb.2 φ X Y
2sqb.3 φ P = X 2 + Y 2
2sqb.4 φ A
2sqb.5 φ B
2sqb.6 φ P gcd Y = P A + Y B
Assertion 2sqblem φ P mod 4 = 1

Proof

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