Theorem 4t3lem 9034

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

Hypotheses

Ref	Expression
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

Ref	Expression
4t3lem	|- ( A x. C ) = E

Proof of Theorem 4t3lem

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

Syntax hints:   = wceq 1290   e. wcel 1439  (class class class)co 5666   1c1 7412   + caddc 7414   x. cmul 7416   NN0cn0 8734

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071  ax-sep 3963  ax-cnex 7497  ax-resscn 7498  ax-1cn 7499  ax-1re 7500  ax-icn 7501  ax-addcl 7502  ax-addrcl 7503  ax-mulcl 7504  ax-mulcom 7507  ax-mulass 7509  ax-distr 7510  ax-1rid 7513  ax-rnegex 7515  ax-cnre 7517

This theorem depends on definitions:  df-bi 116  df-3an 927  df-tru 1293  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-ral 2365  df-rex 2366  df-v 2622  df-un 3004  df-in 3006  df-ss 3013  df-sn 3456  df-pr 3457  df-op 3459  df-uni 3660  df-int 3695  df-br 3852  df-iota 4993  df-fv 5036  df-ov 5669  df-inn 8484  df-n0 8735

This theorem is referenced by:  4t3e12  9035  4t4e16  9036  5t2e10  9037  5t3e15  9038  5t4e20  9039  5t5e25  9040  6t3e18  9042  6t4e24  9043  6t5e30  9044  6t6e36  9045  7t3e21  9047  7t4e28  9048  7t5e35  9049  7t6e42  9050  7t7e49  9051  8t3e24  9053  8t4e32  9054  8t5e40  9055  8t6e48  9056  8t7e56  9057  8t8e64  9058  9t3e27  9060  9t4e36  9061  9t5e45  9062  9t6e54  9063  9t7e63  9064  9t8e72  9065  9t9e81  9066