Theorem nncnd 9319

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

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

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 4249  ax-cnex 8270  ax-resscn 8271  ax-1re 8273  ax-addrcl 8276

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 9306

This theorem is used by:  peano5uzti  9756  qapne  10041  ltesubnnd  10172  qtri3or  10677  exbtwnzlemstep  10684  intfracq  10759  flqdiv  10760  modqmulnn  10781  addmodid  10811  modaddmodup  10826  modsumfzodifsn  10835  addmodlteq  10837  facdiv  11178  facndiv  11179  faclbnd  11181  faclbnd6  11184  facubnd  11185  facavg  11186  bccmpl  11194  bcn0  11195  bcn1  11198  bcm1k  11200  bcp1n  11201  bcp1nk  11202  bcval5  11203  bcpasc  11206  permnn  11212  hashf1  11289  hashfac  11290  cvg1nlemcxze  11750  cvg1nlemcau  11752  resqrexlemcalc3  11784  binom11  12255  binom1dif  12256  divcnv  12266  arisum2  12268  trireciplem  12269  trirecip  12270  expcnvap0  12271  geo2sum  12283  geo2lim  12285  cvgratnnlembern  12292  cvgratnnlemnexp  12293  cvgratnnlemmn  12294  cvgratnnlemsumlt  12297  cvgratnnlemfm  12298  cvgratnnlemrate  12299  cvgratz  12301  eftcl  12423  eftabs  12425  efcllemp  12427  ege2le3  12440  efcj  12442  efaddlem  12443  eftlub  12459  eirraplem  12546  oexpneg  12646  divalglemnn  12687  bitsp1  12720  bitsfzolem  12723  bitsfzo  12724  bitsmod  12725  bitscmp  12727  bitsinv1lem  12730  bitsinv1  12731  dvdsgcdidd  12773  bezoutlemnewy  12775  mulgcd  12795  rplpwr  12806  sqgcd  12808  lcmgcdlem  12857  3lcm2e6woprm  12866  cncongr1  12883  cncongr2  12884  prmind2  12900  isprm5  12922  divgcdodd  12923  prmdvdsexpr  12930  sqrt2irrlem  12941  oddpwdclemxy  12949  oddpwdclemodd  12952  oddpwdclemdc  12953  oddpwdc  12954  sqpweven  12955  2sqpwodd  12956  sqrt2irraplemnn  12959  sqrt2irrap  12960  qmuldeneqnum  12975  divnumden  12976  qnumgt0  12978  numdensq  12982  hashdvds  13001  phiprmpw  13002  prmdiv  13015  prmdivdiv  13017  phisum  13021  modprm0  13035  pythagtriplem4  13049  pythagtriplem6  13051  pythagtriplem7  13052  pythagtriplem14  13058  pythagtriplem15  13059  pythagtriplem16  13060  pythagtriplem19  13063  pythagtrip  13064  pcprendvds2  13072  pcpre1  13073  pcpremul  13074  pceulem  13075  pcdiv  13083  pcqmul  13084  pcelnn  13102  pcid  13105  pc2dvds  13111  dvdsprmpweqnn  13117  dvdsprmpweqle  13118  pcaddlem  13120  pcadd  13121  pcfaclem  13130  qexpz  13133  expnprm  13134  oddprmdvds  13135  prmpwdvds  13136  pockthlem  13137  pockthg  13138  infpnlem1  13140  4sqlem6  13164  4sqlem7  13165  4sqlem10  13168  mul4sqlem  13174  4sqlem11  13182  4sqlem12  13183  4sqlem14  13185  4sqlem17  13188  4sqlem18  13189  ballotfilemfc0  13234  ballotfilemfcc  13235  oddennn  13285  evenennn  13286  mulgnndir  13956  mulgnnass  13962  znrrg  14997  logbgcd1irraplemap  16077  log2tlbndlog2  16088  birthdaylem2  16094  birthdaylem3  16095  pellexlem2  16098  wilthlem1  16100  0sgm  16105  mpodvdsmulf1o  16110  1sgmprm  16114  1sgm2ppw  16115  mersenne  16117  perfect1  16118  perfectlem1  16119  perfectlem2  16120  perfect  16121  bcmono  16124  bcp1ctr  16126  bclbnd  16127  lgsval2lem  16141  gausslemma2dlem6  16198  gausslemma2dlem7  16199  gausslemma2d  16200  lgseisenlem1  16201  lgseisenlem4  16204  lgsquadlem1  16208  lgsquadlem2  16209  lgsquadlem3  16210  lgsquad2  16214  m1lgs  16216  2sqlem3  16248  2sqlem4  16249  trilpolemeq1  17101  trilpolemlt1  17102  redcwlpolemeq1  17116  nconstwlpolemgt0  17126