wrdlenge1n0

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

		Ref	Expression
	Assertion	wrdlenge1n0	$⊢ W \in Word V \to (W \neq \emptyset \leftrightarrow 1 \leq \|W\|)$

Step	Hyp	Ref	Expression
1		hashneq0	$⊢ W \in Word V \to (0 < \|W\| \leftrightarrow W \neq \emptyset)$
2		lencl	$⊢ W \in Word V \to \|W\| \in ℕ_{0}$
3	2	nn0zd	$⊢ W \in Word V \to \|W\| \in ℤ$
4		zgt0ge1	$⊢ \|W\| \in ℤ \to (0 < \|W\| \leftrightarrow 1 \leq \|W\|)$
5	3 4	syl	$⊢ W \in Word V \to (0 < \|W\| \leftrightarrow 1 \leq \|W\|)$
6	1 5	bitr3d	$⊢ W \in Word V \to (W \neq \emptyset \leftrightarrow 1 \leq \|W\|)$

Metamath Proof Explorer