nn0cn - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > nn0cn		Structured version Visualization version GIF version

Theorem nn0cn 12482

Description: A nonnegative integer is a complex number. (Contributed by NM, 9-May-2004.)

**Assertion**
Ref	Expression
nn0cn	⊢ (𝐴 ∈ ℕ₀ → 𝐴 ∈ ℂ)

**Proof of Theorem nn0cn**
Step	Hyp	Ref	Expression
1		nn0sscn 12477	. 2 ⊢ ℕ₀ ⊆ ℂ
2	1	sseli 3979	1 ⊢ (𝐴 ∈ ℕ₀ → 𝐴 ∈ ℂ)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∈ wcel 2107 ℂcc 11108 ℕ₀cn0 12472

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5300 ax-nul 5307 ax-pr 5428 ax-un 7725 ax-1cn 11168 ax-icn 11169 ax-addcl 11170 ax-mulcl 11172 ax-i2m1 11178

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-ral 3063 df-rex 3072 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-pss 3968 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-iun 5000 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5575 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-we 5634 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-pred 6301 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-ov 7412 df-om 7856 df-2nd 7976 df-frecs 8266 df-wrecs 8297 df-recs 8371 df-rdg 8410 df-nn 12213 df-n0 12473

This theorem is referenced by: nn0nnaddcl 12503 elnn0nn 12514 nn0sub 12522 difgtsumgt 12525 nn0n0n1ge2 12539 uzaddcl 12888 fzctr 13613 nn0split 13616 elfzoext 13689 zpnn0elfzo1 13706 ubmelm1fzo 13728 subfzo0 13754 quoremnn0ALT 13822 modmuladdnn0 13880 addmodidr 13885 modfzo0difsn 13908 nn0ennn 13944 expadd 14070 expmul 14073 bernneq 14192 bernneq2 14193 faclbnd 14250 faclbnd4lem3 14255 faclbnd4lem4 14256 faclbnd6 14259 bccmpl 14269 bcn0 14270 bcnn 14272 bcnp1n 14274 bcn2 14279 bcp1m1 14280 bcpasc 14281 bcn2p1 14285 hashfzo0 14390 hashfz0 14392 hashxplem 14393 hashdifsnp1 14457 ccatalpha 14543 ccatws1lenp1b 14571 ccatw2s1len 14575 swrdfv2 14611 swrdspsleq 14615 swrdlsw 14617 pfxmpt 14628 addlenrevpfx 14640 pfxswrd 14656 wrdind 14672 wrd2ind 14673 pfxccatin12lem4 14676 pfxccatin12lem1 14678 pfxccatin12lem2 14681 pfxccatin12 14683 swrdccat3blem 14689 repswswrd 14734 repswrevw 14737 cshwidxmodr 14754 2cshw 14763 2cshwcshw 14776 cshwcshid 14778 swrds2 14891 swrd2lsw 14903 iseraltlem2 15629 fsum0diag2 15729 hashiun 15768 ackbijnn 15774 binom1dif 15779 bcxmas 15781 geolim 15816 geomulcvg 15822 risefacval2 15954 fallfacval2 15955 risefaccl 15959 fallfaccl 15960 fallrisefac 15969 risefacp1 15973 fallfacp1 15974 fallfacfac 15989 bpolysum 15997 fsumkthpow 16000 bpoly4 16003 fsumcube 16004 efaddlem 16036 efexp 16044 eftlub 16052 demoivreALT 16144 nn0ob 16327 divalglem4 16339 modremain 16351 mulgcdr 16492 nn0seqcvgd 16507 modprmn0modprm0 16740 coprimeprodsq 16741 coprimeprodsq2 16742 pcexp 16792 dvdsprmpweqle 16819 difsqpwdvds 16820 ramub1lem1 16959 prmop1 16971 smndex2dlinvh 18798 mulgneg2 18988 mndodcongi 19411 oddvdsnn0 19412 sylow1lem1 19466 efgsrel 19602 fincygsubgodd 19982 srgbinomlem4 20052 cnfldmulg 20977 nn0subm 21000 nn0srg 21015 psrbagconf1o 21489 psrbagconf1oOLD 21490 psrass1lemOLD 21493 psrass1lem 21496 psrlidm 21523 psrass1 21525 psrcom 21529 mplsubrglem 21563 mplmonmul 21591 psropprmul 21760 coe1sclmul 21804 coe1sclmul2 21806 dvnadd 25446 ply1divex 25654 elqaalem2 25833 geolim3 25852 dvradcnv 25933 pserdv2 25942 logtayllem 26167 logtayl 26168 cxpmul2 26197 atantayl3 26444 leibpilem2 26446 leibpi 26447 log2cnv 26449 dmgmaddn0 26527 chpp1 26659 0sgmppw 26701 logexprlim 26728 dchrhash 26774 bcctr 26778 bcmono 26780 bcmax 26781 bcp1ctr 26782 2lgslem1c 26896 2lgslem3a 26899 2lgslem3b 26900 2lgslem3c 26901 2lgslem3d 26902 2lgslem3a1 26903 2lgslem3b1 26904 2lgslem3c1 26905 2lgslem3d1 26906 2sqreultlem 26950 2sqreulem2 26955 dchrisumlem1 26992 ostth2lem2 27137 wlklenvclwlk 28912 upgrwlkdvdelem 28993 wwlknp 29097 wwlknlsw 29101 wlkiswwlks1 29121 wlklnwwlkln2lem 29136 wlknwwlksnbij 29142 wwlksnred 29146 wwlksnext 29147 wwlksnredwwlkn 29149 wwlksnextwrd 29151 wwlksnextinj 29153 wwlksnextproplem2 29164 wwlksnextproplem3 29165 wspthsnwspthsnon 29170 clwlkclwwlklem2a1 29245 clwlkclwwlklem2a4 29250 clwlkclwwlklem2a 29251 clwlkclwwlklem2 29253 clwlkclwwlklem3 29254 wwlksext2clwwlk 29310 clwwlknonex2lem2 29361 eucrctshift 29496 eucrct2eupth 29498 numclwwlk2lem1lem 29595 numclwwlk1 29614 numclwwlk7 29644 ipasslem1 30084 ipasslem2 30085 dpfrac1 32058 archirngz 32335 pthhashvtx 34118 subfacval2 34178 bccolsum 34709 faclimlem1 34713 poimirlem28 36516 heiborlem4 36682 heiborlem6 36684 lcmineqlem3 40896 facp2 40959 sticksstones7 40968 fac2xp3 41020 factwoffsmonot 41023 oddnumth 41209 nicomachus 41210 sumcubes 41211 nn0rppwr 41224 pell14qrgt0 41597 pell14qrdich 41607 pell1qrge1 41608 2nn0ind 41684 jm2.17a 41699 jm2.18 41727 jm2.19lem3 41730 proot1ex 41943 bcc0 43099 dvradcnv2 43106 binomcxplemrat 43109 binomcxplemnotnn0 43115 fperiodmullem 44013 stoweidlem10 44726 stoweidlem17 44733 stoweidlem26 44742 stirlinglem5 44794 stirlinglem7 44796 etransclem23 44973 subsubelfzo0 46034 fargshiftfo 46110 fmtnodvds 46212 goldbachthlem1 46213 fmtnofac2lem 46236 fmtnofac1 46238 nn0onn0exALTV 46367 nn0enn0exALTV 46368 nn0mnd 46589 ply1mulgsumlem1 47067 ply1mulgsumlem2 47068 nn0onn0ex 47209 nn0enn0ex 47210 fllog2 47254 dignn0fr 47287 digexp 47293 0dig2nn0e 47298 0dig2nn0o 47299 dignn0ehalf 47303 nn0mulfsum 47310 nn0mullong 47311 itcovalpclem1 47356 itcovalpclem2 47357 itcovalt2lem2lem2 47360 ackval1 47367 ackval2 47368 ackval3 47369

W3C validator