Theorem gzcn 16998

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2142  ‘cfv 6536  ℂcc 11104  ℤcz 12597  ℜcre 15155  ℑcim 15156  ℤ[i]cgz 16995

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-iota 6492  df-fv 6544  df-gz 16996

This theorem is used by:  gznegcl  17001  gzcjcl  17002  gzaddcl  17003  gzmulcl  17004  gzsubcl  17006  gzabssqcl  17007  4sqlem4a  17017  4sqlem4  17018  mul4sqlem  17019  mul4sq  17020  4sqlem12  17022  4sqlem17  17027  gzsubrg  21582  gzrngunitlem  21593  gzrngunit  21594  2sqlem2  27593  mul2sq  27594  2sqlem3  27595  cntotbnd  38475