Metamath Proof Explorer

Theorem 2sqlem8a

Description: Lemma for 2sqlem8 . (Contributed by Mario Carneiro, 4-Jun-2016)

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 )
2sqlem8.n 
|- ( ph -> N e. NN )
2sqlem8.m 
|- ( ph -> M e. ( ZZ>= ` 2 ) )
2sqlem8.1 
|- ( ph -> A e. ZZ )
2sqlem8.2 
|- ( ph -> B e. ZZ )
2sqlem8.3 
|- ( ph -> ( A gcd B ) = 1 )
2sqlem8.4 
|- ( ph -> N = ( ( A ^ 2 ) + ( B ^ 2 ) ) )
2sqlem8.c 
|- C = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )
2sqlem8.d 
|- D = ( ( ( B + ( M / 2 ) ) mod M ) - ( M / 2 ) )
Assertion 2sqlem8a 
|- ( ph -> ( C gcd D ) e. NN )

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 2sqlem8.n 
 |-  ( ph -> N e. NN )
6 2sqlem8.m 
 |-  ( ph -> M e. ( ZZ>= ` 2 ) )
7 2sqlem8.1 
 |-  ( ph -> A e. ZZ )
8 2sqlem8.2 
 |-  ( ph -> B e. ZZ )
9 2sqlem8.3 
 |-  ( ph -> ( A gcd B ) = 1 )
10 2sqlem8.4 
 |-  ( ph -> N = ( ( A ^ 2 ) + ( B ^ 2 ) ) )
11 2sqlem8.c 
 |-  C = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )
12 2sqlem8.d 
 |-  D = ( ( ( B + ( M / 2 ) ) mod M ) - ( M / 2 ) )
13 eluz2b3 
 |-  ( M e. ( ZZ>= ` 2 ) <-> ( M e. NN /\ M =/= 1 ) )
14 6 13 sylib 
 |-  ( ph -> ( M e. NN /\ M =/= 1 ) )
15 14 simpld 
 |-  ( ph -> M e. NN )
16 7 15 11 4sqlem5 
 |-  ( ph -> ( C e. ZZ /\ ( ( A - C ) / M ) e. ZZ ) )
17 16 simpld 
 |-  ( ph -> C e. ZZ )
18 8 15 12 4sqlem5 
 |-  ( ph -> ( D e. ZZ /\ ( ( B - D ) / M ) e. ZZ ) )
19 18 simpld 
 |-  ( ph -> D e. ZZ )
20 14 simprd 
 |-  ( ph -> M =/= 1 )
21 simpr 
 |-  ( ( ph /\ ( C ^ 2 ) = 0 ) -> ( C ^ 2 ) = 0 )
22 7 15 11 21 4sqlem9 
 |-  ( ( ph /\ ( C ^ 2 ) = 0 ) -> ( M ^ 2 ) || ( A ^ 2 ) )
23 22 ex 
 |-  ( ph -> ( ( C ^ 2 ) = 0 -> ( M ^ 2 ) || ( A ^ 2 ) ) )
24 eluzelz 
 |-  ( M e. ( ZZ>= ` 2 ) -> M e. ZZ )
25 6 24 syl 
 |-  ( ph -> M e. ZZ )
26 dvdssq 
 |-  ( ( M e. ZZ /\ A e. ZZ ) -> ( M || A <-> ( M ^ 2 ) || ( A ^ 2 ) ) )
27 25 7 26 syl2anc 
 |-  ( ph -> ( M || A <-> ( M ^ 2 ) || ( A ^ 2 ) ) )
28 23 27 sylibrd 
 |-  ( ph -> ( ( C ^ 2 ) = 0 -> M || A ) )
29 simpr 
 |-  ( ( ph /\ ( D ^ 2 ) = 0 ) -> ( D ^ 2 ) = 0 )
30 8 15 12 29 4sqlem9 
 |-  ( ( ph /\ ( D ^ 2 ) = 0 ) -> ( M ^ 2 ) || ( B ^ 2 ) )
31 30 ex 
 |-  ( ph -> ( ( D ^ 2 ) = 0 -> ( M ^ 2 ) || ( B ^ 2 ) ) )
