Theorem gzcn 16970

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 16969	. 2 ⊢ (𝐴 ∈ ℤ[i] ↔ (𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ℤ ∧ (ℑ‘𝐴) ∈ ℤ))
2	1	simp1bi 1159	1 ⊢ (𝐴 ∈ ℤ[i] → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2144  ‘cfv 6523  ℂcc 11073  ℤcz 12570  ℜcre 15126  ℑcim 15127  ℤ[i]cgz 16967

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5103  df-iota 6479  df-fv 6531  df-gz 16968

This theorem is referenced by:  gznegcl  16973  gzcjcl  16974  gzaddcl  16975  gzmulcl  16976  gzsubcl  16978  gzabssqcl  16979  4sqlem4a  16989  4sqlem4  16990  mul4sqlem  16991  mul4sq  16992  4sqlem12  16994  4sqlem17  16999  gzsubrg  21475  gzrngunitlem  21486  gzrngunit  21487  2sqlem2  27484  mul2sq  27485  2sqlem3  27486  cntotbnd  38300