Theorem nncnd 9092

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

Syntax hints:   → wi 4   ∈ wcel 2180  ℂcc 7965  ℕcn 9078

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 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191  ax-sep 4181  ax-cnex 8058  ax-resscn 8059  ax-1re 8061  ax-addrcl 8064

This theorem depends on definitions:  df-bi 117  df-tru 1378  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-ral 2493  df-v 2781  df-in 3183  df-ss 3190  df-int 3903  df-inn 9079

This theorem is referenced by:  peano5uzti  9523  qapne  9802  qtri3or  10427  exbtwnzlemstep  10434  intfracq  10509  flqdiv  10510  modqmulnn  10531  addmodid  10561  modaddmodup  10576  modsumfzodifsn  10585  addmodlteq  10587  facdiv  10927  facndiv  10928  faclbnd  10930  faclbnd6  10933  facubnd  10934  facavg  10935  bccmpl  10943  bcn0  10944  bcn1  10947  bcm1k  10949  bcp1n  10950  bcp1nk  10951  bcval5  10952  bcpasc  10955  permnn  10960  cvg1nlemcxze  11459  cvg1nlemcau  11461  resqrexlemcalc3  11493  binom11  11963  binom1dif  11964  divcnv  11974  arisum2  11976  trireciplem  11977  trirecip  11978  expcnvap0  11979  geo2sum  11991  geo2lim  11993  cvgratnnlembern  12000  cvgratnnlemnexp  12001  cvgratnnlemmn  12002  cvgratnnlemsumlt  12005  cvgratnnlemfm  12006  cvgratnnlemrate  12007  cvgratz  12009  eftcl  12131  eftabs  12133  efcllemp  12135  ege2le3  12148  efcj  12150  efaddlem  12151  eftlub  12167  eirraplem  12254  oexpneg  12354  divalglemnn  12395  bitsp1  12428  bitsfzolem  12431  bitsfzo  12432  bitsmod  12433  bitscmp  12435  bitsinv1lem  12438  bitsinv1  12439  dvdsgcdidd  12481  bezoutlemnewy  12483  mulgcd  12503  rplpwr  12514  sqgcd  12516  lcmgcdlem  12565  3lcm2e6woprm  12574  cncongr1  12591  cncongr2  12592  prmind2  12608  isprm5  12630  divgcdodd  12631  prmdvdsexpr  12638  sqrt2irrlem  12649  oddpwdclemxy  12657  oddpwdclemodd  12660  oddpwdclemdc  12661  oddpwdc  12662  sqpweven  12663  2sqpwodd  12664  sqrt2irraplemnn  12667  sqrt2irrap  12668  qmuldeneqnum  12683  divnumden  12684  qnumgt0  12686  numdensq  12690  hashdvds  12709  phiprmpw  12710  prmdiv  12723  prmdivdiv  12725  phisum  12729  modprm0  12743  pythagtriplem4  12757  pythagtriplem6  12759  pythagtriplem7  12760  pythagtriplem14  12766  pythagtriplem15  12767  pythagtriplem16  12768  pythagtriplem19  12771  pythagtrip  12772  pcprendvds2  12780  pcpre1  12781  pcpremul  12782  pceulem  12783  pcdiv  12791  pcqmul  12792  pcelnn  12810  pcid  12813  pc2dvds  12819  dvdsprmpweqnn  12825  dvdsprmpweqle  12826  pcaddlem  12828  pcadd  12829  pcfaclem  12838  qexpz  12841  expnprm  12842  oddprmdvds  12843  prmpwdvds  12844  pockthlem  12845  pockthg  12846  infpnlem1  12848  4sqlem6  12872  4sqlem7  12873  4sqlem10  12876  mul4sqlem  12882  4sqlem11  12890  4sqlem12  12891  4sqlem14  12893  4sqlem17  12896  4sqlem18  12897  oddennn  12929  evenennn  12930  mulgnndir  13654  mulgnnass  13660  znrrg  14589  logbgcd1irraplemap  15608  wilthlem1  15619  0sgm  15624  mpodvdsmulf1o  15629  1sgmprm  15633  1sgm2ppw  15634  mersenne  15636  perfect1  15637  perfectlem1  15638  perfectlem2  15639  perfect  15640  lgsval2lem  15654  gausslemma2dlem6  15711  gausslemma2dlem7  15712  gausslemma2d  15713  lgseisenlem1  15714  lgseisenlem4  15717  lgsquadlem1  15721  lgsquadlem2  15722  lgsquadlem3  15723  lgsquad2  15727  m1lgs  15729  2sqlem3  15761  2sqlem4  15762  trilpolemeq1  16319  trilpolemlt1  16320  redcwlpolemeq1  16333  nconstwlpolemgt0  16343