Metamath Proof Explorer

Theorem 4sqlem1

Description: Lemma for 4sq . The set S is the set of all numbers that are expressible as a sum of four squares. Our goal is to show that S = NN0 ; here we show one subset direction. (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 4sqlem1 
|- S C_ NN0

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 zsqcl2 
 |-  ( x e. ZZ -> ( x ^ 2 ) e. NN0 )
3 zsqcl2 
 |-  ( y e. ZZ -> ( y ^ 2 ) e. NN0 )
4 nn0addcl 
 |-  ( ( ( x ^ 2 ) e. NN0 /\ ( y ^ 2 ) e. NN0 ) -> ( ( x ^ 2 ) + ( y ^ 2 ) ) e. NN0 )
5 2 3 4 syl2an 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( ( x ^ 2 ) + ( y ^ 2 ) ) e. NN0 )
6 zsqcl2 
 |-  ( z e. ZZ -> ( z ^ 2 ) e. NN0 )
7 zsqcl2 
 |-  ( w e. ZZ -> ( w ^ 2 ) e. NN0 )
8 nn0addcl 
 |-  ( ( ( z ^ 2 ) e. NN0 /\ ( w ^ 2 ) e. NN0 ) -> ( ( z ^ 2 ) + ( w ^ 2 ) ) e. NN0 )
9 6 7 8 syl2an 
 |-  ( ( z e. ZZ /\ w e. ZZ ) -> ( ( z ^ 2 ) + ( w ^ 2 ) ) e. NN0 )
10 nn0addcl 
 |-  ( ( ( ( x ^ 2 ) + ( y ^ 2 ) ) e. NN0 /\ ( ( z ^ 2 ) + ( w ^ 2 ) ) e. NN0 ) -> ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) e. NN0 )
11 5 9 10 syl2an 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( z e. ZZ /\ w e. ZZ ) ) -> ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) e. NN0 )
12 eleq1a 
 |-  ( ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) e. NN0 -> ( n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) -> n e. NN0 ) )
13 11 12 syl 
 |-  ( ( ( x e. ZZ /\ y e. ZZ ) /\ ( z e. ZZ /\ w e. ZZ ) ) -> ( n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) -> n e. NN0 ) )
14 13 rexlimdvva 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) -> n e. NN0 ) )
15 14 rexlimivv 
 |-  ( 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 ) ) ) -> n e. NN0 )
16 15 abssi 
 |-  { 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 ) ) ) } C_ NN0
17 1 16 eqsstri 
 |-  S C_ NN0