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

Theorem nncnd 10883
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 10872 . 2 ℕ ⊆ ℂ
2 nnred.1 . 2 (𝜑𝐴 ∈ ℕ)
31, 2sseldi 3565 1 (𝜑𝐴 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  cc 9790  cn 10867
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-i2m1 9860  ax-1ne0 9861  ax-rrecex 9864  ax-cnre 9865
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-ov 6530  df-om 6935  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-nn 10868
This theorem is referenced by:  facdiv  12891  facndiv  12892  faclbnd  12894  faclbnd5  12902  faclbnd6  12903  facubnd  12904  facavg  12905  bccmpl  12913  bcn0  12914  bcn1  12917  bcm1k  12919  bcp1n  12920  bcp1nk  12921  bcval5  12922  bcpasc  12925  permnn  12930  hashf1  13050  hashfac  13051  relexpaddnn  13585  binom11  14349  binom1dif  14350  climcndslem2  14367  arisum2  14378  trireciplem  14379  trirecip  14380  geo2sum  14389  geo2lim  14391  fprodfac  14488  risefacfac  14551  fallfacfwd  14552  fallfacval4  14559  bcfallfac  14560  fallfacfac  14561  bpolycl  14568  bpolysum  14569  bpolydiflem  14570  fsumkthpow  14572  eftcl  14589  eftabs  14591  efcllem  14593  ege2le3  14605  efcj  14607  efaddlem  14608  eftlub  14624  eirrlem  14717  sqr2irrlem  14762  oexpneg  14853  pwp1fsum  14898  bitsp1  14937  bitsfzolem  14940  bitsfzo  14941  bitsmod  14942  bitscmp  14944  bitsinv1lem  14947  bitsinv1  14948  2ebits  14953  bitsinvp1  14955  sadcaddlem  14963  sadadd3  14967  bitsres  14979  bitsuz  14980  bitsshft  14981  mulgcd  15049  rplpwr  15060  sqgcd  15062  lcmgcdlem  15103  3lcm2e6woprm  15112  coprmprod  15159  coprmproddvdslem  15160  cncongr1  15165  cncongr2  15166  prmind2  15182  isprm5  15203  divgcdodd  15206  prmdvdsexpr  15213  qmuldeneqnum  15239  divnumden  15240  qnumgt0  15242  numdensq  15246  hashdvds  15264  phiprmpw  15265  prmdiv  15274  prmdivdiv  15276  phisum  15279  modprm0  15294  pythagtriplem4  15308  pythagtriplem6  15310  pythagtriplem7  15311  pythagtriplem14  15317  pythagtriplem15  15318  pythagtriplem19  15322  pythagtrip  15323  pcprendvds2  15330  pcpre1  15331  pcpremul  15332  pceulem  15334  pcdiv  15341  pcqmul  15342  pcelnn  15358  pcid  15361  pc2dvds  15367  dvdsprmpweqnn  15373  dvdsprmpweqle  15374  pcaddlem  15376  pcadd  15377  pcfaclem  15386  qexpz  15389  expnprm  15390  oddprmdvds  15391  prmpwdvds  15392  pockthlem  15393  pockthg  15394  infpnlem1  15398  prmreclem1  15404  prmreclem2  15405  prmreclem3  15406  prmreclem4  15407  prmreclem6  15409  4sqlem6  15431  4sqlem7  15432  4sqlem10  15435  mul4sqlem  15441  4sqlem11  15443  4sqlem12  15444  4sqlem14  15446  4sqlem17  15449  4sqlem18  15450  vdwlem1  15469  vdwlem2  15470  vdwlem3  15471  vdwlem5  15473  vdwlem6  15474  vdwlem8  15476  vdwlem9  15477  vdwlem10  15478  vdwlem12  15480  ramub1lem2  15515  ramcl  15517  prmop1  15526  prmdvdsprmo  15530  prmgaplem7  15545  prmgaplem8  15546  gsumccat  17147  mulgnndir  17338  mulgnndirOLD  17339  mulgnnass  17345  mulgnnassOLD  17346  psgnunilem5  17683  odf1o2  17757  pgp0  17780  sylow1lem1  17782  odcau  17788  sylow2blem3  17806  sylow3lem3  17813  sylow3lem4  17814  gexexlem  18024  ablfacrp2  18235  ablfac1lem  18236  ablfac1eu  18241  pgpfac1lem3a  18244  pgpfac1lem3  18245  zringlpirlem3  19599  znrrg  19678  cpmadugsumlemF  20442  lebnumlem3  22501  ovollb2lem  22980  ovolunlem1a  22988  ovolunlem1  22989  uniioombllem3  23076  uniioombllem4  23077  dyaddisjlem  23086  mbfi1fseqlem3  23207  mbfi1fseqlem4  23208  dgrcolem1  23750  vieta1lem1  23786  vieta1lem2  23787  elqaalem2  23796  elqaalem3  23797  aalioulem1  23808  aaliou3lem2  23819  aaliou3lem8  23821  aaliou3lem6  23824  aaliou3lem9  23826  taylfvallem1  23832  tayl0  23837  taylply2  23843  taylply  23844  dvtaylp  23845  taylthlem1  23848  taylthlem2  23849  pserdvlem2  23903  advlogexp  24118  cxpmul2  24152  cxpeq  24215  atantayl3  24383  leibpi  24386  log2cnv  24388  log2tlbnd  24389  birthdaylem2  24396  birthdaylem3  24397  amgmlem  24433  amgm  24434  emcllem5  24443  fsumharmonic  24455  zetacvg  24458  dmgmdivn0  24471  lgamgulmlem3  24474  lgamgulmlem4  24475  lgamgulmlem5  24476  lgamgulmlem6  24477  lgamgulm2  24479  lgamcvg2  24498  gamcvg  24499  gamcvg2lem  24502  facgam  24509  wilthlem1  24511  wilthlem2  24512  wilthlem3  24513  wilthimp  24515  basellem1  24524  basellem2  24525  basellem3  24526  basellem4  24527  basellem5  24528  basellem8  24531  vmaprm  24560  sgmval2  24586  0sgm  24587  sgmf  24588  vma1  24609  fsumdvdsdiaglem  24626  dvdsflf1o  24630  muinv  24636  dvdsmulf1o  24637  sgmppw  24639  1sgmprm  24641  1sgm2ppw  24642  sgmmul  24643  chtublem  24653  fsumvma2  24656  chpchtsum  24661  logfaclbnd  24664  logexprlim  24667  mersenne  24669  perfect1  24670  perfectlem1  24671  perfectlem2  24672  perfect  24673  dchrsum2  24710  dchrhash  24713  bcmono  24719  bcp1ctr  24721  bclbnd  24722  bposlem1  24726  bposlem2  24727  bposlem3  24728  bposlem5  24730  bposlem6  24731  lgsval2lem  24749  lgsqrlem2  24789  gausslemma2dlem6  24814  gausslemma2dlem7  24815  gausslemma2d  24816  lgseisenlem1  24817  lgseisenlem4  24820  lgsquadlem1  24822  lgsquadlem2  24823  lgsquadlem3  24824  lgsquad2  24828  m1lgs  24830  2sqlem3  24862  2sqlem4  24863  chebbnd1lem1  24875  chebbnd1  24878  rplogsumlem1  24890  rplogsumlem2  24891  rpvmasumlem  24893  dchrisumlem1  24895  dchrmusum2  24900  dchrvmasumlem1  24901  dchrvmasum2lem  24902  dchrvmasum2if  24903  dchrvmasumlem2  24904  dchrvmasumlem3  24905  dchrvmasumiflem1  24907  dchrisum0flblem1  24914  dchrisum0flblem2  24915  dchrisum0fno1  24917  rpvmasum2  24918  rplogsum  24933  mulogsumlem  24937  mulogsum  24938  mulog2sumlem2  24941  vmalogdivsum2  24944  vmalogdivsum  24945  2vmadivsumlem  24946  logsqvma  24948  selberglem2  24952  selberglem3  24953  selberg  24954  selberg2lem  24956  logdivbnd  24962  selberg3lem1  24963  selberg4lem1  24966  pntrsumo1  24971  pntrsumbnd2  24973  selberg3r  24975  selberg4r  24976  selberg34r  24977  pntsval2  24982  pntrlog2bndlem2  24984  pntrlog2bndlem4  24986  pntrlog2bndlem6  24989  pntpbnd1  24992  pntpbnd2  24993  pntlemg  25004  pntlemn  25006  pntlemf  25011  pnt  25020  padicabvf  25037  ostth2lem2  25040  ostth3  25044  hashclwwlkn  26129  eupares  26268  numdenneg  28756  ltesubnnd  28761  1smat1  29004  madjusmdetlem2  29028  madjusmdetlem4  29030  qqhnm  29168  oddpwdc  29549  eulerpartlemsv2  29553  eulerpartlems  29555  eulerpartlemsv3  29556  eulerpartlemgc  29557  eulerpartlemv  29559  eulerpartlemgs2  29575  fibp1  29596  ballotlemfc0  29687  ballotlemfcc  29688  signsvtn0  29779  subfacp1lem1  30221  subfacp1lem5  30226  subfacval2  30229  subfaclim  30230  cvmliftlem2  30328  cvmliftlem7  30333  cvmliftlem10  30336  cvmliftlem11  30337  cvmliftlem13  30338  bcm1nt  30682  bcprod  30683  iprodgam  30687  faclimlem1  30688  faclimlem2  30689  faclim2  30693  nn0prpwlem  31293  nn0prpw  31294  knoppndvlem16  31494  poimirlem1  32376  poimirlem2  32377  poimirlem6  32381  poimirlem7  32382  poimirlem8  32383  poimirlem9  32384  poimirlem10  32385  poimirlem11  32386  poimirlem12  32387  poimirlem13  32388  poimirlem15  32390  poimirlem16  32391  poimirlem17  32392  poimirlem18  32393  poimirlem19  32394  poimirlem20  32395  poimirlem21  32396  poimirlem22  32397  poimirlem23  32398  poimirlem24  32399  poimirlem25  32400  poimirlem26  32401  poimirlem27  32402  poimirlem31  32406  irrapxlem4  36203  irrapxlem5  36204  pellexlem2  36208  pellexlem6  36212  pell1234qrne0  36231  pell1234qrreccl  36232  pell1234qrmulcl  36233  pell1234qrdich  36239  pell14qrdich  36247  pell1qrge1  36248  pell1qr1  36249  pell14qrgapw  36254  rmxyneg  36299  rmxm1  36313  rmxluc  36315  rmxdbl  36318  jm2.19lem1  36370  jm2.27c  36388  itgpowd  36615  relexpmulnn  36816  relexpmulg  36817  inductionexd  37269  hashnzfzclim  37339  bcccl  37356  bcc0  37357  bccp1k  37358  bccm1k  37359  binomcxplemwb  37365  fsumnncl  38435  mccllem  38461  clim1fr1  38465  sumnnodd  38494  dvsinexp  38595  dvxpaek  38627  dvnxpaek  38629  dvnprodlem2  38634  itgsinexplem1  38642  itgsinexp  38643  stoweidlem1  38691  stoweidlem11  38701  stoweidlem25  38715  stoweidlem26  38716  stoweidlem34  38724  stoweidlem37  38727  stoweidlem38  38728  stoweidlem42  38732  wallispi2lem1  38761  wallispi2  38763  stirlinglem4  38767  stirlinglem5  38768  stirlinglem10  38773  stirlinglem15  38778  dirkertrigeqlem3  38790  dirkertrigeq  38791  dirkercncflem2  38794  dirkercncflem4  38796  fourierdlem11  38808  fourierdlem15  38812  fourierdlem79  38875  fourierdlem83  38879  sqwvfourb  38919  etransclem14  38938  etransclem15  38939  etransclem20  38944  etransclem21  38945  etransclem22  38946  etransclem23  38947  etransclem24  38948  etransclem25  38949  etransclem28  38952  etransclem31  38955  etransclem32  38956  etransclem33  38957  etransclem34  38958  etransclem35  38959  etransclem38  38962  etransclem41  38965  etransclem44  38968  etransclem45  38969  etransclem47  38971  etransclem48  38972  nnfoctbdjlem  39145  deccarry  39739  iccpartgtprec  39756  fmtnoodd  39781  fmtnorec2lem  39790  fmtnorec2  39791  fmtnodvds  39792  goldbachthlem2  39794  fmtnorec3  39796  fmtnorec4  39797  fmtnoprmfac1lem  39812  fmtnoprmfac1  39813  fmtnoprmfac2lem1  39814  fmtnoprmfac2  39815  2pwp1prm  39839  sfprmdvdsmersenne  39856  lighneallem4b  39862  lighneal  39864  proththdlem  39866  proththd  39867  oexpnegALTV  39924  perfectALTVlem1  39962  perfectALTVlem2  39963  perfectALTV  39964  fusgrhashclwwlkn  41258  eucrct2eupth  41408  nnpw2pmod  42170  nnolog2flm1  42177  blennn0em1  42178  blengt1fldiv2p1  42180  nn0sumshdiglemB  42207  amgmlemALT  42314
  Copyright terms: Public domain W3C validator