Metamath Proof Explorer

Theorem len0nnbi

Description: The length of a word is a positive integer iff the word is not empty. (Contributed by AV, 22-Mar-2022)

Ref Expression
Assertion len0nnbi ⊢ W ∈ Word S → W ≠ ∅ ↔ W ∈ ℕ

Proof

Step Hyp Ref Expression
1 lennncl ⊢ W ∈ Word S ∧ W ≠ ∅ → W ∈ ℕ
2 1 ex ⊢ W ∈ Word S → W ≠ ∅ → W ∈ ℕ
3 nnge1 ⊢ W ∈ ℕ → 1 ≤ W
4 wrdlenge1n0 ⊢ W ∈ Word S → W ≠ ∅ ↔ 1 ≤ W
5 3 4 imbitrrid ⊢ W ∈ Word S → W ∈ ℕ → W ≠ ∅
6 2 5 impbid ⊢ W ∈ Word S → W ≠ ∅ ↔ W ∈ ℕ