Theorem nncnd 9132

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℂcc 8005  ℕcn 9118

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 4202  ax-cnex 8098  ax-resscn 8099  ax-1re 8101  ax-addrcl 8104

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 2801  df-in 3203  df-ss 3210  df-int 3924  df-inn 9119

This theorem is referenced by:  peano5uzti  9563  qapne  9842  qtri3or  10468  exbtwnzlemstep  10475  intfracq  10550  flqdiv  10551  modqmulnn  10572  addmodid  10602  modaddmodup  10617  modsumfzodifsn  10626  addmodlteq  10628  facdiv  10968  facndiv  10969  faclbnd  10971  faclbnd6  10974  facubnd  10975  facavg  10976  bccmpl  10984  bcn0  10985  bcn1  10988  bcm1k  10990  bcp1n  10991  bcp1nk  10992  bcval5  10993  bcpasc  10996  permnn  11001  cvg1nlemcxze  11501  cvg1nlemcau  11503  resqrexlemcalc3  11535  binom11  12005  binom1dif  12006  divcnv  12016  arisum2  12018  trireciplem  12019  trirecip  12020  expcnvap0  12021  geo2sum  12033  geo2lim  12035  cvgratnnlembern  12042  cvgratnnlemnexp  12043  cvgratnnlemmn  12044  cvgratnnlemsumlt  12047  cvgratnnlemfm  12048  cvgratnnlemrate  12049  cvgratz  12051  eftcl  12173  eftabs  12175  efcllemp  12177  ege2le3  12190  efcj  12192  efaddlem  12193  eftlub  12209  eirraplem  12296  oexpneg  12396  divalglemnn  12437  bitsp1  12470  bitsfzolem  12473  bitsfzo  12474  bitsmod  12475  bitscmp  12477  bitsinv1lem  12480  bitsinv1  12481  dvdsgcdidd  12523  bezoutlemnewy  12525  mulgcd  12545  rplpwr  12556  sqgcd  12558  lcmgcdlem  12607  3lcm2e6woprm  12616  cncongr1  12633  cncongr2  12634  prmind2  12650  isprm5  12672  divgcdodd  12673  prmdvdsexpr  12680  sqrt2irrlem  12691  oddpwdclemxy  12699  oddpwdclemodd  12702  oddpwdclemdc  12703  oddpwdc  12704  sqpweven  12705  2sqpwodd  12706  sqrt2irraplemnn  12709  sqrt2irrap  12710  qmuldeneqnum  12725  divnumden  12726  qnumgt0  12728  numdensq  12732  hashdvds  12751  phiprmpw  12752  prmdiv  12765  prmdivdiv  12767  phisum  12771  modprm0  12785  pythagtriplem4  12799  pythagtriplem6  12801  pythagtriplem7  12802  pythagtriplem14  12808  pythagtriplem15  12809  pythagtriplem16  12810  pythagtriplem19  12813  pythagtrip  12814  pcprendvds2  12822  pcpre1  12823  pcpremul  12824  pceulem  12825  pcdiv  12833  pcqmul  12834  pcelnn  12852  pcid  12855  pc2dvds  12861  dvdsprmpweqnn  12867  dvdsprmpweqle  12868  pcaddlem  12870  pcadd  12871  pcfaclem  12880  qexpz  12883  expnprm  12884  oddprmdvds  12885  prmpwdvds  12886  pockthlem  12887  pockthg  12888  infpnlem1  12890  4sqlem6  12914  4sqlem7  12915  4sqlem10  12918  mul4sqlem  12924  4sqlem11  12932  4sqlem12  12933  4sqlem14  12935  4sqlem17  12938  4sqlem18  12939  oddennn  12971  evenennn  12972  mulgnndir  13696  mulgnnass  13702  znrrg  14632  logbgcd1irraplemap  15651  wilthlem1  15662  0sgm  15667  mpodvdsmulf1o  15672  1sgmprm  15676  1sgm2ppw  15677  mersenne  15679  perfect1  15680  perfectlem1  15681  perfectlem2  15682  perfect  15683  lgsval2lem  15697  gausslemma2dlem6  15754  gausslemma2dlem7  15755  gausslemma2d  15756  lgseisenlem1  15757  lgseisenlem4  15760  lgsquadlem1  15764  lgsquadlem2  15765  lgsquadlem3  15766  lgsquad2  15770  m1lgs  15772  2sqlem3  15804  2sqlem4  15805  trilpolemeq1  16438  trilpolemlt1  16439  redcwlpolemeq1  16452  nconstwlpolemgt0  16462