Metamath Proof Explorer

Theorem 4sqlem3

Description: Lemma for 4sq . Sufficient condition to be in S . (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 4sqlem3 
|- ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 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 eqid 
 |-  ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) )
3 oveq1 
 |-  ( c = C -> ( c ^ 2 ) = ( C ^ 2 ) )
4 3 oveq1d 
 |-  ( c = C -> ( ( c ^ 2 ) + ( d ^ 2 ) ) = ( ( C ^ 2 ) + ( d ^ 2 ) ) )
5 4 oveq2d 
 |-  ( c = C -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( d ^ 2 ) ) ) )
6 5 eqeq2d 
 |-  ( c = C -> ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) <-> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( d ^ 2 ) ) ) ) )
7 oveq1 
 |-  ( d = D -> ( d ^ 2 ) = ( D ^ 2 ) )
8 7 oveq2d 
 |-  ( d = D -> ( ( C ^ 2 ) + ( d ^ 2 ) ) = ( ( C ^ 2 ) + ( D ^ 2 ) ) )
9 8 oveq2d 
 |-  ( d = D -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( d ^ 2 ) ) ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) )
10 9 eqeq2d 
 |-  ( d = D -> ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( d ^ 2 ) ) ) <-> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) ) )
11 6 10 rspc2ev 
 |-  ( ( C e. ZZ /\ D e. ZZ /\ ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) ) -> E. c e. ZZ E. d e. ZZ ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) )
12 2 11 mp3an3 
 |-  ( ( C e. ZZ /\ D e. ZZ ) -> E. c e. ZZ E. d e. ZZ ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) )
13 oveq1 
 |-  ( a = A -> ( a ^ 2 ) = ( A ^ 2 ) )
14 13 oveq1d 
 |-  ( a = A -> ( ( a ^ 2 ) + ( b ^ 2 ) ) = ( ( A ^ 2 ) + ( b ^ 2 ) ) )
15 14 oveq1d 
 |-  ( a = A -> ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) = ( ( ( A ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) )
16 15 eqeq2d 
 |-  ( a = A -> ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) = ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) <-> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) = ( ( ( A ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) ) )
17 16 2rexbidv 
 |-  ( a = A -> ( E. c e. ZZ E. d e. ZZ ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) = ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) <-> E. c e. ZZ E. d e. ZZ ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) = ( ( ( A ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) ) )
18 oveq1 
 |-  ( b = B -> ( b ^ 2 ) = ( B ^ 2 ) )
19 18 oveq2d 
 |-  ( b = B -> ( ( A ^ 2 ) + ( b ^ 2 ) ) = ( ( A ^ 2 ) + ( B ^ 2 ) ) )
20 19 oveq1d 
 |-  ( b = B -> ( ( ( A ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) )
21 20 eqeq2d 
 |-  ( b = B -> ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) = ( ( ( A ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) <-> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) ) )
22 21 2rexbidv 
 |-  ( b = B -> ( E. c e. ZZ E. d e. ZZ ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) = ( ( ( A ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) <-> E. c e. ZZ E. d e. ZZ ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) ) )
23 17 22 rspc2ev 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ E. c e. ZZ E. d e. ZZ ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) ) -> E. a e. ZZ E. b e. ZZ E. c e. ZZ E. d e. ZZ ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) = ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) )
24 23 3expa 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ E. c e. ZZ E. d e. ZZ ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) ) -> E. a e. ZZ E. b e. ZZ E. c e. ZZ E. d e. ZZ ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) = ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) )
25 1 4sqlem2 
 |-  ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) e. S <-> E. a e. ZZ E. b e. ZZ E. c e. ZZ E. d e. ZZ ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) = ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) )
26 24 25 sylibr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ E. c e. ZZ E. d e. ZZ ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) e. S )
27 12 26 sylan2 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) e. S )