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	⊢ ( 𝑊 ∈ Word 𝑆 → ( 𝑊 ≠ ∅ ↔ ( ♯ ‘ 𝑊 ) ∈ ℕ ) )

Proof

Step	Hyp	Ref	Expression
1		lennncl	⊢ ( ( 𝑊 ∈ Word 𝑆 ∧ 𝑊 ≠ ∅ ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
2	1	ex	⊢ ( 𝑊 ∈ Word 𝑆 → ( 𝑊 ≠ ∅ → ( ♯ ‘ 𝑊 ) ∈ ℕ ) )
3		nnge1	⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ → 1 ≤ ( ♯ ‘ 𝑊 ) )
4		wrdlenge1n0	⊢ ( 𝑊 ∈ Word 𝑆 → ( 𝑊 ≠ ∅ ↔ 1 ≤ ( ♯ ‘ 𝑊 ) ) )
5	3 4	imbitrrid	⊢ ( 𝑊 ∈ Word 𝑆 → ( ( ♯ ‘ 𝑊 ) ∈ ℕ → 𝑊 ≠ ∅ ) )
6	2 5	impbid	⊢ ( 𝑊 ∈ Word 𝑆 → ( 𝑊 ≠ ∅ ↔ ( ♯ ‘ 𝑊 ) ∈ ℕ ) )