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 ∈ ℕ 0 ↔ ∃ a ∈ ℤ ∃ b ∈ ℤ ∃ c ∈ ℤ ∃ d ∈ ℤ 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 → ∃ z ∈ ℤ ∃ w ∈ ℤ m = x 2 + y 2 + z 2 + w 2 ↔ ∃ z ∈ ℤ ∃ w ∈ ℤ n = x 2 + y 2 + z 2 + w 2
3 2 2rexbidv ⊢ m = n → ∃ x ∈ ℤ ∃ y ∈ ℤ ∃ z ∈ ℤ ∃ w ∈ ℤ m = x 2 + y 2 + z 2 + w 2 ↔ ∃ x ∈ ℤ ∃ y ∈ ℤ ∃ z ∈ ℤ ∃ w ∈ ℤ n = x 2 + y 2 + z 2 + w 2
4 3 cbvabv ⊢ m | ∃ x ∈ ℤ ∃ y ∈ ℤ ∃ z ∈ ℤ ∃ w ∈ ℤ m = x 2 + y 2 + z 2 + w 2 = n | ∃ x ∈ ℤ ∃ y ∈ ℤ ∃ z ∈ ℤ ∃ w ∈ ℤ n = x 2 + y 2 + z 2 + w 2
5 4 4sqlem19 ⊢ ℕ 0 = m | ∃ x ∈ ℤ ∃ y ∈ ℤ ∃ z ∈ ℤ ∃ w ∈ ℤ m = x 2 + y 2 + z 2 + w 2
6 5 4sqlem2 ⊢ A ∈ ℕ 0 ↔ ∃ a ∈ ℤ ∃ b ∈ ℤ ∃ c ∈ ℤ ∃ d ∈ ℤ A = a 2 + b 2 + c 2 + d 2