Step |
Hyp |
Ref |
Expression |
1 |
|
nummul1c.1 |
|- T e. NN0 |
2 |
|
nummul1c.2 |
|- P e. NN0 |
3 |
|
nummul1c.3 |
|- A e. NN0 |
4 |
|
nummul1c.4 |
|- B e. NN0 |
5 |
|
nummul1c.5 |
|- N = ( ( T x. A ) + B ) |
6 |
|
nummul1c.6 |
|- D e. NN0 |
7 |
|
nummul1c.7 |
|- E e. NN0 |
8 |
|
nummul1c.8 |
|- ( ( A x. P ) + E ) = C |
9 |
|
nummul1c.9 |
|- ( B x. P ) = ( ( T x. E ) + D ) |
10 |
1 3 4
|
numcl |
|- ( ( T x. A ) + B ) e. NN0 |
11 |
5 10
|
eqeltri |
|- N e. NN0 |
12 |
11 2
|
num0u |
|- ( N x. P ) = ( ( N x. P ) + 0 ) |
13 |
|
0nn0 |
|- 0 e. NN0 |
14 |
1 13
|
num0h |
|- 0 = ( ( T x. 0 ) + 0 ) |
15 |
7
|
nn0cni |
|- E e. CC |
16 |
15
|
addid2i |
|- ( 0 + E ) = E |
17 |
16
|
oveq2i |
|- ( ( A x. P ) + ( 0 + E ) ) = ( ( A x. P ) + E ) |
18 |
17 8
|
eqtri |
|- ( ( A x. P ) + ( 0 + E ) ) = C |
19 |
4 2
|
num0u |
|- ( B x. P ) = ( ( B x. P ) + 0 ) |
20 |
19 9
|
eqtr3i |
|- ( ( B x. P ) + 0 ) = ( ( T x. E ) + D ) |
21 |
1 3 4 13 13 5 14 2 6 7 18 20
|
nummac |
|- ( ( N x. P ) + 0 ) = ( ( T x. C ) + D ) |
22 |
12 21
|
eqtri |
|- ( N x. P ) = ( ( T x. C ) + D ) |