Description: A word with length at least 1 is not empty. (Contributed by AV, 14-Oct-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | wrdlenge1n0 | |- ( W e. Word V -> ( W =/= (/) <-> 1 <_ ( # ` W ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hashneq0 | |- ( W e. Word V -> ( 0 < ( # ` W ) <-> W =/= (/) ) ) |
|
2 | lencl | |- ( W e. Word V -> ( # ` W ) e. NN0 ) |
|
3 | 2 | nn0zd | |- ( W e. Word V -> ( # ` W ) e. ZZ ) |
4 | zgt0ge1 | |- ( ( # ` W ) e. ZZ -> ( 0 < ( # ` W ) <-> 1 <_ ( # ` W ) ) ) |
|
5 | 3 4 | syl | |- ( W e. Word V -> ( 0 < ( # ` W ) <-> 1 <_ ( # ` W ) ) ) |
6 | 1 5 | bitr3d | |- ( W e. Word V -> ( W =/= (/) <-> 1 <_ ( # ` W ) ) ) |