`∀[a,b,c:ℤ].  ((imin(a;b) + c) = imin(a + c;b + c) ∈ ℤ)`

Proof

Definitions occuring in Statement :  imin: `imin(a;b)` uall: `∀[x:A]. B[x]` add: `n + m` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` top: `Top` true: `True` squash: `↓T` subtype_rel: `A ⊆r B` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` implies: `P `` Q` prop: `ℙ`
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin addEquality hypothesisEquality hypothesis productElimination independent_isectElimination intEquality sqequalRule isect_memberEquality axiomEquality because_Cache voidElimination voidEquality multiplyEquality minusEquality natural_numberEquality applyEquality lambdaEquality imageElimination imageMemberEquality baseClosed equalityTransitivity equalitySymmetry independent_functionElimination universeEquality

Latex:
\mforall{}[a,b,c:\mBbbZ{}].    ((imin(a;b)  +  c)  =  imin(a  +  c;b  +  c))

Date html generated: 2017_04_14-AM-09_14_42
Last ObjectModification: 2017_02_27-PM-03_51_55

Theory : int_2

Home Index