| Step |
Hyp |
Ref |
Expression |
| 1 |
|
right0s |
Could not format ( _R ` 0s ) = (/) : No typesetting found for |- ( _R ` 0s ) = (/) with typecode |- |
| 2 |
1
|
imaeq2i |
Could not format ( -us " ( _R ` 0s ) ) = ( -us " (/) ) : No typesetting found for |- ( -us " ( _R ` 0s ) ) = ( -us " (/) ) with typecode |- |
| 3 |
|
ima0 |
Could not format ( -us " (/) ) = (/) : No typesetting found for |- ( -us " (/) ) = (/) with typecode |- |
| 4 |
2 3
|
eqtri |
Could not format ( -us " ( _R ` 0s ) ) = (/) : No typesetting found for |- ( -us " ( _R ` 0s ) ) = (/) with typecode |- |
| 5 |
|
left0s |
Could not format ( _L ` 0s ) = (/) : No typesetting found for |- ( _L ` 0s ) = (/) with typecode |- |
| 6 |
5
|
imaeq2i |
Could not format ( -us " ( _L ` 0s ) ) = ( -us " (/) ) : No typesetting found for |- ( -us " ( _L ` 0s ) ) = ( -us " (/) ) with typecode |- |
| 7 |
6 3
|
eqtri |
Could not format ( -us " ( _L ` 0s ) ) = (/) : No typesetting found for |- ( -us " ( _L ` 0s ) ) = (/) with typecode |- |
| 8 |
4 7
|
oveq12i |
Could not format ( ( -us " ( _R ` 0s ) ) |s ( -us " ( _L ` 0s ) ) ) = ( (/) |s (/) ) : No typesetting found for |- ( ( -us " ( _R ` 0s ) ) |s ( -us " ( _L ` 0s ) ) ) = ( (/) |s (/) ) with typecode |- |
| 9 |
|
0sno |
Could not format 0s e. No : No typesetting found for |- 0s e. No with typecode |- |
| 10 |
|
negsfv |
Could not format ( 0s e. No -> ( -us ` 0s ) = ( ( -us " ( _R ` 0s ) ) |s ( -us " ( _L ` 0s ) ) ) ) : No typesetting found for |- ( 0s e. No -> ( -us ` 0s ) = ( ( -us " ( _R ` 0s ) ) |s ( -us " ( _L ` 0s ) ) ) ) with typecode |- |
| 11 |
9 10
|
ax-mp |
Could not format ( -us ` 0s ) = ( ( -us " ( _R ` 0s ) ) |s ( -us " ( _L ` 0s ) ) ) : No typesetting found for |- ( -us ` 0s ) = ( ( -us " ( _R ` 0s ) ) |s ( -us " ( _L ` 0s ) ) ) with typecode |- |
| 12 |
|
df-0s |
Could not format 0s = ( (/) |s (/) ) : No typesetting found for |- 0s = ( (/) |s (/) ) with typecode |- |
| 13 |
8 11 12
|
3eqtr4i |
Could not format ( -us ` 0s ) = 0s : No typesetting found for |- ( -us ` 0s ) = 0s with typecode |- |