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 ( 𝐴 ∈ ℕ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 ) ) ) )