Step * 2 of Lemma equipollent-multiply


1. : ℕ
2. : ℕ
3. p1 : ℕa
4. p2 : ℤ
5. 0 ≤ p2
6. p2 < b
⊢ p2 < (a b) p1 b
BY
(((InstLemma `mul_bounds_1a` [⌜p1⌝; ⌜b⌝])⋅ THENM (InstLemma `mul_preserves_le` [⌜p1⌝; ⌜1⌝; ⌜b⌝])⋅THEN Auto) }


Latex:


Latex:

1.  a  :  \mBbbN{}
2.  b  :  \mBbbN{}
3.  p1  :  \mBbbN{}a
4.  p2  :  \mBbbZ{}
5.  0  \mleq{}  p2
6.  p2  <  b
\mvdash{}  p2  <  (a  *  b)  -  p1  *  b


By


Latex:
(((InstLemma  `mul\_bounds\_1a`  [\mkleeneopen{}p1\mkleeneclose{};  \mkleeneopen{}b\mkleeneclose{}])\mcdot{}
  THENM  (InstLemma  `mul\_preserves\_le`  [\mkleeneopen{}p1\mkleeneclose{};  \mkleeneopen{}a  -  1\mkleeneclose{};  \mkleeneopen{}b\mkleeneclose{}])\mcdot{}
  )
  THEN  Auto
  )




Home Index