Theorem nncnd 9057

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

Syntax hints:   → wi 4   ∈ wcel 2177  ℂcc 7930  ℕcn 9043

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188  ax-sep 4166  ax-cnex 8023  ax-resscn 8024  ax-1re 8026  ax-addrcl 8029

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-v 2775  df-in 3173  df-ss 3180  df-int 3888  df-inn 9044

This theorem is referenced by:  peano5uzti  9488  qapne  9767  qtri3or  10390  exbtwnzlemstep  10397  intfracq  10472  flqdiv  10473  modqmulnn  10494  addmodid  10524  modaddmodup  10539  modsumfzodifsn  10548  addmodlteq  10550  facdiv  10890  facndiv  10891  faclbnd  10893  faclbnd6  10896  facubnd  10897  facavg  10898  bccmpl  10906  bcn0  10907  bcn1  10910  bcm1k  10912  bcp1n  10913  bcp1nk  10914  bcval5  10915  bcpasc  10918  permnn  10923  cvg1nlemcxze  11337  cvg1nlemcau  11339  resqrexlemcalc3  11371  binom11  11841  binom1dif  11842  divcnv  11852  arisum2  11854  trireciplem  11855  trirecip  11856  expcnvap0  11857  geo2sum  11869  geo2lim  11871  cvgratnnlembern  11878  cvgratnnlemnexp  11879  cvgratnnlemmn  11880  cvgratnnlemsumlt  11883  cvgratnnlemfm  11884  cvgratnnlemrate  11885  cvgratz  11887  eftcl  12009  eftabs  12011  efcllemp  12013  ege2le3  12026  efcj  12028  efaddlem  12029  eftlub  12045  eirraplem  12132  oexpneg  12232  divalglemnn  12273  bitsp1  12306  bitsfzolem  12309  bitsfzo  12310  bitsmod  12311  bitscmp  12313  bitsinv1lem  12316  bitsinv1  12317  dvdsgcdidd  12359  bezoutlemnewy  12361  mulgcd  12381  rplpwr  12392  sqgcd  12394  lcmgcdlem  12443  3lcm2e6woprm  12452  cncongr1  12469  cncongr2  12470  prmind2  12486  isprm5  12508  divgcdodd  12509  prmdvdsexpr  12516  sqrt2irrlem  12527  oddpwdclemxy  12535  oddpwdclemodd  12538  oddpwdclemdc  12539  oddpwdc  12540  sqpweven  12541  2sqpwodd  12542  sqrt2irraplemnn  12545  sqrt2irrap  12546  qmuldeneqnum  12561  divnumden  12562  qnumgt0  12564  numdensq  12568  hashdvds  12587  phiprmpw  12588  prmdiv  12601  prmdivdiv  12603  phisum  12607  modprm0  12621  pythagtriplem4  12635  pythagtriplem6  12637  pythagtriplem7  12638  pythagtriplem14  12644  pythagtriplem15  12645  pythagtriplem16  12646  pythagtriplem19  12649  pythagtrip  12650  pcprendvds2  12658  pcpre1  12659  pcpremul  12660  pceulem  12661  pcdiv  12669  pcqmul  12670  pcelnn  12688  pcid  12691  pc2dvds  12697  dvdsprmpweqnn  12703  dvdsprmpweqle  12704  pcaddlem  12706  pcadd  12707  pcfaclem  12716  qexpz  12719  expnprm  12720  oddprmdvds  12721  prmpwdvds  12722  pockthlem  12723  pockthg  12724  infpnlem1  12726  4sqlem6  12750  4sqlem7  12751  4sqlem10  12754  mul4sqlem  12760  4sqlem11  12768  4sqlem12  12769  4sqlem14  12771  4sqlem17  12774  4sqlem18  12775  oddennn  12807  evenennn  12808  mulgnndir  13531  mulgnnass  13537  znrrg  14466  logbgcd1irraplemap  15485  wilthlem1  15496  0sgm  15501  mpodvdsmulf1o  15506  1sgmprm  15510  1sgm2ppw  15511  mersenne  15513  perfect1  15514  perfectlem1  15515  perfectlem2  15516  perfect  15517  lgsval2lem  15531  gausslemma2dlem6  15588  gausslemma2dlem7  15589  gausslemma2d  15590  lgseisenlem1  15591  lgseisenlem4  15594  lgsquadlem1  15598  lgsquadlem2  15599  lgsquadlem3  15600  lgsquad2  15604  m1lgs  15606  2sqlem3  15638  2sqlem4  15639  trilpolemeq1  16053  trilpolemlt1  16054  redcwlpolemeq1  16067  nconstwlpolemgt0  16077