Theorem 4sqlem4a

Description: Lemma for 4sqlem4 . (Contributed by Mario Carneiro, 14-Jul-2014)

	Ref	Expression
Hypothesis	4sq.1	⊢ 𝑆 = { 𝑛 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ 𝑛 = ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) + ( ( 𝑧 ↑ 2 ) + ( 𝑤 ↑ 2 ) ) ) }
Assertion	4sqlem4a	⊢ ( ( 𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i] ) → ( ( ( abs ‘ 𝐴 ) ↑ 2 ) + ( ( abs ‘ 𝐵 ) ↑ 2 ) ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		4sq.1	⊢ 𝑆 = { 𝑛 ∣ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℤ 𝑛 = ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) + ( ( 𝑧 ↑ 2 ) + ( 𝑤 ↑ 2 ) ) ) }
2		gzcn	⊢ ( 𝐴 ∈ ℤ[i] → 𝐴 ∈ ℂ )
3	2	absvalsq2d	⊢ ( 𝐴 ∈ ℤ[i] → ( ( abs ‘ 𝐴 ) ↑ 2 ) = ( ( ( ℜ ‘ 𝐴 ) ↑ 2 ) + ( ( ℑ ‘ 𝐴 ) ↑ 2 ) ) )
4		gzcn	⊢ ( 𝐵 ∈ ℤ[i] → 𝐵 ∈ ℂ )
5	4	absvalsq2d	⊢ ( 𝐵 ∈ ℤ[i] → ( ( abs ‘ 𝐵 ) ↑ 2 ) = ( ( ( ℜ ‘ 𝐵 ) ↑ 2 ) + ( ( ℑ ‘ 𝐵 ) ↑ 2 ) ) )
6	3 5	oveqan12d	⊢ ( ( 𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i] ) → ( ( ( abs ‘ 𝐴 ) ↑ 2 ) + ( ( abs ‘ 𝐵 ) ↑ 2 ) ) = ( ( ( ( ℜ ‘ 𝐴 ) ↑ 2 ) + ( ( ℑ ‘ 𝐴 ) ↑ 2 ) ) + ( ( ( ℜ ‘ 𝐵 ) ↑ 2 ) + ( ( ℑ ‘ 𝐵 ) ↑ 2 ) ) ) )
7		elgz	⊢ ( 𝐴 ∈ ℤ[i] ↔ ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ℤ ∧ ( ℑ ‘ 𝐴 ) ∈ ℤ ) )
8	7	simp2bi	⊢ ( 𝐴 ∈ ℤ[i] → ( ℜ ‘ 𝐴 ) ∈ ℤ )
9	7	simp3bi	⊢ ( 𝐴 ∈ ℤ[i] → ( ℑ ‘ 𝐴 ) ∈ ℤ )
10	8 9	jca	⊢ ( 𝐴 ∈ ℤ[i] → ( ( ℜ ‘ 𝐴 ) ∈ ℤ ∧ ( ℑ ‘ 𝐴 ) ∈ ℤ ) )
11		elgz	⊢ ( 𝐵 ∈ ℤ[i] ↔ ( 𝐵 ∈ ℂ ∧ ( ℜ ‘ 𝐵 ) ∈ ℤ ∧ ( ℑ ‘ 𝐵 ) ∈ ℤ ) )
12	11	simp2bi	⊢ ( 𝐵 ∈ ℤ[i] → ( ℜ ‘ 𝐵 ) ∈ ℤ )
13	11	simp3bi	⊢ ( 𝐵 ∈ ℤ[i] → ( ℑ ‘ 𝐵 ) ∈ ℤ )
14	12 13	jca	⊢ ( 𝐵 ∈ ℤ[i] → ( ( ℜ ‘ 𝐵 ) ∈ ℤ ∧ ( ℑ ‘ 𝐵 ) ∈ ℤ ) )
15	1	4sqlem3	⊢ ( ( ( ( ℜ ‘ 𝐴 ) ∈ ℤ ∧ ( ℑ ‘ 𝐴 ) ∈ ℤ ) ∧ ( ( ℜ ‘ 𝐵 ) ∈ ℤ ∧ ( ℑ ‘ 𝐵 ) ∈ ℤ ) ) → ( ( ( ( ℜ ‘ 𝐴 ) ↑ 2 ) + ( ( ℑ ‘ 𝐴 ) ↑ 2 ) ) + ( ( ( ℜ ‘ 𝐵 ) ↑ 2 ) + ( ( ℑ ‘ 𝐵 ) ↑ 2 ) ) ) ∈ 𝑆 )
16	10 14 15	syl2an	⊢ ( ( 𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i] ) → ( ( ( ( ℜ ‘ 𝐴 ) ↑ 2 ) + ( ( ℑ ‘ 𝐴 ) ↑ 2 ) ) + ( ( ( ℜ ‘ 𝐵 ) ↑ 2 ) + ( ( ℑ ‘ 𝐵 ) ↑ 2 ) ) ) ∈ 𝑆 )
17	6 16	eqeltrd	⊢ ( ( 𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i] ) → ( ( ( abs ‘ 𝐴 ) ↑ 2 ) + ( ( abs ‘ 𝐵 ) ↑ 2 ) ) ∈ 𝑆 )