Step
*
1
1
of Lemma
expectation-rv-add-cubed
1. v : ℚ
2. v1 : ℚ
⊢ ((2 * v * v * v1) + (2 * v * v1 * v1) + (v * v * v) + (v * v * v1) + (v * v1 * v1) + (v1 * v1 * v1))
= ((3 * v * v * v1) + (3 * v * v1 * v1) + (v * v * v) + (v1 * v1 * v1))
∈ ℚ
BY
{ GenConclTerms Auto [⌜v * v * v1⌝;⌜v * v1 * v1⌝;⌜v * v * v⌝;⌜v1 * v1 * v1⌝]⋅ }
1
1. v : ℚ
2. v1 : ℚ
3. v2 : ℚ
4. (v * v * v1) = v2 ∈ ℚ
5. v3 : ℚ
6. (v * v1 * v1) = v3 ∈ ℚ
7. v4 : ℚ
8. (v * v * v) = v4 ∈ ℚ
9. v5 : ℚ
10. (v1 * v1 * v1) = v5 ∈ ℚ
⊢ ((2 * v2) + (2 * v3) + v4 + v2 + v3 + v5) = ((3 * v2) + (3 * v3) + v4 + v5) ∈ ℚ
Latex:
Latex:
1.  v  :  \mBbbQ{}
2.  v1  :  \mBbbQ{}
\mvdash{}  ((2  *  v  *  v  *  v1)
+  (2  *  v  *  v1  *  v1)
+  (v  *  v  *  v)
+  (v  *  v  *  v1)
+  (v  *  v1  *  v1)
+  (v1  *  v1  *  v1))
=  ((3  *  v  *  v  *  v1)  +  (3  *  v  *  v1  *  v1)  +  (v  *  v  *  v)  +  (v1  *  v1  *  v1))
By
Latex:
GenConclTerms  Auto  [\mkleeneopen{}v  *  v  *  v1\mkleeneclose{};\mkleeneopen{}v  *  v1  *  v1\mkleeneclose{};\mkleeneopen{}v  *  v  *  v\mkleeneclose{};\mkleeneopen{}v1  *  v1  *  v1\mkleeneclose{}]\mcdot{}
Home
Index