---

Step * 2 1 1 1 1 of Lemma reg-seq-list-add_wf


1. L : ℝ List
2. n : ℕ+@i
3. m : ℕ+@i
4. x : ℝ@i
⊢ |(m * (x n)) - n * (x m)| ∈ {...2 * (n + m)}
BY
{ ((MemTypeCD THEN Auto)
   THEN D (-1)
   THEN (Unhide THENA Auto)
   THEN UnfoldTopAb (-1)
   THEN Reduce (-1)
   THEN (BHyp (-1) THEN Auto)⋅) }

---

Latex:

---

Latex:

1.  L  :  \mBbbR{}  List
2.  n  :  \mBbbN{}\msupplus{}@i
3.  m  :  \mBbbN{}\msupplus{}@i
4.  x  :  \mBbbR{}@i
\mvdash{}  |(m  *  (x  n))  -  n  *  (x  m)|  \mmember{}  \{...2  *  (n  +  m)\}


By

---

Latex:
((MemTypeCD  THEN  Auto)
  THEN  D  (-1)
  THEN  (Unhide  THENA  Auto)
  THEN  UnfoldTopAb  (-1)
  THEN  Reduce  (-1)
  THEN  (BHyp  (-1)  THEN  Auto)\mcdot{})

---

Home Index