Theorem nncnd 9150

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℂcc 8023  ℕcn 9136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-sep 4205  ax-cnex 8116  ax-resscn 8117  ax-1re 8119  ax-addrcl 8122

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-v 2802  df-in 3204  df-ss 3211  df-int 3927  df-inn 9137

This theorem is referenced by:  peano5uzti  9581  qapne  9866  qtri3or  10493  exbtwnzlemstep  10500  intfracq  10575  flqdiv  10576  modqmulnn  10597  addmodid  10627  modaddmodup  10642  modsumfzodifsn  10651  addmodlteq  10653  facdiv  10993  facndiv  10994  faclbnd  10996  faclbnd6  10999  facubnd  11000  facavg  11001  bccmpl  11009  bcn0  11010  bcn1  11013  bcm1k  11015  bcp1n  11016  bcp1nk  11017  bcval5  11018  bcpasc  11021  permnn  11026  cvg1nlemcxze  11536  cvg1nlemcau  11538  resqrexlemcalc3  11570  binom11  12040  binom1dif  12041  divcnv  12051  arisum2  12053  trireciplem  12054  trirecip  12055  expcnvap0  12056  geo2sum  12068  geo2lim  12070  cvgratnnlembern  12077  cvgratnnlemnexp  12078  cvgratnnlemmn  12079  cvgratnnlemsumlt  12082  cvgratnnlemfm  12083  cvgratnnlemrate  12084  cvgratz  12086  eftcl  12208  eftabs  12210  efcllemp  12212  ege2le3  12225  efcj  12227  efaddlem  12228  eftlub  12244  eirraplem  12331  oexpneg  12431  divalglemnn  12472  bitsp1  12505  bitsfzolem  12508  bitsfzo  12509  bitsmod  12510  bitscmp  12512  bitsinv1lem  12515  bitsinv1  12516  dvdsgcdidd  12558  bezoutlemnewy  12560  mulgcd  12580  rplpwr  12591  sqgcd  12593  lcmgcdlem  12642  3lcm2e6woprm  12651  cncongr1  12668  cncongr2  12669  prmind2  12685  isprm5  12707  divgcdodd  12708  prmdvdsexpr  12715  sqrt2irrlem  12726  oddpwdclemxy  12734  oddpwdclemodd  12737  oddpwdclemdc  12738  oddpwdc  12739  sqpweven  12740  2sqpwodd  12741  sqrt2irraplemnn  12744  sqrt2irrap  12745  qmuldeneqnum  12760  divnumden  12761  qnumgt0  12763  numdensq  12767  hashdvds  12786  phiprmpw  12787  prmdiv  12800  prmdivdiv  12802  phisum  12806  modprm0  12820  pythagtriplem4  12834  pythagtriplem6  12836  pythagtriplem7  12837  pythagtriplem14  12843  pythagtriplem15  12844  pythagtriplem16  12845  pythagtriplem19  12848  pythagtrip  12849  pcprendvds2  12857  pcpre1  12858  pcpremul  12859  pceulem  12860  pcdiv  12868  pcqmul  12869  pcelnn  12887  pcid  12890  pc2dvds  12896  dvdsprmpweqnn  12902  dvdsprmpweqle  12903  pcaddlem  12905  pcadd  12906  pcfaclem  12915  qexpz  12918  expnprm  12919  oddprmdvds  12920  prmpwdvds  12921  pockthlem  12922  pockthg  12923  infpnlem1  12925  4sqlem6  12949  4sqlem7  12950  4sqlem10  12953  mul4sqlem  12959  4sqlem11  12967  4sqlem12  12968  4sqlem14  12970  4sqlem17  12973  4sqlem18  12974  oddennn  13006  evenennn  13007  mulgnndir  13731  mulgnnass  13737  znrrg  14667  logbgcd1irraplemap  15686  wilthlem1  15697  0sgm  15702  mpodvdsmulf1o  15707  1sgmprm  15711  1sgm2ppw  15712  mersenne  15714  perfect1  15715  perfectlem1  15716  perfectlem2  15717  perfect  15718  lgsval2lem  15732  gausslemma2dlem6  15789  gausslemma2dlem7  15790  gausslemma2d  15791  lgseisenlem1  15792  lgseisenlem4  15795  lgsquadlem1  15799  lgsquadlem2  15800  lgsquadlem3  15801  lgsquad2  15805  m1lgs  15807  2sqlem3  15839  2sqlem4  15840  trilpolemeq1  16594  trilpolemlt1  16595  redcwlpolemeq1  16608  nconstwlpolemgt0  16618