Step * of Lemma from-upto_wf

[n,m:ℤ].  ([n, m) ∈ {x:ℤ(n ≤ x) ∧ x < m}  List)
BY
Assert ⌜∀d:ℕ. ∀n,m:ℤ.  (((m n) ≤ d)  ([n, m) ∈ {x:ℤ(n ≤ x) ∧ x < m}  List))⌝⋅ }

1
.....assertion..... 
d:ℕ. ∀n,m:ℤ.  (((m n) ≤ d)  ([n, m) ∈ {x:ℤ(n ≤ x) ∧ x < m}  List))

2
1. ∀d:ℕ. ∀n,m:ℤ.  (((m n) ≤ d)  ([n, m) ∈ {x:ℤ(n ≤ x) ∧ x < m}  List))
⊢ ∀[n,m:ℤ].  ([n, m) ∈ {x:ℤ(n ≤ x) ∧ x < m}  List)


Latex:


Latex:
\mforall{}[n,m:\mBbbZ{}].    ([n,  m)  \mmember{}  \{x:\mBbbZ{}|  (n  \mleq{}  x)  \mwedge{}  x  <  m\}    List)


By


Latex:
Assert  \mkleeneopen{}\mforall{}d:\mBbbN{}.  \mforall{}n,m:\mBbbZ{}.    (((m  -  n)  \mleq{}  d)  {}\mRightarrow{}  ([n,  m)  \mmember{}  \{x:\mBbbZ{}|  (n  \mleq{}  x)  \mwedge{}  x  <  m\}    List))\mkleeneclose{}\mcdot{}




Home Index