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 8355 | . 2 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ) | |
2 | 1 | recnd 7147 | 1 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1433 ℂcc 6979 ℤcz 8351 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-io 662 ax-5 1376 ax-7 1377 ax-gen 1378 ax-ie1 1422 ax-ie2 1423 ax-8 1435 ax-10 1436 ax-11 1437 ax-i12 1438 ax-bndl 1439 ax-4 1440 ax-17 1459 ax-i9 1463 ax-ial 1467 ax-i5r 1468 ax-ext 2063 ax-resscn 7068 |
This theorem depends on definitions: df-bi 115 df-3or 920 df-3an 921 df-tru 1287 df-nf 1390 df-sb 1686 df-clab 2068 df-cleq 2074 df-clel 2077 df-nfc 2208 df-rex 2354 df-rab 2357 df-v 2603 df-un 2977 df-in 2979 df-ss 2986 df-sn 3404 df-pr 3405 df-op 3407 df-uni 3602 df-br 3786 df-iota 4887 df-fv 4930 df-ov 5535 df-neg 7282 df-z 8352 |
This theorem is referenced by: zsscn 8359 zaddcllempos 8388 peano2zm 8389 zaddcllemneg 8390 zaddcl 8391 zsubcl 8392 zrevaddcl 8401 nzadd 8403 zlem1lt 8407 zltlem1 8408 zapne 8422 zdiv 8435 zdivadd 8436 zdivmul 8437 zextlt 8439 zneo 8448 zeo2 8453 peano5uzti 8455 zindd 8465 divfnzn 8706 qmulz 8708 zq 8711 qaddcl 8720 qnegcl 8721 qmulcl 8722 qreccl 8727 fzen 9062 uzsubsubfz 9066 fz01en 9072 fzmmmeqm 9076 fzsubel 9078 fztp 9095 fzsuc2 9096 fzrev2 9102 fzrev3 9104 elfzp1b 9114 fzrevral 9122 fzrevral2 9123 fzrevral3 9124 fzshftral 9125 fzoaddel2 9202 fzosubel2 9204 eluzgtdifelfzo 9206 fzocatel 9208 elfzom1elp1fzo 9211 fzval3 9213 zpnn0elfzo1 9217 fzosplitprm1 9243 fzoshftral 9247 flqzadd 9300 2tnp1ge0ge0 9303 ceilid 9317 intfracq 9322 zmod10 9342 modqmuladdnn0 9370 addmodlteq 9400 frecfzen2 9420 iseqshft2 9452 isermono 9457 m1expeven 9523 expsubap 9524 zesq 9591 sqoddm1div8 9625 bccmpl 9681 shftuz 9705 nnabscl 9986 climshftlemg 10141 climshft 10143 dvdsval2 10198 iddvds 10208 1dvds 10209 dvds0 10210 negdvdsb 10211 dvdsnegb 10212 0dvds 10215 dvdsmul1 10217 iddvdsexp 10219 muldvds1 10220 muldvds2 10221 dvdscmul 10222 dvdsmulc 10223 summodnegmod 10226 modmulconst 10227 dvds2ln 10228 dvds2add 10229 dvds2sub 10230 dvdstr 10232 dvdssub2 10237 dvdsadd 10238 dvdsaddr 10239 dvdssub 10240 dvdssubr 10241 dvdsadd2b 10242 dvdsabseq 10247 divconjdvds 10249 alzdvds 10254 addmodlteqALT 10259 zeo3 10267 odd2np1lem 10271 odd2np1 10272 even2n 10273 oddp1even 10275 mulsucdiv2z 10285 zob 10291 ltoddhalfle 10293 halfleoddlt 10294 opoe 10295 omoe 10296 opeo 10297 omeo 10298 m1exp1 10301 divalgb 10325 divalgmod 10327 modremain 10329 ndvdssub 10330 ndvdsadd 10331 flodddiv4 10334 flodddiv4t2lthalf 10337 gcdneg 10373 gcdadd 10376 gcdid 10377 modgcd 10382 dvdsgcd 10401 mulgcd 10405 absmulgcd 10406 mulgcdr 10407 gcddiv 10408 gcdmultiplez 10410 dvdssqim 10413 dvdssq 10420 bezoutr1 10422 lcmneg 10456 lcmgcdlem 10459 lcmgcd 10460 lcmid 10462 lcm1 10463 coprmdvds 10474 coprmdvds2 10475 qredeq 10478 qredeu 10479 divgcdcoprmex 10484 cncongr1 10485 cncongr2 10486 prmdvdsexp 10527 rpexp1i 10533 sqrt2irr 10541 |
Copyright terms: Public domain | W3C validator |