---

Step * 1 of Lemma itop_split


1. g : IMonoid
2. a : ℤ
3. b : ℤ
4. c : ℤ
⊢ (∀[E:{a..c-} ⟶ |g|]. (Π(*,e) a ≤ j < c. E[j] = (Π(*,e) a ≤ j < b. E[j] * Π(*,e) b ≤ j < c. E[j]) ∈ |g|)) supposing 
     ((b ≤ c) and 
     (a ≤ b))
BY
{ MoveToConcl 3 
THEN BackThruLemma `int_le_to_int_upper` 
THENA Auto }

1
1. g : IMonoid
2. a : ℤ
3. c : ℤ
⊢ ∀b:{a...}
    ∀[E:{a..c-} ⟶ |g|]. (Π(*,e) a ≤ j < c. E[j] = (Π(*,e) a ≤ j < b. E[j] * Π(*,e) b ≤ j < c. E[j]) ∈ |g|) 
    supposing b ≤ c

---

Latex:

---

Latex:

1.  g  :  IMonoid
2.  a  :  \mBbbZ{}
3.  b  :  \mBbbZ{}
4.  c  :  \mBbbZ{}
\mvdash{}  (\mforall{}[E:\{a..c\msupminus{}\}  {}\mrightarrow{}  |g|]
          (\mPi{}(*,e)  a  \mleq{}  j  <  c.  E[j]  =  (\mPi{}(*,e)  a  \mleq{}  j  <  b.  E[j]  *  \mPi{}(*,e)  b  \mleq{}  j  <  c.  E[j])))  supposing 
          ((b  \mleq{}  c)  and 
          (a  \mleq{}  b))


By

---

Latex:
MoveToConcl  3 
THEN  BackThruLemma  `int\_le\_to\_int\_upper` 
THENA  Auto

---

Home Index