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

Theorem nn0cnd 11541
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 11540 . 2 (𝜑𝐴 ∈ ℝ)
32recnd 10256 1 (𝜑𝐴 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2135  cc 10122  0cn0 11480
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-8 2137  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-sep 4929  ax-nul 4937  ax-pow 4988  ax-pr 5051  ax-un 7110  ax-resscn 10181  ax-1cn 10182  ax-icn 10183  ax-addcl 10184  ax-addrcl 10185  ax-mulcl 10186  ax-mulrcl 10187  ax-i2m1 10192  ax-1ne0 10193  ax-rnegex 10195  ax-rrecex 10196  ax-cnre 10197
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-eu 2607  df-mo 2608  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ne 2929  df-ral 3051  df-rex 3052  df-reu 3053  df-rab 3055  df-v 3338  df-sbc 3573  df-csb 3671  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-pss 3727  df-nul 4055  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4585  df-iun 4670  df-br 4801  df-opab 4861  df-mpt 4878  df-tr 4901  df-id 5170  df-eprel 5175  df-po 5183  df-so 5184  df-fr 5221  df-we 5223  df-xp 5268  df-rel 5269  df-cnv 5270  df-co 5271  df-dm 5272  df-rn 5273  df-res 5274  df-ima 5275  df-pred 5837  df-ord 5883  df-on 5884  df-lim 5885  df-suc 5886  df-iota 6008  df-fun 6047  df-fn 6048  df-f 6049  df-f1 6050  df-fo 6051  df-f1o 6052  df-fv 6053  df-ov 6812  df-om 7227  df-wrecs 7572  df-recs 7633  df-rdg 7671  df-nn 11209  df-n0 11481
This theorem is referenced by:  quoremnn0ALT  12846  expaddzlem  13093  expaddz  13094  expmulz  13096  facdiv  13264  faclbnd4lem3  13272  bcp1n  13293  bcn2m1  13301  bcn2p1  13302  hashgadd  13354  hashdom  13356  hashun3  13361  hashssdif  13388  hashdifpr  13391  hashxplem  13408  hashmap  13410  hashreshashfun  13414  hashbclem  13424  hashf1lem2  13428  hashf1  13429  ccatval3  13547  ccatval21sw  13553  ccatlid  13554  ccatrid  13555  ccatass  13556  ccatrn  13557  lswccatn0lsw  13559  ccatalpha  13561  ccatws1lenp1b  13589  wrdlenccats1lenm1  13590  wrdlenccats1lenm1OLD  13591  ccats1val2  13597  ccatws1lenrevOLD  13602  swrd0f  13623  swrdid  13624  addlenswrd  13634  swrdtrcfvl  13646  swrdccat2  13654  ccatopth2  13667  cats1un  13671  swrdccat3b  13692  spllen  13701  splfv2a  13703  revccat  13711  cshwlen  13741  cshwidxmod  13745  repswcshw  13754  2cshwid  13756  cshweqdif2  13761  relexpaddg  13988  rtrclreclem3  13995  isercoll2  14594  iseraltlem3  14609  hash2iun1dif1  14751  binomlem  14756  bcxmas  14762  incexclem  14763  incexc  14764  incexc2  14765  climcndslem1  14776  climcndslem2  14777  arisum  14787  arisum2  14788  geomulcvg  14802  mertens  14813  risefacval2  14936  fallfacval2  14937  fallfacval3  14938  risefallfac  14950  risefacp1  14955  fallfacp1  14956  fallfacfwd  14962  binomfallfaclem1  14965  binomfallfaclem2  14966  binomrisefac  14968  bpolycl  14978  bpolysum  14979  bpolydiflem  14980  fsumkthpow  14982  bpoly4  14985  effsumlt  15036  dvdsexp  15247  nn0ob  15298  divalgmod  15327  divalgmodOLD  15328  bitsinv1lem  15361  sadcp1  15375  sadcaddlem  15377  sadadd2lem  15379  sadadd3  15381  sadaddlem  15386  sadasslem  15390  smupp1  15400  smumullem  15412  mulgcd  15463  absmulgcd  15464  mulgcdr  15465  gcddiv  15466  lcmgcd  15518  lcmid  15520  lcm1  15521  3lcm2e6woprm  15526  6lcm4e12  15527  mulgcddvds  15567  qredeu  15570  divgcdcoprm0  15577  divgcdcoprmex  15578  cncongr1  15579  cncongr2  15580  odzdvds  15698  powm2modprm  15706  coprimeprodsq  15711  pceulem  15748  pczpre  15750  pcqmul  15756  pcaddlem  15790  pcmpt  15794  pcmpt2  15795  sumhash  15798  oddprmdvds  15805  mul4sq  15856  4sqlem12  15858  vdwapun  15876  vdwlem2  15884  vdwlem3  15885  vdwlem6  15888  vdwlem8  15890  vdwlem9  15891  ramub1lem2  15929  ramcl  15931  mulgnn0dir  17768  mulgnn0ass  17775  lagsubg2  17852  psgnunilem2  18111  odmodnn0  18155  odmulg  18169  odmulgeq  18170  odinv  18174  sylow1lem1  18209  sylow2a  18230  sylow2blem3  18233  sylow3lem3  18240  sylow3lem4  18241  efginvrel2  18336  efgsval2  18342  efgsp1  18346  efgredlemg  18351  efgredleme  18352  efgcpbllemb  18364  odadd2  18448  odadd  18449  torsubg  18453  frgpnabllem1  18472  pgpfaclem1  18676  srgbinomlem3  18738  srgbinomlem4  18739  mplcoe5  19666  coe1tmmul2  19844  coe1tmmul2fv  19846  coe1pwmulfv  19848  nn0srg  20014  mbfi1fseqlem3  23679  dvn2bss  23888  tdeglem4  24015  tdeglem2  24016  mdegmullem  24033  coe1mul3  24054  ply1divex  24091  fta1glem1  24120  plyaddlem1  24164  plymullem1  24165  coeeulem  24175  coemulc  24206  dgrmulc  24222  dgrcolem2  24225  dgrco  24226  dvply1  24234  dvply2g  24235  plydivlem4  24246  fta1lem  24257  vieta1lem1  24260  aareccl  24276  aaliou3lem8  24295  taylply2  24317  dvtaylp  24319  dvntaylp  24320  dvntaylp0  24321  dvradcnv  24370  pserdvlem2  24377  advlogexp  24596  cxpeq  24693  atantayl3  24861  birthdaylem2  24874  harmonicbnd4  24932  dmgmaddnn0  24948  lgamucov  24959  wilthlem2  24990  basellem2  25003  basellem3  25004  basellem5  25006  0sgm  25065  sgmppw  25117  chtublem  25131  chpval2  25138  sumdchr2  25190  bcp1ctr  25199  lgslem1  25217  gausslemma2dlem6  25292  gausslemma2d  25294  lgseisenlem2  25296  lgseisenlem3  25297  lgsquadlem1  25300  lgsquadlem2  25301  lgsquad2lem2  25305  m1lgs  25308  2lgslem1c  25313  2lgslem3a  25316  2lgslem3b  25317  2lgslem3c  25318  2lgslem3d  25319  2sqlem8  25346  dchrisumlem1  25373  dchrisum0flblem2  25393  rpvmasum2  25396  mulogsumlem  25415  selberg2lem  25434  pntrsumo1  25449  pntrlog2bndlem4  25464  finsumvtxdg2ssteplem4  26650  vtxdgoddnumeven  26655  wlklenvm1  26723  crctcshlem4  26919  crctcsh  26923  wlklnwwlkln2lem  26987  wwlksnred  27006  wwlksnext  27007  wwlksnextbi  27008  wwlksnredwwlkn  27009  wwlksnextproplem2  27024  rusgrnumwwlks  27092  rusgrnumwwlk  27093  clwwlkccatlem  27108  clwlkclwwlk  27121  clwwlkwwlksb  27180  eupth2lem3lem3  27378  eupth2lem3lem6  27381  fusgreghash2wsp  27488  frrusgrord0lem  27489  numclwwlk1  27516  numclwwlk3  27549  ex-lcm  27622  ex-ind-dvds  27625  nnmulge  29820  divnumden2  29869  2sqmod  29953  omndmul2  30017  omndmul3  30018  archiabllem1a  30050  oddpwdc  30721  eulerpartlemsv2  30725  eulerpartlems  30727  eulerpartlemsv3  30728  eulerpartlemv  30731  eulerpartlemb  30735  iwrdsplit  30754  ballotlemgun  30891  ccatmulgnn0dir  30924  ofcccat  30925  signsplypnf  30932  signslema  30944  signstfvn  30951  signstfveq0  30959  signsvtp  30965  signsvtn  30966  signlem0  30969  signshf  30970  fsum2dsub  30990  hashreprin  31003  breprexp  31016  circlemeth  31023  subfacp1lem6  31470  subfacval2  31472  subfaclim  31473  cvmliftlem7  31576  elmrsubrn  31720  bcprod  31927  bccolsum  31928  faclimlem1  31932  faclim2  31937  fwddifnp1  32574  knoppndvlem6  32810  knoppndvlem14  32818  poimirlem4  33722  poimirlem5  33723  poimirlem6  33724  poimirlem7  33725  poimirlem10  33728  poimirlem11  33729  poimirlem12  33730  poimirlem16  33734  poimirlem17  33735  poimirlem19  33737  poimirlem20  33738  poimirlem22  33740  poimirlem24  33742  poimirlem25  33743  poimirlem29  33747  poimirlem31  33749  rmxyneg  37983  rmxyadd  37984  rmyp1  37996  rmxm1  37997  rmym1  37998  rmxluc  37999  rmyluc  38000  rmxdbl  38002  rmydbl  38003  jm2.18  38053  jm2.19lem1  38054  jm2.19lem2  38055  jm2.22  38060  jm2.23  38061  jm2.25  38064  jm2.27c  38072  rmxdiophlem  38080  expdioph  38088  hbtlem4  38194  itgpowd  38298  relexpmulg  38500  radcnvrat  39011  nzprmdif  39016  bcc0  39037  bccp1k  39038  bccbc  39042  binomcxplemnn0  39046  binomcxplemrat  39047  binomcxplemfrat  39048  binomcxplemnotnn0  39053  fzisoeu  40009  mccllem  40328  dvxpaek  40654  dvnxpaek  40656  dvnmul  40657  dvnprodlem1  40660  dvnprodlem2  40661  stoweidlem24  40740  stirlinglem3  40792  stirlinglem7  40796  fourierdlem36  40859  fourierdlem47  40869  etransclem23  40973  etransclem32  40982  etransclem48  40998  fz0addcom  41833  addlenpfx  41904  pfxfv  41905  pfxtrcfvl  41911  pfxpfx  41921  ccats1pfxeq  41927  fmtnom1nn  41950  fmtnof1  41953  fmtnorec1  41955  sqrtpwpw2p  41956  fmtnorec2lem  41960  fmtnorec3  41966  fmtnofac2lem  41986  fmtnofac2  41987  fmtnofac1  41988  pwdif  42007  lighneallem3  42030  lighneallem4b  42032  altgsumbc  42636  altgsumbcALT  42637  nnpw2pmod  42883  dignn0ehalf  42917  nn0sumshdiglemA  42919  nn0sumshdiglemB  42920  nn0sumshdiglem2  42922  nn0mullong  42925  aacllem  43056
  Copyright terms: Public domain W3C validator