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	⊢ ( 𝐴 ∈ ℕ0 ↔ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ 𝐴 = ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqeq1	⊢ ( 𝑚 = 𝑛 → ( 𝑚 = ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) + ( ( 𝑧 ↑ 2 ) + ( 𝑤 ↑ 2 ) ) ) ↔ 𝑛 = ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) + ( ( 𝑧 ↑ 2 ) + ( 𝑤 ↑ 2 ) ) ) ) )
2	1	2rexbidv	⊢ ( 𝑚 = 𝑛 → ( ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ 𝑚 = ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) + ( ( 𝑧 ↑ 2 ) + ( 𝑤 ↑ 2 ) ) ) ↔ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ 𝑛 = ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) + ( ( 𝑧 ↑ 2 ) + ( 𝑤 ↑ 2 ) ) ) ) )
3	2	2rexbidv	⊢ ( 𝑚 = 𝑛 → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ 𝑚 = ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) + ( ( 𝑧 ↑ 2 ) + ( 𝑤 ↑ 2 ) ) ) ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ 𝑛 = ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) + ( ( 𝑧 ↑ 2 ) + ( 𝑤 ↑ 2 ) ) ) ) )
4	3	cbvabv	⊢ { 𝑚 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ 𝑚 = ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) + ( ( 𝑧 ↑ 2 ) + ( 𝑤 ↑ 2 ) ) ) } = { 𝑛 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ 𝑛 = ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) + ( ( 𝑧 ↑ 2 ) + ( 𝑤 ↑ 2 ) ) ) }
5	4	4sqlem19	⊢ ℕ0 = { 𝑚 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ 𝑚 = ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) + ( ( 𝑧 ↑ 2 ) + ( 𝑤 ↑ 2 ) ) ) }
6	5	4sqlem2	⊢ ( 𝐴 ∈ ℕ0 ↔ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ∃ 𝑐 ∈ ℤ ∃ 𝑑 ∈ ℤ 𝐴 = ( ( ( 𝑎 ↑ 2 ) + ( 𝑏 ↑ 2 ) ) + ( ( 𝑐 ↑ 2 ) + ( 𝑑 ↑ 2 ) ) ) )