Theorem nn0cn 12423

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

Assertion

Ref	Expression
nn0cn	⊢ (𝐴 ∈ ℕ0 → 𝐴 ∈ ℂ)

Proof of Theorem nn0cn

Step	Hyp	Ref	Expression
1		nn0sscn 12418	. 2 ⊢ ℕ0 ⊆ ℂ
2	1	sseli 3931	1 ⊢ (𝐴 ∈ ℕ0 → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 11036  ℕ₀cn0 12413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379  ax-un 7690  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-mulcl 11100  ax-i2m1 11106

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7371  df-om 7819  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-nn 12158  df-n0 12414

This theorem is referenced by:  nn0nnaddcl  12444  elnn0nn  12455  nn0sub  12463  difgtsumgt  12466  nn0le2x  12467  nn0n0n1ge2  12481  uzaddcl  12829  fzctr  13568  nn0split  13571  elfzoext  13650  zpnn0elfzo1  13667  ubmelm1fzo  13691  subfzo0  13720  quoremnn0ALT  13789  modmuladdnn0  13850  addmodidr  13855  modfzo0difsn  13878  nn0ennn  13914  expadd  14039  expmul  14042  bernneq  14164  bernneq2  14165  faclbnd  14225  faclbnd4lem3  14230  faclbnd4lem4  14231  faclbnd6  14234  bccmpl  14244  bcn0  14245  bcnn  14247  bcnp1n  14249  bcn2  14254  bcp1m1  14255  bcpasc  14256  bcn2p1  14260  hashfzo0  14365  hashfz0  14367  hashxplem  14368  hashdifsnp1  14441  ccatalpha  14529  ccatws1lenp1b  14557  ccatw2s1len  14561  swrdfv2  14597  swrdspsleq  14601  swrdlsw  14603  pfxmpt  14614  pfxswrd  14641  wrdind  14657  wrd2ind  14658  pfxccatin12lem4  14661  pfxccatin12lem1  14663  pfxccatin12lem2  14666  pfxccatin12  14668  swrdccat3blem  14674  repswswrd  14719  repswrevw  14722  cshwidxmodr  14739  2cshw  14748  2cshwcshw  14760  cshwcshid  14762  swrds2  14875  swrd2lsw  14887  iseraltlem2  15618  fsum0diag2  15718  hashiun  15757  ackbijnn  15763  binom1dif  15768  bcxmas  15770  geolim  15805  geomulcvg  15811  risefacval2  15945  fallfacval2  15946  risefaccl  15950  fallfaccl  15951  fallrisefac  15960  risefacp1  15964  fallfacp1  15965  fallfacfac  15980  bpolysum  15988  fsumkthpow  15991  bpoly4  15994  fsumcube  15995  efaddlem  16028  efexp  16038  eftlub  16046  demoivreALT  16138  nn0ob  16323  divalglem4  16335  modremain  16347  mulgcdr  16489  nn0rppwr  16500  nn0seqcvgd  16509  modprmn0modprm0  16747  coprimeprodsq  16748  coprimeprodsq2  16749  pcexp  16799  dvdsprmpweqle  16826  difsqpwdvds  16827  ramub1lem1  16966  prmop1  16978  chnccat  18561  smndex2dlinvh  18854  mulgneg2  19050  mndodcongi  19484  oddvdsnn0  19485  sylow1lem1  19539  efgsrel  19675  fincygsubgodd  20055  srgbinomlem4  20176  cnfldmulg  21370  nn0subm  21389  nn0srg  21404  psrbagconf1o  21897  psrass1lem  21900  psrlidm  21929  psrass1  21931  psrcom  21935  mplsubrglem  21971  mplmonmul  22003  psdmul  22121  psdmvr  22124  psropprmul  22190  coe1sclmul  22236  coe1sclmul2  22238  dvnadd  25899  ply1divex  26110  elqaalem2  26296  geolim3  26315  dvradcnv  26398  pserdv2  26408  logtayllem  26636  logtayl  26637  cxpmul2  26666  atantayl3  26917  leibpilem2  26919  leibpi  26920  log2cnv  26922  dmgmaddn0  27001  chpp1  27133  0sgmppw  27177  logexprlim  27204  dchrhash  27250  bcctr  27254  bcmono  27256  bcmax  27257  bcp1ctr  27258  2lgslem1c  27372  2lgslem3a  27375  2lgslem3b  27376  2lgslem3c  27377  2lgslem3d  27378  2lgslem3a1  27379  2lgslem3b1  27380  2lgslem3c1  27381  2lgslem3d1  27382  2sqreultlem  27426  2sqreulem2  27431  dchrisumlem1  27468  ostth2lem2  27613  wlklenvclwlk  29739  upgrwlkdvdelem  29821  wwlknp  29928  wwlknlsw  29932  wlkiswwlks1  29952  wlklnwwlkln2lem  29967  wlknwwlksnbij  29973  wwlksnred  29977  wwlksnext  29978  wwlksnredwwlkn  29980  wwlksnextwrd  29982  wwlksnextinj  29984  wwlksnextproplem2  29995  wwlksnextproplem3  29996  wspthsnwspthsnon  30001  clwlkclwwlklem2a1  30079  clwlkclwwlklem2a4  30084  clwlkclwwlklem2a  30085  clwlkclwwlklem2  30087  clwlkclwwlklem3  30088  wwlksext2clwwlk  30144  clwwlknonex2lem2  30195  eucrctshift  30330  eucrct2eupth  30332  numclwwlk2lem1lem  30429  numclwwlk1  30448  numclwwlk7  30478  ipasslem1  30919  ipasslem2  30920  dpfrac1  32984  archirngz  33283  psrmonmul  33727  nn0constr  33939  pthhashvtx  35344  subfacval2  35403  bccolsum  35955  faclimlem1  35959  poimirlem28  37899  heiborlem4  38065  heiborlem6  38067  lcmineqlem3  42401  facp2  42513  sticksstones7  42522  oddnumth  42681  nicomachus  42682  sumcubes  42683  pell14qrgt0  43216  pell14qrdich  43226  pell1qrge1  43227  2nn0ind  43302  jm2.17a  43317  jm2.18  43345  jm2.19lem3  43348  proot1ex  43553  bcc0  44696  dvradcnv2  44703  binomcxplemrat  44706  binomcxplemnotnn0  44712  fperiodmullem  45665  stoweidlem10  46368  stoweidlem17  46375  stoweidlem26  46384  stirlinglem5  46436  stirlinglem7  46438  etransclem23  46615  cjnpoly  47249  subsubelfzo0  47686  fargshiftfo  47802  fmtnodvds  47904  goldbachthlem1  47905  fmtnofac2lem  47928  fmtnofac1  47930  nn0onn0exALTV  48059  nn0enn0exALTV  48060  isubgr3stgrlem2  48327  nn0mnd  48539  ply1mulgsumlem1  48746  ply1mulgsumlem2  48747  nn0onn0ex  48883  nn0enn0ex  48884  fllog2  48928  dignn0fr  48961  digexp  48967  0dig2nn0e  48972  0dig2nn0o  48973  dignn0ehalf  48977  nn0mulfsum  48984  nn0mullong  48985  itcovalpclem1  49030  itcovalpclem2  49031  itcovalt2lem2lem2  49034  ackval1  49041  ackval2  49042  ackval3  49043