`∀[i1,i2,j1,j2:ℤ].  (i1 + i2 < j1 + j2) supposing ((i2 ≤ j2) and i1 < j1)`

Proof

Definitions occuring in Statement :  less_than: `a < b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` le: `A ≤ B` add: `n + m` int: `ℤ`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` implies: `P `` Q` uall: `∀[x:A]. B[x]` uimplies: `b supposing a` prop: `ℙ` and: `P ∧ Q` uiff: `uiff(P;Q)` or: `P ∨ Q` guard: `{T}`
Lemmas referenced :  add-monotonic le_wf less_than_wf member-less_than equal_wf le-iff-less-or-equal
Rules used in proof :  cut introduction extract_by_obid sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity dependent_functionElimination thin hypothesisEquality independent_functionElimination hypothesis isectElimination addEquality because_Cache intEquality isect_memberFormation sqequalRule isect_memberEquality independent_isectElimination equalityTransitivity equalitySymmetry productElimination lemma_by_obid unionElimination inrFormation inlFormation

Latex:
\mforall{}[i1,i2,j1,j2:\mBbbZ{}].    (i1  +  i2  <  j1  +  j2)  supposing  ((i2  \mleq{}  j2)  and  i1  <  j1)

Date html generated: 2019_06_20-AM-11_22_54
Last ObjectModification: 2018_08_17-PM-00_00_07

Theory : arithmetic

Home Index