Theorem 2m1e1 12353

Description: 2 - 1 = 1. The result is on the right-hand-side to be consistent with similar proofs like 4p4e8 12383. (Contributed by David A. Wheeler, 4-Jan-2017.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)

Assertion

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

Proof of Theorem 2m1e1

Step	Hyp	Ref	Expression
1		ax-1cn 11146	. 2 ⊢ 1 ∈ ℂ
2		df-2 12291	. 2 ⊢ 2 = (1 + 1)
3	1, 1, 2	mvrladdi 11463	1 ⊢ (2 − 1) = 1

Syntax hints:   = wceq 1563  (class class class)co 7400  1c1 11089   − cmin 11429  2c2 12283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5250  ax-nul 5260  ax-pow 5326  ax-pr 5394  ax-un 7722  ax-resscn 11145  ax-1cn 11146  ax-icn 11147  ax-addcl 11148  ax-addrcl 11149  ax-mulcl 11150  ax-mulrcl 11151  ax-mulcom 11152  ax-addass 11153  ax-mulass 11154  ax-distr 11155  ax-i2m1 11156  ax-1ne0 11157  ax-1rid 11158  ax-rnegex 11159  ax-rrecex 11160  ax-cnre 11161  ax-pre-lttri 11162  ax-pre-lttrn 11163  ax-pre-ltadd 11164

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5105  df-opab 5167  df-mpt 5186  df-id 5546  df-po 5559  df-so 5560  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-riota 7357  df-ov 7403  df-oprab 7404  df-mpo 7405  df-er 8682  df-en 8932  df-dom 8933  df-sdom 8934  df-pnf 11233  df-mnf 11234  df-ltxr 11236  df-sub 11431  df-2 12291

This theorem is referenced by:  1e2m1  12355  subhalfhalf  12466  addltmul  12468  xp1d2m1eqxm1d2  12486  nn0lt2  12647  nn0le2is012  12648  zeo  12670  ge2halflem1  13121  fzo0to2pr  13767  fzosplitprm1  13795  bcn2  14343  lsws2  14929  swrds2m  14966  wrdl2exs2  14971  swrd2lsw  14977  geo2sum2  15916  bpolydiflem  16096  bpoly2  16099  fsumcube  16102  ege2le3  16132  cos2tsin  16223  odd2np1  16387  oddp1even  16390  oddge22np1  16395  prmdiv  16832  vfermltlALT  16850  prmo2  17088  ex-chn2  18682  htpycc  25096  pco1  25131  pcohtpylem  25135  pcopt  25138  pcorevlem  25142  cos2pi  26595  atans2  27050  log2ublem3  27067  ppiprm  27269  ppinprm  27270  chtprm  27271  chtnprm  27272  chtublem  27329  chtub  27330  lgslem4  27418  gausslemma2dlem1a  27483  lgseisenlem1  27493  2lgslem3c  27516  2sq2  27551  rplogsumlem1  27602  logdivsum  27651  log2sumbnd  27662  axlowdim  29216  wwlksnextwrd  30151  rusgrnumwwlkl1  30225  clwlkclwwlklem2a1  30248  clwlkclwwlklem2a4  30253  clwlkclwwlklem2  30256  clwlkclwwlklem3  30257  clwwlkn2  30300  clwwlkext2edg  30312  numclwlk2lem2f  30633  frgrregord013  30651  ex-fl  30703  xnn01gt  33023  wrdt2ind  33181  cshw1s2  33188  cyc2fv1  33349  cyc2fv2  33350  archirngz  33417  cos9thpiminplylem5  34088  eulerpartlemd  34668  fibp1  34703  fib3  34705  ballotlem2  34791  subfacp1lem5  35542  dnibndlem10  36933  dvasin  38210  areacirclem1  38214  lcm2un  42638  lcmineqlem22  42674  aks4d1p1p6  42697  aks4d1p1p5  42699  aks4d1p1  42700  5bc2eq10  42766  readvrec2  42977  trclfvdecomr  44311  hashnzfz2  44890  lhe4.4ex1a  44898  infleinflem2  45945  sumnnodd  46205  stoweidlem26  46599  wallispilem4  46641  wallispi2lem1  46644  wallispi2lem2  46645  fouriersw  46804  modp2nep1  47966  modm1nem2  47968  fmtnorec2lem  48150  fmtnorec3  48156  fmtnorec4  48157  m5prm  48206  sfprmdvdsmersenne  48211  lighneallem3  48215  3exp4mod41  48224  gpg3nbgrvtx0  48697  pgnbgreunbgrlem2lem1  48735  pgnbgreunbgrlem2lem2  48736  2nodd  48793  nnolog2flm1  49222