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  10500  exbtwnzlemstep  10507  intfracq  10582  flqdiv  10583  modqmulnn  10604  addmodid  10634  modaddmodup  10649  modsumfzodifsn  10658  addmodlteq  10660  facdiv  11000  facndiv  11001  faclbnd  11003  faclbnd6  11006  facubnd  11007  facavg  11008  bccmpl  11016  bcn0  11017  bcn1  11020  bcm1k  11022  bcp1n  11023  bcp1nk  11024  bcval5  11025  bcpasc  11028  permnn  11033  cvg1nlemcxze  11543  cvg1nlemcau  11545  resqrexlemcalc3  11577  binom11  12048  binom1dif  12049  divcnv  12059  arisum2  12061  trireciplem  12062  trirecip  12063  expcnvap0  12064  geo2sum  12076  geo2lim  12078  cvgratnnlembern  12085  cvgratnnlemnexp  12086  cvgratnnlemmn  12087  cvgratnnlemsumlt  12090  cvgratnnlemfm  12091  cvgratnnlemrate  12092  cvgratz  12094  eftcl  12216  eftabs  12218  efcllemp  12220  ege2le3  12233  efcj  12235  efaddlem  12236  eftlub  12252  eirraplem  12339  oexpneg  12439  divalglemnn  12480  bitsp1  12513  bitsfzolem  12516  bitsfzo  12517  bitsmod  12518  bitscmp  12520  bitsinv1lem  12523  bitsinv1  12524  dvdsgcdidd  12566  bezoutlemnewy  12568  mulgcd  12588  rplpwr  12599  sqgcd  12601  lcmgcdlem  12650  3lcm2e6woprm  12659  cncongr1  12676  cncongr2  12677  prmind2  12693  isprm5  12715  divgcdodd  12716  prmdvdsexpr  12723  sqrt2irrlem  12734  oddpwdclemxy  12742  oddpwdclemodd  12745  oddpwdclemdc  12746  oddpwdc  12747  sqpweven  12748  2sqpwodd  12749  sqrt2irraplemnn  12752  sqrt2irrap  12753  qmuldeneqnum  12768  divnumden  12769  qnumgt0  12771  numdensq  12775  hashdvds  12794  phiprmpw  12795  prmdiv  12808  prmdivdiv  12810  phisum  12814  modprm0  12828  pythagtriplem4  12842  pythagtriplem6  12844  pythagtriplem7  12845  pythagtriplem14  12851  pythagtriplem15  12852  pythagtriplem16  12853  pythagtriplem19  12856  pythagtrip  12857  pcprendvds2  12865  pcpre1  12866  pcpremul  12867  pceulem  12868  pcdiv  12876  pcqmul  12877  pcelnn  12895  pcid  12898  pc2dvds  12904  dvdsprmpweqnn  12910  dvdsprmpweqle  12911  pcaddlem  12913  pcadd  12914  pcfaclem  12923  qexpz  12926  expnprm  12927  oddprmdvds  12928  prmpwdvds  12929  pockthlem  12930  pockthg  12931  infpnlem1  12933  4sqlem6  12957  4sqlem7  12958  4sqlem10  12961  mul4sqlem  12967  4sqlem11  12975  4sqlem12  12976  4sqlem14  12978  4sqlem17  12981  4sqlem18  12982  oddennn  13014  evenennn  13015  mulgnndir  13739  mulgnnass  13745  znrrg  14676  logbgcd1irraplemap  15695  wilthlem1  15706  0sgm  15711  mpodvdsmulf1o  15716  1sgmprm  15720  1sgm2ppw  15721  mersenne  15723  perfect1  15724  perfectlem1  15725  perfectlem2  15726  perfect  15727  lgsval2lem  15741  gausslemma2dlem6  15798  gausslemma2dlem7  15799  gausslemma2d  15800  lgseisenlem1  15801  lgseisenlem4  15804  lgsquadlem1  15808  lgsquadlem2  15809  lgsquadlem3  15810  lgsquad2  15814  m1lgs  15816  2sqlem3  15848  2sqlem4  15849  trilpolemeq1  16647  trilpolemlt1  16648  redcwlpolemeq1  16661  nconstwlpolemgt0  16671