Metamath Proof Explorer

Theorem lennncl

Description: The length of a nonempty word is a positive integer. (Contributed by Mario Carneiro, 1-Oct-2015)

Ref Expression
Assertion lennncl 
|- ( ( W e. Word S /\ W =/= (/) ) -> ( # ` W ) e. NN )

Proof

Step Hyp Ref Expression
1 wrdfin 
 |-  ( W e. Word S -> W e. Fin )
2 hashnncl 
 |-  ( W e. Fin -> ( ( # ` W ) e. NN <-> W =/= (/) ) )
3 1 2 syl 
 |-  ( W e. Word S -> ( ( # ` W ) e. NN <-> W =/= (/) ) )
4 3 biimpar 
 |-  ( ( W e. Word S /\ W =/= (/) ) -> ( # ` W ) e. NN )