Nuprl Lemma : le_functionality

`∀[a,b,c,d:ℤ].  ({a ≤ d supposing b ≤ c}) supposing ((c ≤ d) and (b ≥ a ))`

Proof

Definitions occuring in Statement :  uimplies: `b supposing a` uall: `∀[x:A]. B[x]` guard: `{T}` ge: `i ≥ j ` le: `A ≤ B` int: `ℤ`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` guard: `{T}` le: `A ≤ B` and: `P ∧ Q` ge: `i ≥ j ` not: `¬A` implies: `P `` Q` false: `False` prop: `ℙ`
Lemmas referenced :  le_transitivity le_wf less_than'_wf ge_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution productElimination thin hypothesis lemma_by_obid isectElimination hypothesisEquality independent_isectElimination sqequalRule independent_pairEquality lambdaEquality dependent_functionElimination because_Cache axiomEquality isect_memberEquality equalityTransitivity equalitySymmetry intEquality voidElimination

Latex:
\mforall{}[a,b,c,d:\mBbbZ{}].    (\{a  \mleq{}  d  supposing  b  \mleq{}  c\})  supposing  ((c  \mleq{}  d)  and  (b  \mgeq{}  a  ))

Date html generated: 2016_05_13-PM-03_30_49
Last ObjectModification: 2015_12_26-AM-09_46_27

Theory : arithmetic

Home Index