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