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 ⊢ 𝑆 = { 𝑛 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ 𝑛 = ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) + ( ( 𝑧 ↑ 2 ) + ( 𝑤 ↑ 2 ) ) ) }
Assertion 4sqlem1 𝑆 ⊆ ℕ0

Proof

Step Hyp Ref Expression
1 4sq.1 ⊢ 𝑆 = { 𝑛 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ 𝑛 = ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) + ( ( 𝑧 ↑ 2 ) + ( 𝑤 ↑ 2 ) ) ) }
2 zsqcl2 ⊢ ( 𝑥 ∈ ℤ → ( 𝑥 ↑ 2 ) ∈ ℕ0 )
3 zsqcl2 ⊢ ( 𝑦 ∈ ℤ → ( 𝑦 ↑ 2 ) ∈ ℕ0 )
4 nn0addcl ⊢ ( ( ( 𝑥 ↑ 2 ) ∈ ℕ0 ∧ ( 𝑦 ↑ 2 ) ∈ ℕ0 ) → ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ∈ ℕ0 )
5 2 3 4 syl2an ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ∈ ℕ0 )
6 zsqcl2 ⊢ ( 𝑧 ∈ ℤ → ( 𝑧 ↑ 2 ) ∈ ℕ0 )
7 zsqcl2 ⊢ ( 𝑤 ∈ ℤ → ( 𝑤 ↑ 2 ) ∈ ℕ0 )
8 nn0addcl ⊢ ( ( ( 𝑧 ↑ 2 ) ∈ ℕ0 ∧ ( 𝑤 ↑ 2 ) ∈ ℕ0 ) → ( ( 𝑧 ↑ 2 ) + ( 𝑤 ↑ 2 ) ) ∈ ℕ0 )
9 6 7 8 syl2an ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℤ ) → ( ( 𝑧 ↑ 2 ) + ( 𝑤 ↑ 2 ) ) ∈ ℕ0 )
10 nn0addcl ⊢ ( ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ∈ ℕ0 ∧ ( ( 𝑧 ↑ 2 ) + ( 𝑤 ↑ 2 ) ) ∈ ℕ0 ) → ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) + ( ( 𝑧 ↑ 2 ) + ( 𝑤 ↑ 2 ) ) ) ∈ ℕ0 )
11 5 9 10 syl2an ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℤ ) ) → ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) + ( ( 𝑧 ↑ 2 ) + ( 𝑤 ↑ 2 ) ) ) ∈ ℕ0 )
12 eleq1a ⊢ ( ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) + ( ( 𝑧 ↑ 2 ) + ( 𝑤 ↑ 2 ) ) ) ∈ ℕ0 → ( 𝑛 = ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) + ( ( 𝑧 ↑ 2 ) + ( 𝑤 ↑ 2 ) ) ) → 𝑛 ∈ ℕ0 ) )
13 11 12 syl ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℤ ) ) → ( 𝑛 = ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) + ( ( 𝑧 ↑ 2 ) + ( 𝑤 ↑ 2 ) ) ) → 𝑛 ∈ ℕ0 ) )
14 13 rexlimdvva ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ 𝑛 = ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) + ( ( 𝑧 ↑ 2 ) + ( 𝑤 ↑ 2 ) ) ) → 𝑛 ∈ ℕ0 ) )
15 14 rexlimivv ⊢ ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ 𝑛 = ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) + ( ( 𝑧 ↑ 2 ) + ( 𝑤 ↑ 2 ) ) ) → 𝑛 ∈ ℕ0 )
16 15 abssi ⊢ { 𝑛 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ 𝑛 = ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) + ( ( 𝑧 ↑ 2 ) + ( 𝑤 ↑ 2 ) ) ) } ⊆ ℕ0
17 1 16 eqsstri ⊢ 𝑆 ⊆ ℕ0