Theorem nncnd 12354

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ℂcc 11201  ℕcn 12338

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7751  ax-1cn 11261  ax-addcl 11263

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7423  df-om 7878  df-2nd 8002  df-frecs 8302  df-wrecs 8333  df-recs 8382  df-rdg 8421  df-nn 12339

This theorem is used by:  nnadddir  12397  nnmul1com  12398  nnmulcom  12399  nneo  12786  facdiv  14434  facndiv  14435  faclbnd  14437  faclbnd5  14445  faclbnd6  14446  facubnd  14447  facavg  14448  bccmpl  14456  bcn0  14457  bcn1  14460  bcm1k  14462  bcp1n  14463  bcp1nk  14464  bcval5  14465  bcpasc  14468  permnn  14473  hashf1  14605  hashfac  14606  relexpaddnn  15209  binom11  16006  binom1dif  16007  climcndslem2  16024  arisum2  16035  trireciplem  16036  trirecip  16037  geo2sum  16047  geo2lim  16049  fprodfac  16145  risefacfac  16206  fallfacfwd  16207  fallfacval4  16214  bcfallfac  16215  fallfacfac  16216  bpolycl  16223  bpolysum  16224  bpolydiflem  16225  fsumkthpow  16227  eftcl  16244  eftabs  16246  efcllem  16248  ege2le3  16261  efcj  16263  efaddlem  16264  eftlub  16282  eirrlem  16377  sqrt2irrlem  16421  oexpneg  16520  pwp1fsum  16566  bitsp1  16606  bitsfzolem  16609  bitsfzo  16610  bitsmod  16611  bitscmp  16613  bitsinv1lem  16616  bitsinv1  16617  2ebits  16622  bitsinvp1  16624  sadcaddlem  16632  sadadd3  16636  bitsres  16648  bitsuz  16649  bitsshft  16650  dvdsgcdidd  16715  mulgcd  16726  rplpwr  16737  sqgcd  16741  expgcd  16742  nn0expgcd  16743  lcmgcdlem  16786  3lcm2e6woprm  16795  coprmprod  16841  coprmproddvdslem  16842  cncongr1  16847  cncongr2  16848  prmind2  16865  isprm5  16888  divgcdodd  16891  prmdvdsexpr  16898  qmuldeneqnum  16928  divnumden  16929  qnumgt0  16931  numdensq  16935  numdenexp  16942  hashdvds  16957  phiprmpw  16958  prmdiv  16967  prmdivdiv  16969  phisum  16973  modprm0  16988  pythagtriplem4  17002  pythagtriplem6  17004  pythagtriplem7  17005  pythagtriplem14  17011  pythagtriplem15  17012  pythagtriplem19  17016  pythagtrip  17017  pcprendvds2  17024  pcpre1  17025  pcpremul  17026  pceulem  17028  pcdiv  17035  pcqmul  17036  pcelnn  17053  pcid  17056  pc2dvds  17062  dvdsprmpweqnn  17068  dvdsprmpweqle  17069  pcaddlem  17071  pcadd  17072  pcfaclem  17081  qexpz  17084  expnprm  17085  oddprmdvds  17086  prmpwdvds  17087  pockthlem  17088  pockthg  17089  infpnlem1  17093  prmreclem1  17099  prmreclem2  17100  prmreclem3  17101  prmreclem4  17102  prmreclem6  17104  4sqlem6  17126  4sqlem7  17127  4sqlem10  17130  mul4sqlem  17136  4sqlem11  17138  4sqlem12  17139  4sqlem14  17141  4sqlem17  17144  4sqlem18  17145  vdwlem1  17164  vdwlem2  17165  vdwlem3  17166  vdwlem5  17168  vdwlem6  17169  vdwlem8  17171  vdwlem9  17172  vdwlem10  17173  vdwlem12  17175  ramub1lem2  17210  ramcl  17212  prmop1  17221  prmdvdsprmo  17225  prmgaplem7  17240  prmgaplem8  17241  chnub  18801  gsumsgrpccat  19041  mulgnndir  19318  mulgnnass  19324  psgnunilem5  19713  odf1o2  19792  pgp0  19815  sylow1lem1  19817  odcau  19823  sylow2blem3  19841  sylow3lem3  19848  sylow3lem4  19849  gexexlem  20071  ablfacrp2  20288  ablfac1lem  20289  ablfac1eu  20294  pgpfac1lem3a  20297  pgpfac1lem3  20298  fincygsubgodexd  20334  zringlpirlem3  21775  znrrg  21876  psdpw  22496  cpmadugsumlemF  23199  lebnumlem3  25289  ovollb2lem  25814  ovolunlem1a  25822  ovolunlem1  25823  uniioombllem3  25911  uniioombllem4  25912  dyaddisjlem  25921  mbfi1fseqlem3  26043  mbfi1fseqlem4  26044  itgpowd  26375  dgrcolem1  26597  vieta1lem1  26638  vieta1lem2  26639  elqaalem2  26648  elqaalem3  26649  aalioulem1  26664  aaliou3lem2  26675  aaliou3lem8  26677  aaliou3lem6  26680  aaliou3lem9  26682  taylfvallem1  26689  tayl0  26694  taylply2  26700  taylply  26701  dvtaylp  26702  taylthlem1  26705  taylthlem2  26706  pserdvlem2  26760  advlogexp  26988  cxpmul2  27022  cxpeq  27090  rtprmirr  27093  atantayl3  27272  leibpi  27275  log2cnv  27277  log2tlbnd  27278  birthdaylem2  27285  birthdaylem3  27286  amgmlem  27322  amgm  27323  emcllem5  27332  fsumharmonic  27344  zetacvg  27347  dmgmdivn0  27360  lgamgulmlem3  27363  lgamgulmlem4  27364  lgamgulmlem5  27365  lgamgulmlem6  27366  lgamgulm2  27368  lgamcvg2  27387  gamcvg  27388  gamcvg2lem  27391  facgam  27398  wilthlem1  27400  wilthlem2  27401  wilthlem3  27402  wilthimp  27404  basellem1  27413  basellem2  27414  basellem3  27415  basellem4  27416  basellem5  27417  basellem8  27420  vmaprm  27449  sgmval2  27475  0sgm  27476  sgmf  27477  vma1  27498  fsumdvdsdiaglem  27515  dvdsflf1o  27519  muinv  27525  mpodvdsmulf1o  27526  dvdsmulf1o  27528  sgmppw  27529  1sgmprm  27531  1sgm2ppw  27532  sgmmul  27533  chtublem  27543  fsumvma2  27546  chpchtsum  27551  logfaclbnd  27554  logexprlim  27557  mersenne  27559  perfect1  27560  perfectlem1  27561  perfectlem2  27562  perfect  27563  dchrsum2  27600  dchrhash  27603  bcmono  27609  bcp1ctr  27611  bclbnd  27612  bposlem1  27616  bposlem2  27617  bposlem3  27618  bposlem5  27620  bposlem6  27621  lgsval2lem  27639  lgsqrlem2  27679  gausslemma2dlem6  27704  gausslemma2dlem7  27705  gausslemma2d  27706  lgseisenlem1  27707  lgseisenlem4  27710  lgsquadlem1  27712  lgsquadlem2  27713  lgsquadlem3  27714  lgsquad2  27718  m1lgs  27720  2sqlem3  27752  2sqlem4  27753  chebbnd1lem1  27801  chebbnd1  27804  rplogsumlem1  27816  rplogsumlem2  27817  rpvmasumlem  27819  dchrisumlem1  27821  dchrmusum2  27826  dchrvmasumlem1  27827  dchrvmasum2lem  27828  dchrvmasum2if  27829  dchrvmasumlem2  27830  dchrvmasumlem3  27831  dchrvmasumiflem1  27833  dchrisum0flblem1  27840  dchrisum0flblem2  27841  dchrisum0fno1  27843  rpvmasum2  27844  rplogsum  27859  mulogsumlem  27863  mulogsum  27864  mulog2sumlem2  27867  vmalogdivsum2  27870  vmalogdivsum  27871  2vmadivsumlem  27872  logsqvma  27874  selberglem2  27878  selberglem3  27879  selberg  27880  selberg2lem  27882  logdivbnd  27888  selberg3lem1  27889  selberg4lem1  27892  pntrsumo1  27897  pntrsumbnd2  27899  selberg3r  27901  selberg4r  27902  selberg34r  27903  pntsval2  27908  pntrlog2bndlem2  27910  pntrlog2bndlem4  27912  pntrlog2bndlem6  27915  pntpbnd1  27918  pntpbnd2  27919  pntlemg  27930  pntlemn  27932  pntlemf  27937  pnt  27946  padicabvf  27963  ostth2lem2  27966  ostth3  27970  fltabcoprmex  27976  fltaccoprm  27977  fltbccoprm  27978  fltne  27980  flt4lem3  27983  flt4lem5elem  27986  flt4lem5a  27987  flt4lem5b  27988  flt4lem5c  27989  flt4lem5d  27990  flt4lem5e  27991  flt4lem5f  27992  flt4lem6  27993  flt4lem7  27994  nna4b4nsq  27995  flt4  27996  flt4ALT  27997  fltoprm  28000  fusgrhashclwwlkn  30675  eucrct2eupth  30851  nrt2irr  31079  elq2  33449  numdenneg  33452  ltesubnnd  33460  2exple2exp  33471  oexpled  33473  gsummptp1  33664  1arithidomlem2  34114  1arithidom  34115  zringfrac  34132  cos9thpiminplylem1  34460  cos9thpiminplylem2  34461  1smat1  34482  madjusmdetlem2  34506  madjusmdetlem4  34508  qqhnm  34668  oddpwdc  35032  eulerpartlemsv2  35036  eulerpartlems  35038  eulerpartlemsv3  35039  eulerpartlemgc  35040  eulerpartlemv  35042  eulerpartlemgs2  35058  fibp1  35079  ballotlemfc0  35171  ballotlemfcc  35172  signsvtn0  35245  reprpmtf1o  35301  vtscl  35313  hgt750lemb  35331  tgoldbachgt  35338  subfacp1lem1  36030  subfacp1lem5  36035  subfacval2  36038  subfaclim  36039  cvmliftlem2  36137  cvmliftlem7  36142  cvmliftlem10  36145  cvmliftlem11  36146  cvmliftlem13  36147  bcm1nt  36594  bcprod  36595  iprodgam  36599  faclimlem1  36600  faclimlem2  36601  faclim2  36605  nn0prpwlem  37202  nn0prpw  37203  knoppcnlem10  37460  knoppndvlem16  37485  poimirlem1  38632  poimirlem2  38633  poimirlem6  38637  poimirlem7  38638  poimirlem8  38639  poimirlem9  38640  poimirlem10  38641  poimirlem11  38642  poimirlem12  38643  poimirlem13  38644  poimirlem15  38646  poimirlem16  38647  poimirlem17  38648  poimirlem18  38649  poimirlem19  38650  poimirlem20  38651  poimirlem21  38652  poimirlem22  38653  poimirlem23  38654  poimirlem24  38655  poimirlem25  38656  poimirlem26  38657  poimirlem27  38658  poimirlem31  38662  nnproddivdvdsd  43143  lcmfunnnd  43155  lcmineqlem3  43174  lcmineqlem4  43175  lcmineqlem6  43177  lcmineqlem8  43179  lcmineqlem10  43181  lcmineqlem11  43182  lcmineqlem12  43183  lcmineqlem16  43187  lcmineqlem18  43189  lcmineqlem23  43194  dvrelogpow2b  43211  aks4d1p1p2  43213  aks4d1p1  43219  aks4d1p8  43230  primrootsunit1  43240  primrootscoprmpow  43242  posbezout  43243  primrootscoprbij  43245  primrootspoweq0  43249  aks6d1c1p3  43253  aks6d1c1p8  43258  aks6d1c2p2  43262  hashscontpow1  43264  2np3bcnp1  43287  2ap1caineq  43288  sticksstones10  43298  sticksstones12a  43300  sticksstones16  43305  sticksstones22  43311  bcled  43321  bcle2d  43322  aks6d1c7lem1  43323  aks6d1c7  43327  unitscyglem2  43339  unitscyglem4  43341  unitscyglem5  43342  aks5lem8  43344  oddnumth  43461  nicomachus  43462  zaddcom  43621  fltltc  43765  fltnltalem  43766  fltnlta  43767  irrapxlem4  43925  irrapxlem5  43926  pellexlem2  43930  pellexlem6  43934  pell1234qrne0  43953  pell1234qrreccl  43954  pell1234qrmulcl  43955  pell1234qrdich  43961  pell14qrdich  43969  pell1qrge1  43970  pell1qr1  43971  pell14qrgapw  43976  rmxyneg  44020  rmxm1  44034  rmxluc  44036  rmxdbl  44039  jm2.19lem1  44089  jm2.27c  44107  relexpmulnn  44802  relexpmulg  44803  inductionexd  45248  hashnzfzclim  45399  bcccl  45416  bcc0  45417  bccp1k  45418  bccm1k  45419  binomcxplemwb  45425  fsumnncl  46677  mccllem  46702  clim1fr1  46706  sumnnodd  46735  dvsinexp  47014  dvxpaek  47043  dvnxpaek  47045  dvnprodlem2  47050  itgsinexplem1  47057  itgsinexp  47058  stoweidlem1  47104  stoweidlem11  47114  stoweidlem25  47128  stoweidlem26  47129  stoweidlem34  47137  stoweidlem37  47140  stoweidlem38  47141  stoweidlem42  47145  wallispi2lem1  47174  wallispi2  47176  stirlinglem4  47180  stirlinglem5  47181  stirlinglem10  47186  stirlinglem15  47191  dirkertrigeqlem3  47203  dirkertrigeq  47204  dirkercncflem2  47207  dirkercncflem4  47209  fourierdlem11  47221  fourierdlem15  47225  fourierdlem79  47288  fourierdlem83  47292  sqwvfourb  47332  etransclem14  47351  etransclem15  47352  etransclem20  47357  etransclem21  47358  etransclem22  47359  etransclem23  47360  etransclem24  47361  etransclem25  47362  etransclem28  47365  etransclem31  47368  etransclem32  47369  etransclem33  47370  etransclem34  47371  etransclem35  47372  etransclem38  47375  etransclem41  47378  etransclem44  47381  etransclem45  47382  etransclem47  47384  etransclem48  47385  nnfoctbdjlem  47558  deccarry  48474  iccpartgtprec  48595  fmtnoodd  48711  fmtnorec2lem  48720  fmtnorec2  48721  fmtnodvds  48722  goldbachthlem2  48724  fmtnorec3  48726  fmtnorec4  48727  fmtnoprmfac1lem  48742  fmtnoprmfac1  48743  fmtnoprmfac2lem1  48744  fmtnoprmfac2  48745  2pwp1prm  48767  sfprmdvdsmersenne  48781  lighneallem4b  48787  lighneal  48789  proththdlem  48791  proththd  48792  ppivalnnprm  48803  oexpnegALTV  48868  perfectALTVlem1  48912  perfectALTVlem2  48913  perfectALTV  48914  nnpw2pmod  49788  nnolog2flm1  49795  blennn0em1  49796  blengt1fldiv2p1  49798  nn0sumshdiglemB  49825  amgmlemALT  51156