Step |
Hyp |
Ref |
Expression |
1 |
|
dpval2.a |
|
2 |
|
dpval2.b |
|
3 |
1 2
|
dpmul10 |
Could not format ( ( A . B ) x. ; 1 0 ) = ; A B : No typesetting found for |- ( ( A . B ) x. ; 1 0 ) = ; A B with typecode |- |
4 |
3
|
oveq1i |
Could not format ( ( ( A . B ) x. ; 1 0 ) / ; 1 0 ) = ( ; A B / ; 1 0 ) : No typesetting found for |- ( ( ( A . B ) x. ; 1 0 ) / ; 1 0 ) = ( ; A B / ; 1 0 ) with typecode |- |
5 |
|
dpcl |
|
6 |
1 2 5
|
mp2an |
|
7 |
6
|
recni |
|
8 |
|
10nn |
|
9 |
8
|
nncni |
|
10 |
8
|
nnne0i |
|
11 |
7 9 10
|
divcan4i |
|
12 |
4 11
|
eqtr3i |
Could not format ( ; A B / ; 1 0 ) = ( A . B ) : No typesetting found for |- ( ; A B / ; 1 0 ) = ( A . B ) with typecode |- |