---

Step * 1 1 1 2 1 1 of Lemma maxsegsum_singleton


1. x : @i
2. p : ||[x]||@i
3. q : {p..||[x]||}@i
 x  seg_sum(p;q;[x]) 
BY
{ (((Reduce 2 THEN Assert p = 0 THEN Auto) THEN (HypSubst (-1) 0 THENA Auto))
   THEN (Reduce 3 THEN Assert q = 0 THEN Auto)
   THEN (HypSubst (-1) 0 THENA Auto)) }

1
1. x : @i
2. p : 1@i
3. q : {p..1}@i
4. p = 0
5. q = 0
 x  seg_sum(0;0;[x]) 

---

Latex:



1.  x  :  \mBbbZ{}@i
2.  p  :  \mBbbN{}||[x]||@i
3.  q  :  \{p..||[x]||\msupminus{}\}@i
\mvdash{}  x  \mgeq{}  seg\_sum(p;q;[x]) 


By

(((Reduce  2  THEN  Assert  \mkleeneopen{}p  =  0\mkleeneclose{}\mcdot{}  THEN  Auto)  THEN  (HypSubst  (-1)  0  THENA  Auto))
  THEN  (Reduce  3  THEN  Assert  \mkleeneopen{}q  =  0\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  (HypSubst  (-1)  0  THENA  Auto))

---

Home Index