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

Proof

Definitions occuring in Statement :  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` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` rev_uimplies: `rev_uimplies(P;Q)` or: `P ∨ Q` implies: `P `` Q` guard: `{T}` prop: `ℙ` uall: `∀[x:A]. B[x]` subtype_rel: `A ⊆r B` le: `A ≤ B` not: `¬A` false: `False` top: `Top`
Rules used in proof :  cut introduction extract_by_obid sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity dependent_functionElimination thin hypothesisEquality hypothesis productElimination independent_isectElimination addEquality unionElimination inlFormation independent_functionElimination sqequalRule inrFormation isectElimination because_Cache applyEquality intEquality baseApply closedConclusion baseClosed isect_memberFormation independent_pairEquality lambdaEquality axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality voidElimination voidEquality

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

Date html generated: 2019_06_20-AM-11_22_52
Last ObjectModification: 2018_08_17-AM-11_59_31

Theory : arithmetic

Home Index