Step
*
2
1
1
1
2
1
of Lemma
from-upto-is-nil
1. n : ℤ
2. m : ℤ
3. m ≤ n
4. u : {x:ℤ| (n ≤ x) ∧ x < m}
5. v : {x:ℤ| (n ≤ x) ∧ x < m} List
6. [n, m) = [u / v] ∈ ({x:ℤ| (n ≤ x) ∧ x < m} List)
7. [u / v] = [] ∈ (ℤ List)
⊢ uiff([u / v] ~ [];m ≤ n)
BY
{ (ImpossibleEq Auto (-1) THEN Auto) }
Latex:
Latex:
1. n : \mBbbZ{}
2. m : \mBbbZ{}
3. m \mleq{} n
4. u : \{x:\mBbbZ{}| (n \mleq{} x) \mwedge{} x < m\}
5. v : \{x:\mBbbZ{}| (n \mleq{} x) \mwedge{} x < m\} List
6. [n, m) = [u / v]
7. [u / v] = []
\mvdash{} uiff([u / v] \msim{} [];m \mleq{} n)
By
Latex:
(ImpossibleEq Auto (-1) THEN Auto)
Home
Index