MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nn0cnd Structured version   Visualization version   GIF version

Theorem nn0cnd 11949
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
StepHypRef Expression
1 nn0red.1 . . 3 (𝜑𝐴 ∈ ℕ0)
21nn0red 11948 . 2 (𝜑𝐴 ∈ ℝ)
32recnd 10662 1 (𝜑𝐴 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2112  cc 10528  0cn0 11889
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-i2m1 10598  ax-1ne0 10599  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-reu 3116  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-ov 7142  df-om 7565  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-nn 11630  df-n0 11890
This theorem is referenced by:  quoremnn0ALT  13224  expaddzlem  13472  expaddz  13473  expmulz  13475  facdiv  13647  faclbnd4lem3  13655  bcp1n  13676  bcn2m1  13684  bcn2p1  13685  hashgadd  13738  hashdom  13740  hashun3  13745  hashssdif  13773  hashdifpr  13776  hashxplem  13794  hashmap  13796  hashreshashfun  13800  hashbclem  13810  hashf1lem2  13814  hashf1  13815  ccatval3  13928  ccatval21sw  13934  ccatlid  13935  ccatrid  13936  ccatass  13937  ccatrn  13938  lswccatn0lsw  13940  ccatalpha  13942  ccatws1lenp1b  13970  wrdlenccats1lenm1  13971  ccats1val2  13978  swrdccat2  14026  pfxfv  14039  addlenpfx  14048  pfxtrcfvl  14054  pfxpfx  14065  ccats1pfxeq  14071  ccatopth2  14074  cats1un  14078  swrdccat3b  14097  spllen  14111  splfv2a  14113  revccat  14123  cshwlen  14156  cshwidxmod  14160  repswcshw  14169  2cshwid  14171  cshweqdif2  14176  relexpaddg  14407  rtrclreclem3  14414  isercoll2  15020  iseraltlem3  15035  hash2iun1dif1  15174  binomlem  15179  bcxmas  15185  incexclem  15186  incexc  15187  incexc2  15188  climcndslem1  15199  climcndslem2  15200  arisum  15210  arisum2  15211  pwdif  15218  geomulcvg  15227  mertens  15237  risefacval2  15359  fallfacval2  15360  fallfacval3  15361  risefallfac  15373  risefacp1  15378  fallfacp1  15379  fallfacfwd  15385  binomfallfaclem1  15388  binomfallfaclem2  15389  binomrisefac  15391  bpolycl  15401  bpolysum  15402  bpolydiflem  15403  fsumkthpow  15405  bpoly4  15408  effsumlt  15459  dvdsexp  15672  nn0ob  15728  divalgmod  15750  bitsinv1lem  15783  sadcp1  15797  sadcaddlem  15799  sadadd2lem  15801  sadadd3  15803  sadaddlem  15808  sadasslem  15812  smupp1  15822  smumullem  15834  mulgcd  15889  absmulgcd  15890  mulgcdr  15891  gcddiv  15892  lcmgcd  15944  lcmid  15946  lcm1  15947  3lcm2e6woprm  15952  6lcm4e12  15953  mulgcddvds  15992  qredeu  15995  divgcdcoprm0  16002  divgcdcoprmex  16003  cncongr1  16004  cncongr2  16005  odzdvds  16125  powm2modprm  16133  coprimeprodsq  16138  pceulem  16175  pczpre  16177  pcqmul  16183  pcaddlem  16217  pcmpt  16221  pcmpt2  16222  sumhash  16225  oddprmdvds  16232  mul4sq  16283  4sqlem12  16285  vdwapun  16303  vdwlem2  16311  vdwlem3  16312  vdwlem6  16315  vdwlem8  16317  vdwlem9  16318  ramub1lem2  16356  ramcl  16358  mulgnn0dir  18252  mulgnn0ass  18258  lagsubg2  18336  psgnunilem2  18618  odmodnn0  18663  odmulg  18678  odmulgeq  18679  odinv  18683  sylow1lem1  18718  sylow2a  18739  sylow2blem3  18742  sylow3lem3  18749  sylow3lem4  18750  efginvrel2  18848  efgsval2  18854  efgsp1  18858  efgredlemg  18863  efgredleme  18864  efgcpbllemb  18876  odadd2  18965  odadd  18966  torsubg  18970  frgpnabllem1  18989  pgpfaclem1  19199  fincygsubgodd  19230  srgbinomlem3  19288  srgbinomlem4  19289  nn0srg  20164  mplcoe5  20711  coe1tmmul2  20908  coe1tmmul2fv  20910  coe1pwmulfv  20912  mbfi1fseqlem3  24324  dvn2bss  24536  itgpowd  24656  tdeglem4  24664  tdeglem2  24665  mdegmullem  24682  coe1mul3  24703  ply1divex  24740  fta1glem1  24769  plyaddlem1  24813  plymullem1  24814  coeeulem  24824  coemulc  24855  dgrmulc  24871  dgrcolem2  24874  dgrco  24875  dvply1  24883  dvply2g  24884  plydivlem4  24895  fta1lem  24906  vieta1lem1  24909  aareccl  24925  aaliou3lem8  24944  taylply2  24966  dvtaylp  24968  dvntaylp  24969  dvntaylp0  24970  dvradcnv  25019  pserdvlem2  25026  advlogexp  25249  cxpeq  25349  atantayl3  25528  birthdaylem2  25541  harmonicbnd4  25599  dmgmaddnn0  25615  lgamucov  25626  wilthlem2  25657  basellem2  25670  basellem3  25671  basellem5  25673  0sgm  25732  sgmppw  25784  chtublem  25798  chpval2  25805  sumdchr2  25857  bcp1ctr  25866  lgslem1  25884  gausslemma2dlem6  25959  gausslemma2d  25961  lgseisenlem2  25963  lgseisenlem3  25964  lgsquadlem1  25967  lgsquadlem2  25968  lgsquad2lem2  25972  m1lgs  25975  2lgslem1c  25980  2lgslem3a  25983  2lgslem3b  25984  2lgslem3c  25985  2lgslem3d  25986  2sqlem8  26013  2sq2  26020  2sqmod  26023  dchrisumlem1  26076  dchrisum0flblem2  26096  rpvmasum2  26099  mulogsumlem  26118  selberg2lem  26137  pntrsumo1  26152  pntrlog2bndlem4  26167  finsumvtxdg2ssteplem4  27341  vtxdgoddnumeven  27346  wlklenvm1  27414  wlklenvclwlk  27447  crctcshlem4  27609  crctcsh  27613  wlklnwwlkln2lem  27671  wlknwwlksnbij  27677  wwlksnred  27681  wwlksnext  27682  wwlksnextbi  27683  wwlksnredwwlkn  27684  wwlksnextproplem2  27699  rusgrnumwwlks  27763  rusgrnumwwlk  27764  clwwlkccatlem  27777  clwlkclwwlk  27790  clwwlkwwlksb  27842  eupth2lem3lem3  28018  eupth2lem3lem6  28021  fusgreghash2wsp  28126  frrusgrord0lem  28127  numclwwlk1  28149  numclwwlk3  28173  ex-lcm  28246  ex-ind-dvds  28249  nnmulge  30503  divnumden2  30563  ccatf1  30654  pfxlsw2ccat  30655  wrdt2ind  30656  omndmul2  30766  omndmul3  30767  cycpmco2lem2  30822  cycpmco2lem3  30823  cycpmco2lem4  30824  cycpmco2lem5  30825  cycpmco2lem6  30826  cycpmco2lem7  30827  cycpmco2  30828  archiabllem1a  30873  freshmansdream  30912  oddpwdc  31720  eulerpartlemsv2  31724  eulerpartlems  31726  eulerpartlemsv3  31727  eulerpartlemv  31730  eulerpartlemb  31734  iwrdsplit  31753  ballotlemgun  31890  ccatmulgnn0dir  31920  ofcccat  31921  signsplypnf  31928  signslema  31940  signstfvn  31947  signstfveq0  31955  signsvtp  31961  signsvtn  31962  signlem0  31965  signshf  31966  fsum2dsub  31986  hashreprin  31999  breprexp  32012  circlemeth  32019  lpadlem2  32059  lpadlen2  32060  revpfxsfxrev  32470  revwlk  32479  subfacp1lem6  32540  subfacval2  32542  subfaclim  32543  cvmliftlem7  32646  elmrsubrn  32875  bcprod  33078  bccolsum  33079  faclimlem1  33083  faclim2  33088  fwddifnp1  33734  knoppndvlem6  33964  knoppndvlem14  33972  poimirlem4  35054  poimirlem5  35055  poimirlem6  35056  poimirlem7  35057  poimirlem10  35060  poimirlem11  35061  poimirlem12  35062  poimirlem16  35066  poimirlem17  35067  poimirlem19  35069  poimirlem20  35070  poimirlem22  35072  poimirlem24  35074  poimirlem25  35075  poimirlem29  35079  poimirlem31  35081  lcmineqlem1  39310  lcmineqlem2  39311  lcmineqlem12  39321  lcmineqlem17  39326  2np3bcnp1  39339  2ap1caineq  39340  ccatcan2d  39409  frlmvscadiccat  39427  fltnltalem  39605  3cubeslem3l  39614  3cubeslem3r  39615  rmxyneg  39848  rmxyadd  39849  rmyp1  39861  rmxm1  39862  rmym1  39863  rmxluc  39864  rmyluc  39865  rmxdbl  39867  rmydbl  39868  jm2.18  39916  jm2.19lem1  39917  jm2.19lem2  39918  jm2.22  39923  jm2.23  39924  jm2.25  39927  jm2.27c  39935  rmxdiophlem  39943  expdioph  39951  hbtlem4  40057  relexpmulg  40398  radcnvrat  41005  nzprmdif  41010  bcc0  41031  bccp1k  41032  bccbc  41036  binomcxplemnn0  41040  binomcxplemrat  41041  binomcxplemfrat  41042  binomcxplemnotnn0  41047  fzisoeu  41919  mccllem  42226  dvxpaek  42569  dvnxpaek  42571  dvnmul  42572  dvnprodlem1  42575  dvnprodlem2  42576  stoweidlem24  42653  stirlinglem3  42705  stirlinglem7  42709  fourierdlem36  42772  fourierdlem47  42782  etransclem23  42886  etransclem32  42895  etransclem48  42911  fz0addcom  43861  fmtnom1nn  44036  fmtnof1  44039  fmtnorec1  44041  sqrtpwpw2p  44042  fmtnorec2lem  44046  fmtnorec3  44052  fmtnofac2lem  44072  fmtnofac2  44073  fmtnofac1  44074  lighneallem3  44112  lighneallem4b  44114  altgsumbc  44741  altgsumbcALT  44742  nnpw2pmod  44984  dignn0ehalf  45018  nn0sumshdiglemA  45020  nn0sumshdiglemB  45021  nn0sumshdiglem2  45023  nn0mullong  45026  itcovalpclem2  45072  itcovalt2lem2lem2  45075  itcovalt2lem1  45076  aacllem  45316
  Copyright terms: Public domain W3C validator