This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 4sq

Description: Lagrange's four-square theorem, or Bachet's conjecture: every nonnegative integer is expressible as a sum of four squares. This is Metamath 100 proof #19. (Contributed by Mario Carneiro, 16-Jul-2014)

Ref Expression
Assertion 4sq 
|- ( A e. NN0 <-> E. a e. ZZ E. b e. ZZ E. c e. ZZ E. d e. ZZ A = ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 eqeq1 
 |-  ( m = n -> ( m = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) <-> n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) ) )
2 1 2rexbidv 
 |-  ( m = n -> ( E. z e. ZZ E. w e. ZZ m = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) <-> E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) ) )
3 2 2rexbidv 
 |-  ( m = n -> ( E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ m = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) <-> 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 ) ) ) ) )
4 3 cbvabv 
 |-  { m | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ m = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) } = { 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 ) ) ) }
5 4 4sqlem19 
 |-  NN0 = { m | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ m = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }
6 5 4sqlem2 
 |-  ( A e. NN0 <-> E. a e. ZZ E. b e. ZZ E. c e. ZZ E. d e. ZZ A = ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) )