Theorem gzcn 16903

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

Syntax hints:   → wi 4   ∈ wcel 2109  ‘cfv 6511  ℂcc 11066  ℤcz 12529  ℜcre 15063  ℑcim 15064  ℤ[i]cgz 16900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-gz 16901

This theorem is referenced by:  gznegcl  16906  gzcjcl  16907  gzaddcl  16908  gzmulcl  16909  gzsubcl  16911  gzabssqcl  16912  4sqlem4a  16922  4sqlem4  16923  mul4sqlem  16924  mul4sq  16925  4sqlem12  16927  4sqlem17  16932  gzsubrg  21338  gzrngunitlem  21349  gzrngunit  21350  2sqlem2  27329  mul2sq  27330  2sqlem3  27331  cntotbnd  37790