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
|- ( W e. Word V -> ( W =/= (/) <-> 1 <_ ( # ` W ) ) )

Proof

Step Hyp Ref Expression
1 hashneq0
 |-  ( W e. Word V -> ( 0 < ( # ` W ) <-> W =/= (/) ) )
2 lencl
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
3 2 nn0zd
 |-  ( W e. Word V -> ( # ` W ) e. ZZ )
4 zgt0ge1
 |-  ( ( # ` W ) e. ZZ -> ( 0 < ( # ` W ) <-> 1 <_ ( # ` W ) ) )
5 3 4 syl
 |-  ( W e. Word V -> ( 0 < ( # ` W ) <-> 1 <_ ( # ` W ) ) )
6 1 5 bitr3d
 |-  ( W e. Word V -> ( W =/= (/) <-> 1 <_ ( # ` W ) ) )