Theorem nn0cnd 12447

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 12446	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3	2	recnd 11143	1 ⊢ (𝜑 → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11007  ℕ₀cn0 12384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371  ax-un 7671  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-i2m1 11077  ax-1ne0 11078  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6249  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-ov 7352  df-om 7800  df-2nd 7925  df-frecs 8214  df-wrecs 8245  df-recs 8294  df-rdg 8332  df-nn 12129  df-n0 12385

This theorem is referenced by:  quoremnn0ALT  13761  expaddzlem  14012  expaddz  14013  expmulz  14015  facdiv  14194  faclbnd4lem3  14202  bcp1n  14223  bcn2m1  14231  bcn2p1  14232  hashgadd  14284  hashdom  14286  hashun3  14291  hashssdif  14319  hashdifpr  14322  hashxplem  14340  hashmap  14342  hashreshashfun  14346  hashbclem  14359  hashf1lem2  14363  hashf1  14364  ccatval3  14486  ccatval21sw  14492  ccatlid  14493  ccatrid  14494  ccatass  14495  ccatrn  14496  lswccatn0lsw  14498  ccatalpha  14500  ccatws1lenp1b  14528  wrdlenccats1lenm1  14529  ccats1val2  14534  swrdccat2  14576  pfxfv  14589  addlenpfx  14597  pfxtrcfvl  14603  pfxpfx  14614  lenrevpfxcctswrd  14618  ccats1pfxeq  14620  ccatopth2  14623  cats1un  14627  swrdccat3b  14646  spllen  14660  splfv2a  14662  revccat  14672  cshwlen  14705  cshwidxmod  14709  repswcshw  14718  2cshwid  14720  cshweqdif2  14725  relexpaddg  14960  rtrclreclem3  14967  isercoll2  15576  iseraltlem3  15591  hash2iun1dif1  15731  binomlem  15736  bcxmas  15742  incexclem  15743  incexc  15744  incexc2  15745  climcndslem1  15756  climcndslem2  15757  arisum  15767  arisum2  15768  pwdif  15775  geomulcvg  15783  mertens  15793  risefacval2  15917  fallfacval2  15918  fallfacval3  15919  risefallfac  15931  risefacp1  15936  fallfacp1  15937  fallfacfwd  15943  binomfallfaclem1  15946  binomfallfaclem2  15947  binomrisefac  15949  bpolycl  15959  bpolysum  15960  bpolydiflem  15961  fsumkthpow  15963  bpoly4  15966  effsumlt  16020  dvdsexp  16239  nn0ob  16295  divalgmod  16317  bitsinv1lem  16352  sadcp1  16366  sadcaddlem  16368  sadadd2lem  16370  sadadd3  16372  sadaddlem  16377  sadasslem  16381  smupp1  16391  smumullem  16403  mulgcd  16459  absmulgcd  16460  mulgcdr  16461  gcddiv  16462  lcmgcd  16518  lcmid  16520  lcm1  16521  3lcm2e6woprm  16526  6lcm4e12  16527  mulgcddvds  16566  qredeu  16569  divgcdcoprm0  16576  divgcdcoprmex  16577  cncongr1  16578  cncongr2  16579  odzdvds  16707  powm2modprm  16715  coprimeprodsq  16720  pceulem  16757  pczpre  16759  pcqmul  16765  pcaddlem  16800  pcmpt  16804  pcmpt2  16805  sumhash  16808  oddprmdvds  16815  mul4sq  16866  4sqlem12  16868  vdwapun  16886  vdwlem2  16894  vdwlem3  16895  vdwlem6  16898  vdwlem8  16900  vdwlem9  16901  ramub1lem2  16939  ramcl  16941  mulgnn0dir  18983  mulgnn0ass  18989  lagsubg2  19073  psgnunilem2  19374  odmodnn0  19419  odmulg  19435  odmulgeq  19436  odinv  19440  sylow1lem1  19477  sylow2a  19498  sylow2blem3  19501  sylow3lem3  19508  sylow3lem4  19509  efginvrel2  19606  efgsval2  19612  efgsp1  19616  efgredlemg  19621  efgredleme  19622  efgcpbllemb  19634  odadd2  19728  odadd  19729  torsubg  19733  frgpnabllem1  19752  pgpfaclem1  19962  fincygsubgodd  19993  omndmul2  20012  omndmul3  20013  srgbinomlem3  20113  srgbinomlem4  20114  nn0srg  21344  freshmansdream  21481  mplcoe5  21945  mhpmulcl  22034  mhppwdeg  22035  psdmplcl  22047  psdmul  22051  coe1tmmul2  22160  coe1tmmul2fv  22162  coe1pwmulfv  22164  mbfi1fseqlem3  25616  dvn2bss  25830  itgpowd  25955  tdeglem4  25963  tdeglem2  25964  mdegmullem  25981  coe1mul3  26002  ply1divex  26040  fta1glem1  26071  plyaddlem1  26116  plymullem1  26117  coeeulem  26127  coemulc  26158  dgrmulc  26175  dgrcolem2  26178  dgrco  26179  dvply1  26189  dvply2g  26190  dvply2gOLD  26191  plydivlem4  26202  fta1lem  26213  vieta1lem1  26216  aareccl  26232  aaliou3lem8  26251  taylply2  26273  taylply2OLD  26274  dvtaylp  26276  dvntaylp  26277  dvntaylp0  26278  dvradcnv  26328  pserdvlem2  26336  advlogexp  26562  cxpeq  26665  atantayl3  26847  birthdaylem2  26860  harmonicbnd4  26919  dmgmaddnn0  26935  lgamucov  26946  wilthlem2  26977  basellem2  26990  basellem3  26991  basellem5  26993  0sgm  27052  sgmppw  27106  chtublem  27120  chpval2  27127  sumdchr2  27179  bcp1ctr  27188  lgslem1  27206  gausslemma2dlem6  27281  gausslemma2d  27283  lgseisenlem2  27285  lgseisenlem3  27286  lgsquadlem1  27289  lgsquadlem2  27290  lgsquad2lem2  27294  m1lgs  27297  2lgslem1c  27302  2lgslem3a  27305  2lgslem3b  27306  2lgslem3c  27307  2lgslem3d  27308  2sqlem8  27335  2sq2  27342  2sqmod  27345  dchrisumlem1  27398  dchrisum0flblem2  27418  rpvmasum2  27421  mulogsumlem  27440  selberg2lem  27459  pntrsumo1  27474  pntrlog2bndlem4  27489  finsumvtxdg2ssteplem4  29494  vtxdgoddnumeven  29499  wlklenvm1  29567  wlklenvclwlk  29599  crctcshlem4  29765  crctcsh  29769  wlklnwwlkln2lem  29827  wlknwwlksnbij  29833  wwlksnred  29837  wwlksnext  29838  wwlksnextbi  29839  wwlksnredwwlkn  29840  wwlksnextproplem2  29855  rusgrnumwwlks  29919  rusgrnumwwlk  29920  clwwlkccatlem  29933  clwlkclwwlk  29946  clwwlkwwlksb  29998  eupth2lem3lem3  30174  eupth2lem3lem6  30177  fusgreghash2wsp  30282  frrusgrord0lem  30283  numclwwlk1  30305  numclwwlk3  30329  ex-lcm  30402  ex-ind-dvds  30405  nnmulge  32682  elq2  32756  divnumden2  32760  ccatf1  32890  pfxlsw2ccat  32892  ccatws1f1o  32893  wrdt2ind  32895  cycpmco2lem2  33069  cycpmco2lem3  33070  cycpmco2lem4  33071  cycpmco2lem5  33072  cycpmco2lem6  33073  cycpmco2lem7  33074  cycpmco2  33075  archiabllem1a  33133  ply1dg3rt0irred  33518  iconstr  33733  cos9thpiminplylem1  33749  oddpwdc  34322  eulerpartlemsv2  34326  eulerpartlems  34328  eulerpartlemsv3  34329  eulerpartlemv  34332  eulerpartlemb  34336  iwrdsplit  34355  ballotlemgun  34493  ccatmulgnn0dir  34510  ofcccat  34511  signsplypnf  34518  signslema  34530  signstfvn  34537  signstfveq0  34545  signsvtp  34551  signsvtn  34552  signlem0  34555  signshf  34556  fsum2dsub  34575  hashreprin  34588  breprexp  34601  circlemeth  34608  lpadlem2  34648  lpadlen2  34649  revpfxsfxrev  35093  revwlk  35102  subfacp1lem6  35162  subfacval2  35164  subfaclim  35165  cvmliftlem7  35268  elmrsubrn  35497  bcprod  35715  bccolsum  35716  faclimlem1  35720  faclim2  35725  fwddifnp1  36143  knoppndvlem6  36495  knoppndvlem14  36503  poimirlem4  37608  poimirlem5  37609  poimirlem6  37610  poimirlem7  37611  poimirlem10  37614  poimirlem11  37615  poimirlem12  37616  poimirlem16  37620  poimirlem17  37621  poimirlem19  37623  poimirlem20  37624  poimirlem22  37626  poimirlem24  37628  poimirlem25  37629  poimirlem29  37633  poimirlem31  37635  lcmineqlem1  42006  lcmineqlem2  42007  lcmineqlem12  42017  lcmineqlem17  42022  primrootscoprmpow  42076  aks6d1c2p2  42096  deg1gprod  42117  deg1pow  42118  2np3bcnp1  42121  2ap1caineq  42122  sticksstones7  42129  sticksstones9  42131  sticksstones10  42132  sticksstones11  42133  sticksstones12a  42134  sticksstones12  42135  sticksstones22  42145  aks6d1c6lem1  42147  aks6d1c6lem3  42149  bcled  42155  bcle2d  42156  aks6d1c7lem1  42157  unitscyglem2  42173  unitscyglem4  42175  ccatcan2d  42228  fz1sump1  42287  sumcubes  42290  zaddcomlem  42440  frlmvscadiccat  42483  fltnltalem  42639  3cubeslem3l  42663  3cubeslem3r  42664  rmxyneg  42897  rmxyadd  42898  rmyp1  42910  rmxm1  42911  rmym1  42912  rmxluc  42913  rmyluc  42914  rmxdbl  42916  rmydbl  42917  jm2.18  42965  jm2.19lem1  42966  jm2.19lem2  42967  jm2.22  42972  jm2.23  42973  jm2.25  42976  jm2.27c  42984  rmxdiophlem  42992  expdioph  43000  hbtlem4  43103  relexpmulg  43687  radcnvrat  44291  nzprmdif  44296  bcc0  44317  bccp1k  44318  bccbc  44322  binomcxplemnn0  44326  binomcxplemrat  44327  binomcxplemfrat  44328  binomcxplemnotnn0  44333  fzisoeu  45286  mccllem  45582  dvxpaek  45925  dvnxpaek  45927  dvnmul  45928  dvnprodlem1  45931  dvnprodlem2  45932  stoweidlem24  46009  stirlinglem3  46061  stirlinglem7  46065  fourierdlem36  46128  fourierdlem47  46138  etransclem23  46242  etransclem32  46251  etransclem48  46267  fz0addcom  47305  fmtnom1nn  47520  fmtnof1  47523  fmtnorec1  47525  sqrtpwpw2p  47526  fmtnorec2lem  47530  fmtnorec3  47536  fmtnofac2lem  47556  fmtnofac2  47557  fmtnofac1  47558  lighneallem3  47595  lighneallem4b  47597  altgsumbc  48340  altgsumbcALT  48341  nnpw2pmod  48572  dignn0ehalf  48606  nn0sumshdiglemA  48608  nn0sumshdiglemB  48609  nn0sumshdiglem2  48611  nn0mullong  48614  itcovalpclem2  48660  itcovalt2lem2lem2  48663  itcovalt2lem1  48664  aacllem  49790