Step
*
of Lemma
rmul_assoc
∀[a,b,c:ℝ]. (((a * b) * c) = (a * b * c))
BY
{ (Auto
THEN BLemma `req-iff-bdd-diff`
THEN Auto
THEN (RWO "rmul-bdd-diff-reg-seq-mul" 0 THENA Auto)
THEN (RW (AddrC [2] (LemmaC `reg-seq-mul-comm`)) 0 THENA Auto)
THEN RWO "rmul-bdd-diff-reg-seq-mul" 0
THEN Auto) }
Latex:
Latex:
\mforall{}[a,b,c:\mBbbR{}]. (((a * b) * c) = (a * b * c))
By
Latex:
(Auto
THEN BLemma `req-iff-bdd-diff`
THEN Auto
THEN (RWO "rmul-bdd-diff-reg-seq-mul" 0 THENA Auto)
THEN (RW (AddrC [2] (LemmaC `reg-seq-mul-comm`)) 0 THENA Auto)
THEN RWO "rmul-bdd-diff-reg-seq-mul" 0
THEN Auto)
Home
Index