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

Theorem div1d 11627
Description: A number divided by 1 is itself. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
div1d.1 (𝜑𝐴 ∈ ℂ)
Assertion
Ref Expression
div1d (𝜑 → (𝐴 / 1) = 𝐴)

Proof of Theorem div1d
StepHypRef Expression
1 div1d.1 . 2 (𝜑𝐴 ∈ ℂ)
2 div1 11548 . 2 (𝐴 ∈ ℂ → (𝐴 / 1) = 𝐴)
31, 2syl 17 1 (𝜑 → (𝐴 / 1) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1543  wcel 2112  (class class class)co 7234  cc 10754  1c1 10757   / cdiv 11516
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-sep 5208  ax-nul 5215  ax-pow 5274  ax-pr 5338  ax-un 7544  ax-resscn 10813  ax-1cn 10814  ax-icn 10815  ax-addcl 10816  ax-addrcl 10817  ax-mulcl 10818  ax-mulrcl 10819  ax-mulcom 10820  ax-addass 10821  ax-mulass 10822  ax-distr 10823  ax-i2m1 10824  ax-1ne0 10825  ax-1rid 10826  ax-rnegex 10827  ax-rrecex 10828  ax-cnre 10829  ax-pre-lttri 10830  ax-pre-lttrn 10831  ax-pre-ltadd 10832  ax-pre-mulgt0 10833
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rmo 3071  df-rab 3072  df-v 3424  df-sbc 3711  df-csb 3828  df-dif 3885  df-un 3887  df-in 3889  df-ss 3899  df-nul 4254  df-if 4456  df-pw 4531  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4836  df-br 5070  df-opab 5132  df-mpt 5152  df-id 5471  df-po 5485  df-so 5486  df-xp 5574  df-rel 5575  df-cnv 5576  df-co 5577  df-dm 5578  df-rn 5579  df-res 5580  df-ima 5581  df-iota 6358  df-fun 6402  df-fn 6403  df-f 6404  df-f1 6405  df-fo 6406  df-f1o 6407  df-fv 6408  df-riota 7191  df-ov 7237  df-oprab 7238  df-mpo 7239  df-er 8414  df-en 8650  df-dom 8651  df-sdom 8652  df-pnf 10896  df-mnf 10897  df-xr 10898  df-ltxr 10899  df-le 10900  df-sub 11091  df-neg 11092  df-div 11517
This theorem is referenced by:  zq  12577  divlt1lt  12682  divle1le  12683  nnledivrp  12725  modfrac  13486  iexpcyc  13805  geo2sum2  15468  fallfacfac  15637  bpolysum  15645  sin01gt0  15781  bits0  16017  cncongrcoprm  16257  isprm6  16301  divdenle  16335  qden1elz  16343  pczpre  16430  prmreclem2  16500  mul4sq  16537  psgnunilem4  18919  znidomb  20556  iblcnlem1  24714  itgcnlem  24716  iblabsr  24756  iblmulc2  24757  aaliou2b  25263  aaliou3lem3  25266  tayl0  25283  logtayl2  25579  root1cj  25671  elogb  25682  logblog  25704  ang180lem4  25724  isosctrlem3  25732  dquartlem1  25763  efrlim  25881  amgmlem  25901  fsumharmonic  25923  lgamgulmlem5  25944  lgamcvg2  25966  1sgm2ppw  26110  logexprlim  26135  perfectlem2  26140  sum2dchr  26184  dchrvmasum2lem  26406  dchrisum0flblem2  26419  dchrisum0lem1  26426  mulog2sumlem2  26445  selbergb  26459  selberg2b  26462  selberg3lem1  26467  selberg3lem2  26468  pntrmax  26474  pntrlog2bndlem2  26488  pntrlog2bndlem4  26490  pntrlog2bndlem6a  26492  pntrlog2bnd  26494  pntlemk  26516  kbpj  30066  faclimlem1  33456  knoppndvlem17  34476  iblmulc2nc  35611  lcmineqlem11  39813  expgrowth  41661  bccn1  41670  binomcxplemnotnn0  41682  ltdivgt1  42603  0ellimcdiv  42898  sinaover2ne0  43117  dvnxpaek  43191  stoweidlem7  43256  stoweidlem36  43285  stoweidlem42  43291  stoweidlem51  43300  stoweidlem59  43308  stirlinglem6  43328  stirlinglem7  43329  stirlinglem10  43332  stirlinglem15  43337  dirkertrigeq  43350  fourierdlem60  43415  fourierdlem61  43416  etransclem14  43497  etransclem24  43507  etransclem25  43508  etransclem35  43518  bits0ALTV  44837  perfectALTVlem2  44880  0dig2nn0e  45664  0dig2nn0o  45665  line2  45804  amgmwlem  46210
  Copyright terms: Public domain W3C validator