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

Theorem nn0cnd 12476
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 12475 . 2 (𝜑𝐴 ∈ ℝ)
32recnd 11184 1 (𝜑𝐴 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  cc 11050  0cn0 12414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pr 5385  ax-un 7673  ax-resscn 11109  ax-1cn 11110  ax-icn 11111  ax-addcl 11112  ax-addrcl 11113  ax-mulcl 11114  ax-mulrcl 11115  ax-i2m1 11120  ax-1ne0 11121  ax-rnegex 11123  ax-rrecex 11124  ax-cnre 11125
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-reu 3355  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-ov 7361  df-om 7804  df-2nd 7923  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-nn 12155  df-n0 12415
This theorem is referenced by:  quoremnn0ALT  13763  expaddzlem  14012  expaddz  14013  expmulz  14015  facdiv  14188  faclbnd4lem3  14196  bcp1n  14217  bcn2m1  14225  bcn2p1  14226  hashgadd  14278  hashdom  14280  hashun3  14285  hashssdif  14313  hashdifpr  14316  hashxplem  14334  hashmap  14336  hashreshashfun  14340  hashbclem  14350  hashf1lem2  14356  hashf1  14357  ccatval3  14468  ccatval21sw  14474  ccatlid  14475  ccatrid  14476  ccatass  14477  ccatrn  14478  lswccatn0lsw  14480  ccatalpha  14482  ccatws1lenp1b  14510  wrdlenccats1lenm1  14511  ccats1val2  14516  swrdccat2  14558  pfxfv  14571  addlenpfx  14580  pfxtrcfvl  14586  pfxpfx  14597  ccats1pfxeq  14603  ccatopth2  14606  cats1un  14610  swrdccat3b  14629  spllen  14643  splfv2a  14645  revccat  14655  cshwlen  14688  cshwidxmod  14692  repswcshw  14701  2cshwid  14703  cshweqdif2  14708  relexpaddg  14939  rtrclreclem3  14946  isercoll2  15554  iseraltlem3  15569  hash2iun1dif1  15710  binomlem  15715  bcxmas  15721  incexclem  15722  incexc  15723  incexc2  15724  climcndslem1  15735  climcndslem2  15736  arisum  15746  arisum2  15747  pwdif  15754  geomulcvg  15762  mertens  15772  risefacval2  15894  fallfacval2  15895  fallfacval3  15896  risefallfac  15908  risefacp1  15913  fallfacp1  15914  fallfacfwd  15920  binomfallfaclem1  15923  binomfallfaclem2  15924  binomrisefac  15926  bpolycl  15936  bpolysum  15937  bpolydiflem  15938  fsumkthpow  15940  bpoly4  15943  effsumlt  15994  dvdsexp  16211  nn0ob  16267  divalgmod  16289  bitsinv1lem  16322  sadcp1  16336  sadcaddlem  16338  sadadd2lem  16340  sadadd3  16342  sadaddlem  16347  sadasslem  16351  smupp1  16361  smumullem  16373  mulgcd  16430  absmulgcd  16431  mulgcdr  16432  gcddiv  16433  lcmgcd  16484  lcmid  16486  lcm1  16487  3lcm2e6woprm  16492  6lcm4e12  16493  mulgcddvds  16532  qredeu  16535  divgcdcoprm0  16542  divgcdcoprmex  16543  cncongr1  16544  cncongr2  16545  odzdvds  16668  powm2modprm  16676  coprimeprodsq  16681  pceulem  16718  pczpre  16720  pcqmul  16726  pcaddlem  16761  pcmpt  16765  pcmpt2  16766  sumhash  16769  oddprmdvds  16776  mul4sq  16827  4sqlem12  16829  vdwapun  16847  vdwlem2  16855  vdwlem3  16856  vdwlem6  16859  vdwlem8  16861  vdwlem9  16862  ramub1lem2  16900  ramcl  16902  mulgnn0dir  18907  mulgnn0ass  18913  lagsubg2  18992  psgnunilem2  19278  odmodnn0  19323  odmulg  19339  odmulgeq  19340  odinv  19344  sylow1lem1  19381  sylow2a  19402  sylow2blem3  19405  sylow3lem3  19412  sylow3lem4  19413  efginvrel2  19510  efgsval2  19516  efgsp1  19520  efgredlemg  19525  efgredleme  19526  efgcpbllemb  19538  odadd2  19628  odadd  19629  torsubg  19633  frgpnabllem1  19652  pgpfaclem1  19861  fincygsubgodd  19892  srgbinomlem3  19960  srgbinomlem4  19961  nn0srg  20870  mplcoe5  21444  mhpmulcl  21542  mhppwdeg  21543  coe1tmmul2  21650  coe1tmmul2fv  21652  coe1pwmulfv  21654  mbfi1fseqlem3  25085  dvn2bss  25297  itgpowd  25417  tdeglem4  25427  tdeglem4OLD  25428  tdeglem2  25429  mdegmullem  25446  coe1mul3  25467  ply1divex  25504  fta1glem1  25533  plyaddlem1  25577  plymullem1  25578  coeeulem  25588  coemulc  25619  dgrmulc  25635  dgrcolem2  25638  dgrco  25639  dvply1  25647  dvply2g  25648  plydivlem4  25659  fta1lem  25670  vieta1lem1  25673  aareccl  25689  aaliou3lem8  25708  taylply2  25730  dvtaylp  25732  dvntaylp  25733  dvntaylp0  25734  dvradcnv  25783  pserdvlem2  25790  advlogexp  26013  cxpeq  26113  atantayl3  26292  birthdaylem2  26305  harmonicbnd4  26363  dmgmaddnn0  26379  lgamucov  26390  wilthlem2  26421  basellem2  26434  basellem3  26435  basellem5  26437  0sgm  26496  sgmppw  26548  chtublem  26562  chpval2  26569  sumdchr2  26621  bcp1ctr  26630  lgslem1  26648  gausslemma2dlem6  26723  gausslemma2d  26725  lgseisenlem2  26727  lgseisenlem3  26728  lgsquadlem1  26731  lgsquadlem2  26732  lgsquad2lem2  26736  m1lgs  26739  2lgslem1c  26744  2lgslem3a  26747  2lgslem3b  26748  2lgslem3c  26749  2lgslem3d  26750  2sqlem8  26777  2sq2  26784  2sqmod  26787  dchrisumlem1  26840  dchrisum0flblem2  26860  rpvmasum2  26863  mulogsumlem  26882  selberg2lem  26901  pntrsumo1  26916  pntrlog2bndlem4  26931  finsumvtxdg2ssteplem4  28499  vtxdgoddnumeven  28504  wlklenvm1  28573  wlklenvclwlk  28606  crctcshlem4  28768  crctcsh  28772  wlklnwwlkln2lem  28830  wlknwwlksnbij  28836  wwlksnred  28840  wwlksnext  28841  wwlksnextbi  28842  wwlksnredwwlkn  28843  wwlksnextproplem2  28858  rusgrnumwwlks  28922  rusgrnumwwlk  28923  clwwlkccatlem  28936  clwlkclwwlk  28949  clwwlkwwlksb  29001  eupth2lem3lem3  29177  eupth2lem3lem6  29180  fusgreghash2wsp  29285  frrusgrord0lem  29286  numclwwlk1  29308  numclwwlk3  29332  ex-lcm  29405  ex-ind-dvds  29408  nnmulge  31658  divnumden2  31717  ccatf1  31808  pfxlsw2ccat  31809  wrdt2ind  31810  omndmul2  31923  omndmul3  31924  cycpmco2lem2  31979  cycpmco2lem3  31980  cycpmco2lem4  31981  cycpmco2lem5  31982  cycpmco2lem6  31983  cycpmco2lem7  31984  cycpmco2  31985  archiabllem1a  32030  freshmansdream  32070  oddpwdc  32957  eulerpartlemsv2  32961  eulerpartlems  32963  eulerpartlemsv3  32964  eulerpartlemv  32967  eulerpartlemb  32971  iwrdsplit  32990  ballotlemgun  33127  ccatmulgnn0dir  33157  ofcccat  33158  signsplypnf  33165  signslema  33177  signstfvn  33184  signstfveq0  33192  signsvtp  33198  signsvtn  33199  signlem0  33202  signshf  33203  fsum2dsub  33223  hashreprin  33236  breprexp  33249  circlemeth  33256  lpadlem2  33296  lpadlen2  33297  revpfxsfxrev  33712  revwlk  33721  subfacp1lem6  33782  subfacval2  33784  subfaclim  33785  cvmliftlem7  33888  elmrsubrn  34117  bcprod  34314  bccolsum  34315  faclimlem1  34319  faclim2  34324  fwddifnp1  34753  knoppndvlem6  34983  knoppndvlem14  34991  poimirlem4  36085  poimirlem5  36086  poimirlem6  36087  poimirlem7  36088  poimirlem10  36091  poimirlem11  36092  poimirlem12  36093  poimirlem16  36097  poimirlem17  36098  poimirlem19  36100  poimirlem20  36101  poimirlem22  36103  poimirlem24  36105  poimirlem25  36106  poimirlem29  36110  poimirlem31  36112  lcmineqlem1  40489  lcmineqlem2  40490  lcmineqlem12  40500  lcmineqlem17  40505  aks6d1c2p2  40552  2np3bcnp1  40555  2ap1caineq  40556  sticksstones7  40563  sticksstones9  40565  sticksstones10  40566  sticksstones11  40567  sticksstones12a  40568  sticksstones12  40569  sticksstones22  40579  ccatcan2d  40671  frlmvscadiccat  40684  zaddcomlem  40923  fltnltalem  41003  3cubeslem3l  41012  3cubeslem3r  41013  rmxyneg  41247  rmxyadd  41248  rmyp1  41260  rmxm1  41261  rmym1  41262  rmxluc  41263  rmyluc  41264  rmxdbl  41266  rmydbl  41267  jm2.18  41315  jm2.19lem1  41316  jm2.19lem2  41317  jm2.22  41322  jm2.23  41323  jm2.25  41326  jm2.27c  41334  rmxdiophlem  41342  expdioph  41350  hbtlem4  41456  relexpmulg  41989  radcnvrat  42601  nzprmdif  42606  bcc0  42627  bccp1k  42628  bccbc  42632  binomcxplemnn0  42636  binomcxplemrat  42637  binomcxplemfrat  42638  binomcxplemnotnn0  42643  fzisoeu  43541  mccllem  43845  dvxpaek  44188  dvnxpaek  44190  dvnmul  44191  dvnprodlem1  44194  dvnprodlem2  44195  stoweidlem24  44272  stirlinglem3  44324  stirlinglem7  44328  fourierdlem36  44391  fourierdlem47  44401  etransclem23  44505  etransclem32  44514  etransclem48  44530  fz0addcom  45556  fmtnom1nn  45731  fmtnof1  45734  fmtnorec1  45736  sqrtpwpw2p  45737  fmtnorec2lem  45741  fmtnorec3  45747  fmtnofac2lem  45767  fmtnofac2  45768  fmtnofac1  45769  lighneallem3  45806  lighneallem4b  45808  altgsumbc  46435  altgsumbcALT  46436  nnpw2pmod  46676  dignn0ehalf  46710  nn0sumshdiglemA  46712  nn0sumshdiglemB  46713  nn0sumshdiglem2  46715  nn0mullong  46718  itcovalpclem2  46764  itcovalt2lem2lem2  46767  itcovalt2lem1  46768  aacllem  47255
  Copyright terms: Public domain W3C validator