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

Theorem nncnd 11457
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 11444 . 2 ℕ ⊆ ℂ
2 nnred.1 . 2 (𝜑𝐴 ∈ ℕ)
31, 2sseldi 3857 1 (𝜑𝐴 ∈ ℂ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2050  cc 10333  cn 11439
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2751  ax-sep 5060  ax-nul 5067  ax-pow 5119  ax-pr 5186  ax-un 7279  ax-1cn 10393  ax-addcl 10395
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2760  df-cleq 2772  df-clel 2847  df-nfc 2919  df-ne 2969  df-ral 3094  df-rex 3095  df-reu 3096  df-rab 3098  df-v 3418  df-sbc 3683  df-csb 3788  df-dif 3833  df-un 3835  df-in 3837  df-ss 3844  df-pss 3846  df-nul 4180  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-tp 4446  df-op 4448  df-uni 4713  df-iun 4794  df-br 4930  df-opab 4992  df-mpt 5009  df-tr 5031  df-id 5312  df-eprel 5317  df-po 5326  df-so 5327  df-fr 5366  df-we 5368  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-rn 5418  df-res 5419  df-ima 5420  df-pred 5986  df-ord 6032  df-on 6033  df-lim 6034  df-suc 6035  df-iota 6152  df-fun 6190  df-fn 6191  df-f 6192  df-f1 6193  df-fo 6194  df-f1o 6195  df-fv 6196  df-ov 6979  df-om 7397  df-wrecs 7750  df-recs 7812  df-rdg 7850  df-nn 11440
This theorem is referenced by:  facdiv  13462  facndiv  13463  faclbnd  13465  faclbnd5  13473  faclbnd6  13474  facubnd  13475  facavg  13476  bccmpl  13484  bcn0  13485  bcn1  13488  bcm1k  13490  bcp1n  13491  bcp1nk  13492  bcval5  13493  bcpasc  13496  permnn  13501  hashf1  13628  hashfac  13629  relexpaddnn  14271  binom11  15047  binom1dif  15048  climcndslem2  15065  arisum2  15076  trireciplem  15077  trirecip  15078  geo2sum  15089  geo2lim  15091  fprodfac  15187  risefacfac  15249  fallfacfwd  15250  fallfacval4  15257  bcfallfac  15258  fallfacfac  15259  bpolycl  15266  bpolysum  15267  bpolydiflem  15268  fsumkthpow  15270  eftcl  15287  eftabs  15289  efcllem  15291  ege2le3  15303  efcj  15305  efaddlem  15306  eftlub  15322  eirrlem  15417  sqrt2irrlem  15461  oexpneg  15554  pwp1fsum  15602  bitsp1  15640  bitsfzolem  15643  bitsfzo  15644  bitsmod  15645  bitscmp  15647  bitsinv1lem  15650  bitsinv1  15651  2ebits  15656  bitsinvp1  15658  sadcaddlem  15666  sadadd3  15670  bitsres  15682  bitsuz  15683  bitsshft  15684  mulgcd  15752  rplpwr  15763  sqgcd  15765  lcmgcdlem  15806  3lcm2e6woprm  15815  coprmprod  15861  coprmproddvdslem  15862  cncongr1  15867  cncongr2  15868  prmind2  15885  isprm5  15907  divgcdodd  15910  prmdvdsexpr  15917  qmuldeneqnum  15943  divnumden  15944  qnumgt0  15946  numdensq  15950  hashdvds  15968  phiprmpw  15969  prmdiv  15978  prmdivdiv  15980  phisum  15983  modprm0  15998  pythagtriplem4  16012  pythagtriplem6  16014  pythagtriplem7  16015  pythagtriplem14  16021  pythagtriplem15  16022  pythagtriplem19  16026  pythagtrip  16027  pcprendvds2  16034  pcpre1  16035  pcpremul  16036  pceulem  16038  pcdiv  16045  pcqmul  16046  pcelnn  16062  pcid  16065  pc2dvds  16071  dvdsprmpweqnn  16077  dvdsprmpweqle  16078  pcaddlem  16080  pcadd  16081  pcfaclem  16090  qexpz  16093  expnprm  16094  oddprmdvds  16095  prmpwdvds  16096  pockthlem  16097  pockthg  16098  infpnlem1  16102  prmreclem1  16108  prmreclem2  16109  prmreclem3  16110  prmreclem4  16111  prmreclem6  16113  4sqlem6  16135  4sqlem7  16136  4sqlem10  16139  mul4sqlem  16145  4sqlem11  16147  4sqlem12  16148  4sqlem14  16150  4sqlem17  16153  4sqlem18  16154  vdwlem1  16173  vdwlem2  16174  vdwlem3  16175  vdwlem5  16177  vdwlem6  16178  vdwlem8  16180  vdwlem9  16181  vdwlem10  16182  vdwlem12  16184  ramub1lem2  16219  ramcl  16221  prmop1  16230  prmdvdsprmo  16234  prmgaplem7  16249  prmgaplem8  16250  gsumccat  17846  mulgnndir  18040  mulgnnass  18046  psgnunilem5  18383  psgnunilem5OLD  18384  odf1o2  18459  pgp0  18482  sylow1lem1  18484  odcau  18490  sylow2blem3  18508  sylow3lem3  18515  sylow3lem4  18516  gexexlem  18728  ablfacrp2  18939  ablfac1lem  18940  ablfac1eu  18945  pgpfac1lem3a  18948  pgpfac1lem3  18949  zringlpirlem3  20335  znrrg  20414  cpmadugsumlemF  21188  lebnumlem3  23270  ovollb2lem  23792  ovolunlem1a  23800  ovolunlem1  23801  uniioombllem3  23889  uniioombllem4  23890  dyaddisjlem  23899  mbfi1fseqlem3  24021  mbfi1fseqlem4  24022  dgrcolem1  24566  vieta1lem1  24602  vieta1lem2  24603  elqaalem2  24612  elqaalem3  24613  aalioulem1  24624  aaliou3lem2  24635  aaliou3lem8  24637  aaliou3lem6  24640  aaliou3lem9  24642  taylfvallem1  24648  tayl0  24653  taylply2  24659  taylply  24660  dvtaylp  24661  taylthlem1  24664  taylthlem2  24665  pserdvlem2  24719  advlogexp  24939  cxpmul2  24973  cxpeq  25039  atantayl3  25218  leibpi  25222  log2cnv  25224  log2tlbnd  25225  birthdaylem2  25232  birthdaylem3  25233  amgmlem  25269  amgm  25270  emcllem5  25279  fsumharmonic  25291  zetacvg  25294  dmgmdivn0  25307  lgamgulmlem3  25310  lgamgulmlem4  25311  lgamgulmlem5  25312  lgamgulmlem6  25313  lgamgulm2  25315  lgamcvg2  25334  gamcvg  25335  gamcvg2lem  25338  facgam  25345  wilthlem1  25347  wilthlem2  25348  wilthlem3  25349  wilthimp  25351  basellem1  25360  basellem2  25361  basellem3  25362  basellem4  25363  basellem5  25364  basellem8  25367  vmaprm  25396  sgmval2  25422  0sgm  25423  sgmf  25424  vma1  25445  fsumdvdsdiaglem  25462  dvdsflf1o  25466  muinv  25472  dvdsmulf1o  25473  sgmppw  25475  1sgmprm  25477  1sgm2ppw  25478  sgmmul  25479  chtublem  25489  fsumvma2  25492  chpchtsum  25497  logfaclbnd  25500  logexprlim  25503  mersenne  25505  perfect1  25506  perfectlem1  25507  perfectlem2  25508  perfect  25509  dchrsum2  25546  dchrhash  25549  bcmono  25555  bcp1ctr  25557  bclbnd  25558  bposlem1  25562  bposlem2  25563  bposlem3  25564  bposlem5  25566  bposlem6  25567  lgsval2lem  25585  lgsqrlem2  25625  gausslemma2dlem6  25650  gausslemma2dlem7  25651  gausslemma2d  25652  lgseisenlem1  25653  lgseisenlem4  25656  lgsquadlem1  25658  lgsquadlem2  25659  lgsquadlem3  25660  lgsquad2  25664  m1lgs  25666  2sqlem3  25698  2sqlem4  25699  chebbnd1lem1  25747  chebbnd1  25750  rplogsumlem1  25762  rplogsumlem2  25763  rpvmasumlem  25765  dchrisumlem1  25767  dchrmusum2  25772  dchrvmasumlem1  25773  dchrvmasum2lem  25774  dchrvmasum2if  25775  dchrvmasumlem2  25776  dchrvmasumlem3  25777  dchrvmasumiflem1  25779  dchrisum0flblem1  25786  dchrisum0flblem2  25787  dchrisum0fno1  25789  rpvmasum2  25790  rplogsum  25805  mulogsumlem  25809  mulogsum  25810  mulog2sumlem2  25813  vmalogdivsum2  25816  vmalogdivsum  25817  2vmadivsumlem  25818  logsqvma  25820  selberglem2  25824  selberglem3  25825  selberg  25826  selberg2lem  25828  logdivbnd  25834  selberg3lem1  25835  selberg4lem1  25838  pntrsumo1  25843  pntrsumbnd2  25845  selberg3r  25847  selberg4r  25848  selberg34r  25849  pntsval2  25854  pntrlog2bndlem2  25856  pntrlog2bndlem4  25858  pntrlog2bndlem6  25861  pntpbnd1  25864  pntpbnd2  25865  pntlemg  25876  pntlemn  25878  pntlemf  25883  pnt  25892  padicabvf  25909  ostth2lem2  25912  ostth3  25916  fusgrhashclwwlkn  27603  eucrct2eupthOLD  27776  eucrct2eupth  27777  numdenneg  30279  ltesubnnd  30284  1smat1  30708  madjusmdetlem2  30732  madjusmdetlem4  30734  qqhnm  30872  oddpwdc  31254  eulerpartlemsv2  31258  eulerpartlems  31260  eulerpartlemsv3  31261  eulerpartlemgc  31262  eulerpartlemv  31264  eulerpartlemgs2  31280  fibp1  31302  ballotlemfc0  31393  ballotlemfcc  31394  signsvtn0  31483  signsvtn0OLD  31484  reprpmtf1o  31542  vtscl  31554  hgt750lemb  31572  tgoldbachgt  31579  subfacp1lem1  32008  subfacp1lem5  32013  subfacval2  32016  subfaclim  32017  cvmliftlem2  32115  cvmliftlem7  32120  cvmliftlem10  32123  cvmliftlem11  32124  cvmliftlem13  32125  bcm1nt  32486  bcprod  32487  iprodgam  32491  faclimlem1  32492  faclimlem2  32493  faclim2  32497  nn0prpwlem  33188  nn0prpw  33189  knoppndvlem16  33383  poimirlem1  34331  poimirlem2  34332  poimirlem6  34336  poimirlem7  34337  poimirlem8  34338  poimirlem9  34339  poimirlem10  34340  poimirlem11  34341  poimirlem12  34342  poimirlem13  34343  poimirlem15  34345  poimirlem16  34346  poimirlem17  34347  poimirlem18  34348  poimirlem19  34349  poimirlem20  34350  poimirlem21  34351  poimirlem22  34352  poimirlem23  34353  poimirlem24  34354  poimirlem25  34355  poimirlem26  34356  poimirlem27  34357  poimirlem31  34361  expgcd  38612  nn0expgcd  38613  numdenexp  38615  fltne  38676  fltltc  38677  fltnltalem  38678  fltnlta  38679  irrapxlem4  38815  irrapxlem5  38816  pellexlem2  38820  pellexlem6  38824  pell1234qrne0  38843  pell1234qrreccl  38844  pell1234qrmulcl  38845  pell1234qrdich  38851  pell14qrdich  38859  pell1qrge1  38860  pell1qr1  38861  pell14qrgapw  38866  rmxyneg  38910  rmxm1  38924  rmxluc  38926  rmxdbl  38929  jm2.19lem1  38979  jm2.27c  38997  itgpowd  39214  relexpmulnn  39414  relexpmulg  39415  inductionexd  39865  gcddvdsd  39934  fincygsubgodexd  40045  hashnzfzclim  40067  bcccl  40084  bcc0  40085  bccp1k  40086  bccm1k  40087  binomcxplemwb  40093  fsumnncl  41281  mccllem  41307  clim1fr1  41311  sumnnodd  41340  dvsinexp  41623  dvxpaek  41653  dvnxpaek  41655  dvnprodlem2  41660  itgsinexplem1  41667  itgsinexp  41668  stoweidlem1  41715  stoweidlem11  41725  stoweidlem25  41739  stoweidlem26  41740  stoweidlem34  41748  stoweidlem37  41751  stoweidlem38  41752  stoweidlem42  41756  wallispi2lem1  41785  wallispi2  41787  stirlinglem4  41791  stirlinglem5  41792  stirlinglem10  41797  stirlinglem15  41802  dirkertrigeqlem3  41814  dirkertrigeq  41815  dirkercncflem2  41818  dirkercncflem4  41820  fourierdlem11  41832  fourierdlem15  41836  fourierdlem79  41899  fourierdlem83  41903  sqwvfourb  41943  etransclem14  41962  etransclem15  41963  etransclem20  41968  etransclem21  41969  etransclem22  41970  etransclem23  41971  etransclem24  41972  etransclem25  41973  etransclem28  41976  etransclem31  41979  etransclem32  41980  etransclem33  41981  etransclem34  41982  etransclem35  41983  etransclem38  41986  etransclem41  41989  etransclem44  41992  etransclem45  41993  etransclem47  41995  etransclem48  41996  nnfoctbdjlem  42166  deccarry  42915  iccpartgtprec  42950  fmtnoodd  43061  fmtnorec2lem  43070  fmtnorec2  43071  fmtnodvds  43072  goldbachthlem2  43074  fmtnorec3  43076  fmtnorec4  43077  fmtnoprmfac1lem  43092  fmtnoprmfac1  43093  fmtnoprmfac2lem1  43094  fmtnoprmfac2  43095  2pwp1prm  43117  sfprmdvdsmersenne  43134  lighneallem4b  43140  lighneal  43142  proththdlem  43144  proththd  43145  oexpnegALTV  43208  perfectALTVlem1  43252  perfectALTVlem2  43253  perfectALTV  43254  nnpw2pmod  44009  nnolog2flm1  44016  blennn0em1  44017  blengt1fldiv2p1  44019  nn0sumshdiglemB  44046  amgmlemALT  44269
  Copyright terms: Public domain W3C validator