Theorem nncnd 9328

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ℂcc 8184  ℕcn 9314

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-sep 4251  ax-cnex 8277  ax-resscn 8278  ax-1re 8280  ax-addrcl 8283

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-v 2823  df-in 3226  df-ss 3233  df-int 3971  df-inn 9315

This theorem is used by:  peano5uzti  9766  qapne  10056  ltesubnnd  10188  qtri3or  10693  exbtwnzlemstep  10700  intfracq  10779  flqdiv  10780  modqmulnn  10801  addmodid  10831  modaddmodup  10846  modsumfzodifsn  10855  addmodlteq  10857  facdiv  11199  facndiv  11200  faclbnd  11202  faclbnd6  11205  facubnd  11206  facavg  11207  bccmpl  11215  bcn0  11216  bcn1  11219  bcm1k  11221  bcp1n  11222  bcp1nk  11223  bcval5  11224  bcpasc  11227  permnn  11233  hashf1  11310  hashfac  11311  cvg1nlemcxze  11771  cvg1nlemcau  11773  resqrexlemcalc3  11805  binom11  12279  binom1dif  12280  divcnv  12290  arisum2  12292  trireciplem  12293  trirecip  12294  expcnvap0  12295  geo2sum  12307  geo2lim  12309  cvgratnnlembern  12316  cvgratnnlemnexp  12317  cvgratnnlemmn  12318  cvgratnnlemsumlt  12321  cvgratnnlemfm  12322  cvgratnnlemrate  12323  cvgratz  12325  eftcl  12447  eftabs  12449  efcllemp  12451  ege2le3  12464  efcj  12466  efaddlem  12467  eftlub  12483  eirraplem  12570  oexpneg  12670  divalglemnn  12711  bitsp1  12744  bitsfzolem  12747  bitsfzo  12748  bitsmod  12749  bitscmp  12751  bitsinv1lem  12754  bitsinv1  12755  dvdsgcdidd  12797  bezoutlemnewy  12799  mulgcd  12819  rplpwr  12830  sqgcd  12832  lcmgcdlem  12881  3lcm2e6woprm  12890  cncongr1  12907  cncongr2  12908  prmind2  12924  isprm5  12947  divgcdodd  12948  prmdvdsexpr  12955  sqrt2irrlem  12966  pwbdvdslemn  12970  pwbdvdseulemle  12972  nnmaxpwlemxy  12974  nnmaxpwlemnfac  12977  nnmaxpwlemparts  12978  nnmaxpw  12979  sqpweven  12981  2sqpwodd  12982  sqrt2irraplemnn  12985  sqrt2irrap  12986  qmuldeneqnum  13001  divnumden  13002  qnumgt0  13004  numdensq  13008  hashdvds  13029  phiprmpw  13030  prmdiv  13043  prmdivdiv  13045  phisum  13049  modprm0  13063  pythagtriplem4  13077  pythagtriplem6  13079  pythagtriplem7  13080  pythagtriplem14  13086  pythagtriplem15  13087  pythagtriplem16  13088  pythagtriplem19  13091  pythagtrip  13092  pcprendvds2  13100  pcpre1  13101  pcpremul  13102  pceulem  13103  pcdiv  13111  pcqmul  13112  pcelnn  13130  pcid  13133  pc2dvds  13139  dvdsprmpweqnn  13145  dvdsprmpweqle  13146  pcaddlem  13148  pcadd  13149  pcfaclem  13158  qexpz  13161  expnprm  13162  oddprmdvds  13163  prmpwdvds  13164  pockthlem  13165  pockthg  13166  infpnlem1  13168  4sqlem6  13192  4sqlem7  13193  4sqlem10  13196  mul4sqlem  13202  4sqlem11  13210  4sqlem12  13211  4sqlem14  13213  4sqlem17  13216  4sqlem18  13217  ballotfilemfc0  13291  ballotfilemfcc  13292  oddennn  13342  evenennn  13343  mulgnndir  14014  mulgnnass  14020  znrrg  15105  efnthr  16188  logbgcd1irraplemap  16217  log2tlbndlog2  16232  birthdaylem2  16238  birthdaylem3  16239  pellexlem2  16242  wilthlem1  16244  0sgm  16266  mpodvdsmulf1o  16296  1sgmprm  16300  1sgm2ppw  16301  chtublem  16307  mersenne  16309  perfect1  16310  perfectlem1  16311  perfectlem2  16312  perfect  16313  bcmono  16316  bcp1ctr  16318  bclbnd  16319  bposlem1  16323  bposlem2  16324  bposlem3  16325  bposlem5  16327  bposlem6  16328  lgsval2lem  16346  gausslemma2dlem6  16403  gausslemma2dlem7  16404  gausslemma2d  16405  lgseisenlem1  16406  lgseisenlem4  16409  lgsquadlem1  16413  lgsquadlem2  16414  lgsquadlem3  16415  lgsquad2  16419  m1lgs  16421  2sqlem3  16453  2sqlem4  16454  trilpolemeq1  17308  trilpolemlt1  17309  redcwlpolemeq1  17323  nconstwlpolemgt0  17333