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 eqtr3id ⊢ φ → 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