Metamath Proof Explorer

Theorem 4sqlem4a

Description: Lemma for 4sqlem4 . (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 4sqlem4a ⊢ A ∈ ℤ i ∧ B ∈ ℤ i → A 2 + B 2 ∈ S

Proof

Step Hyp Ref Expression
1 4sq.1 ⊢ S = n | ∃ x ∈ ℤ ∃ y ∈ ℤ ∃ z ∈ ℤ ∃ w ∈ ℤ n = x 2 + y 2 + z 2 + w 2
2 gzcn ⊢ A ∈ ℤ i → A ∈ ℂ
3 2 absvalsq2d ⊢ A ∈ ℤ i → A 2 = ℜ ⁡ A 2 + ℑ ⁡ A 2
4 gzcn ⊢ B ∈ ℤ i → B ∈ ℂ
5 4 absvalsq2d ⊢ B ∈ ℤ i → B 2 = ℜ ⁡ B 2 + ℑ ⁡ B 2
6 3 5 oveqan12d ⊢ A ∈ ℤ i ∧ B ∈ ℤ i → A 2 + B 2 = ℜ ⁡ A 2 + ℑ ⁡ A 2 + ℜ ⁡ B 2 + ℑ ⁡ B 2
7 elgz ⊢ A ∈ ℤ i ↔ A ∈ ℂ ∧ ℜ ⁡ A ∈ ℤ ∧ ℑ ⁡ A ∈ ℤ
8 7 simp2bi ⊢ A ∈ ℤ i → ℜ ⁡ A ∈ ℤ
9 7 simp3bi ⊢ A ∈ ℤ i → ℑ ⁡ A ∈ ℤ
10 8 9 jca ⊢ A ∈ ℤ i → ℜ ⁡ A ∈ ℤ ∧ ℑ ⁡ A ∈ ℤ
11 elgz ⊢ B ∈ ℤ i ↔ B ∈ ℂ ∧ ℜ ⁡ B ∈ ℤ ∧ ℑ ⁡ B ∈ ℤ
12 11 simp2bi ⊢ B ∈ ℤ i → ℜ ⁡ B ∈ ℤ
13 11 simp3bi ⊢ B ∈ ℤ i → ℑ ⁡ B ∈ ℤ
14 12 13 jca ⊢ B ∈ ℤ i → ℜ ⁡ B ∈ ℤ ∧ ℑ ⁡ B ∈ ℤ
15 1 4sqlem3 ⊢ ℜ ⁡ A ∈ ℤ ∧ ℑ ⁡ A ∈ ℤ ∧ ℜ ⁡ B ∈ ℤ ∧ ℑ ⁡ B ∈ ℤ → ℜ ⁡ A 2 + ℑ ⁡ A 2 + ℜ ⁡ B 2 + ℑ ⁡ B 2 ∈ S
16 10 14 15 syl2an ⊢ A ∈ ℤ i ∧ B ∈ ℤ i → ℜ ⁡ A 2 + ℑ ⁡ A 2 + ℜ ⁡ B 2 + ℑ ⁡ B 2 ∈ S
17 6 16 eqeltrd ⊢ A ∈ ℤ i ∧ B ∈ ℤ i → A 2 + B 2 ∈ S