Step
*
of Lemma
rprod-rsub-symmetry
∀n,m:ℤ. ∀x,y:{n..m + 1-} ⟶ ℝ.
rprod(n;m;k.x[k] - y[k]) = (r(-1)^(m - n) + 1 * rprod(n;m;k.y[k] - x[k])) supposing n ≤ m
BY
{ (Intros
THEN (Assert rprod(n;m;k.x[k] - y[k]) = rprod(n;m;k.-(y[k] - x[k])) BY
((BLemma `rprod_functionality` THEN Auto) THEN D 0 THEN Auto))
THEN (RWO "-1" 0 THENA Auto)
THEN BLemma `rprod-rminus`
THEN Auto) }
Latex:
Latex:
\mforall{}n,m:\mBbbZ{}. \mforall{}x,y:\{n..m + 1\msupminus{}\} {}\mrightarrow{} \mBbbR{}.
rprod(n;m;k.x[k] - y[k]) = (r(-1)\^{}(m - n) + 1 * rprod(n;m;k.y[k] - x[k])) supposing n \mleq{} m
By
Latex:
(Intros
THEN (Assert rprod(n;m;k.x[k] - y[k]) = rprod(n;m;k.-(y[k] - x[k])) BY
((BLemma `rprod\_functionality` THEN Auto) THEN D 0 THEN Auto))
THEN (RWO "-1" 0 THENA Auto)
THEN BLemma `rprod-rminus`
THEN Auto)
Home
Index