Theorem nncnd 9301

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

Syntax hints:   → wi 4   ∈ wcel 2209  ℂcc 8171  ℕcn 9287

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 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 4247  ax-cnex 8264  ax-resscn 8265  ax-1re 8267  ax-addrcl 8270

This theorem 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 3969  df-inn 9288

This theorem is referenced by:  peano5uzti  9737  qapne  10022  ltesubnnd  10153  qtri3or  10658  exbtwnzlemstep  10665  intfracq  10740  flqdiv  10741  modqmulnn  10762  addmodid  10792  modaddmodup  10807  modsumfzodifsn  10816  addmodlteq  10818  facdiv  11159  facndiv  11160  faclbnd  11162  faclbnd6  11165  facubnd  11166  facavg  11167  bccmpl  11175  bcn0  11176  bcn1  11179  bcm1k  11181  bcp1n  11182  bcp1nk  11183  bcval5  11184  bcpasc  11187  permnn  11193  hashf1  11270  hashfac  11271  cvg1nlemcxze  11731  cvg1nlemcau  11733  resqrexlemcalc3  11765  binom11  12236  binom1dif  12237  divcnv  12247  arisum2  12249  trireciplem  12250  trirecip  12251  expcnvap0  12252  geo2sum  12264  geo2lim  12266  cvgratnnlembern  12273  cvgratnnlemnexp  12274  cvgratnnlemmn  12275  cvgratnnlemsumlt  12278  cvgratnnlemfm  12279  cvgratnnlemrate  12280  cvgratz  12282  eftcl  12404  eftabs  12406  efcllemp  12408  ege2le3  12421  efcj  12423  efaddlem  12424  eftlub  12440  eirraplem  12527  oexpneg  12627  divalglemnn  12668  bitsp1  12701  bitsfzolem  12704  bitsfzo  12705  bitsmod  12706  bitscmp  12708  bitsinv1lem  12711  bitsinv1  12712  dvdsgcdidd  12754  bezoutlemnewy  12756  mulgcd  12776  rplpwr  12787  sqgcd  12789  lcmgcdlem  12838  3lcm2e6woprm  12847  cncongr1  12864  cncongr2  12865  prmind2  12881  isprm5  12903  divgcdodd  12904  prmdvdsexpr  12911  sqrt2irrlem  12922  oddpwdclemxy  12930  oddpwdclemodd  12933  oddpwdclemdc  12934  oddpwdc  12935  sqpweven  12936  2sqpwodd  12937  sqrt2irraplemnn  12940  sqrt2irrap  12941  qmuldeneqnum  12956  divnumden  12957  qnumgt0  12959  numdensq  12963  hashdvds  12982  phiprmpw  12983  prmdiv  12996  prmdivdiv  12998  phisum  13002  modprm0  13016  pythagtriplem4  13030  pythagtriplem6  13032  pythagtriplem7  13033  pythagtriplem14  13039  pythagtriplem15  13040  pythagtriplem16  13041  pythagtriplem19  13044  pythagtrip  13045  pcprendvds2  13053  pcpre1  13054  pcpremul  13055  pceulem  13056  pcdiv  13064  pcqmul  13065  pcelnn  13083  pcid  13086  pc2dvds  13092  dvdsprmpweqnn  13098  dvdsprmpweqle  13099  pcaddlem  13101  pcadd  13102  pcfaclem  13111  qexpz  13114  expnprm  13115  oddprmdvds  13116  prmpwdvds  13117  pockthlem  13118  pockthg  13119  infpnlem1  13121  4sqlem6  13145  4sqlem7  13146  4sqlem10  13149  mul4sqlem  13155  4sqlem11  13163  4sqlem12  13164  4sqlem14  13166  4sqlem17  13169  4sqlem18  13170  ballotfilemfc0  13215  ballotfilemfcc  13216  oddennn  13266  evenennn  13267  mulgnndir  13937  mulgnnass  13943  znrrg  14978  logbgcd1irraplemap  16054  log2tlbndlog2  16065  birthdaylem2  16071  birthdaylem3  16072  pellexlem2  16075  wilthlem1  16077  0sgm  16082  mpodvdsmulf1o  16087  1sgmprm  16091  1sgm2ppw  16092  mersenne  16094  perfect1  16095  perfectlem1  16096  perfectlem2  16097  perfect  16098  lgsval2lem  16112  gausslemma2dlem6  16169  gausslemma2dlem7  16170  gausslemma2d  16171  lgseisenlem1  16172  lgseisenlem4  16175  lgsquadlem1  16179  lgsquadlem2  16180  lgsquadlem3  16181  lgsquad2  16185  m1lgs  16187  2sqlem3  16219  2sqlem4  16220  trilpolemeq1  17063  trilpolemlt1  17064  redcwlpolemeq1  17078  nconstwlpolemgt0  17088