Theorem nncnd 12253

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2143  ℂcc 11102  ℕcn 12237

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404  ax-un 7732  ax-1cn 11162  ax-addcl 11164

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7413  df-om 7859  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-nn 12238

This theorem is used by:  nnadddir  12296  nnmul1com  12297  nnmulcom  12298  nneo  12684  facdiv  14328  facndiv  14329  faclbnd  14331  faclbnd5  14339  faclbnd6  14340  facubnd  14341  facavg  14342  bccmpl  14350  bcn0  14351  bcn1  14354  bcm1k  14356  bcp1n  14357  bcp1nk  14358  bcval5  14359  bcpasc  14362  permnn  14367  hashf1  14499  hashfac  14500  relexpaddnn  15093  binom11  15891  binom1dif  15892  climcndslem2  15909  arisum2  15920  trireciplem  15921  trirecip  15922  geo2sum  15932  geo2lim  15934  fprodfac  16032  risefacfac  16093  fallfacfwd  16094  fallfacval4  16101  bcfallfac  16102  fallfacfac  16103  bpolycl  16110  bpolysum  16111  bpolydiflem  16112  fsumkthpow  16114  eftcl  16131  eftabs  16133  efcllem  16135  ege2le3  16148  efcj  16150  efaddlem  16151  eftlub  16169  eirrlem  16264  sqrt2irrlem  16308  oexpneg  16407  pwp1fsum  16453  bitsp1  16493  bitsfzolem  16496  bitsfzo  16497  bitsmod  16498  bitscmp  16500  bitsinv1lem  16503  bitsinv1  16504  2ebits  16509  bitsinvp1  16511  sadcaddlem  16519  sadadd3  16523  bitsres  16535  bitsuz  16536  bitsshft  16537  dvdsgcdidd  16599  mulgcd  16610  rplpwr  16620  sqgcd  16624  expgcd  16625  nn0expgcd  16626  lcmgcdlem  16668  3lcm2e6woprm  16677  coprmprod  16723  coprmproddvdslem  16724  cncongr1  16729  cncongr2  16730  prmind2  16747  isprm5  16770  divgcdodd  16773  prmdvdsexpr  16780  qmuldeneqnum  16810  divnumden  16811  qnumgt0  16813  numdensq  16817  numdenexp  16823  hashdvds  16838  phiprmpw  16839  prmdiv  16848  prmdivdiv  16850  phisum  16854  modprm0  16869  pythagtriplem4  16883  pythagtriplem6  16885  pythagtriplem7  16886  pythagtriplem14  16892  pythagtriplem15  16893  pythagtriplem19  16897  pythagtrip  16898  pcprendvds2  16905  pcpre1  16906  pcpremul  16907  pceulem  16909  pcdiv  16916  pcqmul  16917  pcelnn  16934  pcid  16937  pc2dvds  16943  dvdsprmpweqnn  16949  dvdsprmpweqle  16950  pcaddlem  16952  pcadd  16953  pcfaclem  16962  qexpz  16965  expnprm  16966  oddprmdvds  16967  prmpwdvds  16968  pockthlem  16969  pockthg  16970  infpnlem1  16974  prmreclem1  16980  prmreclem2  16981  prmreclem3  16982  prmreclem4  16983  prmreclem6  16985  4sqlem6  17007  4sqlem7  17008  4sqlem10  17011  mul4sqlem  17017  4sqlem11  17019  4sqlem12  17020  4sqlem14  17022  4sqlem17  17025  4sqlem18  17026  vdwlem1  17045  vdwlem2  17046  vdwlem3  17047  vdwlem5  17049  vdwlem6  17050  vdwlem8  17052  vdwlem9  17053  vdwlem10  17054  vdwlem12  17056  ramub1lem2  17091  ramcl  17093  prmop1  17102  prmdvdsprmo  17106  prmgaplem7  17121  prmgaplem8  17122  chnub  18682  gsumsgrpccat  18903  mulgnndir  19173  mulgnnass  19179  psgnunilem5  19568  odf1o2  19647  pgp0  19670  sylow1lem1  19672  odcau  19678  sylow2blem3  19696  sylow3lem3  19703  sylow3lem4  19704  gexexlem  19926  ablfacrp2  20143  ablfac1lem  20144  ablfac1eu  20149  pgpfac1lem3a  20152  pgpfac1lem3  20153  fincygsubgodexd  20189  zringlpirlem3  21623  znrrg  21724  psdpw  22342  cpmadugsumlemF  23042  lebnumlem3  25131  ovollb2lem  25656  ovolunlem1a  25664  ovolunlem1  25665  uniioombllem3  25753  uniioombllem4  25754  dyaddisjlem  25763  mbfi1fseqlem3  25885  mbfi1fseqlem4  25886  itgpowd  26218  dgrcolem1  26439  vieta1lem1  26480  vieta1lem2  26481  elqaalem2  26490  elqaalem3  26491  aalioulem1  26504  aaliou3lem2  26515  aaliou3lem8  26517  aaliou3lem6  26520  aaliou3lem9  26522  taylfvallem1  26529  tayl0  26534  taylply2  26540  taylply  26541  dvtaylp  26542  taylthlem1  26545  taylthlem2  26546  pserdvlem2  26600  advlogexp  26829  cxpmul2  26863  cxpeq  26931  rtprmirr  26934  atantayl3  27113  leibpi  27116  log2cnv  27118  log2tlbnd  27119  birthdaylem2  27126  birthdaylem3  27127  amgmlem  27163  amgm  27164  emcllem5  27173  fsumharmonic  27185  zetacvg  27188  dmgmdivn0  27201  lgamgulmlem3  27204  lgamgulmlem4  27205  lgamgulmlem5  27206  lgamgulmlem6  27207  lgamgulm2  27209  lgamcvg2  27228  gamcvg  27229  gamcvg2lem  27232  facgam  27239  wilthlem1  27241  wilthlem2  27242  wilthlem3  27243  wilthimp  27245  basellem1  27254  basellem2  27255  basellem3  27256  basellem4  27257  basellem5  27258  basellem8  27261  vmaprm  27290  sgmval2  27316  0sgm  27317  sgmf  27318  vma1  27339  fsumdvdsdiaglem  27356  dvdsflf1o  27360  muinv  27366  mpodvdsmulf1o  27367  dvdsmulf1o  27369  sgmppw  27370  1sgmprm  27372  1sgm2ppw  27373  sgmmul  27374  chtublem  27384  fsumvma2  27387  chpchtsum  27392  logfaclbnd  27395  logexprlim  27398  mersenne  27400  perfect1  27401  perfectlem1  27402  perfectlem2  27403  perfect  27404  dchrsum2  27441  dchrhash  27444  bcmono  27450  bcp1ctr  27452  bclbnd  27453  bposlem1  27457  bposlem2  27458  bposlem3  27459  bposlem5  27461  bposlem6  27462  lgsval2lem  27480  lgsqrlem2  27520  gausslemma2dlem6  27545  gausslemma2dlem7  27546  gausslemma2d  27547  lgseisenlem1  27548  lgseisenlem4  27551  lgsquadlem1  27553  lgsquadlem2  27554  lgsquadlem3  27555  lgsquad2  27559  m1lgs  27561  2sqlem3  27593  2sqlem4  27594  chebbnd1lem1  27642  chebbnd1  27645  rplogsumlem1  27657  rplogsumlem2  27658  rpvmasumlem  27660  dchrisumlem1  27662  dchrmusum2  27667  dchrvmasumlem1  27668  dchrvmasum2lem  27669  dchrvmasum2if  27670  dchrvmasumlem2  27671  dchrvmasumlem3  27672  dchrvmasumiflem1  27674  dchrisum0flblem1  27681  dchrisum0flblem2  27682  dchrisum0fno1  27684  rpvmasum2  27685  rplogsum  27700  mulogsumlem  27704  mulogsum  27705  mulog2sumlem2  27708  vmalogdivsum2  27711  vmalogdivsum  27712  2vmadivsumlem  27713  logsqvma  27715  selberglem2  27719  selberglem3  27720  selberg  27721  selberg2lem  27723  logdivbnd  27729  selberg3lem1  27730  selberg4lem1  27733  pntrsumo1  27738  pntrsumbnd2  27740  selberg3r  27742  selberg4r  27743  selberg34r  27744  pntsval2  27749  pntrlog2bndlem2  27751  pntrlog2bndlem4  27753  pntrlog2bndlem6  27756  pntpbnd1  27759  pntpbnd2  27760  pntlemg  27771  pntlemn  27773  pntlemf  27778  pnt  27787  padicabvf  27804  ostth2lem2  27807  ostth3  27811  fusgrhashclwwlkn  30439  eucrct2eupth  30605  nrt2irr  30833  elq2  33165  numdenneg  33168  ltesubnnd  33176  2exple2exp  33187  oexpled  33189  gsummptp1  33386  1arithidomlem2  33835  1arithidom  33836  zringfrac  33853  cos9thpiminplylem1  34181  cos9thpiminplylem2  34182  1smat1  34203  madjusmdetlem2  34227  madjusmdetlem4  34229  qqhnm  34389  oddpwdc  34753  eulerpartlemsv2  34757  eulerpartlems  34759  eulerpartlemsv3  34760  eulerpartlemgc  34761  eulerpartlemv  34763  eulerpartlemgs2  34779  fibp1  34800  ballotlemfc0  34892  ballotlemfcc  34893  signsvtn0  34966  reprpmtf1o  35022  vtscl  35034  hgt750lemb  35052  tgoldbachgt  35059  subfacp1lem1  35679  subfacp1lem5  35684  subfacval2  35687  subfaclim  35688  cvmliftlem2  35786  cvmliftlem7  35791  cvmliftlem10  35794  cvmliftlem11  35795  cvmliftlem13  35796  bcm1nt  36237  bcprod  36238  iprodgam  36242  faclimlem1  36243  faclimlem2  36244  faclim2  36248  nn0prpwlem  36861  nn0prpw  36862  knoppcnlem10  37119  knoppndvlem16  37144  poimirlem1  38300  poimirlem2  38301  poimirlem6  38305  poimirlem7  38306  poimirlem8  38307  poimirlem9  38308  poimirlem10  38309  poimirlem11  38310  poimirlem12  38311  poimirlem13  38312  poimirlem15  38314  poimirlem16  38315  poimirlem17  38316  poimirlem18  38317  poimirlem19  38318  poimirlem20  38319  poimirlem21  38320  poimirlem22  38321  poimirlem23  38322  poimirlem24  38323  poimirlem25  38324  poimirlem26  38325  poimirlem27  38326  poimirlem31  38330  nnproddivdvdsd  42795  lcmfunnnd  42807  lcmineqlem3  42826  lcmineqlem4  42827  lcmineqlem6  42829  lcmineqlem8  42831  lcmineqlem10  42833  lcmineqlem11  42834  lcmineqlem12  42835  lcmineqlem16  42839  lcmineqlem18  42841  lcmineqlem23  42846  dvrelogpow2b  42863  aks4d1p1p2  42865  aks4d1p1  42871  aks4d1p8  42882  primrootsunit1  42892  primrootscoprmpow  42894  posbezout  42895  primrootscoprbij  42897  primrootspoweq0  42901  aks6d1c1p3  42905  aks6d1c1p8  42910  aks6d1c2p2  42914  hashscontpow1  42916  2np3bcnp1  42939  2ap1caineq  42940  sticksstones10  42950  sticksstones12a  42952  sticksstones16  42957  sticksstones22  42963  bcled  42973  bcle2d  42974  aks6d1c7lem1  42975  aks6d1c7  42979  unitscyglem2  42991  unitscyglem4  42993  unitscyglem5  42994  aks5lem8  42996  oddnumth  43100  nicomachus  43101  zaddcom  43266  fltabcoprmex  43399  fltaccoprm  43400  fltbccoprm  43401  fltne  43404  flt4lem3  43408  flt4lem5elem  43411  flt4lem5a  43412  flt4lem5b  43413  flt4lem5c  43414  flt4lem5d  43415  flt4lem5e  43416  flt4lem5f  43417  flt4lem6  43418  flt4lem7  43419  nna4b4nsq  43420  fltltc  43421  fltnltalem  43422  fltnlta  43423  irrapxlem4  43580  irrapxlem5  43581  pellexlem2  43585  pellexlem6  43589  pell1234qrne0  43608  pell1234qrreccl  43609  pell1234qrmulcl  43610  pell1234qrdich  43616  pell14qrdich  43624  pell1qrge1  43625  pell1qr1  43626  pell14qrgapw  43631  rmxyneg  43675  rmxm1  43689  rmxluc  43691  rmxdbl  43694  jm2.19lem1  43744  jm2.27c  43762  relexpmulnn  44463  relexpmulg  44464  inductionexd  44909  hashnzfzclim  45060  bcccl  45077  bcc0  45078  bccp1k  45079  bccm1k  45080  binomcxplemwb  45086  fsumnncl  46316  mccllem  46341  clim1fr1  46345  sumnnodd  46374  dvsinexp  46653  dvxpaek  46682  dvnxpaek  46684  dvnprodlem2  46689  itgsinexplem1  46696  itgsinexp  46697  stoweidlem1  46743  stoweidlem11  46753  stoweidlem25  46767  stoweidlem26  46768  stoweidlem34  46776  stoweidlem37  46779  stoweidlem38  46780  stoweidlem42  46784  wallispi2lem1  46813  wallispi2  46815  stirlinglem4  46819  stirlinglem5  46820  stirlinglem10  46825  stirlinglem15  46830  dirkertrigeqlem3  46842  dirkertrigeq  46843  dirkercncflem2  46846  dirkercncflem4  46848  fourierdlem11  46860  fourierdlem15  46864  fourierdlem79  46927  fourierdlem83  46931  sqwvfourb  46971  etransclem14  46990  etransclem15  46991  etransclem20  46996  etransclem21  46997  etransclem22  46998  etransclem23  46999  etransclem24  47000  etransclem25  47001  etransclem28  47004  etransclem31  47007  etransclem32  47008  etransclem33  47009  etransclem34  47010  etransclem35  47011  etransclem38  47014  etransclem41  47017  etransclem44  47020  etransclem45  47021  etransclem47  47023  etransclem48  47024  nnfoctbdjlem  47197  deccarry  48076  iccpartgtprec  48197  fmtnoodd  48313  fmtnorec2lem  48322  fmtnorec2  48323  fmtnodvds  48324  goldbachthlem2  48326  fmtnorec3  48328  fmtnorec4  48329  fmtnoprmfac1lem  48344  fmtnoprmfac1  48345  fmtnoprmfac2lem1  48346  fmtnoprmfac2  48347  2pwp1prm  48369  sfprmdvdsmersenne  48383  lighneallem4b  48389  lighneal  48391  proththdlem  48393  proththd  48394  ppivalnnprm  48405  oexpnegALTV  48470  perfectALTVlem1  48514  perfectALTVlem2  48515  perfectALTV  48516  nnpw2pmod  49391  nnolog2flm1  49398  blennn0em1  49399  blengt1fldiv2p1  49401  nn0sumshdiglemB  49428  amgmlemALT  50678