Theorem 2m1e1 12335

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

Syntax hints:   = wceq 1533  (class class class)co 7401  1c1 11107   − cmin 11441  2c2 12264

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-br 5139  df-opab 5201  df-mpt 5222  df-id 5564  df-po 5578  df-so 5579  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11247  df-mnf 11248  df-ltxr 11250  df-sub 11443  df-2 12272

This theorem is referenced by:  1e2m1  12336  1mhlfehlf  12428  subhalfhalf  12443  addltmul  12445  xp1d2m1eqxm1d2  12463  nn0lt2  12622  nn0le2is012  12623  zeo  12645  fzo0to2pr  13714  fzosplitprm1  13739  bcn2  14276  lsws2  14852  swrds2m  14889  wrdl2exs2  14894  swrd2lsw  14900  geo2sum2  15817  bpolydiflem  15995  bpoly2  15998  fsumcube  16001  ege2le3  16030  cos2tsin  16119  odd2np1  16281  oddp1even  16284  oddge22np1  16289  prmdiv  16717  vfermltlALT  16734  prmo2  16972  htpycc  24828  pco1  24864  pcohtpylem  24868  pcopt  24871  pcorevlem  24875  cos2pi  26328  atans2  26779  log2ublem3  26796  ppiprm  26999  ppinprm  27000  chtprm  27001  chtnprm  27002  chtublem  27060  chtub  27061  lgslem4  27149  gausslemma2dlem1a  27214  lgseisenlem1  27224  2lgslem3c  27247  2sq2  27282  rplogsumlem1  27333  logdivsum  27382  log2sumbnd  27393  axlowdim  28688  wwlksnextwrd  29620  rusgrnumwwlkl1  29691  clwlkclwwlklem2a1  29714  clwlkclwwlklem2a4  29719  clwlkclwwlklem2  29722  clwlkclwwlklem3  29723  clwwlkn2  29766  clwwlkext2edg  29778  numclwlk2lem2f  30099  frgrregord013  30117  ex-fl  30169  xnn01gt  32452  wrdt2ind  32584  cshw1s2  32591  cyc2fv1  32748  cyc2fv2  32749  archirngz  32803  eulerpartlemd  33854  fibp1  33889  fib3  33891  ballotlem2  33976  subfacp1lem5  34664  dnibndlem10  35853  dvasin  37062  areacirclem1  37066  lcm2un  41372  lcmineqlem22  41408  aks4d1p1p6  41431  aks4d1p1p5  41433  aks4d1p1  41434  5bc2eq10  41451  2xp3dxp2ge1d  41515  trclfvdecomr  42968  hashnzfz2  43569  lhe4.4ex1a  43577  infleinflem2  44566  sumnnodd  44831  stoweidlem26  45227  wallispilem4  45269  wallispi2lem1  45272  wallispi2lem2  45273  fouriersw  45432  tworepnotupword  46085  fmtnorec2lem  46695  fmtnorec3  46701  fmtnorec4  46702  m5prm  46751  sfprmdvdsmersenne  46756  lighneallem3  46760  3exp4mod41  46769  2nodd  47035  nnolog2flm1  47464