Theorem nn0cnd 11958

Description: A nonnegative integer is a complex number. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
nn0red.1	⊢ (𝜑 → 𝐴 ∈ ℕ0)

Assertion

Ref	Expression
nn0cnd	⊢ (𝜑 → 𝐴 ∈ ℂ)

Proof of Theorem nn0cnd

Step	Hyp	Ref	Expression
1		nn0red.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℕ0)
2	1	nn0red 11957	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3	2	recnd 10669	1 ⊢ (𝜑 → 𝐴 ∈ ℂ)

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-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-i2m1 10605  ax-1ne0 10606  ax-rnegex 10608  ax-rrecex 10609  ax-cnre 10610

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:  quoremnn0ALT  13226  expaddzlem  13473  expaddz  13474  expmulz  13476  facdiv  13648  faclbnd4lem3  13656  bcp1n  13677  bcn2m1  13685  bcn2p1  13686  hashgadd  13739  hashdom  13741  hashun3  13746  hashssdif  13774  hashdifpr  13777  hashxplem  13795  hashmap  13797  hashreshashfun  13801  hashbclem  13811  hashf1lem2  13815  hashf1  13816  ccatval3  13933  ccatval21sw  13939  ccatlid  13940  ccatrid  13941  ccatass  13942  ccatrn  13943  lswccatn0lsw  13945  ccatalpha  13947  ccatws1lenp1b  13975  wrdlenccats1lenm1  13976  ccats1val2  13983  swrdccat2  14031  pfxfv  14044  addlenpfx  14053  pfxtrcfvl  14059  pfxpfx  14070  ccats1pfxeq  14076  ccatopth2  14079  cats1un  14083  swrdccat3b  14102  spllen  14116  splfv2a  14118  revccat  14128  cshwlen  14161  cshwidxmod  14165  repswcshw  14174  2cshwid  14176  cshweqdif2  14181  relexpaddg  14412  rtrclreclem3  14419  isercoll2  15025  iseraltlem3  15040  hash2iun1dif1  15179  binomlem  15184  bcxmas  15190  incexclem  15191  incexc  15192  incexc2  15193  climcndslem1  15204  climcndslem2  15205  arisum  15215  arisum2  15216  pwdif  15223  geomulcvg  15232  mertens  15242  risefacval2  15364  fallfacval2  15365  fallfacval3  15366  risefallfac  15378  risefacp1  15383  fallfacp1  15384  fallfacfwd  15390  binomfallfaclem1  15393  binomfallfaclem2  15394  binomrisefac  15396  bpolycl  15406  bpolysum  15407  bpolydiflem  15408  fsumkthpow  15410  bpoly4  15413  effsumlt  15464  dvdsexp  15677  nn0ob  15735  divalgmod  15757  bitsinv1lem  15790  sadcp1  15804  sadcaddlem  15806  sadadd2lem  15808  sadadd3  15810  sadaddlem  15815  sadasslem  15819  smupp1  15829  smumullem  15841  mulgcd  15896  absmulgcd  15897  mulgcdr  15898  gcddiv  15899  lcmgcd  15951  lcmid  15953  lcm1  15954  3lcm2e6woprm  15959  6lcm4e12  15960  mulgcddvds  15999  qredeu  16002  divgcdcoprm0  16009  divgcdcoprmex  16010  cncongr1  16011  cncongr2  16012  odzdvds  16132  powm2modprm  16140  coprimeprodsq  16145  pceulem  16182  pczpre  16184  pcqmul  16190  pcaddlem  16224  pcmpt  16228  pcmpt2  16229  sumhash  16232  oddprmdvds  16239  mul4sq  16290  4sqlem12  16292  vdwapun  16310  vdwlem2  16318  vdwlem3  16319  vdwlem6  16322  vdwlem8  16324  vdwlem9  16325  ramub1lem2  16363  ramcl  16365  mulgnn0dir  18257  mulgnn0ass  18263  lagsubg2  18341  psgnunilem2  18623  odmodnn0  18668  odmulg  18683  odmulgeq  18684  odinv  18688  sylow1lem1  18723  sylow2a  18744  sylow2blem3  18747  sylow3lem3  18754  sylow3lem4  18755  efginvrel2  18853  efgsval2  18859  efgsp1  18863  efgredlemg  18868  efgredleme  18869  efgcpbllemb  18881  odadd2  18969  odadd  18970  torsubg  18974  frgpnabllem1  18993  pgpfaclem1  19203  fincygsubgodd  19234  srgbinomlem3  19292  srgbinomlem4  19293  mplcoe5  20249  coe1tmmul2  20444  coe1tmmul2fv  20446  coe1pwmulfv  20448  nn0srg  20615  mbfi1fseqlem3  24318  dvn2bss  24527  tdeglem4  24654  tdeglem2  24655  mdegmullem  24672  coe1mul3  24693  ply1divex  24730  fta1glem1  24759  plyaddlem1  24803  plymullem1  24804  coeeulem  24814  coemulc  24845  dgrmulc  24861  dgrcolem2  24864  dgrco  24865  dvply1  24873  dvply2g  24874  plydivlem4  24885  fta1lem  24896  vieta1lem1  24899  aareccl  24915  aaliou3lem8  24934  taylply2  24956  dvtaylp  24958  dvntaylp  24959  dvntaylp0  24960  dvradcnv  25009  pserdvlem2  25016  advlogexp  25238  cxpeq  25338  atantayl3  25517  birthdaylem2  25530  harmonicbnd4  25588  dmgmaddnn0  25604  lgamucov  25615  wilthlem2  25646  basellem2  25659  basellem3  25660  basellem5  25662  0sgm  25721  sgmppw  25773  chtublem  25787  chpval2  25794  sumdchr2  25846  bcp1ctr  25855  lgslem1  25873  gausslemma2dlem6  25948  gausslemma2d  25950  lgseisenlem2  25952  lgseisenlem3  25953  lgsquadlem1  25956  lgsquadlem2  25957  lgsquad2lem2  25961  m1lgs  25964  2lgslem1c  25969  2lgslem3a  25972  2lgslem3b  25973  2lgslem3c  25974  2lgslem3d  25975  2sqlem8  26002  2sq2  26009  2sqmod  26012  dchrisumlem1  26065  dchrisum0flblem2  26085  rpvmasum2  26088  mulogsumlem  26107  selberg2lem  26126  pntrsumo1  26141  pntrlog2bndlem4  26156  finsumvtxdg2ssteplem4  27330  vtxdgoddnumeven  27335  wlklenvm1  27403  wlklenvclwlk  27436  crctcshlem4  27598  crctcsh  27602  wlklnwwlkln2lem  27660  wlknwwlksnbij  27666  wwlksnred  27670  wwlksnext  27671  wwlksnextbi  27672  wwlksnredwwlkn  27673  wwlksnextproplem2  27689  rusgrnumwwlks  27753  rusgrnumwwlk  27754  clwwlkccatlem  27767  clwlkclwwlk  27780  clwwlkwwlksb  27833  eupth2lem3lem3  28009  eupth2lem3lem6  28012  fusgreghash2wsp  28117  frrusgrord0lem  28118  numclwwlk1  28140  numclwwlk3  28164  ex-lcm  28237  ex-ind-dvds  28240  nnmulge  30474  divnumden2  30534  ccatf1  30625  pfxlsw2ccat  30626  wrdt2ind  30627  omndmul2  30713  omndmul3  30714  cycpmco2lem2  30769  cycpmco2lem3  30770  cycpmco2lem4  30771  cycpmco2lem5  30772  cycpmco2lem6  30773  cycpmco2lem7  30774  cycpmco2  30775  archiabllem1a  30820  freshmansdream  30859  oddpwdc  31612  eulerpartlemsv2  31616  eulerpartlems  31618  eulerpartlemsv3  31619  eulerpartlemv  31622  eulerpartlemb  31626  iwrdsplit  31645  ballotlemgun  31782  ccatmulgnn0dir  31812  ofcccat  31813  signsplypnf  31820  signslema  31832  signstfvn  31839  signstfveq0  31847  signsvtp  31853  signsvtn  31854  signlem0  31857  signshf  31858  fsum2dsub  31878  hashreprin  31891  breprexp  31904  circlemeth  31911  lpadlem2  31951  lpadlen2  31952  revpfxsfxrev  32362  revwlk  32371  subfacp1lem6  32432  subfacval2  32434  subfaclim  32435  cvmliftlem7  32538  elmrsubrn  32767  bcprod  32970  bccolsum  32971  faclimlem1  32975  faclim2  32980  fwddifnp1  33626  knoppndvlem6  33856  knoppndvlem14  33864  poimirlem4  34911  poimirlem5  34912  poimirlem6  34913  poimirlem7  34914  poimirlem10  34917  poimirlem11  34918  poimirlem12  34919  poimirlem16  34923  poimirlem17  34924  poimirlem19  34926  poimirlem20  34927  poimirlem22  34929  poimirlem24  34931  poimirlem25  34932  poimirlem29  34936  poimirlem31  34938  ccatcan2d  39147  frlmvscadiccat  39165  fltnltalem  39294  3cubeslem3l  39303  3cubeslem3r  39304  rmxyneg  39537  rmxyadd  39538  rmyp1  39550  rmxm1  39551  rmym1  39552  rmxluc  39553  rmyluc  39554  rmxdbl  39556  rmydbl  39557  jm2.18  39605  jm2.19lem1  39606  jm2.19lem2  39607  jm2.22  39612  jm2.23  39613  jm2.25  39616  jm2.27c  39624  rmxdiophlem  39632  expdioph  39640  hbtlem4  39746  itgpowd  39841  relexpmulg  40075  radcnvrat  40666  nzprmdif  40671  bcc0  40692  bccp1k  40693  bccbc  40697  binomcxplemnn0  40701  binomcxplemrat  40702  binomcxplemfrat  40703  binomcxplemnotnn0  40708  fzisoeu  41587  mccllem  41898  dvxpaek  42245  dvnxpaek  42247  dvnmul  42248  dvnprodlem1  42251  dvnprodlem2  42252  stoweidlem24  42329  stirlinglem3  42381  stirlinglem7  42385  fourierdlem36  42448  fourierdlem47  42458  etransclem23  42562  etransclem32  42571  etransclem48  42587  fz0addcom  43537  fmtnom1nn  43714  fmtnof1  43717  fmtnorec1  43719  sqrtpwpw2p  43720  fmtnorec2lem  43724  fmtnorec3  43730  fmtnofac2lem  43750  fmtnofac2  43751  fmtnofac1  43752  lighneallem3  43792  lighneallem4b  43794  altgsumbc  44420  altgsumbcALT  44421  nnpw2pmod  44663  dignn0ehalf  44697  nn0sumshdiglemA  44699  nn0sumshdiglemB  44700  nn0sumshdiglem2  44702  nn0mullong  44705  aacllem  44922