Theorem nncnd 8996

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

Syntax hints:   → wi 4   ∈ wcel 2164  ℂcc 7870  ℕcn 8982

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-sep 4147  ax-cnex 7963  ax-resscn 7964  ax-1re 7966  ax-addrcl 7969

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-v 2762  df-in 3159  df-ss 3166  df-int 3871  df-inn 8983

This theorem is referenced by:  peano5uzti  9425  qapne  9704  qtri3or  10310  exbtwnzlemstep  10316  intfracq  10391  flqdiv  10392  modqmulnn  10413  addmodid  10443  modaddmodup  10458  modsumfzodifsn  10467  addmodlteq  10469  facdiv  10809  facndiv  10810  faclbnd  10812  faclbnd6  10815  facubnd  10816  facavg  10817  bccmpl  10825  bcn0  10826  bcn1  10829  bcm1k  10831  bcp1n  10832  bcp1nk  10833  bcval5  10834  bcpasc  10837  permnn  10842  cvg1nlemcxze  11126  cvg1nlemcau  11128  resqrexlemcalc3  11160  binom11  11629  binom1dif  11630  divcnv  11640  arisum2  11642  trireciplem  11643  trirecip  11644  expcnvap0  11645  geo2sum  11657  geo2lim  11659  cvgratnnlembern  11666  cvgratnnlemnexp  11667  cvgratnnlemmn  11668  cvgratnnlemsumlt  11671  cvgratnnlemfm  11672  cvgratnnlemrate  11673  cvgratz  11675  eftcl  11797  eftabs  11799  efcllemp  11801  ege2le3  11814  efcj  11816  efaddlem  11817  eftlub  11833  eirraplem  11920  oexpneg  12018  divalglemnn  12059  dvdsgcdidd  12131  bezoutlemnewy  12133  mulgcd  12153  rplpwr  12164  sqgcd  12166  lcmgcdlem  12215  3lcm2e6woprm  12224  cncongr1  12241  cncongr2  12242  prmind2  12258  isprm5  12280  divgcdodd  12281  prmdvdsexpr  12288  sqrt2irrlem  12299  oddpwdclemxy  12307  oddpwdclemodd  12310  oddpwdclemdc  12311  oddpwdc  12312  sqpweven  12313  2sqpwodd  12314  sqrt2irraplemnn  12317  sqrt2irrap  12318  qmuldeneqnum  12333  divnumden  12334  qnumgt0  12336  numdensq  12340  hashdvds  12359  phiprmpw  12360  prmdiv  12373  prmdivdiv  12375  phisum  12378  modprm0  12392  pythagtriplem4  12406  pythagtriplem6  12408  pythagtriplem7  12409  pythagtriplem14  12415  pythagtriplem15  12416  pythagtriplem16  12417  pythagtriplem19  12420  pythagtrip  12421  pcprendvds2  12429  pcpre1  12430  pcpremul  12431  pceulem  12432  pcdiv  12440  pcqmul  12441  pcelnn  12459  pcid  12462  pc2dvds  12468  dvdsprmpweqnn  12474  dvdsprmpweqle  12475  pcaddlem  12477  pcadd  12478  pcfaclem  12487  qexpz  12490  expnprm  12491  oddprmdvds  12492  prmpwdvds  12493  pockthlem  12494  pockthg  12495  infpnlem1  12497  4sqlem6  12521  4sqlem7  12522  4sqlem10  12525  mul4sqlem  12531  4sqlem11  12539  4sqlem12  12540  4sqlem14  12542  4sqlem17  12545  4sqlem18  12546  oddennn  12549  evenennn  12550  mulgnndir  13221  mulgnnass  13227  znrrg  14148  logbgcd1irraplemap  15101  wilthlem1  15112  lgsval2lem  15126  gausslemma2dlem6  15183  gausslemma2dlem7  15184  gausslemma2d  15185  lgseisenlem1  15186  lgseisenlem4  15189  lgsquadlem1  15191  m1lgs  15192  2sqlem3  15204  2sqlem4  15205  trilpolemeq1  15530  trilpolemlt1  15531  redcwlpolemeq1  15544  nconstwlpolemgt0  15554