Theorem nn0cn 11908

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 10535  ℕ₀cn0 11898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-mulcl 10599  ax-i2m1 10605

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-ov 7159  df-om 7581  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-nn 11639  df-n0 11899

This theorem is referenced by:  nn0nnaddcl  11929  elnn0nn  11940  nn0sub  11948  difgtsumgt  11951  nn0n0n1ge2  11963  uzaddcl  12305  fzctr  13020  nn0split  13023  elfzoext  13095  zpnn0elfzo1  13112  ubmelm1fzo  13134  subfzo0  13160  quoremnn0ALT  13226  modmuladdnn0  13284  addmodidr  13289  modfzo0difsn  13312  nn0ennn  13348  expadd  13472  expmul  13475  bernneq  13591  bernneq2  13592  faclbnd  13651  faclbnd4lem3  13656  faclbnd4lem4  13657  faclbnd6  13660  bccmpl  13670  bcn0  13671  bcnn  13673  bcnp1n  13675  bcn2  13680  bcp1m1  13681  bcpasc  13682  bcn2p1  13686  hashfzo0  13792  hashfz0  13794  hashxplem  13795  hashdifsnp1  13855  ccatalpha  13947  ccatws1lenp1b  13975  ccatw2s1len  13980  swrdfv2  14023  swrdspsleq  14027  swrdlsw  14029  pfxmpt  14040  addlenrevpfx  14052  pfxswrd  14068  wrdind  14084  wrd2ind  14085  pfxccatin12lem4  14088  pfxccatin12lem1  14090  pfxccatin12lem2  14093  pfxccatin12  14095  swrdccat3blem  14101  repswswrd  14146  repswrevw  14149  cshwidxmodr  14166  2cshw  14175  2cshwcshw  14187  cshwcshid  14189  swrds2  14302  swrd2lsw  14314  iseraltlem2  15039  fsum0diag2  15138  hashiun  15177  ackbijnn  15183  binom1dif  15188  bcxmas  15190  geolim  15226  geomulcvg  15232  risefacval2  15364  fallfacval2  15365  risefaccl  15369  fallfaccl  15370  fallrisefac  15379  risefacp1  15383  fallfacp1  15384  fallfacfac  15399  bpolysum  15407  fsumkthpow  15410  bpoly4  15413  fsumcube  15414  efaddlem  15446  efexp  15454  eftlub  15462  demoivreALT  15554  nn0ob  15735  divalglem4  15747  modremain  15759  mulgcdr  15898  nn0seqcvgd  15914  modprmn0modprm0  16144  coprimeprodsq  16145  coprimeprodsq2  16146  pcexp  16196  dvdsprmpweqle  16222  difsqpwdvds  16223  ramub1lem1  16362  prmop1  16374  smndex2dlinvh  18082  mulgneg2  18261  mndodcongi  18671  oddvdsnn0  18672  sylow1lem1  18723  efgsrel  18860  fincygsubgodd  19234  srgbinomlem4  19293  psrbagconf1o  20154  psrass1lem  20157  psrlidm  20183  psrass1  20185  psrcom  20189  mplsubrglem  20219  mplmonmul  20245  psropprmul  20406  coe1sclmul  20450  coe1sclmul2  20452  cnfldmulg  20577  nn0subm  20600  nn0srg  20615  dvnadd  24526  ply1divex  24730  elqaalem2  24909  geolim3  24928  dvradcnv  25009  pserdv2  25018  logtayllem  25242  logtayl  25243  cxpmul2  25272  atantayl3  25517  leibpilem2  25519  leibpi  25520  log2cnv  25522  dmgmaddn0  25600  chpp1  25732  0sgmppw  25774  logexprlim  25801  dchrhash  25847  bcctr  25851  bcmono  25853  bcmax  25854  bcp1ctr  25855  2lgslem1c  25969  2lgslem3a  25972  2lgslem3b  25973  2lgslem3c  25974  2lgslem3d  25975  2lgslem3a1  25976  2lgslem3b1  25977  2lgslem3c1  25978  2lgslem3d1  25979  2sqreultlem  26023  2sqreulem2  26028  dchrisumlem1  26065  ostth2lem2  26210  wlklenvclwlk  27436  wlklenvclwlkOLD  27437  upgrwlkdvdelem  27517  wwlknp  27621  wwlknlsw  27625  wlkiswwlks1  27645  wlklnwwlkln2lem  27660  wlknwwlksnbij  27666  wwlksnred  27670  wwlksnext  27671  wwlksnredwwlkn  27673  wwlksnextwrd  27675  wwlksnextinj  27677  wwlksnextproplem2  27689  wwlksnextproplem3  27690  wspthsnwspthsnon  27695  clwlkclwwlklem2a1  27770  clwlkclwwlklem2a4  27775  clwlkclwwlklem2a  27776  clwlkclwwlklem2  27778  clwlkclwwlklem3  27779  wwlksext2clwwlk  27836  clwwlknonex2lem2  27887  eucrctshift  28022  eucrct2eupth  28024  numclwwlk2lem1lem  28121  numclwwlk1  28140  numclwwlk7  28170  ipasslem1  28608  ipasslem2  28609  dpfrac1  30568  archirngz  30818  pthhashvtx  32374  subfacval2  32434  bccolsum  32971  faclimlem1  32975  poimirlem28  34935  heiborlem4  35107  heiborlem6  35109  fac2xp3  39114  facp2  39115  factwoffsmonot  39118  nn0rppwr  39202  pell14qrgt0  39476  pell14qrdich  39486  pell1qrge1  39487  2nn0ind  39562  jm2.17a  39577  jm2.18  39605  jm2.19lem3  39608  proot1ex  39821  bcc0  40692  dvradcnv2  40699  binomcxplemrat  40702  binomcxplemnotnn0  40708  fperiodmullem  41590  stoweidlem10  42315  stoweidlem17  42322  stoweidlem26  42331  stirlinglem5  42383  stirlinglem7  42385  etransclem23  42562  subsubelfzo0  43546  fargshiftfo  43622  fmtnodvds  43726  goldbachthlem1  43727  fmtnofac2lem  43750  fmtnofac1  43752  nn0onn0exALTV  43884  nn0enn0exALTV  43885  nn0mnd  44106  ply1mulgsumlem1  44460  ply1mulgsumlem2  44461  nn0onn0ex  44603  nn0enn0ex  44604  fllog2  44648  dignn0fr  44681  digexp  44687  0dig2nn0e  44692  0dig2nn0o  44693  dignn0ehalf  44697  nn0mulfsum  44704  nn0mullong  44705