Theorem nncnd 12202

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 12191	. 2 ⊢ ℕ ⊆ ℂ
2		nnred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
3	1, 2	sselid 3944	1 ⊢ (𝜑 → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11066  ℕcn 12186

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711  ax-1cn 11126  ax-addcl 11128

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-ov 7390  df-om 7843  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-nn 12187

This theorem is referenced by:  nneo  12618  facdiv  14252  facndiv  14253  faclbnd  14255  faclbnd5  14263  faclbnd6  14264  facubnd  14265  facavg  14266  bccmpl  14274  bcn0  14275  bcn1  14278  bcm1k  14280  bcp1n  14281  bcp1nk  14282  bcval5  14283  bcpasc  14286  permnn  14291  hashf1  14422  hashfac  14423  relexpaddnn  15017  binom11  15798  binom1dif  15799  climcndslem2  15816  arisum2  15827  trireciplem  15828  trirecip  15829  geo2sum  15839  geo2lim  15841  fprodfac  15939  risefacfac  16001  fallfacfwd  16002  fallfacval4  16009  bcfallfac  16010  fallfacfac  16011  bpolycl  16018  bpolysum  16019  bpolydiflem  16020  fsumkthpow  16022  eftcl  16039  eftabs  16041  efcllem  16043  ege2le3  16056  efcj  16058  efaddlem  16059  eftlub  16077  eirrlem  16172  sqrt2irrlem  16216  oexpneg  16315  pwp1fsum  16361  bitsp1  16401  bitsfzolem  16404  bitsfzo  16405  bitsmod  16406  bitscmp  16408  bitsinv1lem  16411  bitsinv1  16412  2ebits  16417  bitsinvp1  16419  sadcaddlem  16427  sadadd3  16431  bitsres  16443  bitsuz  16444  bitsshft  16445  dvdsgcdidd  16507  mulgcd  16518  rplpwr  16528  sqgcd  16532  expgcd  16533  nn0expgcd  16534  lcmgcdlem  16576  3lcm2e6woprm  16585  coprmprod  16631  coprmproddvdslem  16632  cncongr1  16637  cncongr2  16638  prmind2  16655  isprm5  16677  divgcdodd  16680  prmdvdsexpr  16687  qmuldeneqnum  16717  divnumden  16718  qnumgt0  16720  numdensq  16724  numdenexp  16730  hashdvds  16745  phiprmpw  16746  prmdiv  16755  prmdivdiv  16757  phisum  16761  modprm0  16776  pythagtriplem4  16790  pythagtriplem6  16792  pythagtriplem7  16793  pythagtriplem14  16799  pythagtriplem15  16800  pythagtriplem19  16804  pythagtrip  16805  pcprendvds2  16812  pcpre1  16813  pcpremul  16814  pceulem  16816  pcdiv  16823  pcqmul  16824  pcelnn  16841  pcid  16844  pc2dvds  16850  dvdsprmpweqnn  16856  dvdsprmpweqle  16857  pcaddlem  16859  pcadd  16860  pcfaclem  16869  qexpz  16872  expnprm  16873  oddprmdvds  16874  prmpwdvds  16875  pockthlem  16876  pockthg  16877  infpnlem1  16881  prmreclem1  16887  prmreclem2  16888  prmreclem3  16889  prmreclem4  16890  prmreclem6  16892  4sqlem6  16914  4sqlem7  16915  4sqlem10  16918  mul4sqlem  16924  4sqlem11  16926  4sqlem12  16927  4sqlem14  16929  4sqlem17  16932  4sqlem18  16933  vdwlem1  16952  vdwlem2  16953  vdwlem3  16954  vdwlem5  16956  vdwlem6  16957  vdwlem8  16959  vdwlem9  16960  vdwlem10  16961  vdwlem12  16963  ramub1lem2  16998  ramcl  17000  prmop1  17009  prmdvdsprmo  17013  prmgaplem7  17028  prmgaplem8  17029  gsumsgrpccat  18767  mulgnndir  19035  mulgnnass  19041  psgnunilem5  19424  odf1o2  19503  pgp0  19526  sylow1lem1  19528  odcau  19534  sylow2blem3  19552  sylow3lem3  19559  sylow3lem4  19560  gexexlem  19782  ablfacrp2  19999  ablfac1lem  20000  ablfac1eu  20005  pgpfac1lem3a  20008  pgpfac1lem3  20009  fincygsubgodexd  20045  zringlpirlem3  21374  znrrg  21475  psdpw  22057  cpmadugsumlemF  22763  lebnumlem3  24862  ovollb2lem  25389  ovolunlem1a  25397  ovolunlem1  25398  uniioombllem3  25486  uniioombllem4  25487  dyaddisjlem  25496  mbfi1fseqlem3  25618  mbfi1fseqlem4  25619  itgpowd  25957  dgrcolem1  26179  vieta1lem1  26218  vieta1lem2  26219  elqaalem2  26228  elqaalem3  26229  aalioulem1  26240  aaliou3lem2  26251  aaliou3lem8  26253  aaliou3lem6  26256  aaliou3lem9  26258  taylfvallem1  26264  tayl0  26269  taylply2  26275  taylply2OLD  26276  taylply  26277  dvtaylp  26278  taylthlem1  26281  taylthlem2  26282  taylthlem2OLD  26283  pserdvlem2  26338  advlogexp  26564  cxpmul2  26598  cxpeq  26667  rtprmirr  26670  atantayl3  26849  leibpi  26852  log2cnv  26854  log2tlbnd  26855  birthdaylem2  26862  birthdaylem3  26863  amgmlem  26900  amgm  26901  emcllem5  26910  fsumharmonic  26922  zetacvg  26925  dmgmdivn0  26938  lgamgulmlem3  26941  lgamgulmlem4  26942  lgamgulmlem5  26943  lgamgulmlem6  26944  lgamgulm2  26946  lgamcvg2  26965  gamcvg  26966  gamcvg2lem  26969  facgam  26976  wilthlem1  26978  wilthlem2  26979  wilthlem3  26980  wilthimp  26982  basellem1  26991  basellem2  26992  basellem3  26993  basellem4  26994  basellem5  26995  basellem8  26998  vmaprm  27027  sgmval2  27053  0sgm  27054  sgmf  27055  vma1  27076  fsumdvdsdiaglem  27093  dvdsflf1o  27097  muinv  27103  mpodvdsmulf1o  27104  dvdsmulf1o  27106  sgmppw  27108  1sgmprm  27110  1sgm2ppw  27111  sgmmul  27112  chtublem  27122  fsumvma2  27125  chpchtsum  27130  logfaclbnd  27133  logexprlim  27136  mersenne  27138  perfect1  27139  perfectlem1  27140  perfectlem2  27141  perfect  27142  dchrsum2  27179  dchrhash  27182  bcmono  27188  bcp1ctr  27190  bclbnd  27191  bposlem1  27195  bposlem2  27196  bposlem3  27197  bposlem5  27199  bposlem6  27200  lgsval2lem  27218  lgsqrlem2  27258  gausslemma2dlem6  27283  gausslemma2dlem7  27284  gausslemma2d  27285  lgseisenlem1  27286  lgseisenlem4  27289  lgsquadlem1  27291  lgsquadlem2  27292  lgsquadlem3  27293  lgsquad2  27297  m1lgs  27299  2sqlem3  27331  2sqlem4  27332  chebbnd1lem1  27380  chebbnd1  27383  rplogsumlem1  27395  rplogsumlem2  27396  rpvmasumlem  27398  dchrisumlem1  27400  dchrmusum2  27405  dchrvmasumlem1  27406  dchrvmasum2lem  27407  dchrvmasum2if  27408  dchrvmasumlem2  27409  dchrvmasumlem3  27410  dchrvmasumiflem1  27412  dchrisum0flblem1  27419  dchrisum0flblem2  27420  dchrisum0fno1  27422  rpvmasum2  27423  rplogsum  27438  mulogsumlem  27442  mulogsum  27443  mulog2sumlem2  27446  vmalogdivsum2  27449  vmalogdivsum  27450  2vmadivsumlem  27451  logsqvma  27453  selberglem2  27457  selberglem3  27458  selberg  27459  selberg2lem  27461  logdivbnd  27467  selberg3lem1  27468  selberg4lem1  27471  pntrsumo1  27476  pntrsumbnd2  27478  selberg3r  27480  selberg4r  27481  selberg34r  27482  pntsval2  27487  pntrlog2bndlem2  27489  pntrlog2bndlem4  27491  pntrlog2bndlem6  27494  pntpbnd1  27497  pntpbnd2  27498  pntlemg  27509  pntlemn  27511  pntlemf  27516  pnt  27525  padicabvf  27542  ostth2lem2  27545  ostth3  27549  fusgrhashclwwlkn  30008  eucrct2eupth  30174  nrt2irr  30402  elq2  32736  numdenneg  32739  ltesubnnd  32747  2exple2exp  32770  oexpled  32772  chnub  32938  1arithidomlem2  33507  1arithidom  33508  zringfrac  33525  cos9thpiminplylem1  33772  cos9thpiminplylem2  33773  1smat1  33794  madjusmdetlem2  33818  madjusmdetlem4  33820  qqhnm  33980  oddpwdc  34345  eulerpartlemsv2  34349  eulerpartlems  34351  eulerpartlemsv3  34352  eulerpartlemgc  34353  eulerpartlemv  34355  eulerpartlemgs2  34371  fibp1  34392  ballotlemfc0  34484  ballotlemfcc  34485  signsvtn0  34561  reprpmtf1o  34617  vtscl  34629  hgt750lemb  34647  tgoldbachgt  34654  subfacp1lem1  35166  subfacp1lem5  35171  subfacval2  35174  subfaclim  35175  cvmliftlem2  35273  cvmliftlem7  35278  cvmliftlem10  35281  cvmliftlem11  35282  cvmliftlem13  35283  bcm1nt  35724  bcprod  35725  iprodgam  35729  faclimlem1  35730  faclimlem2  35731  faclim2  35735  nn0prpwlem  36310  nn0prpw  36311  knoppcnlem10  36490  knoppndvlem16  36515  poimirlem1  37615  poimirlem2  37616  poimirlem6  37620  poimirlem7  37621  poimirlem8  37622  poimirlem9  37623  poimirlem10  37624  poimirlem11  37625  poimirlem12  37626  poimirlem13  37627  poimirlem15  37629  poimirlem16  37630  poimirlem17  37631  poimirlem18  37632  poimirlem19  37633  poimirlem20  37634  poimirlem21  37635  poimirlem22  37636  poimirlem23  37637  poimirlem24  37638  poimirlem25  37639  poimirlem26  37640  poimirlem27  37641  poimirlem31  37645  nnproddivdvdsd  41988  lcmfunnnd  42000  lcmineqlem3  42019  lcmineqlem4  42020  lcmineqlem6  42022  lcmineqlem8  42024  lcmineqlem10  42026  lcmineqlem11  42027  lcmineqlem12  42028  lcmineqlem16  42032  lcmineqlem18  42034  lcmineqlem23  42039  dvrelogpow2b  42056  aks4d1p1p2  42058  aks4d1p1  42064  aks4d1p8  42075  primrootsunit1  42085  primrootscoprmpow  42087  posbezout  42088  primrootscoprbij  42090  primrootspoweq0  42094  aks6d1c1p3  42098  aks6d1c1p8  42103  aks6d1c2p2  42107  hashscontpow1  42109  2np3bcnp1  42132  2ap1caineq  42133  sticksstones10  42143  sticksstones12a  42145  sticksstones16  42150  sticksstones22  42156  bcled  42166  bcle2d  42167  aks6d1c7lem1  42168  aks6d1c7  42172  unitscyglem2  42184  unitscyglem4  42186  unitscyglem5  42187  aks5lem8  42189  nnadddir  42258  nnmul1com  42259  nnmulcom  42260  oddnumth  42299  nicomachus  42300  zaddcom  42452  fltabcoprmex  42627  fltaccoprm  42628  fltbccoprm  42629  fltne  42632  flt4lem3  42636  flt4lem5elem  42639  flt4lem5a  42640  flt4lem5b  42641  flt4lem5c  42642  flt4lem5d  42643  flt4lem5e  42644  flt4lem5f  42645  flt4lem6  42646  flt4lem7  42647  nna4b4nsq  42648  fltltc  42649  fltnltalem  42650  fltnlta  42651  irrapxlem4  42813  irrapxlem5  42814  pellexlem2  42818  pellexlem6  42822  pell1234qrne0  42841  pell1234qrreccl  42842  pell1234qrmulcl  42843  pell1234qrdich  42849  pell14qrdich  42857  pell1qrge1  42858  pell1qr1  42859  pell14qrgapw  42864  rmxyneg  42909  rmxm1  42923  rmxluc  42925  rmxdbl  42928  jm2.19lem1  42978  jm2.27c  42996  relexpmulnn  43698  relexpmulg  43699  inductionexd  44144  hashnzfzclim  44311  bcccl  44328  bcc0  44329  bccp1k  44330  bccm1k  44331  binomcxplemwb  44337  fsumnncl  45570  mccllem  45595  clim1fr1  45599  sumnnodd  45628  dvsinexp  45909  dvxpaek  45938  dvnxpaek  45940  dvnprodlem2  45945  itgsinexplem1  45952  itgsinexp  45953  stoweidlem1  45999  stoweidlem11  46009  stoweidlem25  46023  stoweidlem26  46024  stoweidlem34  46032  stoweidlem37  46035  stoweidlem38  46036  stoweidlem42  46040  wallispi2lem1  46069  wallispi2  46071  stirlinglem4  46075  stirlinglem5  46076  stirlinglem10  46081  stirlinglem15  46086  dirkertrigeqlem3  46098  dirkertrigeq  46099  dirkercncflem2  46102  dirkercncflem4  46104  fourierdlem11  46116  fourierdlem15  46120  fourierdlem79  46183  fourierdlem83  46187  sqwvfourb  46227  etransclem14  46246  etransclem15  46247  etransclem20  46252  etransclem21  46253  etransclem22  46254  etransclem23  46255  etransclem24  46256  etransclem25  46257  etransclem28  46260  etransclem31  46263  etransclem32  46264  etransclem33  46265  etransclem34  46266  etransclem35  46267  etransclem38  46270  etransclem41  46273  etransclem44  46276  etransclem45  46277  etransclem47  46279  etransclem48  46280  nnfoctbdjlem  46453  deccarry  47312  iccpartgtprec  47421  fmtnoodd  47534  fmtnorec2lem  47543  fmtnorec2  47544  fmtnodvds  47545  goldbachthlem2  47547  fmtnorec3  47549  fmtnorec4  47550  fmtnoprmfac1lem  47565  fmtnoprmfac1  47566  fmtnoprmfac2lem1  47567  fmtnoprmfac2  47568  2pwp1prm  47590  sfprmdvdsmersenne  47604  lighneallem4b  47610  lighneal  47612  proththdlem  47614  proththd  47615  oexpnegALTV  47678  perfectALTVlem1  47722  perfectALTVlem2  47723  perfectALTV  47724  nnpw2pmod  48572  nnolog2flm1  48579  blennn0em1  48580  blengt1fldiv2p1  48582  nn0sumshdiglemB  48609  amgmlemALT  49792