### Nuprl Lemma : lt_int_eq_false_elim_sqequal

`∀[i,j:ℤ].  ¬i < j supposing i <z j ~ ff`

Proof

Definitions occuring in Statement :  lt_int: `i <z j` bfalse: `ff` less_than: `a < b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` not: `¬A` int: `ℤ` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` not: `¬A` implies: `P `` Q` false: `False` uiff: `uiff(P;Q)` and: `P ∧ Q` prop: `ℙ` subtype_rel: `A ⊆r B`
Lemmas referenced :  int_subtype_base less_than_wf assert_of_lt_int assert_of_ff
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation thin sqequalRule hypothesis lemma_by_obid sqequalHypSubstitution independent_functionElimination isectElimination hypothesisEquality productElimination independent_isectElimination because_Cache promote_hyp voidElimination lambdaEquality dependent_functionElimination sqequalIntensionalEquality baseApply closedConclusion baseClosed applyEquality isect_memberEquality equalityTransitivity equalitySymmetry intEquality

Latex:
\mforall{}[i,j:\mBbbZ{}].    \mneg{}i  <  j  supposing  i  <z  j  \msim{}  ff

Date html generated: 2016_05_13-PM-04_10_32
Last ObjectModification: 2016_01_18-PM-05_39_42

Theory : subtype_1

Home Index