Theorem nncnd 9247

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

Syntax hints:   → wi 4   ∈ wcel 2203  ℂcc 8121  ℕcn 9233

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214  ax-sep 4227  ax-cnex 8214  ax-resscn 8215  ax-1re 8217  ax-addrcl 8220

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-v 2814  df-in 3216  df-ss 3223  df-int 3949  df-inn 9234

This theorem is referenced by:  peano5uzti  9682  qapne  9967  qtri3or  10596  exbtwnzlemstep  10603  intfracq  10678  flqdiv  10679  modqmulnn  10700  addmodid  10730  modaddmodup  10745  modsumfzodifsn  10754  addmodlteq  10756  facdiv  11096  facndiv  11097  faclbnd  11099  faclbnd6  11102  facubnd  11103  facavg  11104  bccmpl  11112  bcn0  11113  bcn1  11116  bcm1k  11118  bcp1n  11119  bcp1nk  11120  bcval5  11121  bcpasc  11124  permnn  11129  cvg1nlemcxze  11660  cvg1nlemcau  11662  resqrexlemcalc3  11694  binom11  12165  binom1dif  12166  divcnv  12176  arisum2  12178  trireciplem  12179  trirecip  12180  expcnvap0  12181  geo2sum  12193  geo2lim  12195  cvgratnnlembern  12202  cvgratnnlemnexp  12203  cvgratnnlemmn  12204  cvgratnnlemsumlt  12207  cvgratnnlemfm  12208  cvgratnnlemrate  12209  cvgratz  12211  eftcl  12333  eftabs  12335  efcllemp  12337  ege2le3  12350  efcj  12352  efaddlem  12353  eftlub  12369  eirraplem  12456  oexpneg  12556  divalglemnn  12597  bitsp1  12630  bitsfzolem  12633  bitsfzo  12634  bitsmod  12635  bitscmp  12637  bitsinv1lem  12640  bitsinv1  12641  dvdsgcdidd  12683  bezoutlemnewy  12685  mulgcd  12705  rplpwr  12716  sqgcd  12718  lcmgcdlem  12767  3lcm2e6woprm  12776  cncongr1  12793  cncongr2  12794  prmind2  12810  isprm5  12832  divgcdodd  12833  prmdvdsexpr  12840  sqrt2irrlem  12851  oddpwdclemxy  12859  oddpwdclemodd  12862  oddpwdclemdc  12863  oddpwdc  12864  sqpweven  12865  2sqpwodd  12866  sqrt2irraplemnn  12869  sqrt2irrap  12870  qmuldeneqnum  12885  divnumden  12886  qnumgt0  12888  numdensq  12892  hashdvds  12911  phiprmpw  12912  prmdiv  12925  prmdivdiv  12927  phisum  12931  modprm0  12945  pythagtriplem4  12959  pythagtriplem6  12961  pythagtriplem7  12962  pythagtriplem14  12968  pythagtriplem15  12969  pythagtriplem16  12970  pythagtriplem19  12973  pythagtrip  12974  pcprendvds2  12982  pcpre1  12983  pcpremul  12984  pceulem  12985  pcdiv  12993  pcqmul  12994  pcelnn  13012  pcid  13015  pc2dvds  13021  dvdsprmpweqnn  13027  dvdsprmpweqle  13028  pcaddlem  13030  pcadd  13031  pcfaclem  13040  qexpz  13043  expnprm  13044  oddprmdvds  13045  prmpwdvds  13046  pockthlem  13047  pockthg  13048  infpnlem1  13050  4sqlem6  13074  4sqlem7  13075  4sqlem10  13078  mul4sqlem  13084  4sqlem11  13092  4sqlem12  13093  4sqlem14  13095  4sqlem17  13098  4sqlem18  13099  oddennn  13132  evenennn  13133  mulgnndir  13857  mulgnnass  13863  znrrg  14795  logbgcd1irraplemap  15821  pellexlem2  15833  wilthlem1  15835  0sgm  15840  mpodvdsmulf1o  15845  1sgmprm  15849  1sgm2ppw  15850  mersenne  15852  perfect1  15853  perfectlem1  15854  perfectlem2  15855  perfect  15856  lgsval2lem  15870  gausslemma2dlem6  15927  gausslemma2dlem7  15928  gausslemma2d  15929  lgseisenlem1  15930  lgseisenlem4  15933  lgsquadlem1  15937  lgsquadlem2  15938  lgsquadlem3  15939  lgsquad2  15943  m1lgs  15945  2sqlem3  15977  2sqlem4  15978  trilpolemeq1  16811  trilpolemlt1  16812  redcwlpolemeq1  16826  nconstwlpolemgt0  16836