![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > gzcn | Structured version Visualization version GIF version |
Description: A gaussian integer is a complex number. (Contributed by Mario Carneiro, 14-Jul-2014.) |
Ref | Expression |
---|---|
gzcn | ⊢ (𝐴 ∈ ℤ[i] → 𝐴 ∈ ℂ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elgz 16039 | . 2 ⊢ (𝐴 ∈ ℤ[i] ↔ (𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ℤ ∧ (ℑ‘𝐴) ∈ ℤ)) | |
2 | 1 | simp1bi 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 |