Theorem 5tcu2e40

Description: 5 times the cube of 2 is 40. (Contributed by AV, 4-Jul-2020)

	Ref	Expression
Assertion	5tcu2e40	$$⊢52^3=40$$

Proof

Step	Hyp	Ref	Expression
1		cu2	$$⊢2^3=8$$
2	1	oveq2i	$$⊢52^3=5\cdot 8$$
3		5cn	$$⊢5\in ℂ$$
4		8cn	$$⊢8\in ℂ$$
5	3 4	mulcomi	$$⊢5\cdot 8=8\cdot 5$$
6		8t5e40	$$⊢8\cdot 5=40$$
7	2 5 6	3eqtri	$$⊢52^3=40$$