Nuprl Lemma : int-between

i,j:ℤ.  ∃k:ℤ((i ≤ k) ∧ k < j) supposing i < j


Proof




Definitions occuring in Statement :  less_than: a < b uimplies: supposing a le: A ≤ B all: x:A. B[x] exists: x:A. B[x] and: P ∧ Q int:
Definitions unfolded in proof :  all: x:A. B[x] uimplies: supposing a member: t ∈ T uall: [x:A]. B[x] exists: x:A. B[x] and: P ∧ Q prop:
Lemmas referenced :  member-less_than le_weakening and_wf le_wf less_than_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation isect_memberFormation cut introduction lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality independent_isectElimination hypothesis rename dependent_pairFormation because_Cache independent_pairFormation dependent_functionElimination intEquality

Latex:
\mforall{}i,j:\mBbbZ{}.    \mexists{}k:\mBbbZ{}.  ((i  \mleq{}  k)  \mwedge{}  k  <  j)  supposing  i  <  j



Date html generated: 2019_06_20-PM-02_37_37
Last ObjectModification: 2019_06_12-PM-00_26_16

Theory : num_thy_1


Home Index