Theorem nncnd 8933

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

Syntax hints:   → wi 4   ∈ wcel 2148  ℂcc 7809  ℕcn 8919

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 4122  ax-cnex 7902  ax-resscn 7903  ax-1re 7905  ax-addrcl 7908

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 2740  df-in 3136  df-ss 3143  df-int 3846  df-inn 8920

This theorem is referenced by:  peano5uzti  9361  qapne  9639  qtri3or  10243  exbtwnzlemstep  10248  intfracq  10320  flqdiv  10321  modqmulnn  10342  addmodid  10372  modaddmodup  10387  modsumfzodifsn  10396  addmodlteq  10398  facdiv  10718  facndiv  10719  faclbnd  10721  faclbnd6  10724  facubnd  10725  facavg  10726  bccmpl  10734  bcn0  10735  bcn1  10738  bcm1k  10740  bcp1n  10741  bcp1nk  10742  bcval5  10743  bcpasc  10746  permnn  10751  cvg1nlemcxze  10991  cvg1nlemcau  10993  resqrexlemcalc3  11025  binom11  11494  binom1dif  11495  divcnv  11505  arisum2  11507  trireciplem  11508  trirecip  11509  expcnvap0  11510  geo2sum  11522  geo2lim  11524  cvgratnnlembern  11531  cvgratnnlemnexp  11532  cvgratnnlemmn  11533  cvgratnnlemsumlt  11536  cvgratnnlemfm  11537  cvgratnnlemrate  11538  cvgratz  11540  eftcl  11662  eftabs  11664  efcllemp  11666  ege2le3  11679  efcj  11681  efaddlem  11682  eftlub  11698  eirraplem  11784  oexpneg  11882  divalglemnn  11923  dvdsgcdidd  11995  bezoutlemnewy  11997  mulgcd  12017  rplpwr  12028  sqgcd  12030  lcmgcdlem  12077  3lcm2e6woprm  12086  cncongr1  12103  cncongr2  12104  prmind2  12120  isprm5  12142  divgcdodd  12143  prmdvdsexpr  12150  sqrt2irrlem  12161  oddpwdclemxy  12169  oddpwdclemodd  12172  oddpwdclemdc  12173  oddpwdc  12174  sqpweven  12175  2sqpwodd  12176  sqrt2irraplemnn  12179  sqrt2irrap  12180  qmuldeneqnum  12195  divnumden  12196  qnumgt0  12198  numdensq  12202  hashdvds  12221  phiprmpw  12222  prmdiv  12235  prmdivdiv  12237  phisum  12240  modprm0  12254  pythagtriplem4  12268  pythagtriplem6  12270  pythagtriplem7  12271  pythagtriplem14  12277  pythagtriplem15  12278  pythagtriplem16  12279  pythagtriplem19  12282  pythagtrip  12283  pcprendvds2  12291  pcpre1  12292  pcpremul  12293  pceulem  12294  pcdiv  12302  pcqmul  12303  pcelnn  12320  pcid  12323  pc2dvds  12329  dvdsprmpweqnn  12335  dvdsprmpweqle  12336  pcaddlem  12338  pcadd  12339  pcfaclem  12347  qexpz  12350  expnprm  12351  oddprmdvds  12352  prmpwdvds  12353  pockthlem  12354  pockthg  12355  infpnlem1  12357  4sqlem6  12381  4sqlem7  12382  4sqlem10  12385  mul4sqlem  12391  oddennn  12393  evenennn  12394  mulgnndir  13012  mulgnnass  13018  logbgcd1irraplemap  14390  lgsval2lem  14414  lgseisenlem1  14453  m1lgs  14455  2sqlem3  14467  2sqlem4  14468  trilpolemeq1  14791  trilpolemlt1  14792  redcwlpolemeq1  14805  nconstwlpolemgt0  14814