| Step |
Hyp |
Ref |
Expression |
| 1 |
|
decpmulnc.a |
|- A e. NN0 |
| 2 |
|
decpmulnc.b |
|- B e. NN0 |
| 3 |
|
decpmulnc.c |
|- C e. NN0 |
| 4 |
|
decpmulnc.d |
|- D e. NN0 |
| 5 |
|
decpmulnc.1 |
|- ( A x. C ) = E |
| 6 |
|
decpmulnc.2 |
|- ( ( A x. D ) + ( B x. C ) ) = F |
| 7 |
|
decpmul.3 |
|- ( B x. D ) = ; G H |
| 8 |
|
decpmul.4 |
|- ( ; E G + F ) = I |
| 9 |
|
decpmul.g |
|- G e. NN0 |
| 10 |
|
decpmul.h |
|- H e. NN0 |
| 11 |
1 2 3 4 5 6 7
|
decpmulnc |
|- ( ; A B x. ; C D ) = ; ; E F ; G H |
| 12 |
|
dfdec10 |
|- ; ; E F ; G H = ( ( ; 1 0 x. ; E F ) + ; G H ) |
| 13 |
1 3
|
nn0mulcli |
|- ( A x. C ) e. NN0 |
| 14 |
5 13
|
eqeltrri |
|- E e. NN0 |
| 15 |
2 3
|
nn0mulcli |
|- ( B x. C ) e. NN0 |
| 16 |
1 4 15
|
numcl |
|- ( ( A x. D ) + ( B x. C ) ) e. NN0 |
| 17 |
6 16
|
eqeltrri |
|- F e. NN0 |
| 18 |
14 17
|
deccl |
|- ; E F e. NN0 |
| 19 |
|
0nn0 |
|- 0 e. NN0 |
| 20 |
18
|
dec0u |
|- ( ; 1 0 x. ; E F ) = ; ; E F 0 |
| 21 |
|
eqid |
|- ; G H = ; G H |
| 22 |
14 17 9
|
decaddcom |
|- ( ; E F + G ) = ( ; E G + F ) |
| 23 |
22 8
|
eqtri |
|- ( ; E F + G ) = I |
| 24 |
10
|
nn0cni |
|- H e. CC |
| 25 |
24
|
addlidi |
|- ( 0 + H ) = H |
| 26 |
18 19 9 10 20 21 23 25
|
decadd |
|- ( ( ; 1 0 x. ; E F ) + ; G H ) = ; I H |
| 27 |
11 12 26
|
3eqtri |
|- ( ; A B x. ; C D ) = ; I H |