MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2m1e1 Unicode version

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

Proof of Theorem 2m1e1
StepHypRef Expression
1 2cn 10477 . 2
2 ax-1cn 9425 . 2
3 1p1e2 10520 . 2
41, 2, 2, 3subaddrii 9782 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1370  (class class class)co 6174  1c1 9368   cmin 9680  2c2 10456
This theorem is referenced by:  1e2m1  10522  1mhlfehlf  10629  addltmul  10645  zeo  10812  fzo0to2pr  11699  bcn2  12180  swrd2lsw  12638  geo2sum2  13420  ege2le3  13461  cos2tsin  13549  odd2np1  13678  oddp1even  13680  prmdiv  13946  htpycc  20652  pco1  20687  pcohtpylem  20691  pcopt  20694  pcorevlem  20698  cos2pi  22038  atans2  22426  log2ublem3  22443  ppiprm  22589  ppinprm  22590  chtprm  22591  chtnprm  22592  chtublem  22650  chtub  22651  lgslem4  22738  lgseisenlem1  22788  rplogsumlem1  22833  logdivsum  22882  log2sumbnd  22893  axlowdim  23326  wlkntrllem2  23578  ex-fl  23773  archirngz  26324  eulerpartlemd  26867  fibp1  26902  fib3  26904  ballotlem2  26989  subfacp1lem5  27190  bpolydiflem  28315  bpoly2  28318  bpoly4  28320  fsumcube  28321  dvasin  28602  areacirclem1  28606  lhe4.4ex1a  29725  stoweidlem26  29943  wallispilem4  29985  wallispi2lem1  29988  wallispi2lem2  29989  nn0lt2  30308  wwlkextwrd  30482  clwwlkn2  30560  clwlkisclwwlklem2a1  30563  clwlkisclwwlklem2a4  30568  clwlkisclwwlklem1  30571  clwlkisclwwlklem0  30572  clwwlkext2edg  30586  rusgranumwlkl1  30681  frgrawopreglem2  30760  numclwwlkovf2ex  30801  numclwlk1lem2foa  30806  numclwlk2lem2f  30818  frgraregord013  30833  nn0le2is012  30890
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429  ax-sep 4495  ax-nul 4503  ax-pow 4552  ax-pr 4613  ax-un 6456  ax-resscn 9424  ax-1cn 9425  ax-icn 9426  ax-addcl 9427  ax-addrcl 9428  ax-mulcl 9429  ax-mulrcl 9430  ax-mulcom 9431  ax-addass 9432  ax-mulass 9433  ax-distr 9434  ax-i2m1 9435  ax-1ne0 9436  ax-1rid 9437  ax-rnegex 9438  ax-rrecex 9439  ax-cnre 9440  ax-pre-lttri 9441  ax-pre-lttrn 9442  ax-pre-ltadd 9443
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-eu 2263  df-mo 2264  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-ne 2643  df-nel 2644  df-ral 2797  df-rex 2798  df-reu 2799  df-rab 2801  df-v 3054  df-sbc 3269  df-csb 3371  df-dif 3413  df-un 3415  df-in 3417  df-ss 3424  df-nul 3720  df-if 3874  df-pw 3944  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4174  df-br 4375  df-opab 4433  df-mpt 4434  df-id 4718  df-po 4723  df-so 4724  df-xp 4928  df-rel 4929  df-cnv 4930  df-co 4931  df-dm 4932  df-rn 4933  df-res 4934  df-ima 4935  df-iota 5463  df-fun 5502  df-fn 5503  df-f 5504  df-f1 5505  df-fo 5506  df-f1o 5507  df-fv 5508  df-riota 6135  df-ov 6177  df-oprab 6178  df-mpt2 6179  df-er 7185  df-en 7395  df-dom 7396  df-sdom 7397  df-pnf 9505  df-mnf 9506  df-ltxr 9508  df-sub 9682  df-2 10465
  Copyright terms: Public domain W3C validator