Theorem nncnd 12254

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℂcc 11125  ℕcn 12238

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402  ax-un 7727  ax-1cn 11185  ax-addcl 11187

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-ov 7406  df-om 7860  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-rdg 8422  df-nn 12239

This theorem is referenced by:  nneo  12675  facdiv  14303  facndiv  14304  faclbnd  14306  faclbnd5  14314  faclbnd6  14315  facubnd  14316  facavg  14317  bccmpl  14325  bcn0  14326  bcn1  14329  bcm1k  14331  bcp1n  14332  bcp1nk  14333  bcval5  14334  bcpasc  14337  permnn  14342  hashf1  14473  hashfac  14474  relexpaddnn  15068  binom11  15846  binom1dif  15847  climcndslem2  15864  arisum2  15875  trireciplem  15876  trirecip  15877  geo2sum  15887  geo2lim  15889  fprodfac  15987  risefacfac  16049  fallfacfwd  16050  fallfacval4  16057  bcfallfac  16058  fallfacfac  16059  bpolycl  16066  bpolysum  16067  bpolydiflem  16068  fsumkthpow  16070  eftcl  16087  eftabs  16089  efcllem  16091  ege2le3  16104  efcj  16106  efaddlem  16107  eftlub  16125  eirrlem  16220  sqrt2irrlem  16264  oexpneg  16362  pwp1fsum  16408  bitsp1  16448  bitsfzolem  16451  bitsfzo  16452  bitsmod  16453  bitscmp  16455  bitsinv1lem  16458  bitsinv1  16459  2ebits  16464  bitsinvp1  16466  sadcaddlem  16474  sadadd3  16478  bitsres  16490  bitsuz  16491  bitsshft  16492  dvdsgcdidd  16554  mulgcd  16565  rplpwr  16575  sqgcd  16579  expgcd  16580  nn0expgcd  16581  lcmgcdlem  16623  3lcm2e6woprm  16632  coprmprod  16678  coprmproddvdslem  16679  cncongr1  16684  cncongr2  16685  prmind2  16702  isprm5  16724  divgcdodd  16727  prmdvdsexpr  16734  qmuldeneqnum  16764  divnumden  16765  qnumgt0  16767  numdensq  16771  numdenexp  16777  hashdvds  16792  phiprmpw  16793  prmdiv  16802  prmdivdiv  16804  phisum  16808  modprm0  16823  pythagtriplem4  16837  pythagtriplem6  16839  pythagtriplem7  16840  pythagtriplem14  16846  pythagtriplem15  16847  pythagtriplem19  16851  pythagtrip  16852  pcprendvds2  16859  pcpre1  16860  pcpremul  16861  pceulem  16863  pcdiv  16870  pcqmul  16871  pcelnn  16888  pcid  16891  pc2dvds  16897  dvdsprmpweqnn  16903  dvdsprmpweqle  16904  pcaddlem  16906  pcadd  16907  pcfaclem  16916  qexpz  16919  expnprm  16920  oddprmdvds  16921  prmpwdvds  16922  pockthlem  16923  pockthg  16924  infpnlem1  16928  prmreclem1  16934  prmreclem2  16935  prmreclem3  16936  prmreclem4  16937  prmreclem6  16939  4sqlem6  16961  4sqlem7  16962  4sqlem10  16965  mul4sqlem  16971  4sqlem11  16973  4sqlem12  16974  4sqlem14  16976  4sqlem17  16979  4sqlem18  16980  vdwlem1  16999  vdwlem2  17000  vdwlem3  17001  vdwlem5  17003  vdwlem6  17004  vdwlem8  17006  vdwlem9  17007  vdwlem10  17008  vdwlem12  17010  ramub1lem2  17045  ramcl  17047  prmop1  17056  prmdvdsprmo  17060  prmgaplem7  17075  prmgaplem8  17076  gsumsgrpccat  18816  mulgnndir  19084  mulgnnass  19090  psgnunilem5  19473  odf1o2  19552  pgp0  19575  sylow1lem1  19577  odcau  19583  sylow2blem3  19601  sylow3lem3  19608  sylow3lem4  19609  gexexlem  19831  ablfacrp2  20048  ablfac1lem  20049  ablfac1eu  20054  pgpfac1lem3a  20057  pgpfac1lem3  20058  fincygsubgodexd  20094  zringlpirlem3  21423  znrrg  21524  psdpw  22106  cpmadugsumlemF  22812  lebnumlem3  24911  ovollb2lem  25439  ovolunlem1a  25447  ovolunlem1  25448  uniioombllem3  25536  uniioombllem4  25537  dyaddisjlem  25546  mbfi1fseqlem3  25668  mbfi1fseqlem4  25669  itgpowd  26007  dgrcolem1  26229  vieta1lem1  26268  vieta1lem2  26269  elqaalem2  26278  elqaalem3  26279  aalioulem1  26290  aaliou3lem2  26301  aaliou3lem8  26303  aaliou3lem6  26306  aaliou3lem9  26308  taylfvallem1  26314  tayl0  26319  taylply2  26325  taylply2OLD  26326  taylply  26327  dvtaylp  26328  taylthlem1  26331  taylthlem2  26332  taylthlem2OLD  26333  pserdvlem2  26388  advlogexp  26614  cxpmul2  26648  cxpeq  26717  rtprmirr  26720  atantayl3  26899  leibpi  26902  log2cnv  26904  log2tlbnd  26905  birthdaylem2  26912  birthdaylem3  26913  amgmlem  26950  amgm  26951  emcllem5  26960  fsumharmonic  26972  zetacvg  26975  dmgmdivn0  26988  lgamgulmlem3  26991  lgamgulmlem4  26992  lgamgulmlem5  26993  lgamgulmlem6  26994  lgamgulm2  26996  lgamcvg2  27015  gamcvg  27016  gamcvg2lem  27019  facgam  27026  wilthlem1  27028  wilthlem2  27029  wilthlem3  27030  wilthimp  27032  basellem1  27041  basellem2  27042  basellem3  27043  basellem4  27044  basellem5  27045  basellem8  27048  vmaprm  27077  sgmval2  27103  0sgm  27104  sgmf  27105  vma1  27126  fsumdvdsdiaglem  27143  dvdsflf1o  27147  muinv  27153  mpodvdsmulf1o  27154  dvdsmulf1o  27156  sgmppw  27158  1sgmprm  27160  1sgm2ppw  27161  sgmmul  27162  chtublem  27172  fsumvma2  27175  chpchtsum  27180  logfaclbnd  27183  logexprlim  27186  mersenne  27188  perfect1  27189  perfectlem1  27190  perfectlem2  27191  perfect  27192  dchrsum2  27229  dchrhash  27232  bcmono  27238  bcp1ctr  27240  bclbnd  27241  bposlem1  27245  bposlem2  27246  bposlem3  27247  bposlem5  27249  bposlem6  27250  lgsval2lem  27268  lgsqrlem2  27308  gausslemma2dlem6  27333  gausslemma2dlem7  27334  gausslemma2d  27335  lgseisenlem1  27336  lgseisenlem4  27339  lgsquadlem1  27341  lgsquadlem2  27342  lgsquadlem3  27343  lgsquad2  27347  m1lgs  27349  2sqlem3  27381  2sqlem4  27382  chebbnd1lem1  27430  chebbnd1  27433  rplogsumlem1  27445  rplogsumlem2  27446  rpvmasumlem  27448  dchrisumlem1  27450  dchrmusum2  27455  dchrvmasumlem1  27456  dchrvmasum2lem  27457  dchrvmasum2if  27458  dchrvmasumlem2  27459  dchrvmasumlem3  27460  dchrvmasumiflem1  27462  dchrisum0flblem1  27469  dchrisum0flblem2  27470  dchrisum0fno1  27472  rpvmasum2  27473  rplogsum  27488  mulogsumlem  27492  mulogsum  27493  mulog2sumlem2  27496  vmalogdivsum2  27499  vmalogdivsum  27500  2vmadivsumlem  27501  logsqvma  27503  selberglem2  27507  selberglem3  27508  selberg  27509  selberg2lem  27511  logdivbnd  27517  selberg3lem1  27518  selberg4lem1  27521  pntrsumo1  27526  pntrsumbnd2  27528  selberg3r  27530  selberg4r  27531  selberg34r  27532  pntsval2  27537  pntrlog2bndlem2  27539  pntrlog2bndlem4  27541  pntrlog2bndlem6  27544  pntpbnd1  27547  pntpbnd2  27548  pntlemg  27559  pntlemn  27561  pntlemf  27566  pnt  27575  padicabvf  27592  ostth2lem2  27595  ostth3  27599  fusgrhashclwwlkn  30006  eucrct2eupth  30172  nrt2irr  30400  elq2  32736  numdenneg  32739  ltesubnnd  32747  2exple2exp  32770  oexpled  32772  chnub  32938  1arithidomlem2  33497  1arithidom  33498  zringfrac  33515  cos9thpiminplylem1  33762  cos9thpiminplylem2  33763  1smat1  33781  madjusmdetlem2  33805  madjusmdetlem4  33807  qqhnm  33967  oddpwdc  34332  eulerpartlemsv2  34336  eulerpartlems  34338  eulerpartlemsv3  34339  eulerpartlemgc  34340  eulerpartlemv  34342  eulerpartlemgs2  34358  fibp1  34379  ballotlemfc0  34471  ballotlemfcc  34472  signsvtn0  34548  reprpmtf1o  34604  vtscl  34616  hgt750lemb  34634  tgoldbachgt  34641  subfacp1lem1  35147  subfacp1lem5  35152  subfacval2  35155  subfaclim  35156  cvmliftlem2  35254  cvmliftlem7  35259  cvmliftlem10  35262  cvmliftlem11  35263  cvmliftlem13  35264  bcm1nt  35700  bcprod  35701  iprodgam  35705  faclimlem1  35706  faclimlem2  35707  faclim2  35711  nn0prpwlem  36286  nn0prpw  36287  knoppcnlem10  36466  knoppndvlem16  36491  poimirlem1  37591  poimirlem2  37592  poimirlem6  37596  poimirlem7  37597  poimirlem8  37598  poimirlem9  37599  poimirlem10  37600  poimirlem11  37601  poimirlem12  37602  poimirlem13  37603  poimirlem15  37605  poimirlem16  37606  poimirlem17  37607  poimirlem18  37608  poimirlem19  37609  poimirlem20  37610  poimirlem21  37611  poimirlem22  37612  poimirlem23  37613  poimirlem24  37614  poimirlem25  37615  poimirlem26  37616  poimirlem27  37617  poimirlem31  37621  nnproddivdvdsd  41959  lcmfunnnd  41971  lcmineqlem3  41990  lcmineqlem4  41991  lcmineqlem6  41993  lcmineqlem8  41995  lcmineqlem10  41997  lcmineqlem11  41998  lcmineqlem12  41999  lcmineqlem16  42003  lcmineqlem18  42005  lcmineqlem23  42010  dvrelogpow2b  42027  aks4d1p1p2  42029  aks4d1p1  42035  aks4d1p8  42046  primrootsunit1  42056  primrootscoprmpow  42058  posbezout  42059  primrootscoprbij  42061  primrootspoweq0  42065  aks6d1c1p3  42069  aks6d1c1p8  42074  aks6d1c2p2  42078  hashscontpow1  42080  2np3bcnp1  42103  2ap1caineq  42104  sticksstones10  42114  sticksstones12a  42116  sticksstones16  42121  sticksstones22  42127  bcled  42137  bcle2d  42138  aks6d1c7lem1  42139  aks6d1c7  42143  unitscyglem2  42155  unitscyglem4  42157  unitscyglem5  42158  aks5lem8  42160  metakunt8  42171  metakunt15  42178  metakunt16  42179  metakunt20  42183  metakunt28  42191  metakunt30  42193  nnadddir  42267  nnmul1com  42268  nnmulcom  42269  oddnumth  42307  nicomachus  42308  zaddcom  42442  fltabcoprmex  42609  fltaccoprm  42610  fltbccoprm  42611  fltne  42614  flt4lem3  42618  flt4lem5elem  42621  flt4lem5a  42622  flt4lem5b  42623  flt4lem5c  42624  flt4lem5d  42625  flt4lem5e  42626  flt4lem5f  42627  flt4lem6  42628  flt4lem7  42629  nna4b4nsq  42630  fltltc  42631  fltnltalem  42632  fltnlta  42633  irrapxlem4  42795  irrapxlem5  42796  pellexlem2  42800  pellexlem6  42804  pell1234qrne0  42823  pell1234qrreccl  42824  pell1234qrmulcl  42825  pell1234qrdich  42831  pell14qrdich  42839  pell1qrge1  42840  pell1qr1  42841  pell14qrgapw  42846  rmxyneg  42891  rmxm1  42905  rmxluc  42907  rmxdbl  42910  jm2.19lem1  42960  jm2.27c  42978  relexpmulnn  43680  relexpmulg  43681  inductionexd  44126  hashnzfzclim  44294  bcccl  44311  bcc0  44312  bccp1k  44313  bccm1k  44314  binomcxplemwb  44320  fsumnncl  45549  mccllem  45574  clim1fr1  45578  sumnnodd  45607  dvsinexp  45888  dvxpaek  45917  dvnxpaek  45919  dvnprodlem2  45924  itgsinexplem1  45931  itgsinexp  45932  stoweidlem1  45978  stoweidlem11  45988  stoweidlem25  46002  stoweidlem26  46003  stoweidlem34  46011  stoweidlem37  46014  stoweidlem38  46015  stoweidlem42  46019  wallispi2lem1  46048  wallispi2  46050  stirlinglem4  46054  stirlinglem5  46055  stirlinglem10  46060  stirlinglem15  46065  dirkertrigeqlem3  46077  dirkertrigeq  46078  dirkercncflem2  46081  dirkercncflem4  46083  fourierdlem11  46095  fourierdlem15  46099  fourierdlem79  46162  fourierdlem83  46166  sqwvfourb  46206  etransclem14  46225  etransclem15  46226  etransclem20  46231  etransclem21  46232  etransclem22  46233  etransclem23  46234  etransclem24  46235  etransclem25  46236  etransclem28  46239  etransclem31  46242  etransclem32  46243  etransclem33  46244  etransclem34  46245  etransclem35  46246  etransclem38  46249  etransclem41  46252  etransclem44  46255  etransclem45  46256  etransclem47  46258  etransclem48  46259  nnfoctbdjlem  46432  deccarry  47288  iccpartgtprec  47382  fmtnoodd  47495  fmtnorec2lem  47504  fmtnorec2  47505  fmtnodvds  47506  goldbachthlem2  47508  fmtnorec3  47510  fmtnorec4  47511  fmtnoprmfac1lem  47526  fmtnoprmfac1  47527  fmtnoprmfac2lem1  47528  fmtnoprmfac2  47529  2pwp1prm  47551  sfprmdvdsmersenne  47565  lighneallem4b  47571  lighneal  47573  proththdlem  47575  proththd  47576  oexpnegALTV  47639  perfectALTVlem1  47683  perfectALTVlem2  47684  perfectALTV  47685  nnpw2pmod  48511  nnolog2flm1  48518  blennn0em1  48519  blengt1fldiv2p1  48521  nn0sumshdiglemB  48548  amgmlemALT  49615