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 1146	1 ⊢ (𝐴 ∈ ℤ[i] → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6498  ℂcc 11036  ℤcz 12524  ℜcre 15059  ℑcim 15060  ℤ[i]cgz 16900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  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  21401  gzrngunitlem  21412  gzrngunit  21413  2sqlem2  27381  mul2sq  27382  2sqlem3  27383  cntotbnd  38117