Theorem 2m1e1 11764

Description: 2 - 1 = 1. The result is on the right-hand-side to be consistent with similar proofs like 4p4e8 11793. (Contributed by David A. Wheeler, 4-Jan-2017.)

Assertion

Ref	Expression
2m1e1	⊢ (2 − 1) = 1

Proof of Theorem 2m1e1

Step	Hyp	Ref	Expression
1		2cn 11713	. 2 ⊢ 2 ∈ ℂ
2		ax-1cn 10595	. 2 ⊢ 1 ∈ ℂ
3		1p1e2 11763	. 2 ⊢ (1 + 1) = 2
4	1, 2, 2, 3	subaddrii 10975	1 ⊢ (2 − 1) = 1

Syntax hints:   = wceq 1537  (class class class)co 7156  1c1 10538   − cmin 10870  2c2 11693

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-mulcom 10601  ax-addass 10602  ax-mulass 10603  ax-distr 10604  ax-i2m1 10605  ax-1ne0 10606  ax-1rid 10607  ax-rnegex 10608  ax-rrecex 10609  ax-cnre 10610  ax-pre-lttri 10611  ax-pre-lttrn 10612  ax-pre-ltadd 10613

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-po 5474  df-so 5475  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-er 8289  df-en 8510  df-dom 8511  df-sdom 8512  df-pnf 10677  df-mnf 10678  df-ltxr 10680  df-sub 10872  df-2 11701

This theorem is referenced by:  1e2m1  11765  1mhlfehlf  11857  subhalfhalf  11872  addltmul  11874  xp1d2m1eqxm1d2  11892  nn0lt2  12046  nn0le2is012  12047  zeo  12069  fzo0to2pr  13123  fzosplitprm1  13148  bcn2  13680  lsws2  14266  swrds2m  14303  wrdl2exs2  14308  swrd2lsw  14314  geo2sum2  15230  bpolydiflem  15408  bpoly2  15411  fsumcube  15414  ege2le3  15443  cos2tsin  15532  odd2np1  15690  oddp1even  15693  oddge22np1  15698  prmdiv  16122  vfermltlALT  16139  prmo2  16376  htpycc  23584  pco1  23619  pcohtpylem  23623  pcopt  23626  pcorevlem  23630  cos2pi  25062  atans2  25509  log2ublem3  25526  ppiprm  25728  ppinprm  25729  chtprm  25730  chtnprm  25731  chtublem  25787  chtub  25788  lgslem4  25876  gausslemma2dlem1a  25941  lgseisenlem1  25951  2lgslem3c  25974  2sq2  26009  rplogsumlem1  26060  logdivsum  26109  log2sumbnd  26120  axlowdim  26747  wwlksnextwrd  27675  rusgrnumwwlkl1  27747  clwlkclwwlklem2a1  27770  clwlkclwwlklem2a4  27775  clwlkclwwlklem2  27778  clwlkclwwlklem3  27779  clwwlkn2  27822  clwwlkext2edg  27835  numclwlk2lem2f  28156  frgrregord013  28174  ex-fl  28226  xnn01gt  30495  wrdt2ind  30627  cshw1s2  30634  cyc2fv1  30763  cyc2fv2  30764  archirngz  30818  eulerpartlemd  31624  fibp1  31659  fib3  31661  ballotlem2  31746  subfacp1lem5  32431  dnibndlem10  33826  dvasin  34993  areacirclem1  34997  lcm2un  39135  2xp3dxp2ge1d  39146  trclfvdecomr  40122  hashnzfz2  40702  lhe4.4ex1a  40710  infleinflem2  41688  sumnnodd  41960  stoweidlem26  42360  wallispilem4  42402  wallispi2lem1  42405  wallispi2lem2  42406  fouriersw  42565  fmtnorec2lem  43753  fmtnorec3  43759  fmtnorec4  43760  m5prm  43810  sfprmdvdsmersenne  43817  lighneallem3  43821  3exp4mod41  43830  2nodd  44128  nnolog2flm1  44699