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 9189 | . 2 | |
2 | 1 | recnd 7921 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 2135 cc 7745 cz 9185 |
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 699 ax-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-10 1492 ax-11 1493 ax-i12 1494 ax-bndl 1496 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 ax-resscn 7839 |
This theorem depends on definitions: df-bi 116 df-3or 968 df-3an 969 df-tru 1345 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-nfc 2295 df-rex 2448 df-rab 2451 df-v 2726 df-un 3118 df-in 3120 df-ss 3127 df-sn 3579 df-pr 3580 df-op 3582 df-uni 3787 df-br 3980 df-iota 5150 df-fv 5193 df-ov 5842 df-neg 8066 df-z 9186 |
This theorem is referenced by: zsscn 9193 zaddcllempos 9222 peano2zm 9223 zaddcllemneg 9224 zaddcl 9225 zsubcl 9226 zrevaddcl 9235 nzadd 9237 zlem1lt 9241 zltlem1 9242 zapne 9259 zdiv 9273 zdivadd 9274 zdivmul 9275 zextlt 9277 zneo 9286 zeo2 9291 peano5uzti 9293 zindd 9303 divfnzn 9553 qmulz 9555 zq 9558 qaddcl 9567 qnegcl 9568 qmulcl 9569 qreccl 9574 fzen 9972 uzsubsubfz 9976 fz01en 9982 fzmmmeqm 9987 fzsubel 9989 fztp 10007 fzsuc2 10008 fzrev2 10014 fzrev3 10016 elfzp1b 10026 fzrevral 10034 fzrevral2 10035 fzrevral3 10036 fzshftral 10037 fzoaddel2 10122 fzosubel2 10124 eluzgtdifelfzo 10126 fzocatel 10128 elfzom1elp1fzo 10131 fzval3 10133 zpnn0elfzo1 10137 fzosplitprm1 10163 fzoshftral 10167 flqzadd 10227 2tnp1ge0ge0 10230 ceilid 10244 intfracq 10249 zmod10 10269 modqmuladdnn0 10297 addmodlteq 10327 frecfzen2 10356 ser3mono 10407 m1expeven 10496 expsubap 10497 zesq 10567 sqoddm1div8 10602 bccmpl 10661 shftuz 10753 nnabscl 11036 climshftlemg 11237 climshft 11239 mptfzshft 11377 fsumrev 11378 fisum0diag2 11382 efexp 11617 efzval 11618 demoivre 11707 dvdsval2 11724 iddvds 11738 1dvds 11739 dvds0 11740 negdvdsb 11741 dvdsnegb 11742 0dvds 11745 dvdsmul1 11747 iddvdsexp 11749 muldvds1 11750 muldvds2 11751 dvdscmul 11752 dvdsmulc 11753 summodnegmod 11756 modmulconst 11757 dvds2ln 11758 dvds2add 11759 dvds2sub 11760 dvdstr 11762 dvdssub2 11769 dvdsadd 11770 dvdsaddr 11771 dvdssub 11772 dvdssubr 11773 dvdsadd2b 11774 dvdsabseq 11779 divconjdvds 11781 alzdvds 11786 addmodlteqALT 11791 zeo3 11799 odd2np1lem 11803 odd2np1 11804 even2n 11805 oddp1even 11807 mulsucdiv2z 11816 zob 11822 ltoddhalfle 11824 halfleoddlt 11825 opoe 11826 omoe 11827 opeo 11828 omeo 11829 m1exp1 11832 divalgb 11856 divalgmod 11858 modremain 11860 ndvdssub 11861 ndvdsadd 11862 flodddiv4 11865 flodddiv4t2lthalf 11868 gcdneg 11909 gcdadd 11912 gcdid 11913 modgcd 11918 dvdsgcd 11939 mulgcd 11943 absmulgcd 11944 mulgcdr 11945 gcddiv 11946 gcdmultiplez 11948 dvdssqim 11951 dvdssq 11958 bezoutr1 11960 lcmneg 12000 lcmgcdlem 12003 lcmgcd 12004 lcmid 12006 lcm1 12007 coprmdvds 12018 coprmdvds2 12019 qredeq 12022 qredeu 12023 divgcdcoprmex 12028 cncongr1 12029 cncongr2 12030 prmdvdsexp 12074 rpexp1i 12080 sqrt2irr 12088 divnumden 12122 phiprmpw 12148 nnnn0modprm0 12181 modprmn0modprm0 12182 coprimeprodsq2 12184 pclemub 12213 pcprendvds2 12217 pcmul 12227 pcneg 12250 fldivp1 12272 prmpwdvds 12279 zgz 12297 ef2kpi 13325 efper 13326 sinperlem 13327 sin2kpi 13330 cos2kpi 13331 abssinper 13365 sinkpi 13366 coskpi 13367 cxpexprp 13414 |
Copyright terms: Public domain | W3C validator |