Nuprl Lemma : rmul-distrib

`∀[a,b,c:ℝ].  (((a * (b + c)) = ((a * b) + (a * c))) ∧ (((b + c) * a) = ((b * a) + (c * a))))`

Proof

Definitions occuring in Statement :  req: `x = y` rmul: `a * b` radd: `a + b` real: `ℝ` uall: `∀[x:A]. B[x]` and: `P ∧ Q`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` and: `P ∧ Q` cand: `A c∧ B` implies: `P `` Q`
Lemmas referenced :  rmul-distrib1 rmul-distrib2 req_witness rmul_wf radd_wf real_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis independent_pairFormation because_Cache sqequalRule productElimination independent_pairEquality independent_functionElimination isect_memberEquality

Latex:
\mforall{}[a,b,c:\mBbbR{}].    (((a  *  (b  +  c))  =  ((a  *  b)  +  (a  *  c)))  \mwedge{}  (((b  +  c)  *  a)  =  ((b  *  a)  +  (c  *  a))))

Date html generated: 2016_05_18-AM-06_52_30
Last ObjectModification: 2015_12_28-AM-00_30_44

Theory : reals

Home Index