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

Theorem nncnd 10326
Description: A positive integer is a complex number. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
nnred.1  |-  ( ph  ->  A  e.  NN )
Assertion
Ref Expression
nncnd  |-  ( ph  ->  A  e.  CC )

Proof of Theorem nncnd
StepHypRef Expression
1 nnsscn 10315 . 2  |-  NN  C_  CC
2 nnred.1 . 2  |-  ( ph  ->  A  e.  NN )
31, 2sseldi 3342 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1755   CCcc 9268   NNcn 10310
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361  ax-resscn 9327  ax-1cn 9328  ax-icn 9329  ax-addcl 9330  ax-addrcl 9331  ax-mulcl 9332  ax-mulrcl 9333  ax-i2m1 9338  ax-1ne0 9339  ax-rrecex 9342  ax-cnre 9343
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-reu 2712  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-pss 3332  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-tp 3870  df-op 3872  df-uni 4080  df-iun 4161  df-br 4281  df-opab 4339  df-mpt 4340  df-tr 4374  df-eprel 4619  df-id 4623  df-po 4628  df-so 4629  df-fr 4666  df-we 4668  df-ord 4709  df-on 4710  df-lim 4711  df-suc 4712  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-ov 6083  df-om 6466  df-recs 6818  df-rdg 6852  df-nn 10311
This theorem is referenced by:  facdiv  12047  facndiv  12048  faclbnd  12050  faclbnd5  12058  faclbnd6  12059  facubnd  12060  facavg  12061  bccmpl  12069  bcn0  12070  bcn1  12073  bcm1k  12075  bcp1n  12076  bcp1nk  12077  bcval5  12078  bcpasc  12081  permnn  12086  hashf1  12194  hashfac  12195  wrdeqcats1  12352  binom11  13278  binom1dif  13279  climcndslem2  13296  arisum2  13306  trireciplem  13307  trirecip  13308  geo2sum  13316  geo2lim  13318  eftcl  13342  eftabs  13344  efcllem  13346  ege2le3  13358  efcj  13360  efaddlem  13361  eftlub  13376  eirrlem  13469  sqr2irrlem  13513  oexpneg  13578  bitsp1  13610  bitsfzolem  13613  bitsfzo  13614  bitsmod  13615  bitscmp  13617  bitsinv1lem  13620  bitsinv1  13621  2ebits  13626  bitsinvp1  13628  sadcaddlem  13636  sadadd3  13640  bitsres  13652  bitsuz  13653  bitsshft  13654  mulgcd  13713  rplpwr  13723  sqgcd  13725  prmind2  13757  isprm5  13781  prmdvdsexpr  13785  divgcdodd  13788  qmuldeneqnum  13808  divnumden  13809  qnumgt0  13811  numdensq  13815  hashdvds  13833  phiprmpw  13834  prmdiv  13843  prmdivdiv  13845  modprm0  13856  pythagtriplem4  13869  pythagtriplem6  13871  pythagtriplem7  13872  pythagtriplem14  13878  pythagtriplem15  13879  pythagtriplem19  13883  pythagtrip  13884  pcprendvds2  13891  pcpre1  13892  pcpremul  13893  pceulem  13895  pcdiv  13902  pcqmul  13903  pcelnn  13919  pcid  13922  pc2dvds  13928  pcaddlem  13933  pcadd  13934  pcfaclem  13943  qexpz  13946  expnprm  13947  prmpwdvds  13948  pockthlem  13949  pockthg  13950  infpnlem1  13954  prmreclem1  13960  prmreclem2  13961  prmreclem3  13962  prmreclem4  13963  prmreclem6  13965  4sqlem6  13987  4sqlem7  13988  4sqlem10  13991  mul4sqlem  13997  4sqlem11  13999  4sqlem12  14000  4sqlem14  14002  4sqlem17  14005  4sqlem18  14006  vdwlem1  14025  vdwlem2  14026  vdwlem3  14027  vdwlem5  14029  vdwlem6  14030  vdwlem8  14032  vdwlem9  14033  vdwlem10  14034  vdwlem12  14036  ramub1lem2  14071  ramcl  14073  gsumccat  15499  mulgnndir  15629  mulgnnass  15635  psgnunilem5  15980  odf1o2  16052  pgp0  16075  sylow1lem1  16077  odcau  16083  sylow2blem3  16101  sylow3lem3  16108  sylow3lem4  16109  gexexlem  16314  ablfacrp2  16542  ablfac1lem  16543  ablfac1eu  16548  pgpfac1lem3a  16551  pgpfac1lem3  16552  zringlpirlem3  17747  zlpirlem3  17752  znrrg  17840  lebnumlem3  20377  ovollb2lem  20813  ovolunlem1a  20821  ovolunlem1  20822  uniioombllem3  20907  uniioombllem4  20908  dyaddisjlem  20917  mbfi1fseqlem3  21037  mbfi1fseqlem4  21038  dgrcolem1  21625  vieta1lem1  21661  vieta1lem2  21662  elqaalem2  21671  elqaalem3  21672  aalioulem1  21683  aaliou3lem2  21694  aaliou3lem8  21696  aaliou3lem6  21699  aaliou3lem9  21701  taylfvallem1  21707  tayl0  21712  taylply2  21718  taylply  21719  dvtaylp  21720  taylthlem1  21723  taylthlem2  21724  pserdvlem2  21778  advlogexp  21985  cxpmul2  22019  cxpeq  22080  atantayl3  22219  leibpi  22222  log2cnv  22224  log2tlbnd  22225  birthdaylem2  22231  birthdaylem3  22232  amgmlem  22268  amgm  22269  emcllem5  22278  fsumharmonic  22290  wilthlem1  22291  wilthlem2  22292  wilthlem3  22293  basellem1  22303  basellem2  22304  basellem3  22305  basellem4  22306  basellem5  22307  basellem8  22310  vmaprm  22340  sgmval2  22366  0sgm  22367  sgmf  22368  vma1  22389  dvdsdivcl  22406  fsumdvdsdiaglem  22408  dvdsflf1o  22412  muinv  22418  dvdsmulf1o  22419  sgmppw  22421  1sgmprm  22423  1sgm2ppw  22424  sgmmul  22425  chtublem  22435  fsumvma2  22438  chpchtsum  22443  logfaclbnd  22446  logexprlim  22449  mersenne  22451  perfect1  22452  perfectlem1  22453  perfectlem2  22454  perfect  22455  dchrsum2  22492  dchrhash  22495  bcmono  22501  bcp1ctr  22503  bclbnd  22504  bposlem1  22508  bposlem2  22509  bposlem3  22510  bposlem5  22512  bposlem6  22513  lgsval2lem  22530  lgsqrlem2  22566  lgseisenlem1  22573  lgseisenlem4  22576  lgsquadlem1  22578  lgsquadlem2  22579  lgsquadlem3  22580  lgsquad2  22584  m1lgs  22586  2sqlem3  22590  2sqlem4  22591  chebbnd1lem1  22603  chebbnd1  22606  rplogsumlem1  22618  rplogsumlem2  22619  rpvmasumlem  22621  dchrisumlem1  22623  dchrmusum2  22628  dchrvmasumlem1  22629  dchrvmasum2lem  22630  dchrvmasum2if  22631  dchrvmasumlem2  22632  dchrvmasumlem3  22633  dchrvmasumiflem1  22635  dchrisum0flblem1  22642  dchrisum0flblem2  22643  dchrisum0fno1  22645  rpvmasum2  22646  rplogsum  22661  mulogsumlem  22665  mulogsum  22666  mulog2sumlem2  22669  vmalogdivsum2  22672  vmalogdivsum  22673  2vmadivsumlem  22674  logsqvma  22676  selberglem2  22680  selberglem3  22681  selberg  22682  selberg2lem  22684  logdivbnd  22690  selberg3lem1  22691  selberg4lem1  22694  pntrsumo1  22699  pntrsumbnd2  22701  selberg3r  22703  selberg4r  22704  selberg34r  22705  pntsval2  22710  pntrlog2bndlem2  22712  pntrlog2bndlem4  22714  pntrlog2bndlem6  22717  pntpbnd1  22720  pntpbnd2  22721  pntlemg  22732  pntlemn  22734  pntlemf  22739  pnt  22748  padicabvf  22765  ostth2lem2  22768  ostth3  22772  eupares  23419  numdenneg  25909  ltesubnnd  25914  qqhnm  26273  oddpwdc  26585  eulerpartlemsv2  26589  eulerpartlems  26591  eulerpartlemsv3  26592  eulerpartlemgc  26593  eulerpartlemv  26595  eulerpartlemgs2  26611  fibp1  26632  ballotlemfc0  26723  ballotlemfcc  26724  signsvtn0  26819  zetacvg  26849  dmgmdivn0  26862  lgamgulmlem3  26865  lgamgulmlem4  26866  lgamgulmlem5  26867  lgamgulmlem6  26868  lgamgulm2  26870  lgamcvg2  26889  gamcvg  26890  gamcvg2lem  26893  facgam  26900  subfacp1lem1  26915  subfacp1lem5  26920  subfacval2  26923  subfaclim  26924  cvmliftlem2  27023  cvmliftlem7  27028  cvmliftlem10  27031  cvmliftlem11  27032  cvmliftlem13  27033  fprodfac  27330  iprodgam  27353  risefacfac  27385  fallfacfwd  27386  fallfacval4  27393  bcfallfac  27394  fallfacfac  27395  faclimlem1  27396  faclimlem2  27397  faclim2  27401  bpolycl  28042  bpolysum  28043  bpolydiflem  28044  fsumkthpow  28046  nn0prpwlem  28361  nn0prpw  28362  irrapxlem4  29011  irrapxlem5  29012  pellexlem2  29016  pellexlem6  29020  pell1234qrne0  29039  pell1234qrreccl  29040  pell1234qrmulcl  29041  pell1234qrdich  29047  pell14qrdich  29055  pell1qrge1  29056  pell1qr1  29057  pell14qrgapw  29062  rmxyneg  29106  rmxm1  29120  rmxluc  29122  rmxdbl  29125  jm2.19lem1  29183  jm2.27c  29201  phisum  29412  itgpowd  29435  clim1fr1  29620  dvsinexp  29633  itgsinexplem1  29640  itgsinexp  29641  stoweidlem1  29642  stoweidlem11  29652  stoweidlem25  29666  stoweidlem26  29667  stoweidlem34  29675  stoweidlem37  29678  stoweidlem38  29679  stoweidlem42  29683  wallispi2lem1  29712  wallispi2  29714  stirlinglem4  29718  stirlinglem5  29719  stirlinglem10  29724  stirlinglem15  29729  hashclwwlkn  30356
  Copyright terms: Public domain W3C validator