Theorem 4t3lem

Description: Lemma for 4t3e12 and related theorems. (Contributed by Mario Carneiro, 19-Apr-2015)

	Ref	Expression
Hypotheses	4t3lem.1	⊢ 𝐴 ∈ ℕ0
	4t3lem.2	⊢ 𝐵 ∈ ℕ0
	4t3lem.3	⊢ 𝐶 = ( 𝐵 + 1 )
	4t3lem.4	⊢ ( 𝐴 · 𝐵 ) = 𝐷
	4t3lem.5	⊢ ( 𝐷 + 𝐴 ) = 𝐸
Assertion	4t3lem	⊢ ( 𝐴 · 𝐶 ) = 𝐸

Proof

Step	Hyp	Ref	Expression
1		4t3lem.1	⊢ 𝐴 ∈ ℕ0
2		4t3lem.2	⊢ 𝐵 ∈ ℕ0
3		4t3lem.3	⊢ 𝐶 = ( 𝐵 + 1 )
4		4t3lem.4	⊢ ( 𝐴 · 𝐵 ) = 𝐷
5		4t3lem.5	⊢ ( 𝐷 + 𝐴 ) = 𝐸
6	3	oveq2i	⊢ ( 𝐴 · 𝐶 ) = ( 𝐴 · ( 𝐵 + 1 ) )
7	1	nn0cni	⊢ 𝐴 ∈ ℂ
8	2	nn0cni	⊢ 𝐵 ∈ ℂ
9		ax-1cn	⊢ 1 ∈ ℂ
10	7 8 9	adddii	⊢ ( 𝐴 · ( 𝐵 + 1 ) ) = ( ( 𝐴 · 𝐵 ) + ( 𝐴 · 1 ) )
11	7	mulid1i	⊢ ( 𝐴 · 1 ) = 𝐴
12	4 11	oveq12i	⊢ ( ( 𝐴 · 𝐵 ) + ( 𝐴 · 1 ) ) = ( 𝐷 + 𝐴 )
13	10 12	eqtri	⊢ ( 𝐴 · ( 𝐵 + 1 ) ) = ( 𝐷 + 𝐴 )
14	13 5	eqtri	⊢ ( 𝐴 · ( 𝐵 + 1 ) ) = 𝐸
15	6 14	eqtri	⊢ ( 𝐴 · 𝐶 ) = 𝐸