32 dvdssq 
 |-  ( ( M e. ZZ /\ B e. ZZ ) -> ( M || B <-> ( M ^ 2 ) || ( B ^ 2 ) ) )
33 25 8 32 syl2anc 
 |-  ( ph -> ( M || B <-> ( M ^ 2 ) || ( B ^ 2 ) ) )
34 31 33 sylibrd 
 |-  ( ph -> ( ( D ^ 2 ) = 0 -> M || B ) )
35 ax-1ne0 
 |-  1 =/= 0
36 35 a1i 
 |-  ( ph -> 1 =/= 0 )
37 9 36 eqnetrd 
 |-  ( ph -> ( A gcd B ) =/= 0 )
38 37 neneqd 
 |-  ( ph -> -. ( A gcd B ) = 0 )
39 gcdeq0 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) = 0 <-> ( A = 0 /\ B = 0 ) ) )
40 7 8 39 syl2anc 
 |-  ( ph -> ( ( A gcd B ) = 0 <-> ( A = 0 /\ B = 0 ) ) )
41 38 40 mtbid 
 |-  ( ph -> -. ( A = 0 /\ B = 0 ) )
42 dvdslegcd 
 |-  ( ( ( M e. ZZ /\ A e. ZZ /\ B e. ZZ ) /\ -. ( A = 0 /\ B = 0 ) ) -> ( ( M || A /\ M || B ) -> M <_ ( A gcd B ) ) )
43 25 7 8 41 42 syl31anc 
 |-  ( ph -> ( ( M || A /\ M || B ) -> M <_ ( A gcd B ) ) )
44 28 34 43 syl2and 
 |-  ( ph -> ( ( ( C ^ 2 ) = 0 /\ ( D ^ 2 ) = 0 ) -> M <_ ( A gcd B ) ) )
45 9 breq2d 
 |-  ( ph -> ( M <_ ( A gcd B ) <-> M <_ 1 ) )
46 nnle1eq1 
 |-  ( M e. NN -> ( M <_ 1 <-> M = 1 ) )
47 15 46 syl 
 |-  ( ph -> ( M <_ 1 <-> M = 1 ) )
48 45 47 bitrd 
 |-  ( ph -> ( M <_ ( A gcd B ) <-> M = 1 ) )
49 44 48 sylibd 
 |-  ( ph -> ( ( ( C ^ 2 ) = 0 /\ ( D ^ 2 ) = 0 ) -> M = 1 ) )
50 49 necon3ad 
 |-  ( ph -> ( M =/= 1 -> -. ( ( C ^ 2 ) = 0 /\ ( D ^ 2 ) = 0 ) ) )
51 20 50 mpd 
 |-  ( ph -> -. ( ( C ^ 2 ) = 0 /\ ( D ^ 2 ) = 0 ) )
52 17 zcnd 
 |-  ( ph -> C e. CC )
53 sqeq0 
 |-  ( C e. CC -> ( ( C ^ 2 ) = 0 <-> C = 0 ) )
54 52 53 syl 
 |-  ( ph -> ( ( C ^ 2 ) = 0 <-> C = 0 ) )
55 19 zcnd 
 |-  ( ph -> D e. CC )
56 sqeq0 
 |-  ( D e. CC -> ( ( D ^ 2 ) = 0 <-> D = 0 ) )
57 55 56 syl 
 |-  ( ph -> ( ( D ^ 2 ) = 0 <-> D = 0 ) )
58 54 57 anbi12d 
 |-  ( ph -> ( ( ( C ^ 2 ) = 0 /\ ( D ^ 2 ) = 0 ) <-> ( C = 0 /\ D = 0 ) ) )
59 51 58 mtbid 
 |-  ( ph -> -. ( C = 0 /\ D = 0 ) )
60 gcdn0cl 
 |-  ( ( ( C e. ZZ /\ D e. ZZ ) /\ -. ( C = 0 /\ D = 0 ) ) -> ( C gcd D ) e. NN )
61 17 19 59 60 syl21anc 
 |-  ( ph -> ( C gcd D ) e. NN )