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 ⊢ W ∈ Word V ∧ 2 ≤ W → W ≠ ∅

Proof

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