Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > zcn | GIF version |
Description: An integer is a complex number. (Contributed by NM, 9-May-2004.) |
Ref | Expression |
---|---|
zcn | ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zre 9205 | . 2 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ) | |
2 | 1 | recnd 7937 | 1 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2141 ℂcc 7761 ℤcz 9201 |
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 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-ext 2152 ax-resscn 7855 |
This theorem depends on definitions: df-bi 116 df-3or 974 df-3an 975 df-tru 1351 df-nf 1454 df-sb 1756 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-rex 2454 df-rab 2457 df-v 2732 df-un 3125 df-in 3127 df-ss 3134 df-sn 3587 df-pr 3588 df-op 3590 df-uni 3795 df-br 3988 df-iota 5158 df-fv 5204 df-ov 5854 df-neg 8082 df-z 9202 |
This theorem is referenced by: zsscn 9209 zaddcllempos 9238 peano2zm 9239 zaddcllemneg 9240 zaddcl 9241 zsubcl 9242 zrevaddcl 9251 nzadd 9253 zlem1lt 9257 zltlem1 9258 zapne 9275 zdiv 9289 zdivadd 9290 zdivmul 9291 zextlt 9293 zneo 9302 zeo2 9307 peano5uzti 9309 zindd 9319 divfnzn 9569 qmulz 9571 zq 9574 qaddcl 9583 qnegcl 9584 qmulcl 9585 qreccl 9590 fzen 9988 uzsubsubfz 9992 fz01en 9998 fzmmmeqm 10003 fzsubel 10005 fztp 10023 fzsuc2 10024 fzrev2 10030 fzrev3 10032 elfzp1b 10042 fzrevral 10050 fzrevral2 10051 fzrevral3 10052 fzshftral 10053 fzoaddel2 10138 fzosubel2 10140 eluzgtdifelfzo 10142 fzocatel 10144 elfzom1elp1fzo 10147 fzval3 10149 zpnn0elfzo1 10153 fzosplitprm1 10179 fzoshftral 10183 flqzadd 10243 2tnp1ge0ge0 10246 ceilid 10260 intfracq 10265 zmod10 10285 modqmuladdnn0 10313 addmodlteq 10343 frecfzen2 10372 ser3mono 10423 m1expeven 10512 expsubap 10513 zesq 10583 sqoddm1div8 10618 bccmpl 10677 shftuz 10770 nnabscl 11053 climshftlemg 11254 climshft 11256 mptfzshft 11394 fsumrev 11395 fisum0diag2 11399 efexp 11634 efzval 11635 demoivre 11724 dvdsval2 11741 iddvds 11755 1dvds 11756 dvds0 11757 negdvdsb 11758 dvdsnegb 11759 0dvds 11762 dvdsmul1 11764 iddvdsexp 11766 muldvds1 11767 muldvds2 11768 dvdscmul 11769 dvdsmulc 11770 summodnegmod 11773 modmulconst 11774 dvds2ln 11775 dvds2add 11776 dvds2sub 11777 dvdstr 11779 dvdssub2 11786 dvdsadd 11787 dvdsaddr 11788 dvdssub 11789 dvdssubr 11790 dvdsadd2b 11791 dvdsabseq 11796 divconjdvds 11798 alzdvds 11803 addmodlteqALT 11808 zeo3 11816 odd2np1lem 11820 odd2np1 11821 even2n 11822 oddp1even 11824 mulsucdiv2z 11833 zob 11839 ltoddhalfle 11841 halfleoddlt 11842 opoe 11843 omoe 11844 opeo 11845 omeo 11846 m1exp1 11849 divalgb 11873 divalgmod 11875 modremain 11877 ndvdssub 11878 ndvdsadd 11879 flodddiv4 11882 flodddiv4t2lthalf 11885 gcdneg 11926 gcdadd 11929 gcdid 11930 modgcd 11935 dvdsgcd 11956 mulgcd 11960 absmulgcd 11961 mulgcdr 11962 gcddiv 11963 gcdmultiplez 11965 dvdssqim 11968 dvdssq 11975 bezoutr1 11977 lcmneg 12017 lcmgcdlem 12020 lcmgcd 12021 lcmid 12023 lcm1 12024 coprmdvds 12035 coprmdvds2 12036 qredeq 12039 qredeu 12040 divgcdcoprmex 12045 cncongr1 12046 cncongr2 12047 prmdvdsexp 12091 rpexp1i 12097 sqrt2irr 12105 divnumden 12139 phiprmpw 12165 nnnn0modprm0 12198 modprmn0modprm0 12199 coprimeprodsq2 12201 pclemub 12230 pcprendvds2 12234 pcmul 12244 pcneg 12267 fldivp1 12289 prmpwdvds 12296 zgz 12314 ef2kpi 13482 efper 13483 sinperlem 13484 sin2kpi 13487 cos2kpi 13488 abssinper 13522 sinkpi 13523 coskpi 13524 cxpexprp 13571 lgslem3 13658 lgsneg 13680 lgsdir2lem2 13685 lgsdir2lem4 13687 lgsdir2 13689 lgssq 13696 lgsmulsqcoprm 13702 lgsdirnn0 13703 2sqlem2 13706 2sqlem7 13712 |
Copyright terms: Public domain | W3C validator |