Metamath Proof Explorer


Theorem len0nnbi

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 ) )

Proof

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 ) )