Theorem 4t3lem

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

	Ref	Expression
Hypotheses	4t3lem.1	|- A e. NN0
	4t3lem.2	|- B e. NN0
	4t3lem.3	|- C = ( B + 1 )
	4t3lem.4	|- ( A x. B ) = D
	4t3lem.5	|- ( D + A ) = E
Assertion	4t3lem	|- ( A x. C ) = E

Proof

Step	Hyp	Ref	Expression
1		4t3lem.1	|- A e. NN0
2		4t3lem.2	|- B e. NN0
3		4t3lem.3	|- C = ( B + 1 )
4		4t3lem.4	|- ( A x. B ) = D
5		4t3lem.5	|- ( D + A ) = E
6	3	oveq2i	|- ( A x. C ) = ( A x. ( B + 1 ) )
7	1	nn0cni	|- A e. CC
8	2	nn0cni	|- B e. CC
9		ax-1cn	|- 1 e. CC
10	7 8 9	adddii	|- ( A x. ( B + 1 ) ) = ( ( A x. B ) + ( A x. 1 ) )
11	7	mulid1i	|- ( A x. 1 ) = A
12	4 11	oveq12i	|- ( ( A x. B ) + ( A x. 1 ) ) = ( D + A )
13	10 12	eqtri	|- ( A x. ( B + 1 ) ) = ( D + A )
14	13 5	eqtri	|- ( A x. ( B + 1 ) ) = E
15	6 14	eqtri	|- ( A x. C ) = E