### Nuprl Lemma : less_than_transitivity2

`∀[x,y,z:ℤ].  (x < z) supposing (y < z and (x ≤ y))`

Proof

Definitions occuring in Statement :  less_than: `a < b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` le: `A ≤ B` int: `ℤ`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` all: `∀x:A. B[x]` uiff: `uiff(P;Q)` and: `P ∧ Q` or: `P ∨ Q` prop: `ℙ` squash: `↓T` true: `True` subtype_rel: `A ⊆r B` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` implies: `P `` Q`
Lemmas referenced :  le-iff-less-or-equal less_than_wf member-less_than le_wf less_than_transitivity squash_wf true_wf subtype_rel_self iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality hypothesis productElimination independent_isectElimination unionElimination isectElimination sqequalRule isect_memberEquality because_Cache equalityTransitivity equalitySymmetry intEquality applyEquality lambdaEquality imageElimination natural_numberEquality imageMemberEquality baseClosed instantiate universeEquality independent_functionElimination

Latex:
\mforall{}[x,y,z:\mBbbZ{}].    (x  <  z)  supposing  (y  <  z  and  (x  \mleq{}  y))

Date html generated: 2019_06_20-AM-11_22_50
Last ObjectModification: 2018_09_10-PM-01_15_08

Theory : arithmetic

Home Index