MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  div1d Structured version   Unicode version

Theorem div1d 10247
Description: A number divided by 1 is itself. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
div1d.1  |-  ( ph  ->  A  e.  CC )
Assertion
Ref Expression
div1d  |-  ( ph  ->  ( A  /  1
)  =  A )

Proof of Theorem div1d
StepHypRef Expression
1 div1d.1 . 2  |-  ( ph  ->  A  e.  CC )
2 div1 10171 . 2  |-  ( A  e.  CC  ->  ( A  /  1 )  =  A )
31, 2syl 16 1  |-  ( ph  ->  ( A  /  1
)  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1399    e. wcel 1836  (class class class)co 6214   CCcc 9419   1c1 9422    / cdiv 10141
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370  ax-sep 4501  ax-nul 4509  ax-pow 4556  ax-pr 4614  ax-un 6509  ax-resscn 9478  ax-1cn 9479  ax-icn 9480  ax-addcl 9481  ax-addrcl 9482  ax-mulcl 9483  ax-mulrcl 9484  ax-mulcom 9485  ax-addass 9486  ax-mulass 9487  ax-distr 9488  ax-i2m1 9489  ax-1ne0 9490  ax-1rid 9491  ax-rnegex 9492  ax-rrecex 9493  ax-cnre 9494  ax-pre-lttri 9495  ax-pre-lttrn 9496  ax-pre-ltadd 9497  ax-pre-mulgt0 9498
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2232  df-mo 2233  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-ne 2589  df-nel 2590  df-ral 2747  df-rex 2748  df-reu 2749  df-rmo 2750  df-rab 2751  df-v 3049  df-sbc 3266  df-csb 3362  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-nul 3725  df-if 3871  df-pw 3942  df-sn 3958  df-pr 3960  df-op 3964  df-uni 4177  df-br 4381  df-opab 4439  df-mpt 4440  df-id 4722  df-po 4727  df-so 4728  df-xp 4932  df-rel 4933  df-cnv 4934  df-co 4935  df-dm 4936  df-rn 4937  df-res 4938  df-ima 4939  df-iota 5473  df-fun 5511  df-fn 5512  df-f 5513  df-f1 5514  df-fo 5515  df-f1o 5516  df-fv 5517  df-riota 6176  df-ov 6217  df-oprab 6218  df-mpt2 6219  df-er 7247  df-en 7454  df-dom 7455  df-sdom 7456  df-pnf 9559  df-mnf 9560  df-xr 9561  df-ltxr 9562  df-le 9563  df-sub 9738  df-neg 9739  df-div 10142
This theorem is referenced by:  zq  11125  modfrac  11929  iexpcyc  12194  geo2sum2  13704  sin01gt0  13946  bits0  14099  isprm6  14271  divdenle  14303  qden1elz  14311  pczpre  14392  prmreclem2  14456  mul4sq  14493  psgnunilem4  16658  znidomb  18710  iblcnlem1  22298  itgcnlem  22300  iblabsr  22340  iblmulc2  22341  aaliou2b  22841  aaliou3lem3  22844  tayl0  22861  logtayl2  23149  root1cj  23236  elogb  23247  logblog  23269  ang180lem4  23281  isosctrlem3  23289  dquartlem1  23317  efrlim  23435  amgmlem  23455  fsumharmonic  23477  1sgm2ppw  23611  logexprlim  23636  perfectlem2  23641  sum2dchr  23685  dchrvmasum2lem  23817  dchrisum0flblem2  23830  dchrisum0lem1  23837  mulog2sumlem2  23856  selbergb  23870  selberg2b  23873  selberg3lem1  23878  selberg3lem2  23879  pntrmax  23885  pntrlog2bndlem2  23899  pntrlog2bndlem4  23901  pntrlog2bndlem6a  23903  pntrlog2bnd  23905  pntlemk  23927  kbpj  27012  lgamgulmlem5  28800  lgamcvg2  28822  fallfacfac  29369  faclimlem1  29370  bpolysum  30004  iblmulc2nc  30282  expgrowth  31444  bccn1  31453  binomcxplemnotnn0  31465  0ellimcdiv  31856  sinaover2ne0  31869  dvnxpaek  31940  stoweidlem7  31990  stoweidlem36  32019  stoweidlem42  32025  stoweidlem51  32034  stoweidlem59  32042  stirlinglem6  32062  stirlinglem7  32063  stirlinglem10  32066  stirlinglem15  32071  dirkertrigeq  32084  fourierdlem60  32150  fourierdlem61  32151  etransclem14  32232  etransclem24  32242  etransclem25  32243  etransclem35  32253  bits0ALTV  32556  perfectALTVlem2  32579  divlt1lt  33353  0dig2nn0e  33468  0dig2nn0o  33469
  Copyright terms: Public domain W3C validator