Theorem nncnd 8871

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

Syntax hints:   → wi 4   ∈ wcel 2136  ℂcc 7751  ℕcn 8857

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 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147  ax-sep 4100  ax-cnex 7844  ax-resscn 7845  ax-1re 7847  ax-addrcl 7850

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-ral 2449  df-v 2728  df-in 3122  df-ss 3129  df-int 3825  df-inn 8858

This theorem is referenced by:  peano5uzti  9299  qapne  9577  qtri3or  10178  exbtwnzlemstep  10183  intfracq  10255  flqdiv  10256  modqmulnn  10277  addmodid  10307  modaddmodup  10322  modsumfzodifsn  10331  addmodlteq  10333  facdiv  10651  facndiv  10652  faclbnd  10654  faclbnd6  10657  facubnd  10658  facavg  10659  bccmpl  10667  bcn0  10668  bcn1  10671  bcm1k  10673  bcp1n  10674  bcp1nk  10675  bcval5  10676  bcpasc  10679  permnn  10684  cvg1nlemcxze  10924  cvg1nlemcau  10926  resqrexlemcalc3  10958  binom11  11427  binom1dif  11428  divcnv  11438  arisum2  11440  trireciplem  11441  trirecip  11442  expcnvap0  11443  geo2sum  11455  geo2lim  11457  cvgratnnlembern  11464  cvgratnnlemnexp  11465  cvgratnnlemmn  11466  cvgratnnlemsumlt  11469  cvgratnnlemfm  11470  cvgratnnlemrate  11471  cvgratz  11473  eftcl  11595  eftabs  11597  efcllemp  11599  ege2le3  11612  efcj  11614  efaddlem  11615  eftlub  11631  eirraplem  11717  oexpneg  11814  divalglemnn  11855  dvdsgcdidd  11927  bezoutlemnewy  11929  mulgcd  11949  rplpwr  11960  sqgcd  11962  lcmgcdlem  12009  3lcm2e6woprm  12018  cncongr1  12035  cncongr2  12036  prmind2  12052  isprm5  12074  divgcdodd  12075  prmdvdsexpr  12082  sqrt2irrlem  12093  oddpwdclemxy  12101  oddpwdclemodd  12104  oddpwdclemdc  12105  oddpwdc  12106  sqpweven  12107  2sqpwodd  12108  sqrt2irraplemnn  12111  sqrt2irrap  12112  qmuldeneqnum  12127  divnumden  12128  qnumgt0  12130  numdensq  12134  hashdvds  12153  phiprmpw  12154  prmdiv  12167  prmdivdiv  12169  phisum  12172  modprm0  12186  pythagtriplem4  12200  pythagtriplem6  12202  pythagtriplem7  12203  pythagtriplem14  12209  pythagtriplem15  12210  pythagtriplem16  12211  pythagtriplem19  12214  pythagtrip  12215  pcprendvds2  12223  pcpre1  12224  pcpremul  12225  pceulem  12226  pcdiv  12234  pcqmul  12235  pcelnn  12252  pcid  12255  pc2dvds  12261  dvdsprmpweqnn  12267  dvdsprmpweqle  12268  pcaddlem  12270  pcadd  12271  pcfaclem  12279  qexpz  12282  expnprm  12283  oddprmdvds  12284  prmpwdvds  12285  pockthlem  12286  pockthg  12287  infpnlem1  12289  4sqlem6  12313  4sqlem7  12314  4sqlem10  12317  mul4sqlem  12323  oddennn  12325  evenennn  12326  logbgcd1irraplemap  13537  lgsval2lem  13561  2sqlem3  13603  2sqlem4  13604  trilpolemeq1  13929  trilpolemlt1  13930  redcwlpolemeq1  13943  nconstwlpolemgt0  13952