Theorem 4t3lem

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

	Ref	Expression
Hypotheses	4t3lem.1	$$⊢A\in {\mathbb{N}}_0$$
	4t3lem.2	$$⊢B\in {\mathbb{N}}_0$$
	4t3lem.3	$$⊢C=B+1$$
	4t3lem.4	$$⊢AB=D$$
	4t3lem.5	$$⊢D+A=E$$
Assertion	4t3lem	$$⊢AC=E$$

Proof

Step	Hyp	Ref	Expression
1		4t3lem.1	$$⊢A\in {\mathbb{N}}_0$$
2		4t3lem.2	$$⊢B\in {\mathbb{N}}_0$$
3		4t3lem.3	$$⊢C=B+1$$
4		4t3lem.4	$$⊢AB=D$$
5		4t3lem.5	$$⊢D+A=E$$
6	3	oveq2i	$$⊢AC=A\left(B+1\right)$$
7	1	nn0cni	$$⊢A\in ℂ$$
8	2	nn0cni	$$⊢B\in ℂ$$
9		ax-1cn	$$⊢1\in ℂ$$
10	7 8 9	adddii	$$⊢A\left(B+1\right)=AB+A\cdot 1$$
11	7	mulid1i	$$⊢A\cdot 1=A$$
12	4 11	oveq12i	$$⊢AB+A\cdot 1=D+A$$
13	10 12	eqtri	$$⊢A\left(B+1\right)=D+A$$
14	13 5	eqtri	$$⊢A\left(B+1\right)=E$$
15	6 14	eqtri	$$⊢AC=E$$