Metamath Proof Explorer

Theorem 2sqlem9

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

Ref Expression
Hypotheses 2sq.1 
|- S = ran ( w e. Z[i] |-> ( ( abs ` w ) ^ 2 ) )
2sqlem7.2 
|- Y = { z | E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) }
2sqlem9.5 
|- ( ph -> A. b e. ( 1 ... ( M - 1 ) ) A. a e. Y ( b || a -> b e. S ) )
2sqlem9.7 
|- ( ph -> M || N )
2sqlem9.6 
|- ( ph -> M e. NN )
2sqlem9.4 
|- ( ph -> N e. Y )
Assertion 2sqlem9 
|- ( ph -> M e. S )

Proof

Step Hyp Ref Expression
1 2sq.1 
 |-  S = ran ( w e. Z[i] |-> ( ( abs ` w ) ^ 2 ) )
2 2sqlem7.2 
 |-  Y = { z | E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) }
3 2sqlem9.5 
 |-  ( ph -> A. b e. ( 1 ... ( M - 1 ) ) A. a e. Y ( b || a -> b e. S ) )
4 2sqlem9.7 
 |-  ( ph -> M || N )
5 2sqlem9.6 
 |-  ( ph -> M e. NN )
6 2sqlem9.4 
 |-  ( ph -> N e. Y )
7 eqeq1 
 |-  ( z = N -> ( z = ( ( x ^ 2 ) + ( y ^ 2 ) ) <-> N = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) )
8 7 anbi2d 
 |-  ( z = N -> ( ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) <-> ( ( x gcd y ) = 1 /\ N = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) )
9 8 2rexbidv 
 |-  ( z = N -> ( E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) <-> E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ N = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) )
10 oveq1 
 |-  ( x = u -> ( x gcd y ) = ( u gcd y ) )
11 10 eqeq1d 
 |-  ( x = u -> ( ( x gcd y ) = 1 <-> ( u gcd y ) = 1 ) )
12 oveq1 
 |-  ( x = u -> ( x ^ 2 ) = ( u ^ 2 ) )
13 12 oveq1d 
 |-  ( x = u -> ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( ( u ^ 2 ) + ( y ^ 2 ) ) )
14 13 eqeq2d 
 |-  ( x = u -> ( N = ( ( x ^ 2 ) + ( y ^ 2 ) ) <-> N = ( ( u ^ 2 ) + ( y ^ 2 ) ) ) )
15 11 14 anbi12d 
 |-  ( x = u -> ( ( ( x gcd y ) = 1 /\ N = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) <-> ( ( u gcd y ) = 1 /\ N = ( ( u ^ 2 ) + ( y ^ 2 ) ) ) ) )
16 oveq2 
 |-  ( y = v -> ( u gcd y ) = ( u gcd v ) )
17 16 eqeq1d 
 |-  ( y = v -> ( ( u gcd y ) = 1 <-> ( u gcd v ) = 1 ) )
18 oveq1 
 |-  ( y = v -> ( y ^ 2 ) = ( v ^ 2 ) )
19 18 oveq2d 
 |-  ( y = v -> ( ( u ^ 2 ) + ( y ^ 2 ) ) = ( ( u ^ 2 ) + ( v ^ 2 ) ) )
20 19 eqeq2d 
 |-  ( y = v -> ( N = ( ( u ^ 2 ) + ( y ^ 2 ) ) <-> N = ( ( u ^ 2 ) + ( v ^ 2 ) ) ) )
21 17 20 anbi12d 
 |-  ( y = v -> ( ( ( u gcd y ) = 1 /\ N = ( ( u ^ 2 ) + ( y ^ 2 ) ) ) <-> ( ( u gcd v ) = 1 /\ N = ( ( u ^ 2 ) + ( v ^ 2 ) ) ) ) )
22 15 21 cbvrex2vw 
 |-  ( E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ N = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) <-> E. u e. ZZ E. v e. ZZ ( ( u gcd v ) = 1 /\ N = ( ( u ^ 2 ) + ( v ^ 2 ) ) ) )
23 9 22 bitrdi 
 |-  ( z = N -> ( E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) <-> E. u e. ZZ E. v e. ZZ ( ( u gcd v ) = 1 /\ N = ( ( u ^ 2 ) + ( v ^ 2 ) ) ) ) )
24 23 2 elab2g 
 |-  ( N e. Y -> ( N e. Y <-> E. u e. ZZ E. v e. ZZ ( ( u gcd v ) = 1 /\ N = ( ( u ^ 2 ) + ( v ^ 2 ) ) ) ) )
25 24 ibi 
 |-  ( N e. Y -> E. u e. ZZ E. v e. ZZ ( ( u gcd v ) = 1 /\ N = ( ( u ^ 2 ) + ( v ^ 2 ) ) ) )
