Theorem 9t5e45

Description: 9 times 5 equals 45. (Contributed by Mario Carneiro, 19-Apr-2015)

	Ref	Expression
Assertion	9t5e45	⊢ ( 9 · 5 ) = ; 4 5

Proof

Step	Hyp	Ref	Expression
1		9nn0	⊢ 9 ∈ ℕ0
2		4nn0	⊢ 4 ∈ ℕ0
3		df-5	⊢ 5 = ( 4 + 1 )
4		9t4e36	⊢ ( 9 · 4 ) = ; 3 6
5		3nn0	⊢ 3 ∈ ℕ0
6		6nn0	⊢ 6 ∈ ℕ0
7		eqid	⊢ ; 3 6 = ; 3 6
8		3p1e4	⊢ ( 3 + 1 ) = 4
9		5nn0	⊢ 5 ∈ ℕ0
10	1	nn0cni	⊢ 9 ∈ ℂ
11	6	nn0cni	⊢ 6 ∈ ℂ
12		9p6e15	⊢ ( 9 + 6 ) = ; 1 5
13	10 11 12	addcomli	⊢ ( 6 + 9 ) = ; 1 5
14	5 6 1 7 8 9 13	decaddci	⊢ ( ; 3 6 + 9 ) = ; 4 5
15	1 2 3 4 14	4t3lem	⊢ ( 9 · 5 ) = ; 4 5