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 ∈ Word V → W ≠ ∅ ↔ 1 ≤ W

Proof

Step Hyp Ref Expression
1 hashneq0 ⊢ W ∈ Word V → 0 < W ↔ W ≠ ∅
2 lencl ⊢ W ∈ Word V → W ∈ ℕ 0
3 2 nn0zd ⊢ W ∈ Word V → W ∈ ℤ
4 zgt0ge1 ⊢ W ∈ ℤ → 0 < W ↔ 1 ≤ W
5 3 4 syl ⊢ W ∈ Word V → 0 < W ↔ 1 ≤ W
6 1 5 bitr3d ⊢ W ∈ Word V → W ≠ ∅ ↔ 1 ≤ W