26 6 25 syl 
 |-  ( ph -> E. u e. ZZ E. v e. ZZ ( ( u gcd v ) = 1 /\ N = ( ( u ^ 2 ) + ( v ^ 2 ) ) ) )
27 simpr 
 |-  ( ( ( ( ph /\ ( u e. ZZ /\ v e. ZZ ) ) /\ ( ( u gcd v ) = 1 /\ N = ( ( u ^ 2 ) + ( v ^ 2 ) ) ) ) /\ M = 1 ) -> M = 1 )
28 1z 
 |-  1 e. ZZ
29 zgz 
 |-  ( 1 e. ZZ -> 1 e. Z[i] )
30 28 29 ax-mp 
 |-  1 e. Z[i]
31 sq1 
 |-  ( 1 ^ 2 ) = 1
32 31 eqcomi 
 |-  1 = ( 1 ^ 2 )
33 fveq2 
 |-  ( x = 1 -> ( abs ` x ) = ( abs ` 1 ) )
34 abs1 
 |-  ( abs ` 1 ) = 1
35 33 34 eqtrdi 
 |-  ( x = 1 -> ( abs ` x ) = 1 )
36 35 oveq1d 
 |-  ( x = 1 -> ( ( abs ` x ) ^ 2 ) = ( 1 ^ 2 ) )
37 36 rspceeqv 
 |-  ( ( 1 e. Z[i] /\ 1 = ( 1 ^ 2 ) ) -> E. x e. Z[i] 1 = ( ( abs ` x ) ^ 2 ) )
38 30 32 37 mp2an 
 |-  E. x e. Z[i] 1 = ( ( abs ` x ) ^ 2 )
39 1 2sqlem1 
 |-  ( 1 e. S <-> E. x e. Z[i] 1 = ( ( abs ` x ) ^ 2 ) )
40 38 39 mpbir 
 |-  1 e. S
41 27 40 eqeltrdi 
 |-  ( ( ( ( ph /\ ( u e. ZZ /\ v e. ZZ ) ) /\ ( ( u gcd v ) = 1 /\ N = ( ( u ^ 2 ) + ( v ^ 2 ) ) ) ) /\ M = 1 ) -> M e. S )
42 3 ad2antrr 
 |-  ( ( ( ph /\ ( u e. ZZ /\ v e. ZZ ) ) /\ ( ( ( u gcd v ) = 1 /\ N = ( ( u ^ 2 ) + ( v ^ 2 ) ) ) /\ M =/= 1 ) ) -> A. b e. ( 1 ... ( M - 1 ) ) A. a e. Y ( b || a -> b e. S ) )
43 4 ad2antrr 
 |-  ( ( ( ph /\ ( u e. ZZ /\ v e. ZZ ) ) /\ ( ( ( u gcd v ) = 1 /\ N = ( ( u ^ 2 ) + ( v ^ 2 ) ) ) /\ M =/= 1 ) ) -> M || N )
44 1 2 2sqlem7 
 |-  Y C_ ( S i^i NN )
45 inss2 
 |-  ( S i^i NN ) C_ NN
46 44 45 sstri 
 |-  Y C_ NN
47 46 6 sseldi 
 |-  ( ph -> N e. NN )
48 47 ad2antrr 
 |-  ( ( ( ph /\ ( u e. ZZ /\ v e. ZZ ) ) /\ ( ( ( u gcd v ) = 1 /\ N = ( ( u ^ 2 ) + ( v ^ 2 ) ) ) /\ M =/= 1 ) ) -> N e. NN )
49 5 ad2antrr 
 |-  ( ( ( ph /\ ( u e. ZZ /\ v e. ZZ ) ) /\ ( ( ( u gcd v ) = 1 /\ N = ( ( u ^ 2 ) + ( v ^ 2 ) ) ) /\ M =/= 1 ) ) -> M e. NN )
50 simprr 
 |-  ( ( ( ph /\ ( u e. ZZ /\ v e. ZZ ) ) /\ ( ( ( u gcd v ) = 1 /\ N = ( ( u ^ 2 ) + ( v ^ 2 ) ) ) /\ M =/= 1 ) ) -> M =/= 1 )
51 eluz2b3 
 |-  ( M e. ( ZZ>= ` 2 ) <-> ( M e. NN /\ M =/= 1 ) )
52 49 50 51 sylanbrc 
 |-  ( ( ( ph /\ ( u e. ZZ /\ v e. ZZ ) ) /\ ( ( ( u gcd v ) = 1 /\ N = ( ( u ^ 2 ) + ( v ^ 2 ) ) ) /\ M =/= 1 ) ) -> M e. ( ZZ>= ` 2 ) )
