### Nuprl Lemma : lt_int_eq_false_elim

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

Proof

Definitions occuring in Statement :  lt_int: `i <z j` bfalse: `ff` bool: `𝔹` less_than: `a < b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` not: `¬A` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` not: `¬A` implies: `P `` Q` false: `False` prop: `ℙ` le: `A ≤ B` and: `P ∧ Q` guard: `{T}` uiff: `uiff(P;Q)`
Lemmas referenced :  less_than_wf equal_wf bool_wf lt_int_wf bfalse_wf assert_wf le_int_wf le_wf bnot_wf less_than_transitivity1 less_than_irreflexivity uiff_transitivity eqff_to_assert assert_functionality_wrt_uiff bnot_of_lt_int assert_of_le_int
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation thin hypothesis sqequalHypSubstitution independent_functionElimination voidElimination lemma_by_obid isectElimination hypothesisEquality sqequalRule lambdaEquality dependent_functionElimination because_Cache isect_memberEquality equalityTransitivity equalitySymmetry intEquality productElimination independent_isectElimination

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

Date html generated: 2016_05_13-PM-04_01_57
Last ObjectModification: 2015_12_26-AM-10_56_51

Theory : int_1

Home Index