Metamath Proof Explorer

Theorem 2sqlem7

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 ) ) ) }
Assertion 2sqlem7 
|- Y C_ ( S i^i 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 simpr 
 |-  ( ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> z = ( ( x ^ 2 ) + ( y ^ 2 ) ) )
4 3 reximi 
 |-  ( E. y e. ZZ ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> E. y e. ZZ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) )
5 4 reximi 
 |-  ( 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 z = ( ( x ^ 2 ) + ( y ^ 2 ) ) )
6 1 2sqlem2 
 |-  ( z e. S <-> E. x e. ZZ E. y e. ZZ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) )
7 5 6 sylibr 
 |-  ( E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> z e. S )
8 ax-1ne0 
 |-  1 =/= 0
9 gcdeq0 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( ( x gcd y ) = 0 <-> ( x = 0 /\ y = 0 ) ) )
10 9 adantr 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( x gcd y ) = 1 ) -> ( ( x gcd y ) = 0 <-> ( x = 0 /\ y = 0 ) ) )
11 simpr 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( x gcd y ) = 1 ) -> ( x gcd y ) = 1 )
12 11 eqeq1d 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( x gcd y ) = 1 ) -> ( ( x gcd y ) = 0 <-> 1 = 0 ) )
13 10 12 bitr3d 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( x gcd y ) = 1 ) -> ( ( x = 0 /\ y = 0 ) <-> 1 = 0 ) )
14 13 necon3bbid 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( x gcd y ) = 1 ) -> ( -. ( x = 0 /\ y = 0 ) <-> 1 =/= 0 ) )
15 8 14 mpbiri 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( x gcd y ) = 1 ) -> -. ( x = 0 /\ y = 0 ) )
16 zsqcl2 
 |-  ( x e. ZZ -> ( x ^ 2 ) e. NN0 )
17 16 ad2antrr 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( x gcd y ) = 1 ) -> ( x ^ 2 ) e. NN0 )
18 17 nn0red 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( x gcd y ) = 1 ) -> ( x ^ 2 ) e. RR )
19 17 nn0ge0d 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( x gcd y ) = 1 ) -> 0 <_ ( x ^ 2 ) )
20 zsqcl2 
 |-  ( y e. ZZ -> ( y ^ 2 ) e. NN0 )
21 20 ad2antlr 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( x gcd y ) = 1 ) -> ( y ^ 2 ) e. NN0 )
22 21 nn0red 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( x gcd y ) = 1 ) -> ( y ^ 2 ) e. RR )
23 21 nn0ge0d 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( x gcd y ) = 1 ) -> 0 <_ ( y ^ 2 ) )
24 add20 
 |-  ( ( ( ( x ^ 2 ) e. RR /\ 0 <_ ( x ^ 2 ) ) /\ ( ( y ^ 2 ) e. RR /\ 0 <_ ( y ^ 2 ) ) ) -> ( ( ( x ^ 2 ) + ( y ^ 2 ) ) = 0 <-> ( ( x ^ 2 ) = 0 /\ ( y ^ 2 ) = 0 ) ) )
25 18 19 22 23 24 syl22anc 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( x gcd y ) = 1 ) -> ( ( ( x ^ 2 ) + ( y ^ 2 ) ) = 0 <-> ( ( x ^ 2 ) = 0 /\ ( y ^ 2 ) = 0 ) ) )
26 zcn 
 |-  ( x e. ZZ -> x e. CC )
27 26 ad2antrr 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( x gcd y ) = 1 ) -> x e. CC )
28 zcn 
 |-  ( y e. ZZ -> y e. CC )
29 28 ad2antlr 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( x gcd y ) = 1 ) -> y e. CC )
30 sqeq0 
 |-  ( x e. CC -> ( ( x ^ 2 ) = 0 <-> x = 0 ) )
31 sqeq0 
 |-  ( y e. CC -> ( ( y ^ 2 ) = 0 <-> y = 0 ) )
32 30 31 bi2anan9 
 |-  ( ( x e. CC /\ y e. CC ) -> ( ( ( x ^ 2 ) = 0 /\ ( y ^ 2 ) = 0 ) <-> ( x = 0 /\ y = 0 ) ) )
33 27 29 32 syl2anc 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( x gcd y ) = 1 ) -> ( ( ( x ^ 2 ) = 0 /\ ( y ^ 2 ) = 0 ) <-> ( x = 0 /\ y = 0 ) ) )
34 25 33 bitrd 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( x gcd y ) = 1 ) -> ( ( ( x ^ 2 ) + ( y ^ 2 ) ) = 0 <-> ( x = 0 /\ y = 0 ) ) )
35 15 34 mtbird 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( x gcd y ) = 1 ) -> -. ( ( x ^ 2 ) + ( y ^ 2 ) ) = 0 )
36 nn0addcl 
 |-  ( ( ( x ^ 2 ) e. NN0 /\ ( y ^ 2 ) e. NN0 ) -> ( ( x ^ 2 ) + ( y ^ 2 ) ) e. NN0 )
37 16 20 36 syl2an 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( ( x ^ 2 ) + ( y ^ 2 ) ) e. NN0 )
38 37 adantr 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( x gcd y ) = 1 ) -> ( ( x ^ 2 ) + ( y ^ 2 ) ) e. NN0 )
39 elnn0 
 |-  ( ( ( x ^ 2 ) + ( y ^ 2 ) ) e. NN0 <-> ( ( ( x ^ 2 ) + ( y ^ 2 ) ) e. NN \/ ( ( x ^ 2 ) + ( y ^ 2 ) ) = 0 ) )
40 38 39 sylib 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( x gcd y ) = 1 ) -> ( ( ( x ^ 2 ) + ( y ^ 2 ) ) e. NN \/ ( ( x ^ 2 ) + ( y ^ 2 ) ) = 0 ) )
41 40 ord 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( x gcd y ) = 1 ) -> ( -. ( ( x ^ 2 ) + ( y ^ 2 ) ) e. NN -> ( ( x ^ 2 ) + ( y ^ 2 ) ) = 0 ) )
42 35 41 mt3d 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( x gcd y ) = 1 ) -> ( ( x ^ 2 ) + ( y ^ 2 ) ) e. NN )
43 eleq1 
 |-  ( z = ( ( x ^ 2 ) + ( y ^ 2 ) ) -> ( z e. NN <-> ( ( x ^ 2 ) + ( y ^ 2 ) ) e. NN ) )
44 42 43 syl5ibrcom 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( x gcd y ) = 1 ) -> ( z = ( ( x ^ 2 ) + ( y ^ 2 ) ) -> z e. NN ) )
45 44 expimpd 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> z e. NN ) )
46 45 rexlimivv 
 |-  ( E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> z e. NN )
47 7 46 elind 
 |-  ( E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) -> z e. ( S i^i NN ) )
48 47 abssi 
 |-  { z | E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) } C_ ( S i^i NN )
49 2 48 eqsstri 
 |-  Y C_ ( S i^i NN )