Theorem nncnd 9271

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

Syntax hints:   → wi 4   ∈ wcel 2205  ℂcc 8141  ℕcn 9257

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 2216  ax-sep 4233  ax-cnex 8234  ax-resscn 8235  ax-1re 8237  ax-addrcl 8240

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-v 2817  df-in 3220  df-ss 3227  df-int 3955  df-inn 9258

This theorem is referenced by:  peano5uzti  9707  qapne  9992  ltesubnnd  10123  qtri3or  10627  exbtwnzlemstep  10634  intfracq  10709  flqdiv  10710  modqmulnn  10731  addmodid  10761  modaddmodup  10776  modsumfzodifsn  10785  addmodlteq  10787  facdiv  11128  facndiv  11129  faclbnd  11131  faclbnd6  11134  facubnd  11135  facavg  11136  bccmpl  11144  bcn0  11145  bcn1  11148  bcm1k  11150  bcp1n  11151  bcp1nk  11152  bcval5  11153  bcpasc  11156  permnn  11162  cvg1nlemcxze  11695  cvg1nlemcau  11697  resqrexlemcalc3  11729  binom11  12200  binom1dif  12201  divcnv  12211  arisum2  12213  trireciplem  12214  trirecip  12215  expcnvap0  12216  geo2sum  12228  geo2lim  12230  cvgratnnlembern  12237  cvgratnnlemnexp  12238  cvgratnnlemmn  12239  cvgratnnlemsumlt  12242  cvgratnnlemfm  12243  cvgratnnlemrate  12244  cvgratz  12246  eftcl  12368  eftabs  12370  efcllemp  12372  ege2le3  12385  efcj  12387  efaddlem  12388  eftlub  12404  eirraplem  12491  oexpneg  12591  divalglemnn  12632  bitsp1  12665  bitsfzolem  12668  bitsfzo  12669  bitsmod  12670  bitscmp  12672  bitsinv1lem  12675  bitsinv1  12676  dvdsgcdidd  12718  bezoutlemnewy  12720  mulgcd  12740  rplpwr  12751  sqgcd  12753  lcmgcdlem  12802  3lcm2e6woprm  12811  cncongr1  12828  cncongr2  12829  prmind2  12845  isprm5  12867  divgcdodd  12868  prmdvdsexpr  12875  sqrt2irrlem  12886  oddpwdclemxy  12894  oddpwdclemodd  12897  oddpwdclemdc  12898  oddpwdc  12899  sqpweven  12900  2sqpwodd  12901  sqrt2irraplemnn  12904  sqrt2irrap  12905  qmuldeneqnum  12920  divnumden  12921  qnumgt0  12923  numdensq  12927  hashdvds  12946  phiprmpw  12947  prmdiv  12960  prmdivdiv  12962  phisum  12966  modprm0  12980  pythagtriplem4  12994  pythagtriplem6  12996  pythagtriplem7  12997  pythagtriplem14  13003  pythagtriplem15  13004  pythagtriplem16  13005  pythagtriplem19  13008  pythagtrip  13009  pcprendvds2  13017  pcpre1  13018  pcpremul  13019  pceulem  13020  pcdiv  13028  pcqmul  13029  pcelnn  13047  pcid  13050  pc2dvds  13056  dvdsprmpweqnn  13062  dvdsprmpweqle  13063  pcaddlem  13065  pcadd  13066  pcfaclem  13075  qexpz  13078  expnprm  13079  oddprmdvds  13080  prmpwdvds  13081  pockthlem  13082  pockthg  13083  infpnlem1  13085  4sqlem6  13109  4sqlem7  13110  4sqlem10  13113  mul4sqlem  13119  4sqlem11  13127  4sqlem12  13128  4sqlem14  13130  4sqlem17  13133  4sqlem18  13134  ballotfilemfc0  13179  ballotfilemfcc  13180  oddennn  13230  evenennn  13231  mulgnndir  13907  mulgnnass  13913  znrrg  14937  logbgcd1irraplemap  15963  pellexlem2  15975  wilthlem1  15977  0sgm  15982  mpodvdsmulf1o  15987  1sgmprm  15991  1sgm2ppw  15992  mersenne  15994  perfect1  15995  perfectlem1  15996  perfectlem2  15997  perfect  15998  lgsval2lem  16012  gausslemma2dlem6  16069  gausslemma2dlem7  16070  gausslemma2d  16071  lgseisenlem1  16072  lgseisenlem4  16075  lgsquadlem1  16079  lgsquadlem2  16080  lgsquadlem3  16081  lgsquad2  16085  m1lgs  16087  2sqlem3  16119  2sqlem4  16120  trilpolemeq1  16963  trilpolemlt1  16964  redcwlpolemeq1  16978  nconstwlpolemgt0  16989