swrdnd0

Description: The value of a subword operation for inproper arguments is the empty set. (Contributed by AV, 2-Dec-2022)

		Ref	Expression
	Assertion	swrdnd0	$⊢ S \in Word V \to (\neg (F \in (0 \dots L) \land L \in (0 \dots \|S\|)) \to S substr ⟨F, L⟩ = \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		ianor	$⊢ \neg (F \in (0 \dots L) \land L \in (0 \dots \|S\|)) \leftrightarrow (\neg F \in (0 \dots L) \lor \neg L \in (0 \dots \|S\|))$
2		3ianor	$⊢ \neg (F \in ℕ_{0} \land L \in ℕ_{0} \land F \leq L) \leftrightarrow (\neg F \in ℕ_{0} \lor \neg L \in ℕ_{0} \lor \neg F \leq L)$
3		elfz2nn0	$⊢ F \in (0 \dots L) \leftrightarrow (F \in ℕ_{0} \land L \in ℕ_{0} \land F \leq L)$
4	2 3	xchnxbir	$⊢ \neg F \in (0 \dots L) \leftrightarrow (\neg F \in ℕ_{0} \lor \neg L \in ℕ_{0} \lor \neg F \leq L)$
5		3ianor	$⊢ \neg (L \in ℕ_{0} \land \|S\| \in ℕ_{0} \land L \leq \|S\|) \leftrightarrow (\neg L \in ℕ_{0} \lor \neg \|S\| \in ℕ_{0} \lor \neg L \leq \|S\|)$
6		elfz2nn0	$⊢ L \in (0 \dots \|S\|) \leftrightarrow (L \in ℕ_{0} \land \|S\| \in ℕ_{0} \land L \leq \|S\|)$
7	5 6	xchnxbir	$⊢ \neg L \in (0 \dots \|S\|) \leftrightarrow (\neg L \in ℕ_{0} \lor \neg \|S\| \in ℕ_{0} \lor \neg L \leq \|S\|)$
8	4 7	orbi12i	$⊢ (\neg F \in (0 \dots L) \lor \neg L \in (0 \dots \|S\|)) \leftrightarrow ((\neg F \in ℕ_{0} \lor \neg L \in ℕ_{0} \lor \neg F \leq L) \lor (\neg L \in ℕ_{0} \lor \neg \|S\| \in ℕ_{0} \lor \neg L \leq \|S\|))$
9	1 8	bitri	$⊢ \neg (F \in (0 \dots L) \land L \in (0 \dots \|S\|)) \leftrightarrow ((\neg F \in ℕ_{0} \lor \neg L \in ℕ_{0} \lor \neg F \leq L) \lor (\neg L \in ℕ_{0} \lor \neg \|S\| \in ℕ_{0} \lor \neg L \leq \|S\|))$
10		df-3or	$⊢ (\neg F \in ℕ_{0} \lor \neg L \in ℕ_{0} \lor \neg F \leq L) \leftrightarrow ((\neg F \in ℕ_{0} \lor \neg L \in ℕ_{0}) \lor \neg F \leq L)$
11		ianor	$⊢ \neg (F \in ℕ_{0} \land L \in ℕ_{0}) \leftrightarrow (\neg F \in ℕ_{0} \lor \neg L \in ℕ_{0})$
12		swrdnnn0nd	$⊢ (S \in Word V \land \neg (F \in ℕ_{0} \land L \in ℕ_{0})) \to S substr ⟨F, L⟩ = \emptyset$
13	12	expcom	$⊢ \neg (F \in ℕ_{0} \land L \in ℕ_{0}) \to (S \in Word V \to S substr ⟨F, L⟩ = \emptyset)$
14	11 13	sylbir	$⊢ (\neg F \in ℕ_{0} \lor \neg L \in ℕ_{0}) \to (S \in Word V \to S substr ⟨F, L⟩ = \emptyset)$
15		anor	$⊢ (F \in ℕ_{0} \land L \in ℕ_{0}) \leftrightarrow \neg (\neg F \in ℕ_{0} \lor \neg L \in ℕ_{0})$
16		nn0re	$⊢ L \in ℕ_{0} \to L \in ℝ$
17		nn0re	$⊢ F \in ℕ_{0} \to F \in ℝ$
18		ltnle	$⊢ (L \in ℝ \land F \in ℝ) \to (L < F \leftrightarrow \neg F \leq L)$
19	16 17 18	syl2anr	$⊢ (F \in ℕ_{0} \land L \in ℕ_{0}) \to (L < F \leftrightarrow \neg F \leq L)$
20		nn0z	$⊢ F \in ℕ_{0} \to F \in ℤ$
21		nn0z	$⊢ L \in ℕ_{0} \to L \in ℤ$
22	20 21	anim12i	$⊢ (F \in ℕ_{0} \land L \in ℕ_{0}) \to (F \in ℤ \land L \in ℤ)$
23	22	anim2i	$⊢ (S \in Word V \land (F \in ℕ_{0} \land L \in ℕ_{0})) \to (S \in Word V \land (F \in ℤ \land L \in ℤ))$
24		3anass	$⊢ (S \in Word V \land F \in ℤ \land L \in ℤ) \leftrightarrow (S \in Word V \land (F \in ℤ \land L \in ℤ))$
25	23 24	sylibr	$⊢ (S \in Word V \land (F \in ℕ_{0} \land L \in ℕ_{0})) \to (S \in Word V \land F \in ℤ \land L \in ℤ)$
26	25	adantr	$⊢ ((S \in Word V \land (F \in ℕ_{0} \land L \in ℕ_{0})) \land L < F) \to (S \in Word V \land F \in ℤ \land L \in ℤ)$
27	17 16	anim12ci	$⊢ (F \in ℕ_{0} \land L \in ℕ_{0}) \to (L \in ℝ \land F \in ℝ)$
28	27	adantl	$⊢ (S \in Word V \land (F \in ℕ_{0} \land L \in ℕ_{0})) \to (L \in ℝ \land F \in ℝ)$
29		ltle	$⊢ (L \in ℝ \land F \in ℝ) \to (L < F \to L \leq F)$
30	28 29	syl	$⊢ (S \in Word V \land (F \in ℕ_{0} \land L \in ℕ_{0})) \to (L < F \to L \leq F)$
31	30	imp	$⊢ ((S \in Word V \land (F \in ℕ_{0} \land L \in ℕ_{0})) \land L < F) \to L \leq F$
32	31	3mix2d	$⊢ ((S \in Word V \land (F \in ℕ_{0} \land L \in ℕ_{0})) \land L < F) \to (F < 0 \lor L \leq F \lor \|S\| < L)$
33		swrdnd	$⊢ (S \in Word V \land F \in ℤ \land L \in ℤ) \to ((F < 0 \lor L \leq F \lor \|S\| < L) \to S substr ⟨F, L⟩ = \emptyset)$
34	26 32 33	sylc	$⊢ ((S \in Word V \land (F \in ℕ_{0} \land L \in ℕ_{0})) \land L < F) \to S substr ⟨F, L⟩ = \emptyset$
35	34	ex	$⊢ (S \in Word V \land (F \in ℕ_{0} \land L \in ℕ_{0})) \to (L < F \to S substr ⟨F, L⟩ = \emptyset)$
36	35	expcom	$⊢ (F \in ℕ_{0} \land L \in ℕ_{0}) \to (S \in Word V \to (L < F \to S substr ⟨F, L⟩ = \emptyset))$
37	36	com23	$⊢ (F \in ℕ_{0} \land L \in ℕ_{0}) \to (L < F \to (S \in Word V \to S substr ⟨F, L⟩ = \emptyset))$
38	19 37	sylbird	$⊢ (F \in ℕ_{0} \land L \in ℕ_{0}) \to (\neg F \leq L \to (S \in Word V \to S substr ⟨F, L⟩ = \emptyset))$
39	15 38	sylbir	$⊢ \neg (\neg F \in ℕ_{0} \lor \neg L \in ℕ_{0}) \to (\neg F \leq L \to (S \in Word V \to S substr ⟨F, L⟩ = \emptyset))$
40	39	imp	$⊢ (\neg (\neg F \in ℕ_{0} \lor \neg L \in ℕ_{0}) \land \neg F \leq L) \to (S \in Word V \to S substr ⟨F, L⟩ = \emptyset)$
41	14 40	jaoi3	$⊢ ((\neg F \in ℕ_{0} \lor \neg L \in ℕ_{0}) \lor \neg F \leq L) \to (S \in Word V \to S substr ⟨F, L⟩ = \emptyset)$
42	10 41	sylbi	$⊢ (\neg F \in ℕ_{0} \lor \neg L \in ℕ_{0} \lor \neg F \leq L) \to (S \in Word V \to S substr ⟨F, L⟩ = \emptyset)$
43		3anor	$⊢ (F \in ℕ_{0} \land L \in ℕ_{0} \land F \leq L) \leftrightarrow \neg (\neg F \in ℕ_{0} \lor \neg L \in ℕ_{0} \lor \neg F \leq L)$
44		pm2.24	$⊢ L \in ℕ_{0} \to (\neg L \in ℕ_{0} \to (S \in Word V \to S substr ⟨F, L⟩ = \emptyset))$
45	44	3ad2ant2	$⊢ (F \in ℕ_{0} \land L \in ℕ_{0} \land F \leq L) \to (\neg L \in ℕ_{0} \to (S \in Word V \to S substr ⟨F, L⟩ = \emptyset))$
46	45	com12	$⊢ \neg L \in ℕ_{0} \to ((F \in ℕ_{0} \land L \in ℕ_{0} \land F \leq L) \to (S \in Word V \to S substr ⟨F, L⟩ = \emptyset))$
47		pm2.24	$⊢ \|S\| \in ℕ_{0} \to (\neg \|S\| \in ℕ_{0} \to S substr ⟨F, L⟩ = \emptyset)$
48		lencl	$⊢ S \in Word V \to \|S\| \in ℕ_{0}$
49	47 48	syl11	$⊢ \neg \|S\| \in ℕ_{0} \to (S \in Word V \to S substr ⟨F, L⟩ = \emptyset)$
50	49	a1d	$⊢ \neg \|S\| \in ℕ_{0} \to ((F \in ℕ_{0} \land L \in ℕ_{0} \land F \leq L) \to (S \in Word V \to S substr ⟨F, L⟩ = \emptyset))$
51	48	nn0red	$⊢ S \in Word V \to \|S\| \in ℝ$
52	16	3ad2ant2	$⊢ (F \in ℕ_{0} \land L \in ℕ_{0} \land F \leq L) \to L \in ℝ$
53		ltnle	$⊢ (\|S\| \in ℝ \land L \in ℝ) \to (\|S\| < L \leftrightarrow \neg L \leq \|S\|)$
54	51 52 53	syl2anr	$⊢ ((F \in ℕ_{0} \land L \in ℕ_{0} \land F \leq L) \land S \in Word V) \to (\|S\| < L \leftrightarrow \neg L \leq \|S\|)$
55		simpr	$⊢ ((F \in ℕ_{0} \land L \in ℕ_{0} \land F \leq L) \land S \in Word V) \to S \in Word V$
56	20	3ad2ant1	$⊢ (F \in ℕ_{0} \land L \in ℕ_{0} \land F \leq L) \to F \in ℤ$
57	56	adantr	$⊢ ((F \in ℕ_{0} \land L \in ℕ_{0} \land F \leq L) \land S \in Word V) \to F \in ℤ$
58	21	3ad2ant2	$⊢ (F \in ℕ_{0} \land L \in ℕ_{0} \land F \leq L) \to L \in ℤ$
59	58	adantr	$⊢ ((F \in ℕ_{0} \land L \in ℕ_{0} \land F \leq L) \land S \in Word V) \to L \in ℤ$
60	55 57 59	3jca	$⊢ ((F \in ℕ_{0} \land L \in ℕ_{0} \land F \leq L) \land S \in Word V) \to (S \in Word V \land F \in ℤ \land L \in ℤ)$
61		3mix3	$⊢ \|S\| < L \to (F < 0 \lor L \leq F \lor \|S\| < L)$
62	60 61 33	syl2im	$⊢ ((F \in ℕ_{0} \land L \in ℕ_{0} \land F \leq L) \land S \in Word V) \to (\|S\| < L \to S substr ⟨F, L⟩ = \emptyset)$
63	54 62	sylbird	$⊢ ((F \in ℕ_{0} \land L \in ℕ_{0} \land F \leq L) \land S \in Word V) \to (\neg L \leq \|S\| \to S substr ⟨F, L⟩ = \emptyset)$
64	63	com12	$⊢ \neg L \leq \|S\| \to (((F \in ℕ_{0} \land L \in ℕ_{0} \land F \leq L) \land S \in Word V) \to S substr ⟨F, L⟩ = \emptyset)$
65	64	expd	$⊢ \neg L \leq \|S\| \to ((F \in ℕ_{0} \land L \in ℕ_{0} \land F \leq L) \to (S \in Word V \to S substr ⟨F, L⟩ = \emptyset))$
66	46 50 65	3jaoi	$⊢ (\neg L \in ℕ_{0} \lor \neg \|S\| \in ℕ_{0} \lor \neg L \leq \|S\|) \to ((F \in ℕ_{0} \land L \in ℕ_{0} \land F \leq L) \to (S \in Word V \to S substr ⟨F, L⟩ = \emptyset))$
67	43 66	syl5bir	$⊢ (\neg L \in ℕ_{0} \lor \neg \|S\| \in ℕ_{0} \lor \neg L \leq \|S\|) \to (\neg (\neg F \in ℕ_{0} \lor \neg L \in ℕ_{0} \lor \neg F \leq L) \to (S \in Word V \to S substr ⟨F, L⟩ = \emptyset))$
68	67	impcom	$⊢ (\neg (\neg F \in ℕ_{0} \lor \neg L \in ℕ_{0} \lor \neg F \leq L) \land (\neg L \in ℕ_{0} \lor \neg \|S\| \in ℕ_{0} \lor \neg L \leq \|S\|)) \to (S \in Word V \to S substr ⟨F, L⟩ = \emptyset)$
69	42 68	jaoi3	$⊢ ((\neg F \in ℕ_{0} \lor \neg L \in ℕ_{0} \lor \neg F \leq L) \lor (\neg L \in ℕ_{0} \lor \neg \|S\| \in ℕ_{0} \lor \neg L \leq \|S\|)) \to (S \in Word V \to S substr ⟨F, L⟩ = \emptyset)$
70	69	com12	$⊢ S \in Word V \to (((\neg F \in ℕ_{0} \lor \neg L \in ℕ_{0} \lor \neg F \leq L) \lor (\neg L \in ℕ_{0} \lor \neg \|S\| \in ℕ_{0} \lor \neg L \leq \|S\|)) \to S substr ⟨F, L⟩ = \emptyset)$
71	9 70	syl5bi	$⊢ S \in Word V \to (\neg (F \in (0 \dots L) \land L \in (0 \dots \|S\|)) \to S substr ⟨F, L⟩ = \emptyset)$

Metamath Proof Explorer

Theorem swrdnd0

Proof