Theorem dividd 12021

Description: A number divided by itself is one. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
div1d.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
reccld.2	⊢ (𝜑 → 𝐴 ≠ 0)

Assertion

Ref	Expression
dividd	⊢ (𝜑 → (𝐴 / 𝐴) = 1)

Proof of Theorem dividd

Step	Hyp	Ref	Expression
1		div1d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		reccld.2	. 2 ⊢ (𝜑 → 𝐴 ≠ 0)
3		divid 11934	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (𝐴 / 𝐴) = 1)
4	1, 2, 3	syl2anc 582	1 ⊢ (𝜑 → (𝐴 / 𝐴) = 1)

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098   ≠ wne 2929  (class class class)co 7419  ℂcc 11138  0cc0 11140  1c1 11141   / cdiv 11903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-resscn 11197  ax-1cn 11198  ax-icn 11199  ax-addcl 11200  ax-addrcl 11201  ax-mulcl 11202  ax-mulrcl 11203  ax-mulcom 11204  ax-addass 11205  ax-mulass 11206  ax-distr 11207  ax-i2m1 11208  ax-1ne0 11209  ax-1rid 11210  ax-rnegex 11211  ax-rrecex 11212  ax-cnre 11213  ax-pre-lttri 11214  ax-pre-lttrn 11215  ax-pre-ltadd 11216  ax-pre-mulgt0 11217

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5576  df-po 5590  df-so 5591  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-er 8725  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11282  df-mnf 11283  df-xr 11284  df-ltxr 11285  df-le 11286  df-sub 11478  df-neg 11479  df-div 11904

This theorem is referenced by:  nndivtr  12292  divge1  13077  xov1plusxeqvd  13510  quoremz  13856  quoremnn0ALT  13858  intfracq  13860  fldiv  13861  modid0  13898  bcn0  14305  abs1m  15318  georeclim  15854  efaddlem  16073  sqgcd  16539  prmind2  16659  divgcdodd  16684  divnumden  16723  hashgcdlem  16760  pythagtriplem19  16805  pc2dvds  16851  fldivp1  16869  abv1z  20724  dveflem  25955  dvlip  25970  elqaalem2  26300  aareccl  26306  cos02pilt1  26505  efeq1  26507  eff1olem  26527  eflogeq  26581  tanarg  26598  logcnlem4  26624  cxpaddle  26732  logbid1  26745  isosctrlem3  26797  angpieqvdlem  26805  dcubic2  26821  2efiatan  26895  atantan  26900  birthdaylem2  26929  efrlim  26946  efrlimOLD  26947  jensenlem2  26965  logdifbnd  26971  logdiflbnd  26972  emcllem2  26974  emcllem3  26975  emcllem5  26977  dmgmdivn0  27005  lgamgulmlem2  27007  lgamgulmlem5  27010  lgamcvg2  27032  lgam1  27041  basellem8  27065  vmalogdivsum2  27516  2vmadivsumlem  27518  selberg4lem1  27538  pntrmax  27542  pntrlog2bndlem2  27556  pntrlog2bndlem5  27559  pntibndlem2  27569  pntlem3  27587  brbtwn2  28788  axsegconlem10  28809  axpaschlem  28823  axcontlem8  28854  cndprobtot  34187  cvmliftlem11  35036  divcnvlin  35458  iprodgam  35467  faclim2  35473  poimirlem32  37256  dvtan  37274  areacirc  37317  lcmineqlem18  41649  aks4d1p1p7  41677  aks4d1p5  41683  aks6d1c1  41719  expgcd  42029  irrapxlem5  42388  pellexlem6  42396  pell14qrexpclnn0  42428  reglogbas  42457  imo72b2  43744  binomcxplemrat  43929  divcan8d  44832  mccllem  45123  clim1fr1  45127  coseq0  45390  dvnxpaek  45468  stoweidlem1  45527  stoweidlem11  45537  stoweidlem26  45552  wallispilem5  45595  stirlinglem1  45600  stirlinglem3  45602  stirlinglem4  45603  stirlinglem6  45605  stirlinglem7  45606  stirlinglem10  45609  dirkertrigeqlem3  45626  dirkercncflem1  45629  fourierdlem4  45637  fourierdlem6  45639  fourierdlem26  45659  fourierdlem65  45697  etransclem35  45795  sharhght  46391  eenglngeehlnmlem1  47996  eenglngeehlnmlem2  47997  cotsqcscsq  48379