53 simplrl 
 |-  ( ( ( ph /\ ( u e. ZZ /\ v e. ZZ ) ) /\ ( ( ( u gcd v ) = 1 /\ N = ( ( u ^ 2 ) + ( v ^ 2 ) ) ) /\ M =/= 1 ) ) -> u e. ZZ )
54 simplrr 
 |-  ( ( ( ph /\ ( u e. ZZ /\ v e. ZZ ) ) /\ ( ( ( u gcd v ) = 1 /\ N = ( ( u ^ 2 ) + ( v ^ 2 ) ) ) /\ M =/= 1 ) ) -> v e. ZZ )
55 simprll 
 |-  ( ( ( ph /\ ( u e. ZZ /\ v e. ZZ ) ) /\ ( ( ( u gcd v ) = 1 /\ N = ( ( u ^ 2 ) + ( v ^ 2 ) ) ) /\ M =/= 1 ) ) -> ( u gcd v ) = 1 )
56 simprlr 
 |-  ( ( ( ph /\ ( u e. ZZ /\ v e. ZZ ) ) /\ ( ( ( u gcd v ) = 1 /\ N = ( ( u ^ 2 ) + ( v ^ 2 ) ) ) /\ M =/= 1 ) ) -> N = ( ( u ^ 2 ) + ( v ^ 2 ) ) )
57 eqid 
 |-  ( ( ( u + ( M / 2 ) ) mod M ) - ( M / 2 ) ) = ( ( ( u + ( M / 2 ) ) mod M ) - ( M / 2 ) )
58 eqid 
 |-  ( ( ( v + ( M / 2 ) ) mod M ) - ( M / 2 ) ) = ( ( ( v + ( M / 2 ) ) mod M ) - ( M / 2 ) )
59 eqid 
 |-  ( ( ( ( u + ( M / 2 ) ) mod M ) - ( M / 2 ) ) / ( ( ( ( u + ( M / 2 ) ) mod M ) - ( M / 2 ) ) gcd ( ( ( v + ( M / 2 ) ) mod M ) - ( M / 2 ) ) ) ) = ( ( ( ( u + ( M / 2 ) ) mod M ) - ( M / 2 ) ) / ( ( ( ( u + ( M / 2 ) ) mod M ) - ( M / 2 ) ) gcd ( ( ( v + ( M / 2 ) ) mod M ) - ( M / 2 ) ) ) )
60 eqid 
 |-  ( ( ( ( v + ( M / 2 ) ) mod M ) - ( M / 2 ) ) / ( ( ( ( u + ( M / 2 ) ) mod M ) - ( M / 2 ) ) gcd ( ( ( v + ( M / 2 ) ) mod M ) - ( M / 2 ) ) ) ) = ( ( ( ( v + ( M / 2 ) ) mod M ) - ( M / 2 ) ) / ( ( ( ( u + ( M / 2 ) ) mod M ) - ( M / 2 ) ) gcd ( ( ( v + ( M / 2 ) ) mod M ) - ( M / 2 ) ) ) )
61 1 2 42 43 48 52 53 54 55 56 57 58 59 60 2sqlem8 
 |-  ( ( ( ph /\ ( u e. ZZ /\ v e. ZZ ) ) /\ ( ( ( u gcd v ) = 1 /\ N = ( ( u ^ 2 ) + ( v ^ 2 ) ) ) /\ M =/= 1 ) ) -> M e. S )
62 61 anassrs 
 |-  ( ( ( ( ph /\ ( u e. ZZ /\ v e. ZZ ) ) /\ ( ( u gcd v ) = 1 /\ N = ( ( u ^ 2 ) + ( v ^ 2 ) ) ) ) /\ M =/= 1 ) -> M e. S )
63 41 62 pm2.61dane 
 |-  ( ( ( ph /\ ( u e. ZZ /\ v e. ZZ ) ) /\ ( ( u gcd v ) = 1 /\ N = ( ( u ^ 2 ) + ( v ^ 2 ) ) ) ) -> M e. S )
64 63 ex 
 |-  ( ( ph /\ ( u e. ZZ /\ v e. ZZ ) ) -> ( ( ( u gcd v ) = 1 /\ N = ( ( u ^ 2 ) + ( v ^ 2 ) ) ) -> M e. S ) )
65 64 rexlimdvva 
 |-  ( ph -> ( E. u e. ZZ E. v e. ZZ ( ( u gcd v ) = 1 /\ N = ( ( u ^ 2 ) + ( v ^ 2 ) ) ) -> M e. S ) )
66 26 65 mpd 
 |-  ( ph -> M e. S )