![]() |
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 8650 | . 2 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ) | |
2 | 1 | recnd 7419 | 1 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1434 ℂcc 7251 ℤcz 8646 |
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 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2065 ax-resscn 7340 |
This theorem depends on definitions: df-bi 115 df-3or 921 df-3an 922 df-tru 1288 df-nf 1391 df-sb 1688 df-clab 2070 df-cleq 2076 df-clel 2079 df-nfc 2212 df-rex 2359 df-rab 2362 df-v 2614 df-un 2988 df-in 2990 df-ss 2997 df-sn 3428 df-pr 3429 df-op 3431 df-uni 3628 df-br 3812 df-iota 4934 df-fv 4977 df-ov 5594 df-neg 7559 df-z 8647 |
This theorem is referenced by: zsscn 8654 zaddcllempos 8683 peano2zm 8684 zaddcllemneg 8685 zaddcl 8686 zsubcl 8687 zrevaddcl 8696 nzadd 8698 zlem1lt 8702 zltlem1 8703 zapne 8717 zdiv 8730 zdivadd 8731 zdivmul 8732 zextlt 8734 zneo 8743 zeo2 8748 peano5uzti 8750 zindd 8760 divfnzn 9001 qmulz 9003 zq 9006 qaddcl 9015 qnegcl 9016 qmulcl 9017 qreccl 9022 fzen 9352 uzsubsubfz 9356 fz01en 9362 fzmmmeqm 9366 fzsubel 9368 fztp 9385 fzsuc2 9386 fzrev2 9392 fzrev3 9394 elfzp1b 9404 fzrevral 9412 fzrevral2 9413 fzrevral3 9414 fzshftral 9415 fzoaddel2 9493 fzosubel2 9495 eluzgtdifelfzo 9497 fzocatel 9499 elfzom1elp1fzo 9502 fzval3 9504 zpnn0elfzo1 9508 fzosplitprm1 9534 fzoshftral 9538 flqzadd 9594 2tnp1ge0ge0 9597 ceilid 9611 intfracq 9616 zmod10 9636 modqmuladdnn0 9664 addmodlteq 9694 frecfzen2 9723 iseqshft2 9767 isermono 9772 m1expeven 9839 expsubap 9840 zesq 9907 sqoddm1div8 9941 bccmpl 9997 shftuz 10079 nnabscl 10360 climshftlemg 10515 climshft 10517 dvdsval2 10579 iddvds 10589 1dvds 10590 dvds0 10591 negdvdsb 10592 dvdsnegb 10593 0dvds 10596 dvdsmul1 10598 iddvdsexp 10600 muldvds1 10601 muldvds2 10602 dvdscmul 10603 dvdsmulc 10604 summodnegmod 10607 modmulconst 10608 dvds2ln 10609 dvds2add 10610 dvds2sub 10611 dvdstr 10613 dvdssub2 10618 dvdsadd 10619 dvdsaddr 10620 dvdssub 10621 dvdssubr 10622 dvdsadd2b 10623 dvdsabseq 10628 divconjdvds 10630 alzdvds 10635 addmodlteqALT 10640 zeo3 10648 odd2np1lem 10652 odd2np1 10653 even2n 10654 oddp1even 10656 mulsucdiv2z 10665 zob 10671 ltoddhalfle 10673 halfleoddlt 10674 opoe 10675 omoe 10676 opeo 10677 omeo 10678 m1exp1 10681 divalgb 10705 divalgmod 10707 modremain 10709 ndvdssub 10710 ndvdsadd 10711 flodddiv4 10714 flodddiv4t2lthalf 10717 gcdneg 10753 gcdadd 10756 gcdid 10757 modgcd 10762 dvdsgcd 10781 mulgcd 10785 absmulgcd 10786 mulgcdr 10787 gcddiv 10788 gcdmultiplez 10790 dvdssqim 10793 dvdssq 10800 bezoutr1 10802 lcmneg 10836 lcmgcdlem 10839 lcmgcd 10840 lcmid 10842 lcm1 10843 coprmdvds 10854 coprmdvds2 10855 qredeq 10858 qredeu 10859 divgcdcoprmex 10864 cncongr1 10865 cncongr2 10866 prmdvdsexp 10907 rpexp1i 10913 sqrt2irr 10921 divnumden 10954 phiprmpw 10978 |
Copyright terms: Public domain | W3C validator |