Metamath Proof Explorer

Theorem wrdlenge2n0

Description: A word with length at least 2 is not empty. (Contributed by AV, 18-Jun-2018) (Proof shortened by AV, 14-Oct-2018)

Ref Expression
Assertion wrdlenge2n0 ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → 𝑊 ≠ ∅ )

Proof

Step Hyp Ref Expression
1 1red ( 𝑊 ∈ Word 𝑉 → 1 ∈ ℝ )
2 2re 2 ∈ ℝ
3 2 a1i ( 𝑊 ∈ Word 𝑉 → 2 ∈ ℝ )
4 lencl ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
5 4 nn0red ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℝ )
6 1 3 5 3jca ( 𝑊 ∈ Word 𝑉 → ( 1 ∈ ℝ ∧ 2 ∈ ℝ ∧ ( ♯ ‘ 𝑊 ) ∈ ℝ ) )
7 6 adantr ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( 1 ∈ ℝ ∧ 2 ∈ ℝ ∧ ( ♯ ‘ 𝑊 ) ∈ ℝ ) )
8 simpr ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → 2 ≤ ( ♯ ‘ 𝑊 ) )
9 1lt2 1 < 2
10 8 9 jctil ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( 1 < 2 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) )
11 ltleletr ( ( 1 ∈ ℝ ∧ 2 ∈ ℝ ∧ ( ♯ ‘ 𝑊 ) ∈ ℝ ) → ( ( 1 < 2 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → 1 ≤ ( ♯ ‘ 𝑊 ) ) )
12 7 10 11 sylc ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → 1 ≤ ( ♯ ‘ 𝑊 ) )
13 wrdlenge1n0 ( 𝑊 ∈ Word 𝑉 → ( 𝑊 ≠ ∅ ↔ 1 ≤ ( ♯ ‘ 𝑊 ) ) )
14 13 adantr ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑊 ≠ ∅ ↔ 1 ≤ ( ♯ ‘ 𝑊 ) ) )
15 12 14 mpbird ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑊 ) ) → 𝑊 ≠ ∅ )