Theorem nn0cnd 12584

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ℂcc 11115  ℕ₀cn0 12521

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406  ax-un 7742  ax-resscn 11174  ax-1cn 11175  ax-icn 11176  ax-addcl 11177  ax-addrcl 11178  ax-mulcl 11179  ax-mulrcl 11180  ax-i2m1 11185  ax-1ne0 11186  ax-rnegex 11188  ax-rrecex 11189  ax-cnre 11190

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 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7422  df-om 7869  df-2nd 7993  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-nn 12251  df-n0 12522

This theorem is used by:  quoremnn0ALT  13910  expaddzlem  14161  expaddz  14162  expmulz  14164  facdiv  14343  faclbnd4lem3  14351  bcp1n  14372  bcn2m1  14380  bcn2p1  14381  hashgadd  14433  hashdom  14435  hashun3  14440  hashssdif  14469  hashdifpr  14472  hashxplem  14490  hashmap  14492  hashreshashfun  14496  hashbclem  14509  hashf1lem2  14513  hashf1  14514  ccatval3  14636  ccatval21sw  14643  ccatlid  14644  ccatrid  14645  ccatass  14646  ccatrn  14647  ccatf1  14648  lswccatn0lsw  14650  ccatalpha  14652  ccatws1lenp1b  14681  wrdlenccats1lenm1  14682  ccats1val2  14687  swrdccat2  14731  pfxfv  14744  addlenpfx  14752  pfxtrcfvl  14758  pfxpfx  14769  lenrevpfxcctswrd  14773  ccats1pfxeq  14775  ccatopth2  14778  cats1un  14782  swrdccat3b  14801  spllen  14815  splfv2a  14817  revccat  14827  revpfxsfxrev  14829  cshwlen  14862  cshwidxmod  14866  repswcshw  14875  2cshwid  14877  cshweqdif2  14882  relexpaddg  15116  rtrclreclem3  15123  isercoll2  15746  iseraltlem3  15761  fsumconst1  15867  hash2iun1dif1  15901  binomlem  15908  bcxmas  15914  incexclem  15915  incexc  15916  incexc2  15917  climcndslem1  15928  climcndslem2  15929  arisum  15939  arisum2  15940  pwdif  15947  geomulcvg  15955  mertens  15965  risefacval2  16089  fallfacval2  16090  fallfacval3  16091  risefallfac  16103  risefacp1  16107  fallfacp1  16108  fallfacfwd  16114  binomfallfaclem1  16117  binomfallfaclem2  16118  binomrisefac  16120  bpolycl  16130  bpolysum  16131  bpolydiflem  16132  fsumkthpow  16134  bpoly4  16137  effsumlt  16191  dvdsexp  16410  nn0ob  16466  divalgmod  16488  bitsinv1lem  16523  sadcp1  16537  sadcaddlem  16539  sadadd2lem  16541  sadadd3  16543  sadaddlem  16548  sadasslem  16552  smupp1  16562  smumullem  16574  mulgcd  16630  absmulgcd  16631  mulgcdr  16632  gcddiv  16633  lcmgcd  16689  lcmid  16691  lcm1  16692  3lcm2e6woprm  16697  6lcm4e12  16698  mulgcddvds  16737  qredeu  16740  divgcdcoprm0  16747  divgcdcoprmex  16748  cncongr1  16749  cncongr2  16750  odzdvds  16879  powm2modprm  16887  coprimeprodsq  16892  pceulem  16929  pczpre  16931  pcqmul  16937  pcaddlem  16972  pcmpt  16976  pcmpt2  16977  sumhash  16980  oddprmdvds  16987  mul4sq  17038  4sqlem12  17040  vdwapun  17058  vdwlem2  17066  vdwlem3  17067  vdwlem6  17070  vdwlem8  17072  vdwlem9  17073  ramub1lem2  17111  ramcl  17113  chnrev  18707  mulgnn0dir  19216  mulgnn0ass  19222  lagsubg2  19311  psgnunilem2  19611  odmodnn0  19656  odmulg  19672  odmulgeq  19673  odinv  19677  sylow1lem1  19714  sylow2a  19735  sylow2blem3  19738  sylow3lem3  19745  sylow3lem4  19746  efginvrel2  19843  efgsval2  19849  efgsp1  19853  efgredlemg  19858  efgredleme  19859  efgcpbllemb  19871  odadd2  19965  odadd  19966  torsubg  19970  frgpnabllem1  19989  pgpfaclem1  20199  fincygsubgodd  20230  omndmul2  20249  omndmul3  20250  srgbinomlem3  20356  srgbinomlem4  20357  nn0srg  21639  freshmansdream  21776  mplcoe5  22243  mhpmulcl  22364  mhppwdeg  22365  psdmplcl  22377  psdmul  22381  coe1tmmul2  22489  coe1tmmul2fv  22491  coe1pwmulfv  22493  mbfi1fseqlem3  25929  dvn2bss  26142  itgpowd  26262  tdeglem4  26270  tdeglem2  26271  mdegmullem  26288  coe1mul3  26309  ply1divex  26347  fta1glem1  26378  plyaddlem1  26423  plymullem1  26424  coeeulem  26434  coemulc  26465  dgrmulc  26481  dgrcolem2  26484  dgrco  26485  dvply1  26498  dvply2g  26499  plydivlem4  26510  fta1lem  26521  vieta1lem1  26524  aareccl  26542  aaliou3lem8  26561  taylply2  26584  dvtaylp  26586  dvntaylp  26587  dvntaylp0  26588  dvradcnv  26637  pserdvlem2  26644  advlogexp  26873  cxpeq  26975  atantayl3  27157  birthdaylem2  27170  harmonicbnd4  27228  dmgmaddnn0  27244  lgamucov  27255  wilthlem2  27286  basellem2  27299  basellem3  27300  basellem5  27302  0sgm  27361  sgmppw  27414  chtublem  27428  chpval2  27435  sumdchr2  27487  bcp1ctr  27496  lgslem1  27514  gausslemma2dlem6  27589  gausslemma2d  27591  lgseisenlem2  27593  lgseisenlem3  27594  lgsquadlem1  27597  lgsquadlem2  27598  lgsquad2lem2  27602  m1lgs  27605  2lgslem1c  27610  2lgslem3a  27613  2lgslem3b  27614  2lgslem3c  27615  2lgslem3d  27616  2sqlem8  27643  2sq2  27650  2sqmod  27653  dchrisumlem1  27706  dchrisum0flblem2  27726  rpvmasum2  27729  mulogsumlem  27748  selberg2lem  27767  pntrsumo1  27782  pntrlog2bndlem4  27797  finsumvtxdg2ssteplem4  29958  vtxdgoddnumeven  29963  wlklenvm1  30031  wlklenvclwlk  30063  revwlk  30096  crctcshlem4  30238  crctcsh  30242  wlklnwwlkln2lem  30300  wlknwwlksnbij  30306  wwlksnred  30310  wwlksnext  30311  wwlksnextbi  30312  wwlksnredwwlkn  30313  wwlksnextproplem2  30328  rusgrnumwwlks  30395  rusgrnumwwlk  30396  clwwlkccatlem  30409  clwlkclwwlk  30422  clwwlkwwlksb  30474  eupth2lem3lem3  30654  eupth2lem3lem6  30657  fusgreghash2wsp  30762  frrusgrord0lem  30763  numclwwlk1  30785  numclwwlk3  30809  ex-lcm  30882  ex-ind-dvds  30885  nnmulge  33156  elq2  33228  divnumden2  33232  pfxlsw2ccat  33338  ccatws1f1o  33339  wrdt2ind  33341  gsummptrev  33442  gsummptp1  33443  gsummulsubdishift1  33454  cycpmco2lem2  33513  cycpmco2lem3  33514  cycpmco2lem4  33515  cycpmco2lem5  33516  cycpmco2lem6  33517  cycpmco2lem7  33518  cycpmco2  33519  archiabllem1a  33577  gsumind  33731  deg1prod  33939  ply1dg3rt0irred  33940  esplyind  34031  esplyindfv  34032  esplyfvn  34033  vietadeg1  34034  vietalem  34035  vieta  34036  iconstr  34222  cos9thpiminplylem1  34238  oddpwdc  34811  eulerpartlemsv2  34815  eulerpartlems  34817  eulerpartlemsv3  34818  eulerpartlemv  34821  eulerpartlemb  34825  iwrdsplit  34844  ballotlemgun  34982  ccatmulgnn0dir  34999  ofcccat  35000  signsplypnf  35004  signslema  35016  signstfvn  35023  signstfveq0  35031  signsvtp  35037  signsvtn  35038  signlem0  35041  signshf  35042  fsum2dsub  35061  hashreprin  35074  breprexp  35087  circlemeth  35094  lpadlem2  35137  lpadlen2  35138  subfacp1lem6  35716  subfacval2  35718  subfaclim  35719  cvmliftlem7  35822  elmrsubrn  36051  bcprod  36269  bccolsum  36270  faclimlem1  36274  faclim2  36279  fwddifnp1  36696  knoppndvlem6  37165  knoppndvlem14  37173  poimirlem4  38334  poimirlem5  38335  poimirlem6  38336  poimirlem7  38337  poimirlem10  38340  poimirlem11  38341  poimirlem12  38342  poimirlem16  38346  poimirlem17  38347  poimirlem19  38349  poimirlem20  38350  poimirlem22  38352  poimirlem24  38354  poimirlem25  38355  poimirlem29  38359  poimirlem31  38361  lcmineqlem1  42856  lcmineqlem2  42857  lcmineqlem12  42867  lcmineqlem17  42872  primrootscoprmpow  42926  aks6d1c2p2  42946  deg1gprod  42967  deg1pow  42968  2np3bcnp1  42971  2ap1caineq  42972  sticksstones7  42979  sticksstones9  42981  sticksstones10  42982  sticksstones11  42983  sticksstones12a  42984  sticksstones12  42985  sticksstones22  42995  aks6d1c6lem1  42997  aks6d1c6lem3  42999  bcled  43005  bcle2d  43006  aks6d1c7lem1  43007  unitscyglem2  43023  unitscyglem4  43025  ccatcan2d  43079  fz1sump1  43131  sumcubes  43134  zaddcomlem  43297  frlmvscadiccat  43340  fltnltalem  43454  3cubeslem3l  43477  3cubeslem3r  43478  rmxyneg  43707  rmxyadd  43708  rmyp1  43720  rmxm1  43721  rmym1  43722  rmxluc  43723  rmyluc  43724  rmxdbl  43726  rmydbl  43727  jm2.18  43775  jm2.19lem1  43776  jm2.19lem2  43777  jm2.22  43782  jm2.23  43783  jm2.25  43786  jm2.27c  43794  rmxdiophlem  43802  expdioph  43810  hbtlem4  43913  relexpmulg  44496  radcnvrat  45084  nzprmdif  45089  bcc0  45110  bccp1k  45111  bccbc  45115  binomcxplemnn0  45119  binomcxplemrat  45120  binomcxplemfrat  45121  binomcxplemnotnn0  45126  fzisoeu  46079  mccllem  46373  dvxpaek  46714  dvnxpaek  46716  dvnmul  46717  dvnprodlem1  46720  dvnprodlem2  46721  stoweidlem24  46798  stirlinglem3  46850  stirlinglem7  46854  fourierdlem36  46917  fourierdlem47  46927  etransclem23  47031  etransclem32  47040  etransclem48  47056  fz0addcom  48114  fmtnom1nn  48344  fmtnof1  48347  fmtnorec1  48349  sqrtpwpw2p  48350  fmtnorec2lem  48354  fmtnorec3  48360  fmtnofac2lem  48380  fmtnofac2  48381  fmtnofac1  48382  lighneallem3  48419  lighneallem4b  48421  altgsumbc  49191  altgsumbcALT  49192  nnpw2pmod  49422  dignn0ehalf  49456  nn0sumshdiglemA  49458  nn0sumshdiglemB  49459  nn0sumshdiglem2  49461  nn0mullong  49464  itcovalpclem2  49510  itcovalt2lem2lem2  49513  itcovalt2lem1  49514  aacllem  50680