Step
*
1
4
1
1
of Lemma
div_3_to_1
1. v : ℤ
⊢ (0 ≤ v)
⇒
0 < -v
⇒
False
BY
{ Auto }
1
1. v : ℤ
2. 0 ≤ v
3. 0 < -v
⊢ False
Latex:
Latex:
1. v : \mBbbZ{}
\mvdash{} (0 \mleq{} v) {}\mRightarrow{} 0 < -v {}\mRightarrow{} False
By
Latex:
Auto
Home
Index