Theorem 2m1e1 12266

Description: 2 - 1 = 1. The result is on the right-hand-side to be consistent with similar proofs like 4p4e8 12295. (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 12220	. 2 ⊢ 2 ∈ ℂ
2		ax-1cn 11084	. 2 ⊢ 1 ∈ ℂ
3		1p1e2 12265	. 2 ⊢ (1 + 1) = 2
4	1, 2, 2, 3	subaddrii 11470	1 ⊢ (2 − 1) = 1

Syntax hints:   = wceq 1541  (class class class)co 7358  1c1 11027   − cmin 11364  2c2 12200

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-mulcom 11090  ax-addass 11091  ax-mulass 11092  ax-distr 11093  ax-i2m1 11094  ax-1ne0 11095  ax-1rid 11096  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099  ax-pre-lttri 11100  ax-pre-lttrn 11101  ax-pre-ltadd 11102

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-po 5532  df-so 5533  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-er 8635  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11168  df-mnf 11169  df-ltxr 11171  df-sub 11366  df-2 12208

This theorem is referenced by:  1e2m1  12267  subhalfhalf  12375  addltmul  12377  xp1d2m1eqxm1d2  12395  nn0lt2  12555  nn0le2is012  12556  zeo  12578  ge2halflem1  13022  fzo0to2pr  13666  fzosplitprm1  13694  bcn2  14242  lsws2  14827  swrds2m  14864  wrdl2exs2  14869  swrd2lsw  14875  geo2sum2  15797  bpolydiflem  15977  bpoly2  15980  fsumcube  15983  ege2le3  16013  cos2tsin  16104  odd2np1  16268  oddp1even  16271  oddge22np1  16276  prmdiv  16712  vfermltlALT  16730  prmo2  16968  ex-chn2  18561  htpycc  24935  pco1  24971  pcohtpylem  24975  pcopt  24978  pcorevlem  24982  cos2pi  26441  atans2  26897  log2ublem3  26914  ppiprm  27117  ppinprm  27118  chtprm  27119  chtnprm  27120  chtublem  27178  chtub  27179  lgslem4  27267  gausslemma2dlem1a  27332  lgseisenlem1  27342  2lgslem3c  27365  2sq2  27400  rplogsumlem1  27451  logdivsum  27500  log2sumbnd  27511  axlowdim  29034  wwlksnextwrd  29970  rusgrnumwwlkl1  30044  clwlkclwwlklem2a1  30067  clwlkclwwlklem2a4  30072  clwlkclwwlklem2  30075  clwlkclwwlklem3  30076  clwwlkn2  30119  clwwlkext2edg  30131  numclwlk2lem2f  30452  frgrregord013  30470  ex-fl  30522  xnn01gt  32850  wrdt2ind  33035  cshw1s2  33042  cyc2fv1  33203  cyc2fv2  33204  archirngz  33271  cos9thpiminplylem5  33943  eulerpartlemd  34523  fibp1  34558  fib3  34560  ballotlem2  34646  subfacp1lem5  35378  dnibndlem10  36687  dvasin  37905  areacirclem1  37909  lcm2un  42268  lcmineqlem22  42304  aks4d1p1p6  42327  aks4d1p1p5  42329  aks4d1p1  42330  5bc2eq10  42396  readvrec2  42616  trclfvdecomr  43969  hashnzfz2  44562  lhe4.4ex1a  44570  infleinflem2  45615  sumnnodd  45876  stoweidlem26  46270  wallispilem4  46312  wallispi2lem1  46315  wallispi2lem2  46316  fouriersw  46475  modp2nep1  47613  modm1nem2  47615  fmtnorec2lem  47788  fmtnorec3  47794  fmtnorec4  47795  m5prm  47844  sfprmdvdsmersenne  47849  lighneallem3  47853  3exp4mod41  47862  gpg3nbgrvtx0  48322  pgnbgreunbgrlem2lem1  48360  pgnbgreunbgrlem2lem2  48361  2nodd  48418  nnolog2flm1  48836