Theorem nncnd 9162

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

Syntax hints:   → wi 4   ∈ wcel 2201  ℂcc 8035  ℕcn 9148

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 2212  ax-sep 4208  ax-cnex 8128  ax-resscn 8129  ax-1re 8131  ax-addrcl 8134

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-ral 2514  df-v 2803  df-in 3205  df-ss 3212  df-int 3930  df-inn 9149

This theorem is referenced by:  peano5uzti  9593  qapne  9878  qtri3or  10506  exbtwnzlemstep  10513  intfracq  10588  flqdiv  10589  modqmulnn  10610  addmodid  10640  modaddmodup  10655  modsumfzodifsn  10664  addmodlteq  10666  facdiv  11006  facndiv  11007  faclbnd  11009  faclbnd6  11012  facubnd  11013  facavg  11014  bccmpl  11022  bcn0  11023  bcn1  11026  bcm1k  11028  bcp1n  11029  bcp1nk  11030  bcval5  11031  bcpasc  11034  permnn  11039  cvg1nlemcxze  11565  cvg1nlemcau  11567  resqrexlemcalc3  11599  binom11  12070  binom1dif  12071  divcnv  12081  arisum2  12083  trireciplem  12084  trirecip  12085  expcnvap0  12086  geo2sum  12098  geo2lim  12100  cvgratnnlembern  12107  cvgratnnlemnexp  12108  cvgratnnlemmn  12109  cvgratnnlemsumlt  12112  cvgratnnlemfm  12113  cvgratnnlemrate  12114  cvgratz  12116  eftcl  12238  eftabs  12240  efcllemp  12242  ege2le3  12255  efcj  12257  efaddlem  12258  eftlub  12274  eirraplem  12361  oexpneg  12461  divalglemnn  12502  bitsp1  12535  bitsfzolem  12538  bitsfzo  12539  bitsmod  12540  bitscmp  12542  bitsinv1lem  12545  bitsinv1  12546  dvdsgcdidd  12588  bezoutlemnewy  12590  mulgcd  12610  rplpwr  12621  sqgcd  12623  lcmgcdlem  12672  3lcm2e6woprm  12681  cncongr1  12698  cncongr2  12699  prmind2  12715  isprm5  12737  divgcdodd  12738  prmdvdsexpr  12745  sqrt2irrlem  12756  oddpwdclemxy  12764  oddpwdclemodd  12767  oddpwdclemdc  12768  oddpwdc  12769  sqpweven  12770  2sqpwodd  12771  sqrt2irraplemnn  12774  sqrt2irrap  12775  qmuldeneqnum  12790  divnumden  12791  qnumgt0  12793  numdensq  12797  hashdvds  12816  phiprmpw  12817  prmdiv  12830  prmdivdiv  12832  phisum  12836  modprm0  12850  pythagtriplem4  12864  pythagtriplem6  12866  pythagtriplem7  12867  pythagtriplem14  12873  pythagtriplem15  12874  pythagtriplem16  12875  pythagtriplem19  12878  pythagtrip  12879  pcprendvds2  12887  pcpre1  12888  pcpremul  12889  pceulem  12890  pcdiv  12898  pcqmul  12899  pcelnn  12917  pcid  12920  pc2dvds  12926  dvdsprmpweqnn  12932  dvdsprmpweqle  12933  pcaddlem  12935  pcadd  12936  pcfaclem  12945  qexpz  12948  expnprm  12949  oddprmdvds  12950  prmpwdvds  12951  pockthlem  12952  pockthg  12953  infpnlem1  12955  4sqlem6  12979  4sqlem7  12980  4sqlem10  12983  mul4sqlem  12989  4sqlem11  12997  4sqlem12  12998  4sqlem14  13000  4sqlem17  13003  4sqlem18  13004  oddennn  13036  evenennn  13037  mulgnndir  13761  mulgnnass  13767  znrrg  14698  logbgcd1irraplemap  15722  wilthlem1  15733  0sgm  15738  mpodvdsmulf1o  15743  1sgmprm  15747  1sgm2ppw  15748  mersenne  15750  perfect1  15751  perfectlem1  15752  perfectlem2  15753  perfect  15754  lgsval2lem  15768  gausslemma2dlem6  15825  gausslemma2dlem7  15826  gausslemma2d  15827  lgseisenlem1  15828  lgseisenlem4  15831  lgsquadlem1  15835  lgsquadlem2  15836  lgsquadlem3  15837  lgsquad2  15841  m1lgs  15843  2sqlem3  15875  2sqlem4  15876  trilpolemeq1  16711  trilpolemlt1  16712  redcwlpolemeq1  16726  nconstwlpolemgt0  16736