Theorem 1div1e1 10288

Description: 1 divided by 1 is 1 (common case). (Contributed by David A. Wheeler, 7-Dec-2018.)

Assertion

Ref	Expression
1div1e1	|- ( 1 / 1 ) = 1

Proof of Theorem 1div1e1

Step	Hyp	Ref	Expression
1		ax-1cn 9583	. 2 |- 1 e. CC
2		div1 10287	. 2 |- ( 1 e. CC -> ( 1 / 1 ) = 1 )
3	1, 2	ax-mp 5	1 |- ( 1 / 1 ) = 1

Syntax hints:   = wceq 1447   e. wcel 1890  (class class class)co 6275   CCcc 9523   1c1 9526   / cdiv 10257

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1672  ax-4 1685  ax-5 1761  ax-6 1808  ax-7 1854  ax-8 1892  ax-9 1899  ax-10 1918  ax-11 1923  ax-12 1936  ax-13 2091  ax-ext 2431  ax-sep 4496  ax-nul 4505  ax-pow 4553  ax-pr 4611  ax-un 6570  ax-resscn 9582  ax-1cn 9583  ax-icn 9584  ax-addcl 9585  ax-addrcl 9586  ax-mulcl 9587  ax-mulrcl 9588  ax-mulcom 9589  ax-addass 9590  ax-mulass 9591  ax-distr 9592  ax-i2m1 9593  ax-1ne0 9594  ax-1rid 9595  ax-rnegex 9596  ax-rrecex 9597  ax-cnre 9598  ax-pre-lttri 9599  ax-pre-lttrn 9600  ax-pre-ltadd 9601  ax-pre-mulgt0 9602

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 987  df-3an 988  df-tru 1450  df-ex 1667  df-nf 1671  df-sb 1801  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 3014  df-sbc 3235  df-csb 3331  df-dif 3374  df-un 3376  df-in 3378  df-ss 3385  df-nul 3699  df-if 3849  df-pw 3920  df-sn 3936  df-pr 3938  df-op 3942  df-uni 4168  df-br 4374  df-opab 4433  df-mpt 4434  df-id 4726  df-po 4732  df-so 4733  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-iota 5524  df-fun 5562  df-fn 5563  df-f 5564  df-f1 5565  df-fo 5566  df-f1o 5567  df-fv 5568  df-riota 6237  df-ov 6278  df-oprab 6279  df-mpt2 6280  df-er 7349  df-en 7556  df-dom 7557  df-sdom 7558  df-pnf 9663  df-mnf 9664  df-xr 9665  df-ltxr 9666  df-le 9667  df-sub 9848  df-neg 9849  df-div 10258

This theorem is referenced by:  recdiv  10301  reclt1  10489  recgt1  10490  halflt1  10820  expneg  12273  m1expcl2  12287  1exp  12294  resqrex  13324  trireciplem  13930  fproddiv  14025  ef0lem  14143  eft0val  14176  m1expaddsub  17149  gzrngunit  19043  cnmsgnsubg  19155  psgninv  19160  vitali  22582  advlogexp  23611  logtayllem  23615  efrlim  23906  emcllem2  23933  emcllem7  23938  logexprlim  24164  dchrinvcl  24192  bclbnd  24219  lgseisenlem1  24288  lgseisenlem2  24289  lgsquadlem1  24293  dchrmusum2  24343  dchrvmasum2lem  24345  mulogsum  24381  pntrsumo1  24414  pnt2  24462  pnt  24463  qqh1  28795  faclimlem1  30384  faclim  30387  pellexlem2  35675  elpell1qr2  35719  bccn0  36692  binomcxplemradcnv  36701  mccl  37719  dvnprodlem3  37864  stoweidlem13  37929  stoweidlem42  37959  fourierdlem62  38088  sec0  40804