Theorem gzcn 17028

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ‘cfv 6537  ℂcc 11125  ℤcz 12618  ℜcre 15186  ℑcim 15187  ℤ[i]cgz 17025

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-gz 17026

This theorem is used by:  gznegcl  17031  gzcjcl  17032  gzaddcl  17033  gzmulcl  17034  gzsubcl  17036  gzabssqcl  17037  4sqlem4a  17047  4sqlem4  17048  mul4sqlem  17049  mul4sq  17050  4sqlem12  17052  4sqlem17  17057  gzsubrg  21635  gzrngunitlem  21646  gzrngunit  21647  2sqlem2  27652  mul2sq  27653  2sqlem3  27654  cntotbnd  38533