Description: A word with length at least 1 is not empty. (Contributed by AV, 14-Oct-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | wrdlenge1n0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hashneq0 | |
|
2 | lencl | |
|
3 | 2 | nn0zd | |
4 | zgt0ge1 | |
|
5 | 3 4 | syl | |
6 | 1 5 | bitr3d | |