Theorem div1d 11143

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

Step	Hyp	Ref	Expression
1		div1d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		div1 11064	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 / 1) = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 / 1) = 𝐴)

Syntax hints:   → wi 4   = wceq 1601   ∈ wcel 2106  (class class class)co 6922  ℂcc 10270  1c1 10273   / cdiv 11032

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-8 2108  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348  ax-pre-mulgt0 10349

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2550  df-eu 2586  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ne 2969  df-nel 3075  df-ral 3094  df-rex 3095  df-reu 3096  df-rmo 3097  df-rab 3098  df-v 3399  df-sbc 3652  df-csb 3751  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-nul 4141  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4672  df-br 4887  df-opab 4949  df-mpt 4966  df-id 5261  df-po 5274  df-so 5275  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-er 8026  df-en 8242  df-dom 8243  df-sdom 8244  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-sub 10608  df-neg 10609  df-div 11033

This theorem is referenced by:  zq  12101  zqOLD  12102  divlt1lt  12208  divle1le  12209  nnledivrp  12251  modfrac  13002  iexpcyc  13288  geo2sum2  15009  fallfacfac  15178  bpolysum  15186  sin01gt0  15322  bits0  15556  cncongrcoprm  15789  isprm6  15830  divdenle  15861  qden1elz  15869  pczpre  15956  prmreclem2  16025  mul4sq  16062  psgnunilem4  18301  znidomb  20305  iblcnlem1  23991  itgcnlem  23993  iblabsr  24033  iblmulc2  24034  aaliou2b  24533  aaliou3lem3  24536  tayl0  24553  logtayl2  24845  root1cj  24937  elogb  24948  logblog  24970  ang180lem4  24990  isosctrlem3  24998  dquartlem1  25029  efrlim  25148  amgmlem  25168  fsumharmonic  25190  lgamgulmlem5  25211  lgamcvg2  25233  1sgm2ppw  25377  logexprlim  25402  perfectlem2  25407  sum2dchr  25451  dchrvmasum2lem  25637  dchrisum0flblem2  25650  dchrisum0lem1  25657  mulog2sumlem2  25676  selbergb  25690  selberg2b  25693  selberg3lem1  25698  selberg3lem2  25699  pntrmax  25705  pntrlog2bndlem2  25719  pntrlog2bndlem4  25721  pntrlog2bndlem6a  25723  pntrlog2bnd  25725  pntlemk  25747  kbpj  29387  faclimlem1  32223  knoppndvlem17  33101  iblmulc2nc  34084  expgrowth  39472  bccn1  39481  binomcxplemnotnn0  39493  ltdivgt1  40462  0ellimcdiv  40771  sinaover2ne0  40989  dvnxpaek  41067  stoweidlem7  41133  stoweidlem36  41162  stoweidlem42  41168  stoweidlem51  41177  stoweidlem59  41185  stirlinglem6  41205  stirlinglem7  41206  stirlinglem10  41209  stirlinglem15  41214  dirkertrigeq  41227  fourierdlem60  41292  fourierdlem61  41293  etransclem14  41374  etransclem24  41384  etransclem25  41385  etransclem35  41395  bits0ALTV  42597  perfectALTVlem2  42638  0dig2nn0e  43403  0dig2nn0o  43404  line2  43470  amgmwlem  43636