Step * of Lemma from-upto-member

n,m,k:ℤ.  uiff((k ∈ [n, m));(n ≤ k) ∧ k < m)
BY
((UnivCD THENA Auto) THEN RepeatFor ((D THENA Auto))) }

1
1. : ℤ
2. : ℤ
3. : ℤ
4. (k ∈ [n, m))
⊢ (n ≤ k) ∧ k < m

2
1. : ℤ
2. : ℤ
3. : ℤ
4. (n ≤ k) ∧ k < m
⊢ (k ∈ [n, m))


Latex:


Latex:
\mforall{}n,m,k:\mBbbZ{}.    uiff((k  \mmember{}  [n,  m));(n  \mleq{}  k)  \mwedge{}  k  <  m)


By


Latex:
((UnivCD  THENA  Auto)  THEN  RepeatFor  2  ((D  0  THENA  Auto)))




Home Index