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

Metamath Proof Explorer

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 ) ) ∈ 𝑆 )