Description: The length of a word is a positive integer iff the word is not empty. (Contributed by AV, 22-Mar-2022)
Ref | Expression | ||
---|---|---|---|
Assertion | len0nnbi | |- ( W e. Word S -> ( W =/= (/) <-> ( # ` W ) e. NN ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lennncl | |- ( ( W e. Word S /\ W =/= (/) ) -> ( # ` W ) e. NN ) |
|
2 | 1 | ex | |- ( W e. Word S -> ( W =/= (/) -> ( # ` W ) e. NN ) ) |
3 | nnge1 | |- ( ( # ` W ) e. NN -> 1 <_ ( # ` W ) ) |
|
4 | wrdlenge1n0 | |- ( W e. Word S -> ( W =/= (/) <-> 1 <_ ( # ` W ) ) ) |
|
5 | 3 4 | syl5ibr | |- ( W e. Word S -> ( ( # ` W ) e. NN -> W =/= (/) ) ) |
6 | 2 5 | impbid | |- ( W e. Word S -> ( W =/= (/) <-> ( # ` W ) e. NN ) ) |