Theorem 2m1e1 10752

Description: 2 - 1 = 1. The result is on the right-hand-side to be consistent with similar proofs like 4p4e8 10775. (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 10708	. 2 |- 2 e. CC
2		ax-1cn 9623	. 2 |- 1 e. CC
3		1p1e2 10751	. 2 |- ( 1 + 1 ) = 2
4	1, 2, 2, 3	subaddrii 9990	1 |- ( 2 - 1 ) = 1

Syntax hints:   = wceq 1455  (class class class)co 6315   1c1 9566   - cmin 9886   2c2 10687

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-resscn 9622  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-mulcom 9629  ax-addass 9630  ax-mulass 9631  ax-distr 9632  ax-i2m1 9633  ax-1ne0 9634  ax-1rid 9635  ax-rnegex 9636  ax-rrecex 9637  ax-cnre 9638  ax-pre-lttri 9639  ax-pre-lttrn 9640  ax-pre-ltadd 9641

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4417  df-opab 4476  df-mpt 4477  df-id 4768  df-po 4774  df-so 4775  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6277  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-er 7389  df-en 7596  df-dom 7597  df-sdom 7598  df-pnf 9703  df-mnf 9704  df-ltxr 9706  df-sub 9888  df-2 10696

This theorem is referenced by:  1e2m1  10753  1mhlfehlf  10861  addltmul  10877  nn0lt2  11029  zeo  11050  fzo0to2pr  12029  bcn2  12536  lsws2  13035  wrdl2exs2  13071  swrd2lsw  13076  geo2sum2  13979  bpolydiflem  14156  bpoly2  14159  bpoly4  14161  fsumcube  14162  ege2le3  14193  cos2tsin  14282  odd2np1  14414  oddp1even  14416  prmdiv  14782  vfermltlALT  14802  prmo2  15047  htpycc  22060  pco1  22095  pcohtpylem  22099  pcopt  22102  pcorevlem  22106  cos2pi  23480  atans2  23906  log2ublem3  23923  ppiprm  24127  ppinprm  24128  chtprm  24129  chtnprm  24130  chtublem  24188  chtub  24189  lgslem4  24276  lgseisenlem1  24326  rplogsumlem1  24371  logdivsum  24420  log2sumbnd  24431  axlowdim  25040  wlkntrllem2  25339  wwlkextwrd  25505  clwwlkn2  25552  clwlkisclwwlklem2a1  25556  clwlkisclwwlklem2a4  25561  clwlkisclwwlklem1  25564  clwlkisclwwlklem0  25565  clwwlkext2edg  25579  rusgranumwlkl1  25724  frgrawopreglem2  25822  numclwwlkovf2ex  25863  numclwlk1lem2foa  25868  numclwlk2lem2f  25880  frgraregord013  25895  ex-fl  25946  archirngz  28555  eulerpartlemd  29248  fibp1  29283  fib3  29285  ballotlem2  29370  subfacp1lem5  29956  dvasin  32073  areacirclem1  32077  trclfvdecomr  36365  hashnzfz2  36714  lhe4.4ex1a  36722  sumnnodd  37748  stoweidlem26  37924  wallispilem4  37968  wallispi2lem1  37971  wallispi2lem2  37972  fouriersw  38133  xp1d2m1eqxm1d2  38749  3exp4mod41  38954  2nodd  40085  nn0le2is012  40421  nnolog2flm1  40674