MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  gzcn Structured version   Visualization version   GIF version

Theorem gzcn 16040
Description: A gaussian integer is a complex number. (Contributed by Mario Carneiro, 14-Jul-2014.)
Assertion
Ref Expression
gzcn (𝐴 ∈ ℤ[i] → 𝐴 ∈ ℂ)

Proof of Theorem gzcn
StepHypRef Expression
1 elgz 16039 . 2 (𝐴 ∈ ℤ[i] ↔ (𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ℤ ∧ (ℑ‘𝐴) ∈ ℤ))
21simp1bi 1136 1 (𝐴 ∈ ℤ[i] → 𝐴 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  cfv 6135  cc 10270  cz 11728  cre 14244  cim 14245  ℤ[i]cgz 16037
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rex 3096  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4672  df-br 4887  df-iota 6099  df-fv 6143  df-gz 16038
This theorem is referenced by:  gznegcl  16043  gzcjcl  16044  gzaddcl  16045  gzmulcl  16046  gzsubcl  16048  gzabssqcl  16049  4sqlem4a  16059  4sqlem4  16060  mul4sqlem  16061  mul4sq  16062  4sqlem12  16064  4sqlem17  16069  gzsubrg  20196  gzrngunitlem  20207  gzrngunit  20208  2sqlem2  25595  mul2sq  25596  2sqlem3  25597  cntotbnd  34219
  Copyright terms: Public domain W3C validator