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 \in ℕ_{0} \leftrightarrow \exists a \in ℤ \exists b \in ℤ \exists c \in ℤ \exists d \in ℤ A = a^{2} + b^{2} + c^{2} + d^{2}$

Proof

Step	Hyp	Ref	Expression
1		eqeq1	$⊢ m = n \to (m = x^{2} + y^{2} + z^{2} + w^{2} \leftrightarrow n = x^{2} + y^{2} + z^{2} + w^{2})$
2	1	2rexbidv	$⊢ m = n \to (\exists z \in ℤ \exists w \in ℤ m = x^{2} + y^{2} + z^{2} + w^{2} \leftrightarrow \exists z \in ℤ \exists w \in ℤ n = x^{2} + y^{2} + z^{2} + w^{2})$
3	2	2rexbidv	$⊢ m = n \to (\exists x \in ℤ \exists y \in ℤ \exists z \in ℤ \exists w \in ℤ m = x^{2} + y^{2} + z^{2} + w^{2} \leftrightarrow \exists x \in ℤ \exists y \in ℤ \exists z \in ℤ \exists w \in ℤ n = x^{2} + y^{2} + z^{2} + w^{2})$
4	3	cbvabv	$⊢ \{m \| \exists x \in ℤ \exists y \in ℤ \exists z \in ℤ \exists w \in ℤ m = x^{2} + y^{2} + z^{2} + w^{2}\} = \{n \| \exists x \in ℤ \exists y \in ℤ \exists z \in ℤ \exists w \in ℤ n = x^{2} + y^{2} + z^{2} + w^{2}\}$
5	4	4sqlem19	$⊢ ℕ_{0} = \{m \| \exists x \in ℤ \exists y \in ℤ \exists z \in ℤ \exists w \in ℤ m = x^{2} + y^{2} + z^{2} + w^{2}\}$
6	5	4sqlem2	$⊢ A \in ℕ_{0} \leftrightarrow \exists a \in ℤ \exists b \in ℤ \exists c \in ℤ \exists d \in ℤ A = a^{2} + b^{2} + c^{2} + d^{2}$