Theorem gzcn 16910

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

Syntax hints:   → wi 4   ∈ wcel 2109  ‘cfv 6514  ℂcc 11073  ℤcz 12536  ℜcre 15070  ℑcim 15071  ℤ[i]cgz 16907

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-gz 16908

This theorem is referenced by:  gznegcl  16913  gzcjcl  16914  gzaddcl  16915  gzmulcl  16916  gzsubcl  16918  gzabssqcl  16919  4sqlem4a  16929  4sqlem4  16930  mul4sqlem  16931  mul4sq  16932  4sqlem12  16934  4sqlem17  16939  gzsubrg  21345  gzrngunitlem  21356  gzrngunit  21357  2sqlem2  27336  mul2sq  27337  2sqlem3  27338  cntotbnd  37797