Metamath Proof Explorer


Theorem wrdlenge1n0

Description: A word with length at least 1 is not empty. (Contributed by AV, 14-Oct-2018)

Ref Expression
Assertion wrdlenge1n0 WWordVW1W

Proof

Step Hyp Ref Expression
1 hashneq0 WWordV0<WW
2 lencl WWordVW0
3 2 nn0zd WWordVW
4 zgt0ge1 W0<W1W
5 3 4 syl WWordV0<W1W
6 1 5 bitr3d WWordVW1W