Metamath Proof Explorer

Theorem 2sqblem

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

Ref Expression
Hypotheses 2sqb.1 
|- ( ph -> ( P e. Prime /\ P =/= 2 ) )
2sqb.2 
|- ( ph -> ( X e. ZZ /\ Y e. ZZ ) )
2sqb.3 
|- ( ph -> P = ( ( X ^ 2 ) + ( Y ^ 2 ) ) )
2sqb.4 
|- ( ph -> A e. ZZ )
2sqb.5 
|- ( ph -> B e. ZZ )
2sqb.6 
|- ( ph -> ( P gcd Y ) = ( ( P x. A ) + ( Y x. B ) ) )
Assertion 2sqblem 
|- ( ph -> ( P mod 4 ) = 1 )

Proof

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