Theorem nncnd 12210

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

Step	Hyp	Ref	Expression
1		nnsscn 12199	. 2 ⊢ ℕ ⊆ ℂ
2		nnred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
3	1, 2	sselid 3976	1 ⊢ (𝜑 → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2106  ℂcc 11090  ℕcn 12194

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5292  ax-nul 5299  ax-pr 5420  ax-un 7708  ax-1cn 11150  ax-addcl 11152

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4523  df-pw 4598  df-sn 4623  df-pr 4625  df-op 4629  df-uni 4902  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6289  df-ord 6356  df-on 6357  df-lim 6358  df-suc 6359  df-iota 6484  df-fun 6534  df-fn 6535  df-f 6536  df-f1 6537  df-fo 6538  df-f1o 6539  df-fv 6540  df-ov 7396  df-om 7839  df-2nd 7958  df-frecs 8248  df-wrecs 8279  df-recs 8353  df-rdg 8392  df-nn 12195

This theorem is referenced by:  nneo  12628  facdiv  14229  facndiv  14230  faclbnd  14232  faclbnd5  14240  faclbnd6  14241  facubnd  14242  facavg  14243  bccmpl  14251  bcn0  14252  bcn1  14255  bcm1k  14257  bcp1n  14258  bcp1nk  14259  bcval5  14260  bcpasc  14263  permnn  14268  hashf1  14400  hashfac  14401  relexpaddnn  14980  binom11  15760  binom1dif  15761  climcndslem2  15778  arisum2  15789  trireciplem  15790  trirecip  15791  geo2sum  15801  geo2lim  15803  fprodfac  15899  risefacfac  15961  fallfacfwd  15962  fallfacval4  15969  bcfallfac  15970  fallfacfac  15971  bpolycl  15978  bpolysum  15979  bpolydiflem  15980  fsumkthpow  15982  eftcl  15999  eftabs  16001  efcllem  16003  ege2le3  16015  efcj  16017  efaddlem  16018  eftlub  16034  eirrlem  16129  sqrt2irrlem  16173  oexpneg  16270  pwp1fsum  16316  bitsp1  16354  bitsfzolem  16357  bitsfzo  16358  bitsmod  16359  bitscmp  16361  bitsinv1lem  16364  bitsinv1  16365  2ebits  16370  bitsinvp1  16372  sadcaddlem  16380  sadadd3  16384  bitsres  16396  bitsuz  16397  bitsshft  16398  dvdsgcdidd  16461  mulgcd  16472  rplpwr  16481  sqgcd  16484  lcmgcdlem  16525  3lcm2e6woprm  16534  coprmprod  16580  coprmproddvdslem  16581  cncongr1  16586  cncongr2  16587  prmind2  16604  isprm5  16626  divgcdodd  16629  prmdvdsexpr  16636  qmuldeneqnum  16665  divnumden  16666  qnumgt0  16668  numdensq  16672  hashdvds  16690  phiprmpw  16691  prmdiv  16700  prmdivdiv  16702  phisum  16705  modprm0  16720  pythagtriplem4  16734  pythagtriplem6  16736  pythagtriplem7  16737  pythagtriplem14  16743  pythagtriplem15  16744  pythagtriplem19  16748  pythagtrip  16749  pcprendvds2  16756  pcpre1  16757  pcpremul  16758  pceulem  16760  pcdiv  16767  pcqmul  16768  pcelnn  16785  pcid  16788  pc2dvds  16794  dvdsprmpweqnn  16800  dvdsprmpweqle  16801  pcaddlem  16803  pcadd  16804  pcfaclem  16813  qexpz  16816  expnprm  16817  oddprmdvds  16818  prmpwdvds  16819  pockthlem  16820  pockthg  16821  infpnlem1  16825  prmreclem1  16831  prmreclem2  16832  prmreclem3  16833  prmreclem4  16834  prmreclem6  16836  4sqlem6  16858  4sqlem7  16859  4sqlem10  16862  mul4sqlem  16868  4sqlem11  16870  4sqlem12  16871  4sqlem14  16873  4sqlem17  16876  4sqlem18  16877  vdwlem1  16896  vdwlem2  16897  vdwlem3  16898  vdwlem5  16900  vdwlem6  16901  vdwlem8  16903  vdwlem9  16904  vdwlem10  16905  vdwlem12  16907  ramub1lem2  16942  ramcl  16944  prmop1  16953  prmdvdsprmo  16957  prmgaplem7  16972  prmgaplem8  16973  gsumsgrpccat  18696  mulgnndir  18955  mulgnnass  18961  psgnunilem5  19326  odf1o2  19405  pgp0  19428  sylow1lem1  19430  odcau  19436  sylow2blem3  19454  sylow3lem3  19461  sylow3lem4  19462  gexexlem  19680  ablfacrp2  19896  ablfac1lem  19897  ablfac1eu  19902  pgpfac1lem3a  19905  pgpfac1lem3  19906  fincygsubgodexd  19942  zringlpirlem3  20967  znrrg  21054  cpmadugsumlemF  22307  lebnumlem3  24408  ovollb2lem  24934  ovolunlem1a  24942  ovolunlem1  24943  uniioombllem3  25031  uniioombllem4  25032  dyaddisjlem  25041  mbfi1fseqlem3  25164  mbfi1fseqlem4  25165  itgpowd  25496  dgrcolem1  25716  vieta1lem1  25752  vieta1lem2  25753  elqaalem2  25762  elqaalem3  25763  aalioulem1  25774  aaliou3lem2  25785  aaliou3lem8  25787  aaliou3lem6  25790  aaliou3lem9  25792  taylfvallem1  25798  tayl0  25803  taylply2  25809  taylply  25810  dvtaylp  25811  taylthlem1  25814  taylthlem2  25815  pserdvlem2  25869  advlogexp  26092  cxpmul2  26126  cxpeq  26192  atantayl3  26371  leibpi  26374  log2cnv  26376  log2tlbnd  26377  birthdaylem2  26384  birthdaylem3  26385  amgmlem  26421  amgm  26422  emcllem5  26431  fsumharmonic  26443  zetacvg  26446  dmgmdivn0  26459  lgamgulmlem3  26462  lgamgulmlem4  26463  lgamgulmlem5  26464  lgamgulmlem6  26465  lgamgulm2  26467  lgamcvg2  26486  gamcvg  26487  gamcvg2lem  26490  facgam  26497  wilthlem1  26499  wilthlem2  26500  wilthlem3  26501  wilthimp  26503  basellem1  26512  basellem2  26513  basellem3  26514  basellem4  26515  basellem5  26516  basellem8  26519  vmaprm  26548  sgmval2  26574  0sgm  26575  sgmf  26576  vma1  26597  fsumdvdsdiaglem  26614  dvdsflf1o  26618  muinv  26624  dvdsmulf1o  26625  sgmppw  26627  1sgmprm  26629  1sgm2ppw  26630  sgmmul  26631  chtublem  26641  fsumvma2  26644  chpchtsum  26649  logfaclbnd  26652  logexprlim  26655  mersenne  26657  perfect1  26658  perfectlem1  26659  perfectlem2  26660  perfect  26661  dchrsum2  26698  dchrhash  26701  bcmono  26707  bcp1ctr  26709  bclbnd  26710  bposlem1  26714  bposlem2  26715  bposlem3  26716  bposlem5  26718  bposlem6  26719  lgsval2lem  26737  lgsqrlem2  26777  gausslemma2dlem6  26802  gausslemma2dlem7  26803  gausslemma2d  26804  lgseisenlem1  26805  lgseisenlem4  26808  lgsquadlem1  26810  lgsquadlem2  26811  lgsquadlem3  26812  lgsquad2  26816  m1lgs  26818  2sqlem3  26850  2sqlem4  26851  chebbnd1lem1  26899  chebbnd1  26902  rplogsumlem1  26914  rplogsumlem2  26915  rpvmasumlem  26917  dchrisumlem1  26919  dchrmusum2  26924  dchrvmasumlem1  26925  dchrvmasum2lem  26926  dchrvmasum2if  26927  dchrvmasumlem2  26928  dchrvmasumlem3  26929  dchrvmasumiflem1  26931  dchrisum0flblem1  26938  dchrisum0flblem2  26939  dchrisum0fno1  26941  rpvmasum2  26942  rplogsum  26957  mulogsumlem  26961  mulogsum  26962  mulog2sumlem2  26965  vmalogdivsum2  26968  vmalogdivsum  26969  2vmadivsumlem  26970  logsqvma  26972  selberglem2  26976  selberglem3  26977  selberg  26978  selberg2lem  26980  logdivbnd  26986  selberg3lem1  26987  selberg4lem1  26990  pntrsumo1  26995  pntrsumbnd2  26997  selberg3r  26999  selberg4r  27000  selberg34r  27001  pntsval2  27006  pntrlog2bndlem2  27008  pntrlog2bndlem4  27010  pntrlog2bndlem6  27013  pntpbnd1  27016  pntpbnd2  27017  pntlemg  27028  pntlemn  27030  pntlemf  27035  pnt  27044  padicabvf  27061  ostth2lem2  27064  ostth3  27068  fusgrhashclwwlkn  29197  eucrct2eupth  29363  numdenneg  31894  ltesubnnd  31899  1smat1  32615  madjusmdetlem2  32639  madjusmdetlem4  32641  qqhnm  32801  oddpwdc  33184  eulerpartlemsv2  33188  eulerpartlems  33190  eulerpartlemsv3  33191  eulerpartlemgc  33192  eulerpartlemv  33194  eulerpartlemgs2  33210  fibp1  33231  ballotlemfc0  33322  ballotlemfcc  33323  signsvtn0  33412  reprpmtf1o  33469  vtscl  33481  hgt750lemb  33499  tgoldbachgt  33506  subfacp1lem1  34001  subfacp1lem5  34006  subfacval2  34009  subfaclim  34010  cvmliftlem2  34108  cvmliftlem7  34113  cvmliftlem10  34116  cvmliftlem11  34117  cvmliftlem13  34118  bcm1nt  34537  bcprod  34538  iprodgam  34542  faclimlem1  34543  faclimlem2  34544  faclim2  34548  nn0prpwlem  35011  nn0prpw  35012  knoppndvlem16  35207  poimirlem1  36293  poimirlem2  36294  poimirlem6  36298  poimirlem7  36299  poimirlem8  36300  poimirlem9  36301  poimirlem10  36302  poimirlem11  36303  poimirlem12  36304  poimirlem13  36305  poimirlem15  36307  poimirlem16  36308  poimirlem17  36309  poimirlem18  36310  poimirlem19  36311  poimirlem20  36312  poimirlem21  36313  poimirlem22  36314  poimirlem23  36315  poimirlem24  36316  poimirlem25  36317  poimirlem26  36318  poimirlem27  36319  poimirlem31  36323  nnproddivdvdsd  40671  lcmfunnnd  40682  lcmineqlem3  40701  lcmineqlem4  40702  lcmineqlem6  40704  lcmineqlem8  40706  lcmineqlem10  40708  lcmineqlem11  40709  lcmineqlem12  40710  lcmineqlem16  40714  lcmineqlem18  40716  lcmineqlem23  40721  dvrelogpow2b  40738  aks4d1p1p2  40740  aks4d1p1  40746  aks4d1p8  40757  aks6d1c2p2  40762  2np3bcnp1  40765  2ap1caineq  40766  sticksstones10  40776  sticksstones12a  40778  sticksstones16  40783  sticksstones22  40789  metakunt8  40797  metakunt15  40804  metakunt16  40805  metakunt20  40809  metakunt28  40817  metakunt30  40819  nnadddir  40972  nnmul1com  40973  nnmulcom  40974  expgcd  41006  nn0expgcd  41007  numdenexp  41009  zaddcom  41107  fltabcoprmex  41163  fltaccoprm  41164  fltbccoprm  41165  fltne  41168  flt4lem3  41172  flt4lem5elem  41175  flt4lem5a  41176  flt4lem5b  41177  flt4lem5c  41178  flt4lem5d  41179  flt4lem5e  41180  flt4lem5f  41181  flt4lem6  41182  flt4lem7  41183  nna4b4nsq  41184  fltltc  41185  fltnltalem  41186  fltnlta  41187  irrapxlem4  41334  irrapxlem5  41335  pellexlem2  41339  pellexlem6  41343  pell1234qrne0  41362  pell1234qrreccl  41363  pell1234qrmulcl  41364  pell1234qrdich  41370  pell14qrdich  41378  pell1qrge1  41379  pell1qr1  41380  pell14qrgapw  41385  rmxyneg  41430  rmxm1  41444  rmxluc  41446  rmxdbl  41449  jm2.19lem1  41499  jm2.27c  41517  relexpmulnn  42231  relexpmulg  42232  inductionexd  42677  hashnzfzclim  42852  bcccl  42869  bcc0  42870  bccp1k  42871  bccm1k  42872  binomcxplemwb  42878  fsumnncl  44061  mccllem  44086  clim1fr1  44090  sumnnodd  44119  dvsinexp  44400  dvxpaek  44429  dvnxpaek  44431  dvnprodlem2  44436  itgsinexplem1  44443  itgsinexp  44444  stoweidlem1  44490  stoweidlem11  44500  stoweidlem25  44514  stoweidlem26  44515  stoweidlem34  44523  stoweidlem37  44526  stoweidlem38  44527  stoweidlem42  44531  wallispi2lem1  44560  wallispi2  44562  stirlinglem4  44566  stirlinglem5  44567  stirlinglem10  44572  stirlinglem15  44577  dirkertrigeqlem3  44589  dirkertrigeq  44590  dirkercncflem2  44593  dirkercncflem4  44595  fourierdlem11  44607  fourierdlem15  44611  fourierdlem79  44674  fourierdlem83  44678  sqwvfourb  44718  etransclem14  44737  etransclem15  44738  etransclem20  44743  etransclem21  44744  etransclem22  44745  etransclem23  44746  etransclem24  44747  etransclem25  44748  etransclem28  44751  etransclem31  44754  etransclem32  44755  etransclem33  44756  etransclem34  44757  etransclem35  44758  etransclem38  44761  etransclem41  44764  etransclem44  44767  etransclem45  44768  etransclem47  44770  etransclem48  44771  nnfoctbdjlem  44944  deccarry  45791  iccpartgtprec  45860  fmtnoodd  45973  fmtnorec2lem  45982  fmtnorec2  45983  fmtnodvds  45984  goldbachthlem2  45986  fmtnorec3  45988  fmtnorec4  45989  fmtnoprmfac1lem  46004  fmtnoprmfac1  46005  fmtnoprmfac2lem1  46006  fmtnoprmfac2  46007  2pwp1prm  46029  sfprmdvdsmersenne  46043  lighneallem4b  46049  lighneal  46051  proththdlem  46053  proththd  46054  oexpnegALTV  46117  perfectALTVlem1  46161  perfectALTVlem2  46162  perfectALTV  46163  nnpw2pmod  46917  nnolog2flm1  46924  blennn0em1  46925  blengt1fldiv2p1  46927  nn0sumshdiglemB  46954  amgmlemALT  47498