Theorem nncnd 8892

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

Syntax hints:   → wi 4   ∈ wcel 2141  ℂcc 7772  ℕcn 8878

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152  ax-sep 4107  ax-cnex 7865  ax-resscn 7866  ax-1re 7868  ax-addrcl 7871

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-v 2732  df-in 3127  df-ss 3134  df-int 3832  df-inn 8879

This theorem is referenced by:  peano5uzti  9320  qapne  9598  qtri3or  10199  exbtwnzlemstep  10204  intfracq  10276  flqdiv  10277  modqmulnn  10298  addmodid  10328  modaddmodup  10343  modsumfzodifsn  10352  addmodlteq  10354  facdiv  10672  facndiv  10673  faclbnd  10675  faclbnd6  10678  facubnd  10679  facavg  10680  bccmpl  10688  bcn0  10689  bcn1  10692  bcm1k  10694  bcp1n  10695  bcp1nk  10696  bcval5  10697  bcpasc  10700  permnn  10705  cvg1nlemcxze  10946  cvg1nlemcau  10948  resqrexlemcalc3  10980  binom11  11449  binom1dif  11450  divcnv  11460  arisum2  11462  trireciplem  11463  trirecip  11464  expcnvap0  11465  geo2sum  11477  geo2lim  11479  cvgratnnlembern  11486  cvgratnnlemnexp  11487  cvgratnnlemmn  11488  cvgratnnlemsumlt  11491  cvgratnnlemfm  11492  cvgratnnlemrate  11493  cvgratz  11495  eftcl  11617  eftabs  11619  efcllemp  11621  ege2le3  11634  efcj  11636  efaddlem  11637  eftlub  11653  eirraplem  11739  oexpneg  11836  divalglemnn  11877  dvdsgcdidd  11949  bezoutlemnewy  11951  mulgcd  11971  rplpwr  11982  sqgcd  11984  lcmgcdlem  12031  3lcm2e6woprm  12040  cncongr1  12057  cncongr2  12058  prmind2  12074  isprm5  12096  divgcdodd  12097  prmdvdsexpr  12104  sqrt2irrlem  12115  oddpwdclemxy  12123  oddpwdclemodd  12126  oddpwdclemdc  12127  oddpwdc  12128  sqpweven  12129  2sqpwodd  12130  sqrt2irraplemnn  12133  sqrt2irrap  12134  qmuldeneqnum  12149  divnumden  12150  qnumgt0  12152  numdensq  12156  hashdvds  12175  phiprmpw  12176  prmdiv  12189  prmdivdiv  12191  phisum  12194  modprm0  12208  pythagtriplem4  12222  pythagtriplem6  12224  pythagtriplem7  12225  pythagtriplem14  12231  pythagtriplem15  12232  pythagtriplem16  12233  pythagtriplem19  12236  pythagtrip  12237  pcprendvds2  12245  pcpre1  12246  pcpremul  12247  pceulem  12248  pcdiv  12256  pcqmul  12257  pcelnn  12274  pcid  12277  pc2dvds  12283  dvdsprmpweqnn  12289  dvdsprmpweqle  12290  pcaddlem  12292  pcadd  12293  pcfaclem  12301  qexpz  12304  expnprm  12305  oddprmdvds  12306  prmpwdvds  12307  pockthlem  12308  pockthg  12309  infpnlem1  12311  4sqlem6  12335  4sqlem7  12336  4sqlem10  12339  mul4sqlem  12345  oddennn  12347  evenennn  12348  logbgcd1irraplemap  13681  lgsval2lem  13705  2sqlem3  13747  2sqlem4  13748  trilpolemeq1  14072  trilpolemlt1  14073  redcwlpolemeq1  14086  nconstwlpolemgt0  14095