Theorem dividd 11741

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 11654	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (𝐴 / 𝐴) = 1)
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝐴 / 𝐴) = 1)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2110   ≠ wne 2945  (class class class)co 7269  ℂcc 10862  0cc0 10864  1c1 10865   / cdiv 11624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pow 5292  ax-pr 5356  ax-un 7580  ax-resscn 10921  ax-1cn 10922  ax-icn 10923  ax-addcl 10924  ax-addrcl 10925  ax-mulcl 10926  ax-mulrcl 10927  ax-mulcom 10928  ax-addass 10929  ax-mulass 10930  ax-distr 10931  ax-i2m1 10932  ax-1ne0 10933  ax-1rid 10934  ax-rnegex 10935  ax-rrecex 10936  ax-cnre 10937  ax-pre-lttri 10938  ax-pre-lttrn 10939  ax-pre-ltadd 10940  ax-pre-mulgt0 10941

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-nel 3052  df-ral 3071  df-rex 3072  df-reu 3073  df-rmo 3074  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5163  df-id 5489  df-po 5503  df-so 5504  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6389  df-fun 6433  df-fn 6434  df-f 6435  df-f1 6436  df-fo 6437  df-f1o 6438  df-fv 6439  df-riota 7226  df-ov 7272  df-oprab 7273  df-mpo 7274  df-er 8473  df-en 8709  df-dom 8710  df-sdom 8711  df-pnf 11004  df-mnf 11005  df-xr 11006  df-ltxr 11007  df-le 11008  df-sub 11199  df-neg 11200  df-div 11625

This theorem is referenced by:  nndivtr  12012  divge1  12789  xov1plusxeqvd  13221  quoremz  13565  quoremnn0ALT  13567  intfracq  13569  fldiv  13570  modid0  13607  bcn0  14014  abs1m  15037  georeclim  15574  efaddlem  15792  sqgcd  16260  prmind2  16380  divgcdodd  16405  divnumden  16442  hashgcdlem  16479  pythagtriplem19  16524  pc2dvds  16570  fldivp1  16588  abv1z  20082  dveflem  25133  dvlip  25147  elqaalem2  25470  aareccl  25476  cos02pilt1  25672  efeq1  25674  eff1olem  25694  eflogeq  25747  tanarg  25764  logcnlem4  25790  cxpaddle  25895  logbid1  25908  isosctrlem3  25960  angpieqvdlem  25968  dcubic2  25984  2efiatan  26058  atantan  26063  birthdaylem2  26092  efrlim  26109  jensenlem2  26127  logdifbnd  26133  logdiflbnd  26134  emcllem2  26136  emcllem3  26137  emcllem5  26139  dmgmdivn0  26167  lgamgulmlem2  26169  lgamgulmlem5  26172  lgamcvg2  26194  lgam1  26203  basellem8  26227  vmalogdivsum2  26676  2vmadivsumlem  26678  selberg4lem1  26698  pntrmax  26702  pntrlog2bndlem2  26716  pntrlog2bndlem5  26719  pntibndlem2  26729  pntlem3  26747  brbtwn2  27263  axsegconlem10  27284  axpaschlem  27298  axcontlem8  27329  cndprobtot  32391  cvmliftlem11  33245  divcnvlin  33686  iprodgam  33696  faclim2  33702  poimirlem32  35797  dvtan  35815  areacirc  35858  lcmineqlem18  40043  aks4d1p1p7  40071  aks4d1p5  40077  expgcd  40323  irrapxlem5  40637  pellexlem6  40645  pell14qrexpclnn0  40677  reglogbas  40706  imo72b2  41745  binomcxplemrat  41930  divcan8d  42814  mccllem  43101  clim1fr1  43105  coseq0  43368  dvnxpaek  43446  stoweidlem1  43505  stoweidlem11  43515  stoweidlem26  43530  wallispilem5  43573  stirlinglem1  43578  stirlinglem3  43580  stirlinglem4  43581  stirlinglem6  43583  stirlinglem7  43584  stirlinglem10  43587  dirkertrigeqlem3  43604  dirkercncflem1  43607  fourierdlem4  43615  fourierdlem6  43617  fourierdlem26  43637  fourierdlem65  43675  etransclem35  43773  sharhght  44341  eenglngeehlnmlem1  46044  eenglngeehlnmlem2  46045  cotsqcscsq  46425