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