Metamath Proof Explorer

Theorem 4sqlem4a

Description: Lemma for 4sqlem4 . (Contributed by Mario Carneiro, 14-Jul-2014)

Ref Expression
Hypothesis 4sq.1 
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }
Assertion 4sqlem4a 
|- ( ( A e. Z[i] /\ B e. Z[i] ) -> ( ( ( abs ` A ) ^ 2 ) + ( ( abs ` B ) ^ 2 ) ) e. S )

Proof

Step Hyp Ref Expression
1 4sq.1 
 |-  S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }
2 gzcn 
 |-  ( A e. Z[i] -> A e. CC )
3 2 absvalsq2d 
 |-  ( A e. Z[i] -> ( ( abs ` A ) ^ 2 ) = ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) )
4 gzcn 
 |-  ( B e. Z[i] -> B e. CC )
5 4 absvalsq2d 
 |-  ( B e. Z[i] -> ( ( abs ` B ) ^ 2 ) = ( ( ( Re ` B ) ^ 2 ) + ( ( Im ` B ) ^ 2 ) ) )
6 3 5 oveqan12d 
 |-  ( ( A e. Z[i] /\ B e. Z[i] ) -> ( ( ( abs ` A ) ^ 2 ) + ( ( abs ` B ) ^ 2 ) ) = ( ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) + ( ( ( Re ` B ) ^ 2 ) + ( ( Im ` B ) ^ 2 ) ) ) )
7 elgz 
 |-  ( A e. Z[i] <-> ( A e. CC /\ ( Re ` A ) e. ZZ /\ ( Im ` A ) e. ZZ ) )
8 7 simp2bi 
 |-  ( A e. Z[i] -> ( Re ` A ) e. ZZ )
9 7 simp3bi 
 |-  ( A e. Z[i] -> ( Im ` A ) e. ZZ )
10 8 9 jca 
 |-  ( A e. Z[i] -> ( ( Re ` A ) e. ZZ /\ ( Im ` A ) e. ZZ ) )
11 elgz 
 |-  ( B e. Z[i] <-> ( B e. CC /\ ( Re ` B ) e. ZZ /\ ( Im ` B ) e. ZZ ) )
12 11 simp2bi 
 |-  ( B e. Z[i] -> ( Re ` B ) e. ZZ )
13 11 simp3bi 
 |-  ( B e. Z[i] -> ( Im ` B ) e. ZZ )
14 12 13 jca 
 |-  ( B e. Z[i] -> ( ( Re ` B ) e. ZZ /\ ( Im ` B ) e. ZZ ) )
15 1 4sqlem3 
 |-  ( ( ( ( Re ` A ) e. ZZ /\ ( Im ` A ) e. ZZ ) /\ ( ( Re ` B ) e. ZZ /\ ( Im ` B ) e. ZZ ) ) -> ( ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) + ( ( ( Re ` B ) ^ 2 ) + ( ( Im ` B ) ^ 2 ) ) ) e. S )
16 10 14 15 syl2an 
 |-  ( ( A e. Z[i] /\ B e. Z[i] ) -> ( ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) + ( ( ( Re ` B ) ^ 2 ) + ( ( Im ` B ) ^ 2 ) ) ) e. S )
17 6 16 eqeltrd 
 |-  ( ( A e. Z[i] /\ B e. Z[i] ) -> ( ( ( abs ` A ) ^ 2 ) + ( ( abs ` B ) ^ 2 ) ) e. S )