Theorem nn0cn 12656

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 12651	. 2 ⊢ ℕ0 ⊆ ℂ
2	1	sseli 3909	1 ⊢ (𝐴 ∈ ℕ0 → 𝐴 ∈ ℂ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ℂcc 11237  ℕ₀cn0 12646

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398  ax-un 7783  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-mulcl 11301  ax-i2m1 11307

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-pred 6330  df-ord 6391  df-on 6392  df-lim 6393  df-suc 6394  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-ov 7454  df-om 7912  df-2nd 8036  df-frecs 8337  df-wrecs 8368  df-recs 8417  df-rdg 8456  df-nn 12376  df-n0 12647

This theorem is used by:  nn0nnaddcl  12677  elnn0nn  12688  nn0sub  12696  difgtsumgt  12699  nn0le2x  12700  nn0n0n1ge2  12714  uzaddcl  13071  nn0split  13817  elfzoext  13897  zpnn0elfzo1  13914  ubmelm1fzo  13938  subfzo0  13968  quoremnn0ALT  14037  modmuladdnn0  14098  addmodidr  14103  modfzo0difsn  14126  nn0ennn  14162  expadd  14287  expmul  14290  bernneq  14414  bernneq2  14415  faclbnd  14475  faclbnd4lem3  14480  faclbnd4lem4  14481  faclbnd6  14484  bccmpl  14494  bcn0  14495  bcnn  14497  bcnp1n  14499  bcn2  14504  bcp1m1  14505  bcpasc  14506  bcn2p1  14510  hashfzo0  14616  hashfz0  14618  hashxplem  14619  hashdifsnp1  14692  ccatalpha  14781  ccatws1lenp1b  14811  ccatw2s1len  14815  swrdfv2  14853  swrdspsleq  14857  swrdlsw  14859  pfxmpt  14870  pfxswrd  14897  wrdind  14913  wrd2ind  14914  pfxccatin12lem4  14917  pfxccatin12lem1  14919  pfxccatin12lem2  14922  pfxccatin12  14924  swrdccat3blem  14930  repswswrd  14977  repswrevw  14980  cshwidxmodr  14997  2cshw  15006  2cshwcshw  15018  cshwcshid  15020  swrds2  15134  swrd2lsw  15148  iseraltlem2  15894  fsum0diag2  15993  hashiun  16033  ackbijnn  16041  binom1dif  16046  bcxmas  16048  geolim  16083  geomulcvg  16089  risefacval2  16221  fallfacval2  16222  risefaccl  16226  fallfaccl  16227  fallrisefac  16236  risefacp1  16239  fallfacp1  16240  fallfacfac  16255  bpolysum  16263  fsumkthpow  16266  bpoly4  16269  fsumcube  16270  efaddlem  16303  efexp  16313  eftlub  16321  demoivreALT  16413  nn0ob  16598  divalglem4  16610  modremain  16622  mulgcdr  16767  nn0rppwr  16779  nn0seqcvgd  16789  modprmn0modprm0  17029  coprimeprodsq  17030  coprimeprodsq2  17031  pcexp  17081  dvdsprmpweqle  17108  difsqpwdvds  17109  ramub1lem1  17248  prmop1  17260  chnccat  18850  smndex2dlinvh  19166  mulgneg2  19368  mndodcongi  19808  oddvdsnn0  19809  sylow1lem1  19863  efgsrel  19999  fincygsubgodd  20379  srgbinomlem4  20506  cnfldmulg  21762  nn0subm  21782  nn0srg  21797  psrbagconf1o  22292  psrass1lem  22296  psrlidm  22324  psrass1  22326  psrcom  22330  mplsubrglem  22366  mplmonmul  22400  psdmul  22542  psdmvr  22545  psropprmul  22610  coe1sclmul  22656  coe1sclmul2  22658  dvnadd  26304  ply1divex  26510  elqaalem2  26700  geolim3  26723  dvradcnv  26805  pserdv2  26814  logtayllem  27044  logtayl  27045  cxpmul2  27074  atantayl3  27324  leibpilem2  27326  leibpi  27327  log2cnv  27329  dmgmaddn0  27407  chpp1  27539  0sgmppw  27582  logexprlim  27609  dchrhash  27655  bcctr  27659  bcmono  27661  bcmax  27662  bcp1ctr  27663  2lgslem1c  27777  2lgslem3a  27780  2lgslem3b  27781  2lgslem3c  27782  2lgslem3d  27783  2lgslem3a1  27784  2lgslem3b1  27785  2lgslem3c1  27786  2lgslem3d1  27787  2sqreultlem  27831  2sqreulem2  27836  dchrisumlem1  27873  ostth2lem2  28018  wlklenvclwlk  30291  pthhashvtx  30372  upgrwlkdvdelem  30379  wwlknp  30489  wwlknlsw  30493  wlkiswwlks1  30513  wlklnwwlkln2lem  30528  wlknwwlksnbij  30534  wwlksnred  30538  wwlksnext  30539  wwlksnredwwlkn  30541  wwlksnextwrd  30543  wwlksnextinj  30545  wwlksnextproplem2  30556  wwlksnextproplem3  30557  wspthsnwspthsnon  30562  clwlkclwwlklem2a1  30640  clwlkclwwlklem2a4  30645  clwlkclwwlklem2a  30646  clwlkclwwlklem2  30648  clwlkclwwlklem3  30649  wwlksext2clwwlk  30705  clwwlknonex2lem2  30756  eucrctshift  30901  eucrct2eupth  30903  numclwwlk2lem1lem  31000  numclwwlk1  31019  numclwwlk7  31049  ipasslem1  31490  ipasslem2  31491  dpfrac1  33554  archirngz  33849  psrmonmul  34293  nn0constr  34504  subfacval2  36160  bccolsum  36719  faclimlem1  36723  poimirlem28  38834  heiborlem4  39014  heiborlem6  39016  lcmineqlem3  43347  facp2  43459  sticksstones7  43468  oddnumth  43634  nicomachus  43635  sumcubes  43636  pell14qrgt0  44132  pell14qrdich  44142  pell1qrge1  44143  2nn0ind  44218  jm2.17a  44233  jm2.18  44261  jm2.19lem3  44264  proot1ex  44459  bcc0  45585  dvradcnv2  45592  binomcxplemrat  45595  binomcxplemnotnn0  45601  fperiodmullem  46592  stoweidlem10  47293  stoweidlem17  47300  stoweidlem26  47309  stirlinglem5  47361  stirlinglem7  47363  etransclem23  47540  cjnpoly  48212  subsubelfzo0  48670  fargshiftfo  48797  fmtnodvds  48902  goldbachthlem1  48903  fmtnofac2lem  48926  fmtnofac1  48928  nn0onn0exALTV  49070  nn0enn0exALTV  49071  isubgr3stgrlem2  49338  nn0mnd  49549  ply1mulgsumlem1  49829  ply1mulgsumlem2  49830  nn0onn0ex  49966  nn0enn0ex  49967  fllog2  50011  dignn0fr  50044  digexp  50050  0dig2nn0e  50055  0dig2nn0o  50056  dignn0ehalf  50060  nn0mulfsum  50067  nn0mullong  50068  itcovalpclem1  50113  itcovalpclem2  50114  itcovalt2lem2lem2  50117  ackval1  50124  ackval2  50125  ackval3  50126