Theorem 7t5e35

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

	Ref	Expression
Assertion	7t5e35	⊢ ( 7 · 5 ) = ; 3 5

Proof

Step	Hyp	Ref	Expression
1		7nn0	⊢ 7 ∈ ℕ0
2		4nn0	⊢ 4 ∈ ℕ0
3		df-5	⊢ 5 = ( 4 + 1 )
4		7t4e28	⊢ ( 7 · 4 ) = ; 2 8
5		2nn0	⊢ 2 ∈ ℕ0
6		8nn0	⊢ 8 ∈ ℕ0
7		eqid	⊢ ; 2 8 = ; 2 8
8		2p1e3	⊢ ( 2 + 1 ) = 3
9		5nn0	⊢ 5 ∈ ℕ0
10		8p7e15	⊢ ( 8 + 7 ) = ; 1 5
11	5 6 1 7 8 9 10	decaddci	⊢ ( ; 2 8 + 7 ) = ; 3 5
12	1 2 3 4 11	4t3lem	⊢ ( 7 · 5 ) = ; 3 5