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 \in Word V \land 2 \leq \|W\|) \to W \neq \emptyset$

Step	Hyp	Ref	Expression
1		1red	$⊢ W \in Word V \to 1 \in ℝ$
2		2re	$⊢ 2 \in ℝ$
3	2	a1i	$⊢ W \in Word V \to 2 \in ℝ$
4		lencl	$⊢ W \in Word V \to \|W\| \in ℕ_{0}$
5	4	nn0red	$⊢ W \in Word V \to \|W\| \in ℝ$
6	1 3 5	3jca	$⊢ W \in Word V \to (1 \in ℝ \land 2 \in ℝ \land \|W\| \in ℝ)$
7	6	adantr	$⊢ (W \in Word V \land 2 \leq \|W\|) \to (1 \in ℝ \land 2 \in ℝ \land \|W\| \in ℝ)$
8		simpr	$⊢ (W \in Word V \land 2 \leq \|W\|) \to 2 \leq \|W\|$
9		1lt2	$⊢ 1 < 2$
10	8 9	jctil	$⊢ (W \in Word V \land 2 \leq \|W\|) \to (1 < 2 \land 2 \leq \|W\|)$
11		ltleletr	$⊢ (1 \in ℝ \land 2 \in ℝ \land \|W\| \in ℝ) \to ((1 < 2 \land 2 \leq \|W\|) \to 1 \leq \|W\|)$
12	7 10 11	sylc	$⊢ (W \in Word V \land 2 \leq \|W\|) \to 1 \leq \|W\|$
13		wrdlenge1n0	$⊢ W \in Word V \to (W \neq \emptyset \leftrightarrow 1 \leq \|W\|)$
14	13	adantr	$⊢ (W \in Word V \land 2 \leq \|W\|) \to (W \neq \emptyset \leftrightarrow 1 \leq \|W\|)$
15	12 14	mpbird	$⊢ (W \in Word V \land 2 \leq \|W\|) \to W \neq \emptyset$

Metamath Proof Explorer