Theorem nncnd 8936

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

Syntax hints:   → wi 4   ∈ wcel 2148  ℂcc 7812  ℕcn 8922

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-sep 4123  ax-cnex 7905  ax-resscn 7906  ax-1re 7908  ax-addrcl 7911

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-v 2741  df-in 3137  df-ss 3144  df-int 3847  df-inn 8923

This theorem is referenced by:  peano5uzti  9364  qapne  9642  qtri3or  10246  exbtwnzlemstep  10251  intfracq  10323  flqdiv  10324  modqmulnn  10345  addmodid  10375  modaddmodup  10390  modsumfzodifsn  10399  addmodlteq  10401  facdiv  10721  facndiv  10722  faclbnd  10724  faclbnd6  10727  facubnd  10728  facavg  10729  bccmpl  10737  bcn0  10738  bcn1  10741  bcm1k  10743  bcp1n  10744  bcp1nk  10745  bcval5  10746  bcpasc  10749  permnn  10754  cvg1nlemcxze  10994  cvg1nlemcau  10996  resqrexlemcalc3  11028  binom11  11497  binom1dif  11498  divcnv  11508  arisum2  11510  trireciplem  11511  trirecip  11512  expcnvap0  11513  geo2sum  11525  geo2lim  11527  cvgratnnlembern  11534  cvgratnnlemnexp  11535  cvgratnnlemmn  11536  cvgratnnlemsumlt  11539  cvgratnnlemfm  11540  cvgratnnlemrate  11541  cvgratz  11543  eftcl  11665  eftabs  11667  efcllemp  11669  ege2le3  11682  efcj  11684  efaddlem  11685  eftlub  11701  eirraplem  11787  oexpneg  11885  divalglemnn  11926  dvdsgcdidd  11998  bezoutlemnewy  12000  mulgcd  12020  rplpwr  12031  sqgcd  12033  lcmgcdlem  12080  3lcm2e6woprm  12089  cncongr1  12106  cncongr2  12107  prmind2  12123  isprm5  12145  divgcdodd  12146  prmdvdsexpr  12153  sqrt2irrlem  12164  oddpwdclemxy  12172  oddpwdclemodd  12175  oddpwdclemdc  12176  oddpwdc  12177  sqpweven  12178  2sqpwodd  12179  sqrt2irraplemnn  12182  sqrt2irrap  12183  qmuldeneqnum  12198  divnumden  12199  qnumgt0  12201  numdensq  12205  hashdvds  12224  phiprmpw  12225  prmdiv  12238  prmdivdiv  12240  phisum  12243  modprm0  12257  pythagtriplem4  12271  pythagtriplem6  12273  pythagtriplem7  12274  pythagtriplem14  12280  pythagtriplem15  12281  pythagtriplem16  12282  pythagtriplem19  12285  pythagtrip  12286  pcprendvds2  12294  pcpre1  12295  pcpremul  12296  pceulem  12297  pcdiv  12305  pcqmul  12306  pcelnn  12323  pcid  12326  pc2dvds  12332  dvdsprmpweqnn  12338  dvdsprmpweqle  12339  pcaddlem  12341  pcadd  12342  pcfaclem  12350  qexpz  12353  expnprm  12354  oddprmdvds  12355  prmpwdvds  12356  pockthlem  12357  pockthg  12358  infpnlem1  12360  4sqlem6  12384  4sqlem7  12385  4sqlem10  12388  mul4sqlem  12394  oddennn  12396  evenennn  12397  mulgnndir  13022  mulgnnass  13028  logbgcd1irraplemap  14548  lgsval2lem  14572  lgseisenlem1  14611  m1lgs  14613  2sqlem3  14625  2sqlem4  14626  trilpolemeq1  14950  trilpolemlt1  14951  redcwlpolemeq1  14964  nconstwlpolemgt0  14974