Theorem gzcn 16992

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

Syntax hints:   → wi 4   ∈ wcel 2149  ‘cfv 6537  ℂcc 11098  ℤcz 12591  ℜcre 15148  ℑcim 15149  ℤ[i]cgz 16989

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3423  df-v 3463  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4491  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5112  df-iota 6493  df-fv 6545  df-gz 16990

This theorem is referenced by:  gznegcl  16995  gzcjcl  16996  gzaddcl  16997  gzmulcl  16998  gzsubcl  17000  gzabssqcl  17001  4sqlem4a  17011  4sqlem4  17012  mul4sqlem  17013  mul4sq  17014  4sqlem12  17016  4sqlem17  17021  gzsubrg  21540  gzrngunitlem  21551  gzrngunit  21552  2sqlem2  27548  mul2sq  27549  2sqlem3  27550  cntotbnd  38370