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

Metamath Proof Explorer

Theorem 4sqlem1

Description: Lemma for 4sq . The set S is the set of all numbers that are expressible as a sum of four squares. Our goal is to show that S = NN0 ; here we show one subset direction. (Contributed by Mario Carneiro, 14-Jul-2014)

Ref Expression
Hypothesis 4sq.1 ⊢ S = n | ∃ x ∈ ℤ ∃ y ∈ ℤ ∃ z ∈ ℤ ∃ w ∈ ℤ n = x 2 + y 2 + z 2 + w 2
Assertion 4sqlem1 ⊢ S ⊆ ℕ 0

Proof

Step Hyp Ref Expression
1 4sq.1 ⊢ S = n | ∃ x ∈ ℤ ∃ y ∈ ℤ ∃ z ∈ ℤ ∃ w ∈ ℤ n = x 2 + y 2 + z 2 + w 2
2 zsqcl2 ⊢ x ∈ ℤ → x 2 ∈ ℕ 0
3 zsqcl2 ⊢ y ∈ ℤ → y 2 ∈ ℕ 0
4 nn0addcl ⊢ x 2 ∈ ℕ 0 ∧ y 2 ∈ ℕ 0 → x 2 + y 2 ∈ ℕ 0
5 2 3 4 syl2an ⊢ x ∈ ℤ ∧ y ∈ ℤ → x 2 + y 2 ∈ ℕ 0
6 zsqcl2 ⊢ z ∈ ℤ → z 2 ∈ ℕ 0
7 zsqcl2 ⊢ w ∈ ℤ → w 2 ∈ ℕ 0
8 nn0addcl ⊢ z 2 ∈ ℕ 0 ∧ w 2 ∈ ℕ 0 → z 2 + w 2 ∈ ℕ 0
9 6 7 8 syl2an ⊢ z ∈ ℤ ∧ w ∈ ℤ → z 2 + w 2 ∈ ℕ 0
10 nn0addcl ⊢ x 2 + y 2 ∈ ℕ 0 ∧ z 2 + w 2 ∈ ℕ 0 → x 2 + y 2 + z 2 + w 2 ∈ ℕ 0
11 5 9 10 syl2an ⊢ x ∈ ℤ ∧ y ∈ ℤ ∧ z ∈ ℤ ∧ w ∈ ℤ → x 2 + y 2 + z 2 + w 2 ∈ ℕ 0
12 eleq1a ⊢ x 2 + y 2 + z 2 + w 2 ∈ ℕ 0 → n = x 2 + y 2 + z 2 + w 2 → n ∈ ℕ 0
13 11 12 syl ⊢ x ∈ ℤ ∧ y ∈ ℤ ∧ z ∈ ℤ ∧ w ∈ ℤ → n = x 2 + y 2 + z 2 + w 2 → n ∈ ℕ 0
14 13 rexlimdvva ⊢ x ∈ ℤ ∧ y ∈ ℤ → ∃ z ∈ ℤ ∃ w ∈ ℤ n = x 2 + y 2 + z 2 + w 2 → n ∈ ℕ 0
15 14 rexlimivv ⊢ ∃ x ∈ ℤ ∃ y ∈ ℤ ∃ z ∈ ℤ ∃ w ∈ ℤ n = x 2 + y 2 + z 2 + w 2 → n ∈ ℕ 0
16 15 abssi ⊢ n | ∃ x ∈ ℤ ∃ y ∈ ℤ ∃ z ∈ ℤ ∃ w ∈ ℤ n = x 2 + y 2 + z 2 + w 2 ⊆ ℕ 0
17 1 16 eqsstri ⊢ S ⊆ ℕ 0