Theorem nncnd 9157

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℂcc 8030  ℕcn 9143

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-sep 4207  ax-cnex 8123  ax-resscn 8124  ax-1re 8126  ax-addrcl 8129

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-v 2804  df-in 3206  df-ss 3213  df-int 3929  df-inn 9144

This theorem is referenced by:  peano5uzti  9588  qapne  9873  qtri3or  10501  exbtwnzlemstep  10508  intfracq  10583  flqdiv  10584  modqmulnn  10605  addmodid  10635  modaddmodup  10650  modsumfzodifsn  10659  addmodlteq  10661  facdiv  11001  facndiv  11002  faclbnd  11004  faclbnd6  11007  facubnd  11008  facavg  11009  bccmpl  11017  bcn0  11018  bcn1  11021  bcm1k  11023  bcp1n  11024  bcp1nk  11025  bcval5  11026  bcpasc  11029  permnn  11034  cvg1nlemcxze  11544  cvg1nlemcau  11546  resqrexlemcalc3  11578  binom11  12049  binom1dif  12050  divcnv  12060  arisum2  12062  trireciplem  12063  trirecip  12064  expcnvap0  12065  geo2sum  12077  geo2lim  12079  cvgratnnlembern  12086  cvgratnnlemnexp  12087  cvgratnnlemmn  12088  cvgratnnlemsumlt  12091  cvgratnnlemfm  12092  cvgratnnlemrate  12093  cvgratz  12095  eftcl  12217  eftabs  12219  efcllemp  12221  ege2le3  12234  efcj  12236  efaddlem  12237  eftlub  12253  eirraplem  12340  oexpneg  12440  divalglemnn  12481  bitsp1  12514  bitsfzolem  12517  bitsfzo  12518  bitsmod  12519  bitscmp  12521  bitsinv1lem  12524  bitsinv1  12525  dvdsgcdidd  12567  bezoutlemnewy  12569  mulgcd  12589  rplpwr  12600  sqgcd  12602  lcmgcdlem  12651  3lcm2e6woprm  12660  cncongr1  12677  cncongr2  12678  prmind2  12694  isprm5  12716  divgcdodd  12717  prmdvdsexpr  12724  sqrt2irrlem  12735  oddpwdclemxy  12743  oddpwdclemodd  12746  oddpwdclemdc  12747  oddpwdc  12748  sqpweven  12749  2sqpwodd  12750  sqrt2irraplemnn  12753  sqrt2irrap  12754  qmuldeneqnum  12769  divnumden  12770  qnumgt0  12772  numdensq  12776  hashdvds  12795  phiprmpw  12796  prmdiv  12809  prmdivdiv  12811  phisum  12815  modprm0  12829  pythagtriplem4  12843  pythagtriplem6  12845  pythagtriplem7  12846  pythagtriplem14  12852  pythagtriplem15  12853  pythagtriplem16  12854  pythagtriplem19  12857  pythagtrip  12858  pcprendvds2  12866  pcpre1  12867  pcpremul  12868  pceulem  12869  pcdiv  12877  pcqmul  12878  pcelnn  12896  pcid  12899  pc2dvds  12905  dvdsprmpweqnn  12911  dvdsprmpweqle  12912  pcaddlem  12914  pcadd  12915  pcfaclem  12924  qexpz  12927  expnprm  12928  oddprmdvds  12929  prmpwdvds  12930  pockthlem  12931  pockthg  12932  infpnlem1  12934  4sqlem6  12958  4sqlem7  12959  4sqlem10  12962  mul4sqlem  12968  4sqlem11  12976  4sqlem12  12977  4sqlem14  12979  4sqlem17  12982  4sqlem18  12983  oddennn  13015  evenennn  13016  mulgnndir  13740  mulgnnass  13746  znrrg  14677  logbgcd1irraplemap  15696  wilthlem1  15707  0sgm  15712  mpodvdsmulf1o  15717  1sgmprm  15721  1sgm2ppw  15722  mersenne  15724  perfect1  15725  perfectlem1  15726  perfectlem2  15727  perfect  15728  lgsval2lem  15742  gausslemma2dlem6  15799  gausslemma2dlem7  15800  gausslemma2d  15801  lgseisenlem1  15802  lgseisenlem4  15805  lgsquadlem1  15809  lgsquadlem2  15810  lgsquadlem3  15811  lgsquad2  15815  m1lgs  15817  2sqlem3  15849  2sqlem4  15850  trilpolemeq1  16665  trilpolemlt1  16666  redcwlpolemeq1  16679  nconstwlpolemgt0  16689