swrdnd

Description: The value of the subword extractor is the empty set (undefined) if the range is not valid. (Contributed by Alexander van der Vekens, 16-Mar-2018) (Proof shortened by AV, 2-May-2020)

		Ref	Expression
	Assertion	swrdnd	$⊢ (W \in Word V \land F \in ℤ \land L \in ℤ) \to ((F < 0 \lor L \leq F \lor \|W\| < L) \to W substr ⟨F, L⟩ = \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		3orcomb	$⊢ (F < 0 \lor L \leq F \lor \|W\| < L) \leftrightarrow (F < 0 \lor \|W\| < L \lor L \leq F)$
2		df-3or	$⊢ (F < 0 \lor \|W\| < L \lor L \leq F) \leftrightarrow ((F < 0 \lor \|W\| < L) \lor L \leq F)$
3	1 2	bitri	$⊢ (F < 0 \lor L \leq F \lor \|W\| < L) \leftrightarrow ((F < 0 \lor \|W\| < L) \lor L \leq F)$
4		swrdlend	$⊢ (W \in Word V \land F \in ℤ \land L \in ℤ) \to (L \leq F \to W substr ⟨F, L⟩ = \emptyset)$
5	4	com12	$⊢ L \leq F \to ((W \in Word V \land F \in ℤ \land L \in ℤ) \to W substr ⟨F, L⟩ = \emptyset)$
6		swrdval	$⊢ (W \in Word V \land F \in ℤ \land L \in ℤ) \to W substr ⟨F, L⟩ = if ((F ..^L) \subseteq dom W, (i \in (0 ..^L - F) ⟼ W (i + F)), \emptyset)$
7	6	adantl	$⊢ (((F < 0 \lor \|W\| < L) \land \neg L \leq F) \land (W \in Word V \land F \in ℤ \land L \in ℤ)) \to W substr ⟨F, L⟩ = if ((F ..^L) \subseteq dom W, (i \in (0 ..^L - F) ⟼ W (i + F)), \emptyset)$
8		zre	$⊢ F \in ℤ \to F \in ℝ$
9		0red	$⊢ F \in ℤ \to 0 \in ℝ$
10	8 9	ltnled	$⊢ F \in ℤ \to (F < 0 \leftrightarrow \neg 0 \leq F)$
11	10	3ad2ant2	$⊢ (W \in Word V \land F \in ℤ \land L \in ℤ) \to (F < 0 \leftrightarrow \neg 0 \leq F)$
12		lencl	$⊢ W \in Word V \to \|W\| \in ℕ_{0}$
13	12	nn0red	$⊢ W \in Word V \to \|W\| \in ℝ$
14		zre	$⊢ L \in ℤ \to L \in ℝ$
15	13 14	anim12i	$⊢ (W \in Word V \land L \in ℤ) \to (\|W\| \in ℝ \land L \in ℝ)$
16	15	3adant2	$⊢ (W \in Word V \land F \in ℤ \land L \in ℤ) \to (\|W\| \in ℝ \land L \in ℝ)$
17		ltnle	$⊢ (\|W\| \in ℝ \land L \in ℝ) \to (\|W\| < L \leftrightarrow \neg L \leq \|W\|)$
18	16 17	syl	$⊢ (W \in Word V \land F \in ℤ \land L \in ℤ) \to (\|W\| < L \leftrightarrow \neg L \leq \|W\|)$
19	11 18	orbi12d	$⊢ (W \in Word V \land F \in ℤ \land L \in ℤ) \to ((F < 0 \lor \|W\| < L) \leftrightarrow (\neg 0 \leq F \lor \neg L \leq \|W\|))$
20	19	biimpcd	$⊢ (F < 0 \lor \|W\| < L) \to ((W \in Word V \land F \in ℤ \land L \in ℤ) \to (\neg 0 \leq F \lor \neg L \leq \|W\|))$
21	20	adantr	$⊢ ((F < 0 \lor \|W\| < L) \land \neg L \leq F) \to ((W \in Word V \land F \in ℤ \land L \in ℤ) \to (\neg 0 \leq F \lor \neg L \leq \|W\|))$
22	21	imp	$⊢ (((F < 0 \lor \|W\| < L) \land \neg L \leq F) \land (W \in Word V \land F \in ℤ \land L \in ℤ)) \to (\neg 0 \leq F \lor \neg L \leq \|W\|)$
23		ianor	$⊢ \neg (0 \leq F \land L \leq \|W\|) \leftrightarrow (\neg 0 \leq F \lor \neg L \leq \|W\|)$
24	22 23	sylibr	$⊢ (((F < 0 \lor \|W\| < L) \land \neg L \leq F) \land (W \in Word V \land F \in ℤ \land L \in ℤ)) \to \neg (0 \leq F \land L \leq \|W\|)$
25		3simpc	$⊢ (W \in Word V \land F \in ℤ \land L \in ℤ) \to (F \in ℤ \land L \in ℤ)$
26	12	nn0zd	$⊢ W \in Word V \to \|W\| \in ℤ$
27		0z	$⊢ 0 \in ℤ$
28	26 27	jctil	$⊢ W \in Word V \to (0 \in ℤ \land \|W\| \in ℤ)$
29	28	3ad2ant1	$⊢ (W \in Word V \land F \in ℤ \land L \in ℤ) \to (0 \in ℤ \land \|W\| \in ℤ)$
30		ltnle	$⊢ (F \in ℝ \land L \in ℝ) \to (F < L \leftrightarrow \neg L \leq F)$
31	8 14 30	syl2an	$⊢ (F \in ℤ \land L \in ℤ) \to (F < L \leftrightarrow \neg L \leq F)$
32	31	3adant1	$⊢ (W \in Word V \land F \in ℤ \land L \in ℤ) \to (F < L \leftrightarrow \neg L \leq F)$
33	32	biimprcd	$⊢ \neg L \leq F \to ((W \in Word V \land F \in ℤ \land L \in ℤ) \to F < L)$
34	33	adantl	$⊢ ((F < 0 \lor \|W\| < L) \land \neg L \leq F) \to ((W \in Word V \land F \in ℤ \land L \in ℤ) \to F < L)$
35	34	imp	$⊢ (((F < 0 \lor \|W\| < L) \land \neg L \leq F) \land (W \in Word V \land F \in ℤ \land L \in ℤ)) \to F < L$
36		ssfzo12bi	$⊢ ((F \in ℤ \land L \in ℤ) \land (0 \in ℤ \land \|W\| \in ℤ) \land F < L) \to ((F ..^L) \subseteq (0 ..^\|W\|) \leftrightarrow (0 \leq F \land L \leq \|W\|))$
37	25 29 35 36	syl2an23an	$⊢ (((F < 0 \lor \|W\| < L) \land \neg L \leq F) \land (W \in Word V \land F \in ℤ \land L \in ℤ)) \to ((F ..^L) \subseteq (0 ..^\|W\|) \leftrightarrow (0 \leq F \land L \leq \|W\|))$
38	24 37	mtbird	$⊢ (((F < 0 \lor \|W\| < L) \land \neg L \leq F) \land (W \in Word V \land F \in ℤ \land L \in ℤ)) \to \neg (F ..^L) \subseteq (0 ..^\|W\|)$
39		wrddm	$⊢ W \in Word V \to dom W = (0 ..^\|W\|)$
40	39	sseq2d	$⊢ W \in Word V \to ((F ..^L) \subseteq dom W \leftrightarrow (F ..^L) \subseteq (0 ..^\|W\|))$
41	40	notbid	$⊢ W \in Word V \to (\neg (F ..^L) \subseteq dom W \leftrightarrow \neg (F ..^L) \subseteq (0 ..^\|W\|))$
42	41	3ad2ant1	$⊢ (W \in Word V \land F \in ℤ \land L \in ℤ) \to (\neg (F ..^L) \subseteq dom W \leftrightarrow \neg (F ..^L) \subseteq (0 ..^\|W\|))$
43	42	adantl	$⊢ (((F < 0 \lor \|W\| < L) \land \neg L \leq F) \land (W \in Word V \land F \in ℤ \land L \in ℤ)) \to (\neg (F ..^L) \subseteq dom W \leftrightarrow \neg (F ..^L) \subseteq (0 ..^\|W\|))$
44	38 43	mpbird	$⊢ (((F < 0 \lor \|W\| < L) \land \neg L \leq F) \land (W \in Word V \land F \in ℤ \land L \in ℤ)) \to \neg (F ..^L) \subseteq dom W$
45	44	iffalsed	$⊢ (((F < 0 \lor \|W\| < L) \land \neg L \leq F) \land (W \in Word V \land F \in ℤ \land L \in ℤ)) \to if ((F ..^L) \subseteq dom W, (i \in (0 ..^L - F) ⟼ W (i + F)), \emptyset) = \emptyset$
46	7 45	eqtrd	$⊢ (((F < 0 \lor \|W\| < L) \land \neg L \leq F) \land (W \in Word V \land F \in ℤ \land L \in ℤ)) \to W substr ⟨F, L⟩ = \emptyset$
47	46	exp31	$⊢ (F < 0 \lor \|W\| < L) \to (\neg L \leq F \to ((W \in Word V \land F \in ℤ \land L \in ℤ) \to W substr ⟨F, L⟩ = \emptyset))$
48	47	impcom	$⊢ (\neg L \leq F \land (F < 0 \lor \|W\| < L)) \to ((W \in Word V \land F \in ℤ \land L \in ℤ) \to W substr ⟨F, L⟩ = \emptyset)$
49	5 48	jaoi3	$⊢ (L \leq F \lor (F < 0 \lor \|W\| < L)) \to ((W \in Word V \land F \in ℤ \land L \in ℤ) \to W substr ⟨F, L⟩ = \emptyset)$
50	49	orcoms	$⊢ ((F < 0 \lor \|W\| < L) \lor L \leq F) \to ((W \in Word V \land F \in ℤ \land L \in ℤ) \to W substr ⟨F, L⟩ = \emptyset)$
51	3 50	sylbi	$⊢ (F < 0 \lor L \leq F \lor \|W\| < L) \to ((W \in Word V \land F \in ℤ \land L \in ℤ) \to W substr ⟨F, L⟩ = \emptyset)$
52	51	com12	$⊢ (W \in Word V \land F \in ℤ \land L \in ℤ) \to ((F < 0 \lor L \leq F \lor \|W\| < L) \to W substr ⟨F, L⟩ = \emptyset)$

Metamath Proof Explorer

Theorem swrdnd

Proof