Theorem 5tcu2e40

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

	Ref	Expression
Assertion	5tcu2e40	⊢ ( 5 · ( 2 ↑ 3 ) ) = ; 4 0

Proof

Step	Hyp	Ref	Expression
1		cu2	⊢ ( 2 ↑ 3 ) = 8
2	1	oveq2i	⊢ ( 5 · ( 2 ↑ 3 ) ) = ( 5 · 8 )
3		5cn	⊢ 5 ∈ ℂ
4		8cn	⊢ 8 ∈ ℂ
5	3 4	mulcomi	⊢ ( 5 · 8 ) = ( 8 · 5 )
6		8t5e40	⊢ ( 8 · 5 ) = ; 4 0
7	2 5 6	3eqtri	⊢ ( 5 · ( 2 ↑ 3 ) ) = ; 4 0