Theorem gzcn 16854

Description: A gaussian integer is a complex number. (Contributed by Mario Carneiro, 14-Jul-2014.)

Assertion

Ref	Expression
gzcn	⊢ (𝐴 ∈ ℤ[i] → 𝐴 ∈ ℂ)

Proof of Theorem gzcn

Step	Hyp	Ref	Expression
1		elgz 16853	. 2 ⊢ (𝐴 ∈ ℤ[i] ↔ (𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ℤ ∧ (ℑ‘𝐴) ∈ ℤ))
2	1	simp1bi 1145	1 ⊢ (𝐴 ∈ ℤ[i] → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2113  ‘cfv 6489  ℂcc 11014  ℤcz 12478  ℜcre 15014  ℑcim 15015  ℤ[i]cgz 16851

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-iota 6445  df-fv 6497  df-gz 16852

This theorem is referenced by:  gznegcl  16857  gzcjcl  16858  gzaddcl  16859  gzmulcl  16860  gzsubcl  16862  gzabssqcl  16863  4sqlem4a  16873  4sqlem4  16874  mul4sqlem  16875  mul4sq  16876  4sqlem12  16878  4sqlem17  16883  gzsubrg  21368  gzrngunitlem  21379  gzrngunit  21380  2sqlem2  27366  mul2sq  27367  2sqlem3  27368  cntotbnd  37846