Metamath Proof Explorer

Theorem 2sqlem2

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

Ref Expression
Hypothesis 2sq.1 
|- S = ran ( w e. Z[i] |-> ( ( abs ` w ) ^ 2 ) )
Assertion 2sqlem2 
|- ( A e. S <-> E. x e. ZZ E. y e. ZZ A = ( ( x ^ 2 ) + ( y ^ 2 ) ) )

Proof

Step Hyp Ref Expression
1 2sq.1 
 |-  S = ran ( w e. Z[i] |-> ( ( abs ` w ) ^ 2 ) )
2 1 2sqlem1 
 |-  ( A e. S <-> E. z e. Z[i] A = ( ( abs ` z ) ^ 2 ) )
3 elgz 
 |-  ( z e. Z[i] <-> ( z e. CC /\ ( Re ` z ) e. ZZ /\ ( Im ` z ) e. ZZ ) )
4 3 simp2bi 
 |-  ( z e. Z[i] -> ( Re ` z ) e. ZZ )
5 3 simp3bi 
 |-  ( z e. Z[i] -> ( Im ` z ) e. ZZ )
6 gzcn 
 |-  ( z e. Z[i] -> z e. CC )
7 6 absvalsq2d 
 |-  ( z e. Z[i] -> ( ( abs ` z ) ^ 2 ) = ( ( ( Re ` z ) ^ 2 ) + ( ( Im ` z ) ^ 2 ) ) )
8 oveq1 
 |-  ( x = ( Re ` z ) -> ( x ^ 2 ) = ( ( Re ` z ) ^ 2 ) )
9 8 oveq1d 
 |-  ( x = ( Re ` z ) -> ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( ( ( Re ` z ) ^ 2 ) + ( y ^ 2 ) ) )
10 9 eqeq2d 
 |-  ( x = ( Re ` z ) -> ( ( ( abs ` z ) ^ 2 ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) <-> ( ( abs ` z ) ^ 2 ) = ( ( ( Re ` z ) ^ 2 ) + ( y ^ 2 ) ) ) )
11 oveq1 
 |-  ( y = ( Im ` z ) -> ( y ^ 2 ) = ( ( Im ` z ) ^ 2 ) )
12 11 oveq2d 
 |-  ( y = ( Im ` z ) -> ( ( ( Re ` z ) ^ 2 ) + ( y ^ 2 ) ) = ( ( ( Re ` z ) ^ 2 ) + ( ( Im ` z ) ^ 2 ) ) )
13 12 eqeq2d 
 |-  ( y = ( Im ` z ) -> ( ( ( abs ` z ) ^ 2 ) = ( ( ( Re ` z ) ^ 2 ) + ( y ^ 2 ) ) <-> ( ( abs ` z ) ^ 2 ) = ( ( ( Re ` z ) ^ 2 ) + ( ( Im ` z ) ^ 2 ) ) ) )
