Theorem 4t3lem 9432

Description: Lemma for 4t3e12 9433 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 5862	. 2 |- ( A x. C ) = ( A x. ( B + 1 ) )
3		4t3lem.1	. . . . . 6 |- A e. NN0
4	3	nn0cni 9140	. . . . 5 |- A e. CC
5		4t3lem.2	. . . . . 6 |- B e. NN0
6	5	nn0cni 9140	. . . . 5 |- B e. CC
7		ax-1cn 7860	. . . . 5 |- 1 e. CC
8	4, 6, 7	adddii 7923	. . . 4 |- ( A x. ( B + 1 ) ) = ( ( A x. B ) + ( A x. 1 ) )
9		4t3lem.4	. . . . 5 |- ( A x. B ) = D
10	4	mulid1i 7915	. . . . 5 |- ( A x. 1 ) = A
11	9, 10	oveq12i 5863	. . . 4 |- ( ( A x. B ) + ( A x. 1 ) ) = ( D + A )
12	8, 11	eqtri 2191	. . 3 |- ( A x. ( B + 1 ) ) = ( D + A )
13		4t3lem.5	. . 3 |- ( D + A ) = E
14	12, 13	eqtri 2191	. 2 |- ( A x. ( B + 1 ) ) = E
15	2, 14	eqtri 2191	1 |- ( A x. C ) = E

Syntax hints:   = wceq 1348   e. wcel 2141  (class class class)co 5851   1c1 7768   + caddc 7770   x. cmul 7772   NN0cn0 9128

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152  ax-sep 4105  ax-cnex 7858  ax-resscn 7859  ax-1cn 7860  ax-1re 7861  ax-icn 7862  ax-addcl 7863  ax-addrcl 7864  ax-mulcl 7865  ax-mulcom 7868  ax-mulass 7870  ax-distr 7871  ax-1rid 7874  ax-rnegex 7876  ax-cnre 7878

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-rex 2454  df-v 2732  df-un 3125  df-in 3127  df-ss 3134  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3795  df-int 3830  df-br 3988  df-iota 5158  df-fv 5204  df-ov 5854  df-inn 8872  df-n0 9129

This theorem is referenced by:  4t3e12  9433  4t4e16  9434  5t2e10  9435  5t3e15  9436  5t4e20  9437  5t5e25  9438  6t3e18  9440  6t4e24  9441  6t5e30  9442  6t6e36  9443  7t3e21  9445  7t4e28  9446  7t5e35  9447  7t6e42  9448  7t7e49  9449  8t3e24  9451  8t4e32  9452  8t5e40  9453  8t6e48  9454  8t7e56  9455  8t8e64  9456  9t3e27  9458  9t4e36  9459  9t5e45  9460  9t6e54  9461  9t7e63  9462  9t8e72  9463  9t9e81  9464