Theorem 2m1e1 12314

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

Syntax hints:   = wceq 1540  (class class class)co 7390  1c1 11076   − cmin 11412  2c2 12248

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-po 5549  df-so 5550  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11217  df-mnf 11218  df-ltxr 11220  df-sub 11414  df-2 12256

This theorem is referenced by:  1e2m1  12315  subhalfhalf  12423  addltmul  12425  xp1d2m1eqxm1d2  12443  nn0lt2  12604  nn0le2is012  12605  zeo  12627  ge2halflem1  13075  fzo0to2pr  13718  fzosplitprm1  13745  bcn2  14291  lsws2  14877  swrds2m  14914  wrdl2exs2  14919  swrd2lsw  14925  geo2sum2  15847  bpolydiflem  16027  bpoly2  16030  fsumcube  16033  ege2le3  16063  cos2tsin  16154  odd2np1  16318  oddp1even  16321  oddge22np1  16326  prmdiv  16762  vfermltlALT  16780  prmo2  17018  htpycc  24886  pco1  24922  pcohtpylem  24926  pcopt  24929  pcorevlem  24933  cos2pi  26392  atans2  26848  log2ublem3  26865  ppiprm  27068  ppinprm  27069  chtprm  27070  chtnprm  27071  chtublem  27129  chtub  27130  lgslem4  27218  gausslemma2dlem1a  27283  lgseisenlem1  27293  2lgslem3c  27316  2sq2  27351  rplogsumlem1  27402  logdivsum  27451  log2sumbnd  27462  axlowdim  28895  wwlksnextwrd  29834  rusgrnumwwlkl1  29905  clwlkclwwlklem2a1  29928  clwlkclwwlklem2a4  29933  clwlkclwwlklem2  29936  clwlkclwwlklem3  29937  clwwlkn2  29980  clwwlkext2edg  29992  numclwlk2lem2f  30313  frgrregord013  30331  ex-fl  30383  xnn01gt  32700  wrdt2ind  32882  cshw1s2  32889  cyc2fv1  33085  cyc2fv2  33086  archirngz  33150  cos9thpiminplylem5  33783  eulerpartlemd  34364  fibp1  34399  fib3  34401  ballotlem2  34487  subfacp1lem5  35178  dnibndlem10  36482  dvasin  37705  areacirclem1  37709  lcm2un  42009  lcmineqlem22  42045  aks4d1p1p6  42068  aks4d1p1p5  42070  aks4d1p1  42071  5bc2eq10  42137  readvrec2  42356  trclfvdecomr  43724  hashnzfz2  44317  lhe4.4ex1a  44325  infleinflem2  45374  sumnnodd  45635  stoweidlem26  46031  wallispilem4  46073  wallispi2lem1  46076  wallispi2lem2  46077  fouriersw  46236  tworepnotupword  46891  modp2nep1  47372  modm1nem2  47374  fmtnorec2lem  47547  fmtnorec3  47553  fmtnorec4  47554  m5prm  47603  sfprmdvdsmersenne  47608  lighneallem3  47612  3exp4mod41  47621  gpg3nbgrvtx0  48071  pgnbgreunbgrlem2lem1  48108  pgnbgreunbgrlem2lem2  48109  2nodd  48164  nnolog2flm1  48583