This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ≤ ( ♯ ‘ 𝑊 ) ) → 𝑊 ≠ ∅ )