Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > zcn | Unicode version |
Description: An integer is a complex number. (Contributed by NM, 9-May-2004.) |
Ref | Expression |
---|---|
zcn |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zre 9051 | . 2 | |
2 | 1 | recnd 7787 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 1480 cc 7611 cz 9047 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2119 ax-resscn 7705 |
This theorem depends on definitions: df-bi 116 df-3or 963 df-3an 964 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2124 df-cleq 2130 df-clel 2133 df-nfc 2268 df-rex 2420 df-rab 2423 df-v 2683 df-un 3070 df-in 3072 df-ss 3079 df-sn 3528 df-pr 3529 df-op 3531 df-uni 3732 df-br 3925 df-iota 5083 df-fv 5126 df-ov 5770 df-neg 7929 df-z 9048 |
This theorem is referenced by: zsscn 9055 zaddcllempos 9084 peano2zm 9085 zaddcllemneg 9086 zaddcl 9087 zsubcl 9088 zrevaddcl 9097 nzadd 9099 zlem1lt 9103 zltlem1 9104 zapne 9118 zdiv 9132 zdivadd 9133 zdivmul 9134 zextlt 9136 zneo 9145 zeo2 9150 peano5uzti 9152 zindd 9162 divfnzn 9406 qmulz 9408 zq 9411 qaddcl 9420 qnegcl 9421 qmulcl 9422 qreccl 9427 fzen 9816 uzsubsubfz 9820 fz01en 9826 fzmmmeqm 9831 fzsubel 9833 fztp 9851 fzsuc2 9852 fzrev2 9858 fzrev3 9860 elfzp1b 9870 fzrevral 9878 fzrevral2 9879 fzrevral3 9880 fzshftral 9881 fzoaddel2 9963 fzosubel2 9965 eluzgtdifelfzo 9967 fzocatel 9969 elfzom1elp1fzo 9972 fzval3 9974 zpnn0elfzo1 9978 fzosplitprm1 10004 fzoshftral 10008 flqzadd 10064 2tnp1ge0ge0 10067 ceilid 10081 intfracq 10086 zmod10 10106 modqmuladdnn0 10134 addmodlteq 10164 frecfzen2 10193 ser3mono 10244 m1expeven 10333 expsubap 10334 zesq 10403 sqoddm1div8 10437 bccmpl 10493 shftuz 10582 nnabscl 10865 climshftlemg 11064 climshft 11066 mptfzshft 11204 fsumrev 11205 fisum0diag2 11209 efexp 11377 efzval 11378 demoivre 11468 dvdsval2 11485 iddvds 11495 1dvds 11496 dvds0 11497 negdvdsb 11498 dvdsnegb 11499 0dvds 11502 dvdsmul1 11504 iddvdsexp 11506 muldvds1 11507 muldvds2 11508 dvdscmul 11509 dvdsmulc 11510 summodnegmod 11513 modmulconst 11514 dvds2ln 11515 dvds2add 11516 dvds2sub 11517 dvdstr 11519 dvdssub2 11524 dvdsadd 11525 dvdsaddr 11526 dvdssub 11527 dvdssubr 11528 dvdsadd2b 11529 dvdsabseq 11534 divconjdvds 11536 alzdvds 11541 addmodlteqALT 11546 zeo3 11554 odd2np1lem 11558 odd2np1 11559 even2n 11560 oddp1even 11562 mulsucdiv2z 11571 zob 11577 ltoddhalfle 11579 halfleoddlt 11580 opoe 11581 omoe 11582 opeo 11583 omeo 11584 m1exp1 11587 divalgb 11611 divalgmod 11613 modremain 11615 ndvdssub 11616 ndvdsadd 11617 flodddiv4 11620 flodddiv4t2lthalf 11623 gcdneg 11659 gcdadd 11662 gcdid 11663 modgcd 11668 dvdsgcd 11689 mulgcd 11693 absmulgcd 11694 mulgcdr 11695 gcddiv 11696 gcdmultiplez 11698 dvdssqim 11701 dvdssq 11708 bezoutr1 11710 lcmneg 11744 lcmgcdlem 11747 lcmgcd 11748 lcmid 11750 lcm1 11751 coprmdvds 11762 coprmdvds2 11763 qredeq 11766 qredeu 11767 divgcdcoprmex 11772 cncongr1 11773 cncongr2 11774 prmdvdsexp 11815 rpexp1i 11821 sqrt2irr 11829 divnumden 11863 phiprmpw 11887 ef2kpi 12876 efper 12877 sinperlem 12878 sin2kpi 12881 cos2kpi 12882 abssinper 12916 sinkpi 12917 coskpi 12918 |
Copyright terms: Public domain | W3C validator |