MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nncnd Unicode version

Theorem nncnd 10577
Description: A positive integer is a complex number. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
nnred.1
Assertion
Ref Expression
nncnd

Proof of Theorem nncnd
StepHypRef Expression
1 nnsscn 10566 . 2
2 nnred.1 . 2
31, 2sseldi 3501 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818   cc 9511   cn 10561
This theorem is referenced by:  facdiv  12365  facndiv  12366  faclbnd  12368  faclbnd5  12376  faclbnd6  12377  facubnd  12378  facavg  12379  bccmpl  12387  bcn0  12388  bcn1  12391  bcm1k  12393  bcp1n  12394  bcp1nk  12395  bcval5  12396  bcpasc  12399  permnn  12404  hashf1  12506  hashfac  12507  wrdeqcats1  12699  binom11  13644  binom1dif  13645  climcndslem2  13662  arisum2  13672  trireciplem  13673  trirecip  13674  geo2sum  13682  geo2lim  13684  fprodfac  13777  eftcl  13809  eftabs  13811  efcllem  13813  ege2le3  13825  efcj  13827  efaddlem  13828  eftlub  13844  eirrlem  13937  sqr2irrlem  13981  oexpneg  14049  bitsp1  14081  bitsfzolem  14084  bitsfzo  14085  bitsmod  14086  bitscmp  14088  bitsinv1lem  14091  bitsinv1  14092  2ebits  14097  bitsinvp1  14099  sadcaddlem  14107  sadadd3  14111  bitsres  14123  bitsuz  14124  bitsshft  14125  mulgcd  14184  rplpwr  14194  sqgcd  14196  prmind2  14228  isprm5  14253  prmdvdsexpr  14257  divgcdodd  14260  qmuldeneqnum  14280  divnumden  14281  qnumgt0  14283  numdensq  14287  hashdvds  14305  phiprmpw  14306  prmdiv  14315  prmdivdiv  14317  modprm0  14330  pythagtriplem4  14343  pythagtriplem6  14345  pythagtriplem7  14346  pythagtriplem14  14352  pythagtriplem15  14353  pythagtriplem19  14357  pythagtrip  14358  pcprendvds2  14365  pcpre1  14366  pcpremul  14367  pceulem  14369  pcdiv  14376  pcqmul  14377  pcelnn  14393  pcid  14396  pc2dvds  14402  pcaddlem  14407  pcadd  14408  pcfaclem  14417  qexpz  14420  expnprm  14421  prmpwdvds  14422  pockthlem  14423  pockthg  14424  infpnlem1  14428  prmreclem1  14434  prmreclem2  14435  prmreclem3  14436  prmreclem4  14437  prmreclem6  14439  4sqlem6  14461  4sqlem7  14462  4sqlem10  14465  mul4sqlem  14471  4sqlem11  14473  4sqlem12  14474  4sqlem14  14476  4sqlem17  14479  4sqlem18  14480  vdwlem1  14499  vdwlem2  14500  vdwlem3  14501  vdwlem5  14503  vdwlem6  14504  vdwlem8  14506  vdwlem9  14507  vdwlem10  14508  vdwlem12  14510  ramub1lem2  14545  ramcl  14547  gsumccat  16009  mulgnndir  16164  mulgnnass  16170  psgnunilem5  16519  odf1o2  16593  pgp0  16616  sylow1lem1  16618  odcau  16624  sylow2blem3  16642  sylow3lem3  16649  sylow3lem4  16650  gexexlem  16858  ablfacrp2  17118  ablfac1lem  17119  ablfac1eu  17124  pgpfac1lem3a  17127  pgpfac1lem3  17128  zringlpirlem3  18511  zlpirlem3  18516  znrrg  18604  cpmadugsumlemF  19377  lebnumlem3  21463  ovollb2lem  21899  ovolunlem1a  21907  ovolunlem1  21908  uniioombllem3  21994  uniioombllem4  21995  dyaddisjlem  22004  mbfi1fseqlem3  22124  mbfi1fseqlem4  22125  dgrcolem1  22670  vieta1lem1  22706  vieta1lem2  22707  elqaalem2  22716  elqaalem3  22717  aalioulem1  22728  aaliou3lem2  22739  aaliou3lem8  22741  aaliou3lem6  22744  aaliou3lem9  22746  taylfvallem1  22752  tayl0  22757  taylply2  22763  taylply  22764  dvtaylp  22765  taylthlem1  22768  taylthlem2  22769  pserdvlem2  22823  advlogexp  23036  cxpmul2  23070  cxpeq  23131  atantayl3  23270  leibpi  23273  log2cnv  23275  log2tlbnd  23276  birthdaylem2  23282  birthdaylem3  23283  amgmlem  23319  amgm  23320  emcllem5  23329  fsumharmonic  23341  wilthlem1  23342  wilthlem2  23343  wilthlem3  23344  basellem1  23354  basellem2  23355  basellem3  23356  basellem4  23357  basellem5  23358  basellem8  23361  vmaprm  23391  sgmval2  23417  0sgm  23418  sgmf  23419  vma1  23440  dvdsdivcl  23457  fsumdvdsdiaglem  23459  dvdsflf1o  23463  muinv  23469  dvdsmulf1o  23470  sgmppw  23472  1sgmprm  23474  1sgm2ppw  23475  sgmmul  23476  chtublem  23486  fsumvma2  23489  chpchtsum  23494  logfaclbnd  23497  logexprlim  23500  mersenne  23502  perfect1  23503  perfectlem1  23504  perfectlem2  23505  perfect  23506  dchrsum2  23543  dchrhash  23546  bcmono  23552  bcp1ctr  23554  bclbnd  23555  bposlem1  23559  bposlem2  23560  bposlem3  23561  bposlem5  23563  bposlem6  23564  lgsval2lem  23581  lgsqrlem2  23617  lgseisenlem1  23624  lgseisenlem4  23627  lgsquadlem1  23629  lgsquadlem2  23630  lgsquadlem3  23631  lgsquad2  23635  m1lgs  23637  2sqlem3  23641  2sqlem4  23642  chebbnd1lem1  23654  chebbnd1  23657  rplogsumlem1  23669  rplogsumlem2  23670  rpvmasumlem  23672  dchrisumlem1  23674  dchrmusum2  23679  dchrvmasumlem1  23680  dchrvmasum2lem  23681  dchrvmasum2if  23682  dchrvmasumlem2  23683  dchrvmasumlem3  23684  dchrvmasumiflem1  23686  dchrisum0flblem1  23693  dchrisum0flblem2  23694  dchrisum0fno1  23696  rpvmasum2  23697  rplogsum  23712  mulogsumlem  23716  mulogsum  23717  mulog2sumlem2  23720  vmalogdivsum2  23723  vmalogdivsum  23724  2vmadivsumlem  23725  logsqvma  23727  selberglem2  23731  selberglem3  23732  selberg  23733  selberg2lem  23735  logdivbnd  23741  selberg3lem1  23742  selberg4lem1  23745  pntrsumo1  23750  pntrsumbnd2  23752  selberg3r  23754  selberg4r  23755  selberg34r  23756  pntsval2  23761  pntrlog2bndlem2  23763  pntrlog2bndlem4  23765  pntrlog2bndlem6  23768  pntpbnd1  23771  pntpbnd2  23772  pntlemg  23783  pntlemn  23785  pntlemf  23790  pnt  23799  padicabvf  23816  ostth2lem2  23819  ostth3  23823  hashclwwlkn  24836  eupares  24975  numdenneg  27608  ltesubnnd  27612  qqhnm  27971  oddpwdc  28293  eulerpartlemsv2  28297  eulerpartlems  28299  eulerpartlemsv3  28300  eulerpartlemgc  28301  eulerpartlemv  28303  eulerpartlemgs2  28319  fibp1  28340  ballotlemfc0  28431  ballotlemfcc  28432  signsvtn0  28527  zetacvg  28557  dmgmdivn0  28570  lgamgulmlem3  28573  lgamgulmlem4  28574  lgamgulmlem5  28575  lgamgulmlem6  28576  lgamgulm2  28578  lgamcvg2  28597  gamcvg  28598  gamcvg2lem  28601  facgam  28608  subfacp1lem1  28623  subfacp1lem5  28628  subfacval2  28631  subfaclim  28632  cvmliftlem2  28731  cvmliftlem7  28736  cvmliftlem10  28739  cvmliftlem11  28740  cvmliftlem13  28741  iprodgam  29125  risefacfac  29157  fallfacfwd  29158  fallfacval4  29165  bcfallfac  29166  fallfacfac  29167  faclimlem1  29168  faclimlem2  29169  faclim2  29173  bpolycl  29814  bpolysum  29815  bpolydiflem  29816  fsumkthpow  29818  nn0prpwlem  30140  nn0prpw  30141  irrapxlem4  30761  irrapxlem5  30762  pellexlem2  30766  pellexlem6  30770  pell1234qrne0  30789  pell1234qrreccl  30790  pell1234qrmulcl  30791  pell1234qrdich  30797  pell14qrdich  30805  pell1qrge1  30806  pell1qr1  30807  pell14qrgapw  30812  rmxyneg  30856  rmxm1  30870  rmxluc  30872  rmxdbl  30875  jm2.19lem1  30931  jm2.27c  30949  phisum  31159  itgpowd  31182  lcmgcdlem  31212  hashnzfzclim  31227  bcccl  31244  bcc0  31245  bccp1k  31246  bccm1k  31247  binomcxplemwb  31253  fsumnncl  31572  mccllem  31605  clim1fr1  31607  sumnnodd  31636  dvsinexp  31705  dvxpaek  31737  dvnxpaek  31739  dvnprodlem2  31744  itgsinexplem1  31752  itgsinexp  31753  stoweidlem1  31783  stoweidlem11  31793  stoweidlem25  31807  stoweidlem26  31808  stoweidlem34  31816  stoweidlem37  31819  stoweidlem38  31820  stoweidlem42  31824  wallispi2lem1  31853  wallispi2  31855  stirlinglem4  31859  stirlinglem5  31860  stirlinglem10  31865  stirlinglem15  31870  dirkertrigeqlem3  31882  dirkertrigeq  31883  dirkercncflem2  31886  dirkercncflem4  31888  fourierdlem11  31900  fourierdlem15  31904  fourierdlem79  31968  fourierdlem83  31972  sqwvfourb  32012  etransclem14  32031  etransclem15  32032  etransclem20  32037  etransclem21  32038  etransclem22  32039  etransclem23  32040  etransclem24  32041  etransclem25  32042  etransclem28  32045  etransclem31  32048  etransclem32  32049  etransclem33  32050  etransclem34  32051  etransclem35  32052  etransclem38  32055  etransclem41  32058  etransclem44  32061  etransclem45  32062  etransclem47  32064  etransclem48  32065  inductionexd  37967
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592  ax-resscn 9570  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-addrcl 9574  ax-mulcl 9575  ax-mulrcl 9576  ax-i2m1 9581  ax-1ne0 9582  ax-rrecex 9585  ax-cnre 9586
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-pss 3491  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-tp 4034  df-op 4036  df-uni 4250  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-tr 4546  df-eprel 4796  df-id 4800  df-po 4805  df-so 4806  df-fr 4843  df-we 4845  df-ord 4886  df-on 4887  df-lim 4888  df-suc 4889  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-ov 6299  df-om 6701  df-recs 7061  df-rdg 7095  df-nn 10562
  Copyright terms: Public domain W3C validator