Theorem gzcn 17110

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ‘cfv 6538  ℂcc 11198  ℤcz 12693  ℜcre 15264  ℑcim 15265  ℤ[i]cgz 17107

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-gz 17108

This theorem is used by:  gznegcl  17113  gzcjcl  17114  gzaddcl  17115  gzmulcl  17116  gzsubcl  17118  gzabssqcl  17119  4sqlem4a  17129  4sqlem4  17130  mul4sqlem  17131  mul4sq  17132  4sqlem12  17134  4sqlem17  17139  gzsubrg  21727  gzrngunitlem  21738  gzrngunit  21739  2sqlem2  27745  mul2sq  27746  2sqlem3  27747  cntotbnd  38731