Metamath Proof Explorer

Theorem 2sqlem2

Description: Lemma for 2sq . (Contributed by Mario Carneiro, 19-Jun-2015)

Ref Expression
Hypothesis 2sq.1 ⊢ 𝑆 = ran ( 𝑤 ∈ ℤ[i] ↦ ( ( abs ‘ 𝑤 ) ↑ 2 ) )
Assertion 2sqlem2 ( 𝐴 ∈ 𝑆 ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝐴 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )

Proof

Step Hyp Ref Expression
1 2sq.1 ⊢ 𝑆 = ran ( 𝑤 ∈ ℤ[i] ↦ ( ( abs ‘ 𝑤 ) ↑ 2 ) )
2 1 2sqlem1 ⊢ ( 𝐴 ∈ 𝑆 ↔ ∃ 𝑧 ∈ ℤ[i] 𝐴 = ( ( abs ‘ 𝑧 ) ↑ 2 ) )
3 elgz ⊢ ( 𝑧 ∈ ℤ[i] ↔ ( 𝑧 ∈ ℂ ∧ ( ℜ ‘ 𝑧 ) ∈ ℤ ∧ ( ℑ ‘ 𝑧 ) ∈ ℤ ) )
4 3 simp2bi ⊢ ( 𝑧 ∈ ℤ[i] → ( ℜ ‘ 𝑧 ) ∈ ℤ )
5 3 simp3bi ⊢ ( 𝑧 ∈ ℤ[i] → ( ℑ ‘ 𝑧 ) ∈ ℤ )
6 gzcn ⊢ ( 𝑧 ∈ ℤ[i] → 𝑧 ∈ ℂ )
7 6 absvalsq2d ⊢ ( 𝑧 ∈ ℤ[i] → ( ( abs ‘ 𝑧 ) ↑ 2 ) = ( ( ( ℜ ‘ 𝑧 ) ↑ 2 ) + ( ( ℑ ‘ 𝑧 ) ↑ 2 ) ) )
8 oveq1 ⊢ ( 𝑥 = ( ℜ ‘ 𝑧 ) → ( 𝑥 ↑ 2 ) = ( ( ℜ ‘ 𝑧 ) ↑ 2 ) )
9 8 oveq1d ⊢ ( 𝑥 = ( ℜ ‘ 𝑧 ) → ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( ( ( ℜ ‘ 𝑧 ) ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )
10 9 eqeq2d ⊢ ( 𝑥 = ( ℜ ‘ 𝑧 ) → ( ( ( abs ‘ 𝑧 ) ↑ 2 ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ↔ ( ( abs ‘ 𝑧 ) ↑ 2 ) = ( ( ( ℜ ‘ 𝑧 ) ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) )
11 oveq1 ⊢ ( 𝑦 = ( ℑ ‘ 𝑧 ) → ( 𝑦 ↑ 2 ) = ( ( ℑ ‘ 𝑧 ) ↑ 2 ) )
12 11 oveq2d ⊢ ( 𝑦 = ( ℑ ‘ 𝑧 ) → ( ( ( ℜ ‘ 𝑧 ) ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( ( ( ℜ ‘ 𝑧 ) ↑ 2 ) + ( ( ℑ ‘ 𝑧 ) ↑ 2 ) ) )
13 12 eqeq2d ⊢ ( 𝑦 = ( ℑ ‘ 𝑧 ) → ( ( ( abs ‘ 𝑧 ) ↑ 2 ) = ( ( ( ℜ ‘ 𝑧 ) ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ↔ ( ( abs ‘ 𝑧 ) ↑ 2 ) = ( ( ( ℜ ‘ 𝑧 ) ↑ 2 ) + ( ( ℑ ‘ 𝑧 ) ↑ 2 ) ) ) )
14 10 13 rspc2ev ⊢ ( ( ( ℜ ‘ 𝑧 ) ∈ ℤ ∧ ( ℑ ‘ 𝑧 ) ∈ ℤ ∧ ( ( abs ‘ 𝑧 ) ↑ 2 ) = ( ( ( ℜ ‘ 𝑧 ) ↑ 2 ) + ( ( ℑ ‘ 𝑧 ) ↑ 2 ) ) ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( abs ‘ 𝑧 ) ↑ 2 ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )
15 4 5 7 14 syl3anc ⊢ ( 𝑧 ∈ ℤ[i] → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( abs ‘ 𝑧 ) ↑ 2 ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )
16 eqeq1 ⊢ ( 𝐴 = ( ( abs ‘ 𝑧 ) ↑ 2 ) → ( 𝐴 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ↔ ( ( abs ‘ 𝑧 ) ↑ 2 ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) )
17 16 2rexbidv ⊢ ( 𝐴 = ( ( abs ‘ 𝑧 ) ↑ 2 ) → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝐴 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( ( abs ‘ 𝑧 ) ↑ 2 ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) )
18 15 17 syl5ibrcom ⊢ ( 𝑧 ∈ ℤ[i] → ( 𝐴 = ( ( abs ‘ 𝑧 ) ↑ 2 ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝐴 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ) )
19 18 rexlimiv ⊢ ( ∃ 𝑧 ∈ ℤ[i] 𝐴 = ( ( abs ‘ 𝑧 ) ↑ 2 ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝐴 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )
20 2 19 sylbi ⊢ ( 𝐴 ∈ 𝑆 → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝐴 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )
21 gzreim ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑥 + ( i · 𝑦 ) ) ∈ ℤ[i] )
22 zcn ⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
23 ax-icn ⊢ i ∈ ℂ
24 zcn ⊢ ( 𝑦 ∈ ℤ → 𝑦 ∈ ℂ )
25 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( i · 𝑦 ) ∈ ℂ )
26 23 24 25 sylancr ⊢ ( 𝑦 ∈ ℤ → ( i · 𝑦 ) ∈ ℂ )
27 addcl ⊢ ( ( 𝑥 ∈ ℂ ∧ ( i · 𝑦 ) ∈ ℂ ) → ( 𝑥 + ( i · 𝑦 ) ) ∈ ℂ )
28 22 26 27 syl2an ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑥 + ( i · 𝑦 ) ) ∈ ℂ )
29 28 absvalsq2d ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( abs ‘ ( 𝑥 + ( i · 𝑦 ) ) ) ↑ 2 ) = ( ( ( ℜ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) ↑ 2 ) + ( ( ℑ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) ↑ 2 ) ) )
30 zre ⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℝ )
31 zre ⊢ ( 𝑦 ∈ ℤ → 𝑦 ∈ ℝ )
32 crre ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ℜ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) = 𝑥 )
33 30 31 32 syl2an ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ℜ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) = 𝑥 )
34 33 oveq1d ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( ℜ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) ↑ 2 ) = ( 𝑥 ↑ 2 ) )
35 crim ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ℑ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) = 𝑦 )
36 30 31 35 syl2an ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ℑ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) = 𝑦 )
37 36 oveq1d ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( ℑ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) ↑ 2 ) = ( 𝑦 ↑ 2 ) )
38 34 37 oveq12d ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( ( ℜ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) ↑ 2 ) + ( ( ℑ ‘ ( 𝑥 + ( i · 𝑦 ) ) ) ↑ 2 ) ) = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )
39 29 38 eqtr2d ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( ( abs ‘ ( 𝑥 + ( i · 𝑦 ) ) ) ↑ 2 ) )
40 fveq2 ⊢ ( 𝑧 = ( 𝑥 + ( i · 𝑦 ) ) → ( abs ‘ 𝑧 ) = ( abs ‘ ( 𝑥 + ( i · 𝑦 ) ) ) )
41 40 oveq1d ⊢ ( 𝑧 = ( 𝑥 + ( i · 𝑦 ) ) → ( ( abs ‘ 𝑧 ) ↑ 2 ) = ( ( abs ‘ ( 𝑥 + ( i · 𝑦 ) ) ) ↑ 2 ) )
42 41 rspceeqv ⊢ ( ( ( 𝑥 + ( i · 𝑦 ) ) ∈ ℤ[i] ∧ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( ( abs ‘ ( 𝑥 + ( i · 𝑦 ) ) ) ↑ 2 ) ) → ∃ 𝑧 ∈ ℤ[i] ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( ( abs ‘ 𝑧 ) ↑ 2 ) )
43 21 39 42 syl2anc ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ∃ 𝑧 ∈ ℤ[i] ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( ( abs ‘ 𝑧 ) ↑ 2 ) )
44 1 2sqlem1 ⊢ ( ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ∈ 𝑆 ↔ ∃ 𝑧 ∈ ℤ[i] ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) = ( ( abs ‘ 𝑧 ) ↑ 2 ) )
45 43 44 sylibr ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ∈ 𝑆 )
46 eleq1 ⊢ ( 𝐴 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) → ( 𝐴 ∈ 𝑆 ↔ ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) ∈ 𝑆 ) )
47 45 46 syl5ibrcom ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝐴 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) → 𝐴 ∈ 𝑆 ) )
48 47 rexlimivv ⊢ ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝐴 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) → 𝐴 ∈ 𝑆 )
49 20 48 impbii ⊢ ( 𝐴 ∈ 𝑆 ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ 𝐴 = ( ( 𝑥 ↑ 2 ) + ( 𝑦 ↑ 2 ) ) )