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