![]() |
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 8910 | . 2 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ) | |
2 | 1 | recnd 7666 | 1 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1448 ℂcc 7498 ℤcz 8906 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 671 ax-5 1391 ax-7 1392 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-8 1450 ax-10 1451 ax-11 1452 ax-i12 1453 ax-bndl 1454 ax-4 1455 ax-17 1474 ax-i9 1478 ax-ial 1482 ax-i5r 1483 ax-ext 2082 ax-resscn 7587 |
This theorem depends on definitions: df-bi 116 df-3or 931 df-3an 932 df-tru 1302 df-nf 1405 df-sb 1704 df-clab 2087 df-cleq 2093 df-clel 2096 df-nfc 2229 df-rex 2381 df-rab 2384 df-v 2643 df-un 3025 df-in 3027 df-ss 3034 df-sn 3480 df-pr 3481 df-op 3483 df-uni 3684 df-br 3876 df-iota 5024 df-fv 5067 df-ov 5709 df-neg 7807 df-z 8907 |
This theorem is referenced by: zsscn 8914 zaddcllempos 8943 peano2zm 8944 zaddcllemneg 8945 zaddcl 8946 zsubcl 8947 zrevaddcl 8956 nzadd 8958 zlem1lt 8962 zltlem1 8963 zapne 8977 zdiv 8991 zdivadd 8992 zdivmul 8993 zextlt 8995 zneo 9004 zeo2 9009 peano5uzti 9011 zindd 9021 divfnzn 9263 qmulz 9265 zq 9268 qaddcl 9277 qnegcl 9278 qmulcl 9279 qreccl 9284 fzen 9664 uzsubsubfz 9668 fz01en 9674 fzmmmeqm 9679 fzsubel 9681 fztp 9699 fzsuc2 9700 fzrev2 9706 fzrev3 9708 elfzp1b 9718 fzrevral 9726 fzrevral2 9727 fzrevral3 9728 fzshftral 9729 fzoaddel2 9811 fzosubel2 9813 eluzgtdifelfzo 9815 fzocatel 9817 elfzom1elp1fzo 9820 fzval3 9822 zpnn0elfzo1 9826 fzosplitprm1 9852 fzoshftral 9856 flqzadd 9912 2tnp1ge0ge0 9915 ceilid 9929 intfracq 9934 zmod10 9954 modqmuladdnn0 9982 addmodlteq 10012 frecfzen2 10041 ser3mono 10092 m1expeven 10181 expsubap 10182 zesq 10251 sqoddm1div8 10285 bccmpl 10341 shftuz 10430 nnabscl 10712 climshftlemg 10910 climshft 10912 mptfzshft 11050 fsumrev 11051 fisum0diag2 11055 efexp 11186 efzval 11187 demoivre 11276 dvdsval2 11291 iddvds 11301 1dvds 11302 dvds0 11303 negdvdsb 11304 dvdsnegb 11305 0dvds 11308 dvdsmul1 11310 iddvdsexp 11312 muldvds1 11313 muldvds2 11314 dvdscmul 11315 dvdsmulc 11316 summodnegmod 11319 modmulconst 11320 dvds2ln 11321 dvds2add 11322 dvds2sub 11323 dvdstr 11325 dvdssub2 11330 dvdsadd 11331 dvdsaddr 11332 dvdssub 11333 dvdssubr 11334 dvdsadd2b 11335 dvdsabseq 11340 divconjdvds 11342 alzdvds 11347 addmodlteqALT 11352 zeo3 11360 odd2np1lem 11364 odd2np1 11365 even2n 11366 oddp1even 11368 mulsucdiv2z 11377 zob 11383 ltoddhalfle 11385 halfleoddlt 11386 opoe 11387 omoe 11388 opeo 11389 omeo 11390 m1exp1 11393 divalgb 11417 divalgmod 11419 modremain 11421 ndvdssub 11422 ndvdsadd 11423 flodddiv4 11426 flodddiv4t2lthalf 11429 gcdneg 11465 gcdadd 11468 gcdid 11469 modgcd 11474 dvdsgcd 11493 mulgcd 11497 absmulgcd 11498 mulgcdr 11499 gcddiv 11500 gcdmultiplez 11502 dvdssqim 11505 dvdssq 11512 bezoutr1 11514 lcmneg 11548 lcmgcdlem 11551 lcmgcd 11552 lcmid 11554 lcm1 11555 coprmdvds 11566 coprmdvds2 11567 qredeq 11570 qredeu 11571 divgcdcoprmex 11576 cncongr1 11577 cncongr2 11578 prmdvdsexp 11619 rpexp1i 11625 sqrt2irr 11633 divnumden 11666 phiprmpw 11690 |
Copyright terms: Public domain | W3C validator |