Theorem nn0cnd 12117

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

Syntax hints:   → wi 4   ∈ wcel 2112  ℂcc 10692  ℕ₀cn0 12055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307  ax-un 7501  ax-resscn 10751  ax-1cn 10752  ax-icn 10753  ax-addcl 10754  ax-addrcl 10755  ax-mulcl 10756  ax-mulrcl 10757  ax-i2m1 10762  ax-1ne0 10763  ax-rnegex 10765  ax-rrecex 10766  ax-cnre 10767

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ne 2933  df-ral 3056  df-rex 3057  df-reu 3058  df-rab 3060  df-v 3400  df-sbc 3684  df-csb 3799  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-pss 3872  df-nul 4224  df-if 4426  df-pw 4501  df-sn 4528  df-pr 4530  df-tp 4532  df-op 4534  df-uni 4806  df-iun 4892  df-br 5040  df-opab 5102  df-mpt 5121  df-tr 5147  df-id 5440  df-eprel 5445  df-po 5453  df-so 5454  df-fr 5494  df-we 5496  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-pred 6140  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6316  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-ov 7194  df-om 7623  df-wrecs 8025  df-recs 8086  df-rdg 8124  df-nn 11796  df-n0 12056

This theorem is referenced by:  quoremnn0ALT  13395  expaddzlem  13643  expaddz  13644  expmulz  13646  facdiv  13818  faclbnd4lem3  13826  bcp1n  13847  bcn2m1  13855  bcn2p1  13856  hashgadd  13909  hashdom  13911  hashun3  13916  hashssdif  13944  hashdifpr  13947  hashxplem  13965  hashmap  13967  hashreshashfun  13971  hashbclem  13981  hashf1lem2  13987  hashf1  13988  ccatval3  14101  ccatval21sw  14107  ccatlid  14108  ccatrid  14109  ccatass  14110  ccatrn  14111  lswccatn0lsw  14113  ccatalpha  14115  ccatws1lenp1b  14143  wrdlenccats1lenm1  14144  ccats1val2  14151  swrdccat2  14199  pfxfv  14212  addlenpfx  14221  pfxtrcfvl  14227  pfxpfx  14238  ccats1pfxeq  14244  ccatopth2  14247  cats1un  14251  swrdccat3b  14270  spllen  14284  splfv2a  14286  revccat  14296  cshwlen  14329  cshwidxmod  14333  repswcshw  14342  2cshwid  14344  cshweqdif2  14349  relexpaddg  14581  rtrclreclem3  14588  isercoll2  15197  iseraltlem3  15212  hash2iun1dif1  15351  binomlem  15356  bcxmas  15362  incexclem  15363  incexc  15364  incexc2  15365  climcndslem1  15376  climcndslem2  15377  arisum  15387  arisum2  15388  pwdif  15395  geomulcvg  15403  mertens  15413  risefacval2  15535  fallfacval2  15536  fallfacval3  15537  risefallfac  15549  risefacp1  15554  fallfacp1  15555  fallfacfwd  15561  binomfallfaclem1  15564  binomfallfaclem2  15565  binomrisefac  15567  bpolycl  15577  bpolysum  15578  bpolydiflem  15579  fsumkthpow  15581  bpoly4  15584  effsumlt  15635  dvdsexp  15852  nn0ob  15908  divalgmod  15930  bitsinv1lem  15963  sadcp1  15977  sadcaddlem  15979  sadadd2lem  15981  sadadd3  15983  sadaddlem  15988  sadasslem  15992  smupp1  16002  smumullem  16014  mulgcd  16071  absmulgcd  16072  mulgcdr  16073  gcddiv  16074  lcmgcd  16127  lcmid  16129  lcm1  16130  3lcm2e6woprm  16135  6lcm4e12  16136  mulgcddvds  16175  qredeu  16178  divgcdcoprm0  16185  divgcdcoprmex  16186  cncongr1  16187  cncongr2  16188  odzdvds  16311  powm2modprm  16319  coprimeprodsq  16324  pceulem  16361  pczpre  16363  pcqmul  16369  pcaddlem  16404  pcmpt  16408  pcmpt2  16409  sumhash  16412  oddprmdvds  16419  mul4sq  16470  4sqlem12  16472  vdwapun  16490  vdwlem2  16498  vdwlem3  16499  vdwlem6  16502  vdwlem8  16504  vdwlem9  16505  ramub1lem2  16543  ramcl  16545  mulgnn0dir  18475  mulgnn0ass  18481  lagsubg2  18559  psgnunilem2  18841  odmodnn0  18886  odmulg  18901  odmulgeq  18902  odinv  18906  sylow1lem1  18941  sylow2a  18962  sylow2blem3  18965  sylow3lem3  18972  sylow3lem4  18973  efginvrel2  19071  efgsval2  19077  efgsp1  19081  efgredlemg  19086  efgredleme  19087  efgcpbllemb  19099  odadd2  19188  odadd  19189  torsubg  19193  frgpnabllem1  19212  pgpfaclem1  19422  fincygsubgodd  19453  srgbinomlem3  19511  srgbinomlem4  19512  nn0srg  20387  mplcoe5  20951  mhpmulcl  21043  mhppwdeg  21044  coe1tmmul2  21151  coe1tmmul2fv  21153  coe1pwmulfv  21155  mbfi1fseqlem3  24569  dvn2bss  24781  itgpowd  24901  tdeglem4  24911  tdeglem4OLD  24912  tdeglem2  24913  mdegmullem  24930  coe1mul3  24951  ply1divex  24988  fta1glem1  25017  plyaddlem1  25061  plymullem1  25062  coeeulem  25072  coemulc  25103  dgrmulc  25119  dgrcolem2  25122  dgrco  25123  dvply1  25131  dvply2g  25132  plydivlem4  25143  fta1lem  25154  vieta1lem1  25157  aareccl  25173  aaliou3lem8  25192  taylply2  25214  dvtaylp  25216  dvntaylp  25217  dvntaylp0  25218  dvradcnv  25267  pserdvlem2  25274  advlogexp  25497  cxpeq  25597  atantayl3  25776  birthdaylem2  25789  harmonicbnd4  25847  dmgmaddnn0  25863  lgamucov  25874  wilthlem2  25905  basellem2  25918  basellem3  25919  basellem5  25921  0sgm  25980  sgmppw  26032  chtublem  26046  chpval2  26053  sumdchr2  26105  bcp1ctr  26114  lgslem1  26132  gausslemma2dlem6  26207  gausslemma2d  26209  lgseisenlem2  26211  lgseisenlem3  26212  lgsquadlem1  26215  lgsquadlem2  26216  lgsquad2lem2  26220  m1lgs  26223  2lgslem1c  26228  2lgslem3a  26231  2lgslem3b  26232  2lgslem3c  26233  2lgslem3d  26234  2sqlem8  26261  2sq2  26268  2sqmod  26271  dchrisumlem1  26324  dchrisum0flblem2  26344  rpvmasum2  26347  mulogsumlem  26366  selberg2lem  26385  pntrsumo1  26400  pntrlog2bndlem4  26415  finsumvtxdg2ssteplem4  27590  vtxdgoddnumeven  27595  wlklenvm1  27663  wlklenvclwlk  27696  crctcshlem4  27858  crctcsh  27862  wlklnwwlkln2lem  27920  wlknwwlksnbij  27926  wwlksnred  27930  wwlksnext  27931  wwlksnextbi  27932  wwlksnredwwlkn  27933  wwlksnextproplem2  27948  rusgrnumwwlks  28012  rusgrnumwwlk  28013  clwwlkccatlem  28026  clwlkclwwlk  28039  clwwlkwwlksb  28091  eupth2lem3lem3  28267  eupth2lem3lem6  28270  fusgreghash2wsp  28375  frrusgrord0lem  28376  numclwwlk1  28398  numclwwlk3  28422  ex-lcm  28495  ex-ind-dvds  28498  nnmulge  30747  divnumden2  30806  ccatf1  30897  pfxlsw2ccat  30898  wrdt2ind  30899  omndmul2  31011  omndmul3  31012  cycpmco2lem2  31067  cycpmco2lem3  31068  cycpmco2lem4  31069  cycpmco2lem5  31070  cycpmco2lem6  31071  cycpmco2lem7  31072  cycpmco2  31073  archiabllem1a  31118  freshmansdream  31157  oddpwdc  31987  eulerpartlemsv2  31991  eulerpartlems  31993  eulerpartlemsv3  31994  eulerpartlemv  31997  eulerpartlemb  32001  iwrdsplit  32020  ballotlemgun  32157  ccatmulgnn0dir  32187  ofcccat  32188  signsplypnf  32195  signslema  32207  signstfvn  32214  signstfveq0  32222  signsvtp  32228  signsvtn  32229  signlem0  32232  signshf  32233  fsum2dsub  32253  hashreprin  32266  breprexp  32279  circlemeth  32286  lpadlem2  32326  lpadlen2  32327  revpfxsfxrev  32744  revwlk  32753  subfacp1lem6  32814  subfacval2  32816  subfaclim  32817  cvmliftlem7  32920  elmrsubrn  33149  bcprod  33373  bccolsum  33374  faclimlem1  33378  faclim2  33383  fwddifnp1  34153  knoppndvlem6  34383  knoppndvlem14  34391  poimirlem4  35467  poimirlem5  35468  poimirlem6  35469  poimirlem7  35470  poimirlem10  35473  poimirlem11  35474  poimirlem12  35475  poimirlem16  35479  poimirlem17  35480  poimirlem19  35482  poimirlem20  35483  poimirlem22  35485  poimirlem24  35487  poimirlem25  35488  poimirlem29  35492  poimirlem31  35494  lcmineqlem1  39720  lcmineqlem2  39721  lcmineqlem12  39731  lcmineqlem17  39736  2np3bcnp1  39769  2ap1caineq  39770  sticksstones7  39777  sticksstones9  39779  sticksstones10  39780  sticksstones11  39781  sticksstones12a  39782  sticksstones12  39783  ccatcan2d  39873  frlmvscadiccat  39891  fltnltalem  40143  3cubeslem3l  40152  3cubeslem3r  40153  rmxyneg  40386  rmxyadd  40387  rmyp1  40399  rmxm1  40400  rmym1  40401  rmxluc  40402  rmyluc  40403  rmxdbl  40405  rmydbl  40406  jm2.18  40454  jm2.19lem1  40455  jm2.19lem2  40456  jm2.22  40461  jm2.23  40462  jm2.25  40465  jm2.27c  40473  rmxdiophlem  40481  expdioph  40489  hbtlem4  40595  relexpmulg  40936  radcnvrat  41546  nzprmdif  41551  bcc0  41572  bccp1k  41573  bccbc  41577  binomcxplemnn0  41581  binomcxplemrat  41582  binomcxplemfrat  41583  binomcxplemnotnn0  41588  fzisoeu  42453  mccllem  42756  dvxpaek  43099  dvnxpaek  43101  dvnmul  43102  dvnprodlem1  43105  dvnprodlem2  43106  stoweidlem24  43183  stirlinglem3  43235  stirlinglem7  43239  fourierdlem36  43302  fourierdlem47  43312  etransclem23  43416  etransclem32  43425  etransclem48  43441  fz0addcom  44425  fmtnom1nn  44600  fmtnof1  44603  fmtnorec1  44605  sqrtpwpw2p  44606  fmtnorec2lem  44610  fmtnorec3  44616  fmtnofac2lem  44636  fmtnofac2  44637  fmtnofac1  44638  lighneallem3  44675  lighneallem4b  44677  altgsumbc  45304  altgsumbcALT  45305  nnpw2pmod  45545  dignn0ehalf  45579  nn0sumshdiglemA  45581  nn0sumshdiglemB  45582  nn0sumshdiglem2  45584  nn0mullong  45587  itcovalpclem2  45633  itcovalt2lem2lem2  45636  itcovalt2lem1  45637  aacllem  46119