14 10 13 rspc2ev 
 |-  ( ( ( Re ` z ) e. ZZ /\ ( Im ` z ) e. ZZ /\ ( ( abs ` z ) ^ 2 ) = ( ( ( Re ` z ) ^ 2 ) + ( ( Im ` z ) ^ 2 ) ) ) -> E. x e. ZZ E. y e. ZZ ( ( abs ` z ) ^ 2 ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) )
15 4 5 7 14 syl3anc 
 |-  ( z e. Z[i] -> E. x e. ZZ E. y e. ZZ ( ( abs ` z ) ^ 2 ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) )
16 eqeq1 
 |-  ( A = ( ( abs ` z ) ^ 2 ) -> ( A = ( ( x ^ 2 ) + ( y ^ 2 ) ) <-> ( ( abs ` z ) ^ 2 ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) )
17 16 2rexbidv 
 |-  ( A = ( ( abs ` z ) ^ 2 ) -> ( E. x e. ZZ E. y e. ZZ A = ( ( x ^ 2 ) + ( y ^ 2 ) ) <-> E. x e. ZZ E. y e. ZZ ( ( abs ` z ) ^ 2 ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) )
18 15 17 syl5ibrcom 
 |-  ( z e. Z[i] -> ( A = ( ( abs ` z ) ^ 2 ) -> E. x e. ZZ E. y e. ZZ A = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) )
19 18 rexlimiv 
 |-  ( E. z e. Z[i] A = ( ( abs ` z ) ^ 2 ) -> E. x e. ZZ E. y e. ZZ A = ( ( x ^ 2 ) + ( y ^ 2 ) ) )
20 2 19 sylbi 
 |-  ( A e. S -> E. x e. ZZ E. y e. ZZ A = ( ( x ^ 2 ) + ( y ^ 2 ) ) )
21 gzreim 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( x + ( _i x. y ) ) e. Z[i] )
22 zcn 
 |-  ( x e. ZZ -> x e. CC )
23 ax-icn 
 |-  _i e. CC
24 zcn 
 |-  ( y e. ZZ -> y e. CC )
25 mulcl 
 |-  ( ( _i e. CC /\ y e. CC ) -> ( _i x. y ) e. CC )
26 23 24 25 sylancr 
 |-  ( y e. ZZ -> ( _i x. y ) e. CC )
27 addcl 
 |-  ( ( x e. CC /\ ( _i x. y ) e. CC ) -> ( x + ( _i x. y ) ) e. CC )
28 22 26 27 syl2an 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( x + ( _i x. y ) ) e. CC )
29 28 absvalsq2d 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( ( abs ` ( x + ( _i x. y ) ) ) ^ 2 ) = ( ( ( Re ` ( x + ( _i x. y ) ) ) ^ 2 ) + ( ( Im ` ( x + ( _i x. y ) ) ) ^ 2 ) ) )
30 zre 
 |-  ( x e. ZZ -> x e. RR )
31 zre 
 |-  ( y e. ZZ -> y e. RR )
32 crre 
 |-  ( ( x e. RR /\ y e. RR ) -> ( Re ` ( x + ( _i x. y ) ) ) = x )
33 30 31 32 syl2an 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( Re ` ( x + ( _i x. y ) ) ) = x )
34 33 oveq1d 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( ( Re ` ( x + ( _i x. y ) ) ) ^ 2 ) = ( x ^ 2 ) )
35 crim 
 |-  ( ( x e. RR /\ y e. RR ) -> ( Im ` ( x + ( _i x. y ) ) ) = y )
36 30 31 35 syl2an 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( Im ` ( x + ( _i x. y ) ) ) = y )
37 36 oveq1d 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( ( Im ` ( x + ( _i x. y ) ) ) ^ 2 ) = ( y ^ 2 ) )
38 34 37 oveq12d 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( ( ( Re ` ( x + ( _i x. y ) ) ) ^ 2 ) + ( ( Im ` ( x + ( _i x. y ) ) ) ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) )
39 29 38 eqtr2d 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( ( abs ` ( x + ( _i x. y ) ) ) ^ 2 ) )
40 fveq2 
 |-  ( z = ( x + ( _i x. y ) ) -> ( abs ` z ) = ( abs ` ( x + ( _i x. y ) ) ) )
41 40 oveq1d 
 |-  ( z = ( x + ( _i x. y ) ) -> ( ( abs ` z ) ^ 2 ) = ( ( abs ` ( x + ( _i x. y ) ) ) ^ 2 ) )
42 41 rspceeqv 
 |-  ( ( ( x + ( _i x. y ) ) e. Z[i] /\ ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( ( abs ` ( x + ( _i x. y ) ) ) ^ 2 ) ) -> E. z e. Z[i] ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( ( abs ` z ) ^ 2 ) )
43 21 39 42 syl2anc 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> E. z e. Z[i] ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( ( abs ` z ) ^ 2 ) )
44 1 2sqlem1 
 |-  ( ( ( x ^ 2 ) + ( y ^ 2 ) ) e. S <-> E. z e. Z[i] ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( ( abs ` z ) ^ 2 ) )
45 43 44 sylibr 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( ( x ^ 2 ) + ( y ^ 2 ) ) e. S )
46 eleq1 
 |-  ( A = ( ( x ^ 2 ) + ( y ^ 2 ) ) -> ( A e. S <-> ( ( x ^ 2 ) + ( y ^ 2 ) ) e. S ) )
47 45 46 syl5ibrcom 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( A = ( ( x ^ 2 ) + ( y ^ 2 ) ) -> A e. S ) )
48 47 rexlimivv 
 |-  ( E. x e. ZZ E. y e. ZZ A = ( ( x ^ 2 ) + ( y ^ 2 ) ) -> A e. S )
49 20 48 impbii 
 |-  ( A e. S <-> E. x e. ZZ E. y e. ZZ A = ( ( x ^ 2 ) + ( y ^ 2 ) ) )