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 WWordSWW

Proof

Step Hyp Ref Expression
1 wrdfin WWordSWFin
2 hashnncl WFinWW
3 1 2 syl WWordSWW
4 3 biimpar WWordSWW