Step |
Hyp |
Ref |
Expression |
1 |
|
decpmulnc.a |
|
2 |
|
decpmulnc.b |
|
3 |
|
decpmulnc.c |
|
4 |
|
decpmulnc.d |
|
5 |
|
decpmulnc.1 |
|
6 |
|
decpmulnc.2 |
|
7 |
|
decpmulnc.3 |
|
8 |
1 2
|
deccl |
Could not format ; A B e. NN0 : No typesetting found for |- ; A B e. NN0 with typecode |- |
9 |
|
eqid |
Could not format ; C D = ; C D : No typesetting found for |- ; C D = ; C D with typecode |- |
10 |
2 4
|
nn0mulcli |
|
11 |
7 10
|
eqeltrri |
|
12 |
1 4
|
nn0mulcli |
|
13 |
|
eqid |
Could not format ; A B = ; A B : No typesetting found for |- ; A B = ; A B with typecode |- |
14 |
12
|
nn0cni |
|
15 |
2 3
|
nn0mulcli |
|
16 |
15
|
nn0cni |
|
17 |
14 16 6
|
addcomli |
|
18 |
1 2 12 13 3 5 17
|
decrmanc |
Could not format ( ( ; A B x. C ) + ( A x. D ) ) = ; E F : No typesetting found for |- ( ( ; A B x. C ) + ( A x. D ) ) = ; E F with typecode |- |
19 |
|
eqid |
|
20 |
4 1 2 13 19 7
|
decmul1 |
Could not format ( ; A B x. D ) = ; ( A x. D ) G : No typesetting found for |- ( ; A B x. D ) = ; ( A x. D ) G with typecode |- |
21 |
8 3 4 9 11 12 18 20
|
decmul2c |
Could not format ( ; A B x. ; C D ) = ; ; E F G : No typesetting found for |- ( ; A B x. ; C D ) = ; ; E F G with typecode |- |