Step |
Hyp |
Ref |
Expression |
1 |
|
df-1s |
Could not format 1s = ( { 0s } |s (/) ) : No typesetting found for |- 1s = ( { 0s } |s (/) ) with typecode |- |
2 |
|
0sno |
Could not format 0s e. No : No typesetting found for |- 0s e. No with typecode |- |
3 |
|
snelpwi |
Could not format ( 0s e. No -> { 0s } e. ~P No ) : No typesetting found for |- ( 0s e. No -> { 0s } e. ~P No ) with typecode |- |
4 |
2 3
|
ax-mp |
Could not format { 0s } e. ~P No : No typesetting found for |- { 0s } e. ~P No with typecode |- |
5 |
|
nulssgt |
Could not format ( { 0s } e. ~P No -> { 0s } < { 0s } <
|
6 |
4 5
|
ax-mp |
Could not format { 0s } <
|
7 |
|
scutcl |
Could not format ( { 0s } < ( { 0s } |s (/) ) e. No ) : No typesetting found for |- ( { 0s } < ( { 0s } |s (/) ) e. No ) with typecode |- |
8 |
6 7
|
ax-mp |
Could not format ( { 0s } |s (/) ) e. No : No typesetting found for |- ( { 0s } |s (/) ) e. No with typecode |- |
9 |
1 8
|
eqeltri |
Could not format 1s e. No : No typesetting found for |- 1s e. No with typecode |- |