Step
*
1
1
1
2
1
1
1
1
1
of Lemma
rational-IVT
1. M : ℕ+
2. v : ℤ
3. v1 : ℤ
⊢ ((v + 4) ≤ v1) ⇒ (((v + 2) * M) ≤ ((v1 - 2) * M))
BY
{ Auto }
1
1. M : ℕ+
2. v : ℤ
3. v1 : ℤ
4. (v + 4) ≤ v1
⊢ ((v + 2) * M) ≤ ((v1 - 2) * M)
Latex:
Latex:
1. M : \mBbbN{}\msupplus{}
2. v : \mBbbZ{}
3. v1 : \mBbbZ{}
\mvdash{} ((v + 4) \mleq{} v1) {}\mRightarrow{} (((v + 2) * M) \mleq{} ((v1 - 2) * M))
By
Latex:
Auto
Home
Index