Theorem wrdlenge1n0

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

	Ref	Expression
Assertion	wrdlenge1n0	⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 ≠ ∅ ↔ 1 ≤ ( ♯ ‘ 𝑊 ) ) )

Proof

Step	Hyp	Ref	Expression
1		hashneq0	⊢ ( 𝑊 ∈ Word 𝑉 → ( 0 < ( ♯ ‘ 𝑊 ) ↔ 𝑊 ≠ ∅ ) )
2		lencl	⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
3	2	nn0zd	⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℤ )
4		zgt0ge1	⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℤ → ( 0 < ( ♯ ‘ 𝑊 ) ↔ 1 ≤ ( ♯ ‘ 𝑊 ) ) )
5	3 4	syl	⊢ ( 𝑊 ∈ Word 𝑉 → ( 0 < ( ♯ ‘ 𝑊 ) ↔ 1 ≤ ( ♯ ‘ 𝑊 ) ) )
6	1 5	bitr3d	⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 ≠ ∅ ↔ 1 ≤ ( ♯ ‘ 𝑊 ) ) )