Step * 1 1 of Lemma expectation-rv-add-cubed


1. : ℚ
2. v1 : ℚ
⊢ ((2 v1) (2 v1 v1) (v v) (v v1) (v v1 v1) (v1 v1 v1))
((3 v1) (3 v1 v1) (v v) (v1 v1 v1))
∈ ℚ
BY
GenConclTerms Auto [⌜v1⌝;⌜v1 v1⌝;⌜v⌝;⌜v1 v1 v1⌝]⋅ }

1
1. : ℚ
2. v1 : ℚ
3. v2 : ℚ
4. (v v1) v2 ∈ ℚ
5. v3 : ℚ
6. (v v1 v1) v3 ∈ ℚ
7. v4 : ℚ
8. (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