Theorem nncnd 12277

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℂcc 11126  ℕcn 12261

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402  ax-un 7740  ax-1cn 11186  ax-addcl 11188

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7420  df-om 7867  df-2nd 7991  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-nn 12262

This theorem is used by:  nnadddir  12320  nnmul1com  12321  nnmulcom  12322  nneo  12709  facdiv  14355  facndiv  14356  faclbnd  14358  faclbnd5  14366  faclbnd6  14367  facubnd  14368  facavg  14369  bccmpl  14377  bcn0  14378  bcn1  14381  bcm1k  14383  bcp1n  14384  bcp1nk  14385  bcval5  14386  bcpasc  14389  permnn  14394  hashf1  14526  hashfac  14527  relexpaddnn  15128  binom11  15925  binom1dif  15926  climcndslem2  15943  arisum2  15954  trireciplem  15955  trirecip  15956  geo2sum  15966  geo2lim  15968  fprodfac  16066  risefacfac  16127  fallfacfwd  16128  fallfacval4  16135  bcfallfac  16136  fallfacfac  16137  bpolycl  16144  bpolysum  16145  bpolydiflem  16146  fsumkthpow  16148  eftcl  16165  eftabs  16167  efcllem  16169  ege2le3  16182  efcj  16184  efaddlem  16185  eftlub  16203  eirrlem  16298  sqrt2irrlem  16342  oexpneg  16441  pwp1fsum  16487  bitsp1  16527  bitsfzolem  16530  bitsfzo  16531  bitsmod  16532  bitscmp  16534  bitsinv1lem  16537  bitsinv1  16538  2ebits  16543  bitsinvp1  16545  sadcaddlem  16553  sadadd3  16557  bitsres  16569  bitsuz  16570  bitsshft  16571  dvdsgcdidd  16633  mulgcd  16644  rplpwr  16654  sqgcd  16658  expgcd  16659  nn0expgcd  16660  lcmgcdlem  16702  3lcm2e6woprm  16711  coprmprod  16757  coprmproddvdslem  16758  cncongr1  16763  cncongr2  16764  prmind2  16781  isprm5  16804  divgcdodd  16807  prmdvdsexpr  16814  qmuldeneqnum  16844  divnumden  16845  qnumgt0  16847  numdensq  16851  numdenexp  16857  hashdvds  16872  phiprmpw  16873  prmdiv  16882  prmdivdiv  16884  phisum  16888  modprm0  16903  pythagtriplem4  16917  pythagtriplem6  16919  pythagtriplem7  16920  pythagtriplem14  16926  pythagtriplem15  16927  pythagtriplem19  16931  pythagtrip  16932  pcprendvds2  16939  pcpre1  16940  pcpremul  16941  pceulem  16943  pcdiv  16950  pcqmul  16951  pcelnn  16968  pcid  16971  pc2dvds  16977  dvdsprmpweqnn  16983  dvdsprmpweqle  16984  pcaddlem  16986  pcadd  16987  pcfaclem  16996  qexpz  16999  expnprm  17000  oddprmdvds  17001  prmpwdvds  17002  pockthlem  17003  pockthg  17004  infpnlem1  17008  prmreclem1  17014  prmreclem2  17015  prmreclem3  17016  prmreclem4  17017  prmreclem6  17019  4sqlem6  17041  4sqlem7  17042  4sqlem10  17045  mul4sqlem  17051  4sqlem11  17053  4sqlem12  17054  4sqlem14  17056  4sqlem17  17059  4sqlem18  17060  vdwlem1  17079  vdwlem2  17080  vdwlem3  17081  vdwlem5  17083  vdwlem6  17084  vdwlem8  17086  vdwlem9  17087  vdwlem10  17088  vdwlem12  17090  ramub1lem2  17125  ramcl  17127  prmop1  17136  prmdvdsprmo  17140  prmgaplem7  17155  prmgaplem8  17156  chnub  18716  gsumsgrpccat  18955  mulgnndir  19232  mulgnnass  19238  psgnunilem5  19627  odf1o2  19706  pgp0  19729  sylow1lem1  19731  odcau  19737  sylow2blem3  19755  sylow3lem3  19762  sylow3lem4  19763  gexexlem  19985  ablfacrp2  20202  ablfac1lem  20203  ablfac1eu  20208  pgpfac1lem3a  20211  pgpfac1lem3  20212  fincygsubgodexd  20248  zringlpirlem3  21683  znrrg  21784  psdpw  22404  cpmadugsumlemF  23107  lebnumlem3  25197  ovollb2lem  25722  ovolunlem1a  25730  ovolunlem1  25731  uniioombllem3  25819  uniioombllem4  25820  dyaddisjlem  25829  mbfi1fseqlem3  25951  mbfi1fseqlem4  25952  itgpowd  26284  dgrcolem1  26506  vieta1lem1  26549  vieta1lem2  26550  elqaalem2  26559  elqaalem3  26560  aalioulem1  26575  aaliou3lem2  26586  aaliou3lem8  26588  aaliou3lem6  26591  aaliou3lem9  26593  taylfvallem1  26600  tayl0  26605  taylply2  26611  taylply  26612  dvtaylp  26613  taylthlem1  26616  taylthlem2  26617  pserdvlem2  26671  advlogexp  26900  cxpmul2  26934  cxpeq  27002  rtprmirr  27005  atantayl3  27184  leibpi  27187  log2cnv  27189  log2tlbnd  27190  birthdaylem2  27197  birthdaylem3  27198  amgmlem  27234  amgm  27235  emcllem5  27244  fsumharmonic  27256  zetacvg  27259  dmgmdivn0  27272  lgamgulmlem3  27275  lgamgulmlem4  27276  lgamgulmlem5  27277  lgamgulmlem6  27278  lgamgulm2  27280  lgamcvg2  27299  gamcvg  27300  gamcvg2lem  27303  facgam  27310  wilthlem1  27312  wilthlem2  27313  wilthlem3  27314  wilthimp  27316  basellem1  27325  basellem2  27326  basellem3  27327  basellem4  27328  basellem5  27329  basellem8  27332  vmaprm  27361  sgmval2  27387  0sgm  27388  sgmf  27389  vma1  27410  fsumdvdsdiaglem  27427  dvdsflf1o  27431  muinv  27437  mpodvdsmulf1o  27438  dvdsmulf1o  27440  sgmppw  27441  1sgmprm  27443  1sgm2ppw  27444  sgmmul  27445  chtublem  27455  fsumvma2  27458  chpchtsum  27463  logfaclbnd  27466  logexprlim  27469  mersenne  27471  perfect1  27472  perfectlem1  27473  perfectlem2  27474  perfect  27475  dchrsum2  27512  dchrhash  27515  bcmono  27521  bcp1ctr  27523  bclbnd  27524  bposlem1  27528  bposlem2  27529  bposlem3  27530  bposlem5  27532  bposlem6  27533  lgsval2lem  27551  lgsqrlem2  27591  gausslemma2dlem6  27616  gausslemma2dlem7  27617  gausslemma2d  27618  lgseisenlem1  27619  lgseisenlem4  27622  lgsquadlem1  27624  lgsquadlem2  27625  lgsquadlem3  27626  lgsquad2  27630  m1lgs  27632  2sqlem3  27664  2sqlem4  27665  chebbnd1lem1  27713  chebbnd1  27716  rplogsumlem1  27728  rplogsumlem2  27729  rpvmasumlem  27731  dchrisumlem1  27733  dchrmusum2  27738  dchrvmasumlem1  27739  dchrvmasum2lem  27740  dchrvmasum2if  27741  dchrvmasumlem2  27742  dchrvmasumlem3  27743  dchrvmasumiflem1  27745  dchrisum0flblem1  27752  dchrisum0flblem2  27753  dchrisum0fno1  27755  rpvmasum2  27756  rplogsum  27771  mulogsumlem  27775  mulogsum  27776  mulog2sumlem2  27779  vmalogdivsum2  27782  vmalogdivsum  27783  2vmadivsumlem  27784  logsqvma  27786  selberglem2  27790  selberglem3  27791  selberg  27792  selberg2lem  27794  logdivbnd  27800  selberg3lem1  27801  selberg4lem1  27804  pntrsumo1  27809  pntrsumbnd2  27811  selberg3r  27813  selberg4r  27814  selberg34r  27815  pntsval2  27820  pntrlog2bndlem2  27822  pntrlog2bndlem4  27824  pntrlog2bndlem6  27827  pntpbnd1  27830  pntpbnd2  27831  pntlemg  27842  pntlemn  27844  pntlemf  27849  pnt  27858  padicabvf  27875  ostth2lem2  27878  ostth3  27882  fusgrhashclwwlkn  30557  eucrct2eupth  30733  nrt2irr  30961  elq2  33290  numdenneg  33293  ltesubnnd  33301  2exple2exp  33312  oexpled  33314  gsummptp1  33505  1arithidomlem2  33954  1arithidom  33955  zringfrac  33972  cos9thpiminplylem1  34300  cos9thpiminplylem2  34301  1smat1  34322  madjusmdetlem2  34346  madjusmdetlem4  34348  qqhnm  34508  oddpwdc  34873  eulerpartlemsv2  34877  eulerpartlems  34879  eulerpartlemsv3  34880  eulerpartlemgc  34881  eulerpartlemv  34883  eulerpartlemgs2  34899  fibp1  34920  ballotlemfc0  35012  ballotlemfcc  35013  signsvtn0  35086  reprpmtf1o  35142  vtscl  35154  hgt750lemb  35172  tgoldbachgt  35179  subfacp1lem1  35766  subfacp1lem5  35771  subfacval2  35774  subfaclim  35775  cvmliftlem2  35873  cvmliftlem7  35878  cvmliftlem10  35881  cvmliftlem11  35882  cvmliftlem13  35883  bcm1nt  36324  bcprod  36325  iprodgam  36329  faclimlem1  36330  faclimlem2  36331  faclim2  36335  nn0prpwlem  36949  nn0prpw  36950  knoppcnlem10  37207  knoppndvlem16  37232  poimirlem1  38378  poimirlem2  38379  poimirlem6  38383  poimirlem7  38384  poimirlem8  38385  poimirlem9  38386  poimirlem10  38387  poimirlem11  38388  poimirlem12  38389  poimirlem13  38390  poimirlem15  38392  poimirlem16  38393  poimirlem17  38394  poimirlem18  38395  poimirlem19  38396  poimirlem20  38397  poimirlem21  38398  poimirlem22  38399  poimirlem23  38400  poimirlem24  38401  poimirlem25  38402  poimirlem26  38403  poimirlem27  38404  poimirlem31  38408  nnproddivdvdsd  42874  lcmfunnnd  42886  lcmineqlem3  42905  lcmineqlem4  42906  lcmineqlem6  42908  lcmineqlem8  42910  lcmineqlem10  42912  lcmineqlem11  42913  lcmineqlem12  42914  lcmineqlem16  42918  lcmineqlem18  42920  lcmineqlem23  42925  dvrelogpow2b  42942  aks4d1p1p2  42944  aks4d1p1  42950  aks4d1p8  42961  primrootsunit1  42971  primrootscoprmpow  42973  posbezout  42974  primrootscoprbij  42976  primrootspoweq0  42980  aks6d1c1p3  42984  aks6d1c1p8  42989  aks6d1c2p2  42993  hashscontpow1  42995  2np3bcnp1  43018  2ap1caineq  43019  sticksstones10  43029  sticksstones12a  43031  sticksstones16  43036  sticksstones22  43042  bcled  43052  bcle2d  43053  aks6d1c7lem1  43054  aks6d1c7  43058  unitscyglem2  43070  unitscyglem4  43072  unitscyglem5  43073  aks5lem8  43075  oddnumth  43194  nicomachus  43195  zaddcom  43360  fltabcoprmex  43493  fltaccoprm  43494  fltbccoprm  43495  fltne  43498  flt4lem3  43502  flt4lem5elem  43505  flt4lem5a  43506  flt4lem5b  43507  flt4lem5c  43508  flt4lem5d  43509  flt4lem5e  43510  flt4lem5f  43511  flt4lem6  43512  flt4lem7  43513  nna4b4nsq  43514  fltltc  43515  fltnltalem  43516  fltnlta  43517  irrapxlem4  43674  irrapxlem5  43675  pellexlem2  43679  pellexlem6  43683  pell1234qrne0  43702  pell1234qrreccl  43703  pell1234qrmulcl  43704  pell1234qrdich  43710  pell14qrdich  43718  pell1qrge1  43719  pell1qr1  43720  pell14qrgapw  43725  rmxyneg  43769  rmxm1  43783  rmxluc  43785  rmxdbl  43788  jm2.19lem1  43838  jm2.27c  43856  relexpmulnn  44557  relexpmulg  44558  inductionexd  45003  hashnzfzclim  45154  bcccl  45171  bcc0  45172  bccp1k  45173  bccm1k  45174  binomcxplemwb  45180  fsumnncl  46410  mccllem  46435  clim1fr1  46439  sumnnodd  46468  dvsinexp  46747  dvxpaek  46776  dvnxpaek  46778  dvnprodlem2  46783  itgsinexplem1  46790  itgsinexp  46791  stoweidlem1  46837  stoweidlem11  46847  stoweidlem25  46861  stoweidlem26  46862  stoweidlem34  46870  stoweidlem37  46873  stoweidlem38  46874  stoweidlem42  46878  wallispi2lem1  46907  wallispi2  46909  stirlinglem4  46913  stirlinglem5  46914  stirlinglem10  46919  stirlinglem15  46924  dirkertrigeqlem3  46936  dirkertrigeq  46937  dirkercncflem2  46940  dirkercncflem4  46942  fourierdlem11  46954  fourierdlem15  46958  fourierdlem79  47021  fourierdlem83  47025  sqwvfourb  47065  etransclem14  47084  etransclem15  47085  etransclem20  47090  etransclem21  47091  etransclem22  47092  etransclem23  47093  etransclem24  47094  etransclem25  47095  etransclem28  47098  etransclem31  47101  etransclem32  47102  etransclem33  47103  etransclem34  47104  etransclem35  47105  etransclem38  47108  etransclem41  47111  etransclem44  47114  etransclem45  47115  etransclem47  47117  etransclem48  47118  nnfoctbdjlem  47291  deccarry  48207  iccpartgtprec  48328  fmtnoodd  48444  fmtnorec2lem  48453  fmtnorec2  48454  fmtnodvds  48455  goldbachthlem2  48457  fmtnorec3  48459  fmtnorec4  48460  fmtnoprmfac1lem  48475  fmtnoprmfac1  48476  fmtnoprmfac2lem1  48477  fmtnoprmfac2  48478  2pwp1prm  48500  sfprmdvdsmersenne  48514  lighneallem4b  48520  lighneal  48522  proththdlem  48524  proththd  48525  ppivalnnprm  48536  oexpnegALTV  48601  perfectALTVlem1  48645  perfectALTVlem2  48646  perfectALTV  48647  nnpw2pmod  49521  nnolog2flm1  49528  blennn0em1  49529  blengt1fldiv2p1  49531  nn0sumshdiglemB  49558  amgmlemALT  50829