Theorem 5tcu2e40

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

	Ref	Expression
Assertion	5tcu2e40	|- ( 5 x. ( 2 ^ 3 ) ) = ; 4 0

Proof

Step	Hyp	Ref	Expression
1		cu2	|- ( 2 ^ 3 ) = 8
2	1	oveq2i	|- ( 5 x. ( 2 ^ 3 ) ) = ( 5 x. 8 )
3		5cn	|- 5 e. CC
4		8cn	|- 8 e. CC
5	3 4	mulcomi	|- ( 5 x. 8 ) = ( 8 x. 5 )
6		8t5e40	|- ( 8 x. 5 ) = ; 4 0
7	2 5 6	3eqtri	|- ( 5 x. ( 2 ^ 3 ) ) = ; 4 0