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

Theorem nn0cnd 11565
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 11564 . 2 (𝜑𝐴 ∈ ℝ)
32recnd 10280 1 (𝜑𝐴 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2139  cc 10146  0cn0 11504
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115  ax-resscn 10205  ax-1cn 10206  ax-icn 10207  ax-addcl 10208  ax-addrcl 10209  ax-mulcl 10210  ax-mulrcl 10211  ax-i2m1 10216  ax-1ne0 10217  ax-rnegex 10219  ax-rrecex 10220  ax-cnre 10221
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-reu 3057  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-ov 6817  df-om 7232  df-wrecs 7577  df-recs 7638  df-rdg 7676  df-nn 11233  df-n0 11505
This theorem is referenced by:  quoremnn0ALT  12870  expaddzlem  13117  expaddz  13118  expmulz  13120  facdiv  13288  faclbnd4lem3  13296  bcp1n  13317  bcn2m1  13325  bcn2p1  13326  hashgadd  13378  hashdom  13380  hashun3  13385  hashssdif  13412  hashdifpr  13415  hashxplem  13432  hashmap  13434  hashreshashfun  13438  hashbclem  13448  hashf1lem2  13452  hashf1  13453  ccatval3  13571  ccatval21sw  13577  ccatlid  13578  ccatrid  13579  ccatass  13580  ccatrn  13581  lswccatn0lsw  13583  ccatalpha  13585  ccatws1lenp1b  13613  wrdlenccats1lenm1  13614  wrdlenccats1lenm1OLD  13615  ccats1val2  13621  ccatws1lenrevOLD  13626  swrd0f  13647  swrdid  13648  addlenswrd  13658  swrdtrcfvl  13670  swrdccat2  13678  ccatopth2  13691  cats1un  13695  swrdccat3b  13716  spllen  13725  splfv2a  13727  revccat  13735  cshwlen  13765  cshwidxmod  13769  repswcshw  13778  2cshwid  13780  cshweqdif2  13785  relexpaddg  14012  rtrclreclem3  14019  isercoll2  14618  iseraltlem3  14633  hash2iun1dif1  14775  binomlem  14780  bcxmas  14786  incexclem  14787  incexc  14788  incexc2  14789  climcndslem1  14800  climcndslem2  14801  arisum  14811  arisum2  14812  geomulcvg  14826  mertens  14837  risefacval2  14960  fallfacval2  14961  fallfacval3  14962  risefallfac  14974  risefacp1  14979  fallfacp1  14980  fallfacfwd  14986  binomfallfaclem1  14989  binomfallfaclem2  14990  binomrisefac  14992  bpolycl  15002  bpolysum  15003  bpolydiflem  15004  fsumkthpow  15006  bpoly4  15009  effsumlt  15060  dvdsexp  15271  nn0ob  15322  divalgmod  15351  divalgmodOLD  15352  bitsinv1lem  15385  sadcp1  15399  sadcaddlem  15401  sadadd2lem  15403  sadadd3  15405  sadaddlem  15410  sadasslem  15414  smupp1  15424  smumullem  15436  mulgcd  15487  absmulgcd  15488  mulgcdr  15489  gcddiv  15490  lcmgcd  15542  lcmid  15544  lcm1  15545  3lcm2e6woprm  15550  6lcm4e12  15551  mulgcddvds  15591  qredeu  15594  divgcdcoprm0  15601  divgcdcoprmex  15602  cncongr1  15603  cncongr2  15604  odzdvds  15722  powm2modprm  15730  coprimeprodsq  15735  pceulem  15772  pczpre  15774  pcqmul  15780  pcaddlem  15814  pcmpt  15818  pcmpt2  15819  sumhash  15822  oddprmdvds  15829  mul4sq  15880  4sqlem12  15882  vdwapun  15900  vdwlem2  15908  vdwlem3  15909  vdwlem6  15912  vdwlem8  15914  vdwlem9  15915  ramub1lem2  15953  ramcl  15955  mulgnn0dir  17792  mulgnn0ass  17799  lagsubg2  17876  psgnunilem2  18135  odmodnn0  18179  odmulg  18193  odmulgeq  18194  odinv  18198  sylow1lem1  18233  sylow2a  18254  sylow2blem3  18257  sylow3lem3  18264  sylow3lem4  18265  efginvrel2  18360  efgsval2  18366  efgsp1  18370  efgredlemg  18375  efgredleme  18376  efgcpbllemb  18388  odadd2  18472  odadd  18473  torsubg  18477  frgpnabllem1  18496  pgpfaclem1  18700  srgbinomlem3  18762  srgbinomlem4  18763  mplcoe5  19690  coe1tmmul2  19868  coe1tmmul2fv  19870  coe1pwmulfv  19872  nn0srg  20038  mbfi1fseqlem3  23703  dvn2bss  23912  tdeglem4  24039  tdeglem2  24040  mdegmullem  24057  coe1mul3  24078  ply1divex  24115  fta1glem1  24144  plyaddlem1  24188  plymullem1  24189  coeeulem  24199  coemulc  24230  dgrmulc  24246  dgrcolem2  24249  dgrco  24250  dvply1  24258  dvply2g  24259  plydivlem4  24270  fta1lem  24281  vieta1lem1  24284  aareccl  24300  aaliou3lem8  24319  taylply2  24341  dvtaylp  24343  dvntaylp  24344  dvntaylp0  24345  dvradcnv  24394  pserdvlem2  24401  advlogexp  24621  cxpeq  24718  atantayl3  24886  birthdaylem2  24899  harmonicbnd4  24957  dmgmaddnn0  24973  lgamucov  24984  wilthlem2  25015  basellem2  25028  basellem3  25029  basellem5  25031  0sgm  25090  sgmppw  25142  chtublem  25156  chpval2  25163  sumdchr2  25215  bcp1ctr  25224  lgslem1  25242  gausslemma2dlem6  25317  gausslemma2d  25319  lgseisenlem2  25321  lgseisenlem3  25322  lgsquadlem1  25325  lgsquadlem2  25326  lgsquad2lem2  25330  m1lgs  25333  2lgslem1c  25338  2lgslem3a  25341  2lgslem3b  25342  2lgslem3c  25343  2lgslem3d  25344  2sqlem8  25371  dchrisumlem1  25398  dchrisum0flblem2  25418  rpvmasum2  25421  mulogsumlem  25440  selberg2lem  25459  pntrsumo1  25474  pntrlog2bndlem4  25489  finsumvtxdg2ssteplem4  26675  vtxdgoddnumeven  26680  wlklenvm1  26748  crctcshlem4  26944  crctcsh  26948  wlklnwwlkln2lem  27012  wwlksnred  27031  wwlksnext  27032  wwlksnextbi  27033  wwlksnredwwlkn  27034  wwlksnextproplem2  27049  rusgrnumwwlks  27117  rusgrnumwwlk  27118  clwwlkccatlem  27133  clwlkclwwlk  27146  clwwlkwwlksb  27205  eupth2lem3lem3  27403  eupth2lem3lem6  27406  fusgreghash2wsp  27513  frrusgrord0lem  27514  numclwwlk1  27541  numclwwlk3  27574  ex-lcm  27647  ex-ind-dvds  27650  nnmulge  29845  divnumden2  29894  2sqmod  29978  omndmul2  30042  omndmul3  30043  archiabllem1a  30075  oddpwdc  30746  eulerpartlemsv2  30750  eulerpartlems  30752  eulerpartlemsv3  30753  eulerpartlemv  30756  eulerpartlemb  30760  iwrdsplit  30779  ballotlemgun  30916  ccatmulgnn0dir  30949  ofcccat  30950  signsplypnf  30957  signslema  30969  signstfvn  30976  signstfveq0  30984  signsvtp  30990  signsvtn  30991  signlem0  30994  signshf  30995  fsum2dsub  31015  hashreprin  31028  breprexp  31041  circlemeth  31048  subfacp1lem6  31495  subfacval2  31497  subfaclim  31498  cvmliftlem7  31601  elmrsubrn  31745  bcprod  31952  bccolsum  31953  faclimlem1  31957  faclim2  31962  fwddifnp1  32599  knoppndvlem6  32835  knoppndvlem14  32843  poimirlem4  33744  poimirlem5  33745  poimirlem6  33746  poimirlem7  33747  poimirlem10  33750  poimirlem11  33751  poimirlem12  33752  poimirlem16  33756  poimirlem17  33757  poimirlem19  33759  poimirlem20  33760  poimirlem22  33762  poimirlem24  33764  poimirlem25  33765  poimirlem29  33769  poimirlem31  33771  rmxyneg  38005  rmxyadd  38006  rmyp1  38018  rmxm1  38019  rmym1  38020  rmxluc  38021  rmyluc  38022  rmxdbl  38024  rmydbl  38025  jm2.18  38075  jm2.19lem1  38076  jm2.19lem2  38077  jm2.22  38082  jm2.23  38083  jm2.25  38086  jm2.27c  38094  rmxdiophlem  38102  expdioph  38110  hbtlem4  38216  itgpowd  38320  relexpmulg  38522  radcnvrat  39033  nzprmdif  39038  bcc0  39059  bccp1k  39060  bccbc  39064  binomcxplemnn0  39068  binomcxplemrat  39069  binomcxplemfrat  39070  binomcxplemnotnn0  39075  fzisoeu  40031  mccllem  40350  dvxpaek  40676  dvnxpaek  40678  dvnmul  40679  dvnprodlem1  40682  dvnprodlem2  40683  stoweidlem24  40762  stirlinglem3  40814  stirlinglem7  40818  fourierdlem36  40881  fourierdlem47  40891  etransclem23  40995  etransclem32  41004  etransclem48  41020  fz0addcom  41855  addlenpfx  41926  pfxfv  41927  pfxtrcfvl  41933  pfxpfx  41943  ccats1pfxeq  41949  fmtnom1nn  41972  fmtnof1  41975  fmtnorec1  41977  sqrtpwpw2p  41978  fmtnorec2lem  41982  fmtnorec3  41988  fmtnofac2lem  42008  fmtnofac2  42009  fmtnofac1  42010  pwdif  42029  lighneallem3  42052  lighneallem4b  42054  altgsumbc  42658  altgsumbcALT  42659  nnpw2pmod  42905  dignn0ehalf  42939  nn0sumshdiglemA  42941  nn0sumshdiglemB  42942  nn0sumshdiglem2  42944  nn0mullong  42947  aacllem  43078
  Copyright terms: Public domain W3C validator