swrdnnn0nd

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

		Ref	Expression
	Assertion	swrdnnn0nd	$⊢ (S \in Word V \land \neg (F \in ℕ_{0} \land L \in ℕ_{0})) \to S substr ⟨F, L⟩ = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		ianor	$⊢ \neg (F \in ℕ_{0} \land L \in ℕ_{0}) \leftrightarrow (\neg F \in ℕ_{0} \lor \neg L \in ℕ_{0})$
2		ianor	$⊢ \neg (F \in ℤ \land 0 \leq F) \leftrightarrow (\neg F \in ℤ \lor \neg 0 \leq F)$
3		elnn0z	$⊢ F \in ℕ_{0} \leftrightarrow (F \in ℤ \land 0 \leq F)$
4	2 3	xchnxbir	$⊢ \neg F \in ℕ_{0} \leftrightarrow (\neg F \in ℤ \lor \neg 0 \leq F)$
5		ianor	$⊢ \neg (L \in ℤ \land 0 \leq L) \leftrightarrow (\neg L \in ℤ \lor \neg 0 \leq L)$
6		elnn0z	$⊢ L \in ℕ_{0} \leftrightarrow (L \in ℤ \land 0 \leq L)$
7	5 6	xchnxbir	$⊢ \neg L \in ℕ_{0} \leftrightarrow (\neg L \in ℤ \lor \neg 0 \leq L)$
8	4 7	orbi12i	$⊢ (\neg F \in ℕ_{0} \lor \neg L \in ℕ_{0}) \leftrightarrow ((\neg F \in ℤ \lor \neg 0 \leq F) \lor (\neg L \in ℤ \lor \neg 0 \leq L))$
9		or4	$⊢ ((\neg F \in ℤ \lor \neg 0 \leq F) \lor (\neg L \in ℤ \lor \neg 0 \leq L)) \leftrightarrow ((\neg F \in ℤ \lor \neg L \in ℤ) \lor (\neg 0 \leq F \lor \neg 0 \leq L))$
10		ianor	$⊢ \neg (F \in ℤ \land L \in ℤ) \leftrightarrow (\neg F \in ℤ \lor \neg L \in ℤ)$
11	10	bicomi	$⊢ (\neg F \in ℤ \lor \neg L \in ℤ) \leftrightarrow \neg (F \in ℤ \land L \in ℤ)$
12	11	orbi1i	$⊢ ((\neg F \in ℤ \lor \neg L \in ℤ) \lor (\neg 0 \leq F \lor \neg 0 \leq L)) \leftrightarrow (\neg (F \in ℤ \land L \in ℤ) \lor (\neg 0 \leq F \lor \neg 0 \leq L))$
13	9 12	bitri	$⊢ ((\neg F \in ℤ \lor \neg 0 \leq F) \lor (\neg L \in ℤ \lor \neg 0 \leq L)) \leftrightarrow (\neg (F \in ℤ \land L \in ℤ) \lor (\neg 0 \leq F \lor \neg 0 \leq L))$
14	8 13	bitri	$⊢ (\neg F \in ℕ_{0} \lor \neg L \in ℕ_{0}) \leftrightarrow (\neg (F \in ℤ \land L \in ℤ) \lor (\neg 0 \leq F \lor \neg 0 \leq L))$
15	1 14	bitri	$⊢ \neg (F \in ℕ_{0} \land L \in ℕ_{0}) \leftrightarrow (\neg (F \in ℤ \land L \in ℤ) \lor (\neg 0 \leq F \lor \neg 0 \leq L))$
16		swrdnznd	$⊢ \neg (F \in ℤ \land L \in ℤ) \to S substr ⟨F, L⟩ = \emptyset$
17	16	a1d	$⊢ \neg (F \in ℤ \land L \in ℤ) \to (S \in Word V \to S substr ⟨F, L⟩ = \emptyset)$
18		notnotb	$⊢ (F \in ℤ \land L \in ℤ) \leftrightarrow \neg \neg (F \in ℤ \land L \in ℤ)$
19		zre	$⊢ F \in ℤ \to F \in ℝ$
20		0red	$⊢ F \in ℤ \to 0 \in ℝ$
21	19 20	jca	$⊢ F \in ℤ \to (F \in ℝ \land 0 \in ℝ)$
22	21	3ad2ant2	$⊢ (S \in Word V \land F \in ℤ \land L \in ℤ) \to (F \in ℝ \land 0 \in ℝ)$
23		ltnle	$⊢ (F \in ℝ \land 0 \in ℝ) \to (F < 0 \leftrightarrow \neg 0 \leq F)$
24	22 23	syl	$⊢ (S \in Word V \land F \in ℤ \land L \in ℤ) \to (F < 0 \leftrightarrow \neg 0 \leq F)$
25		orc	$⊢ F < 0 \to (F < 0 \lor L \leq F)$
26	24 25	syl6bir	$⊢ (S \in Word V \land F \in ℤ \land L \in ℤ) \to (\neg 0 \leq F \to (F < 0 \lor L \leq F))$
27	26	com12	$⊢ \neg 0 \leq F \to ((S \in Word V \land F \in ℤ \land L \in ℤ) \to (F < 0 \lor L \leq F))$
28		notnotb	$⊢ 0 \leq F \leftrightarrow \neg \neg 0 \leq F$
29	28	a1i	$⊢ (S \in Word V \land F \in ℤ \land L \in ℤ) \to (0 \leq F \leftrightarrow \neg \neg 0 \leq F)$
30		zre	$⊢ L \in ℤ \to L \in ℝ$
31		0red	$⊢ L \in ℤ \to 0 \in ℝ$
32	30 31	jca	$⊢ L \in ℤ \to (L \in ℝ \land 0 \in ℝ)$
33	32	3ad2ant3	$⊢ (S \in Word V \land F \in ℤ \land L \in ℤ) \to (L \in ℝ \land 0 \in ℝ)$
34		ltnle	$⊢ (L \in ℝ \land 0 \in ℝ) \to (L < 0 \leftrightarrow \neg 0 \leq L)$
35	33 34	syl	$⊢ (S \in Word V \land F \in ℤ \land L \in ℤ) \to (L < 0 \leftrightarrow \neg 0 \leq L)$
36	29 35	anbi12d	$⊢ (S \in Word V \land F \in ℤ \land L \in ℤ) \to ((0 \leq F \land L < 0) \leftrightarrow (\neg \neg 0 \leq F \land \neg 0 \leq L))$
37	30	3ad2ant3	$⊢ (S \in Word V \land F \in ℤ \land L \in ℤ) \to L \in ℝ$
38		0red	$⊢ (S \in Word V \land F \in ℤ \land L \in ℤ) \to 0 \in ℝ$
39	19	3ad2ant2	$⊢ (S \in Word V \land F \in ℤ \land L \in ℤ) \to F \in ℝ$
40		ltleletr	$⊢ (L \in ℝ \land 0 \in ℝ \land F \in ℝ) \to ((L < 0 \land 0 \leq F) \to L \leq F)$
41	37 38 39 40	syl3anc	$⊢ (S \in Word V \land F \in ℤ \land L \in ℤ) \to ((L < 0 \land 0 \leq F) \to L \leq F)$
42		olc	$⊢ L \leq F \to (F < 0 \lor L \leq F)$
43	41 42	syl6	$⊢ (S \in Word V \land F \in ℤ \land L \in ℤ) \to ((L < 0 \land 0 \leq F) \to (F < 0 \lor L \leq F))$
44	43	ancomsd	$⊢ (S \in Word V \land F \in ℤ \land L \in ℤ) \to ((0 \leq F \land L < 0) \to (F < 0 \lor L \leq F))$
45	36 44	sylbird	$⊢ (S \in Word V \land F \in ℤ \land L \in ℤ) \to ((\neg \neg 0 \leq F \land \neg 0 \leq L) \to (F < 0 \lor L \leq F))$
46	45	com12	$⊢ (\neg \neg 0 \leq F \land \neg 0 \leq L) \to ((S \in Word V \land F \in ℤ \land L \in ℤ) \to (F < 0 \lor L \leq F))$
47	27 46	jaoi3	$⊢ (\neg 0 \leq F \lor \neg 0 \leq L) \to ((S \in Word V \land F \in ℤ \land L \in ℤ) \to (F < 0 \lor L \leq F))$
48	47	impcom	$⊢ ((S \in Word V \land F \in ℤ \land L \in ℤ) \land (\neg 0 \leq F \lor \neg 0 \leq L)) \to (F < 0 \lor L \leq F)$
49	48	orcd	$⊢ ((S \in Word V \land F \in ℤ \land L \in ℤ) \land (\neg 0 \leq F \lor \neg 0 \leq L)) \to ((F < 0 \lor L \leq F) \lor \|S\| < L)$
50		df-3or	$⊢ (F < 0 \lor L \leq F \lor \|S\| < L) \leftrightarrow ((F < 0 \lor L \leq F) \lor \|S\| < L)$
51	49 50	sylibr	$⊢ ((S \in Word V \land F \in ℤ \land L \in ℤ) \land (\neg 0 \leq F \lor \neg 0 \leq L)) \to (F < 0 \lor L \leq F \lor \|S\| < L)$
52		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)$
53	52	imp	$⊢ ((S \in Word V \land F \in ℤ \land L \in ℤ) \land (F < 0 \lor L \leq F \lor \|S\| < L)) \to S substr ⟨F, L⟩ = \emptyset$
54	51 53	syldan	$⊢ ((S \in Word V \land F \in ℤ \land L \in ℤ) \land (\neg 0 \leq F \lor \neg 0 \leq L)) \to S substr ⟨F, L⟩ = \emptyset$
55	54	ex	$⊢ (S \in Word V \land F \in ℤ \land L \in ℤ) \to ((\neg 0 \leq F \lor \neg 0 \leq L) \to S substr ⟨F, L⟩ = \emptyset)$
56	55	3expb	$⊢ (S \in Word V \land (F \in ℤ \land L \in ℤ)) \to ((\neg 0 \leq F \lor \neg 0 \leq L) \to S substr ⟨F, L⟩ = \emptyset)$
57	56	expcom	$⊢ (F \in ℤ \land L \in ℤ) \to (S \in Word V \to ((\neg 0 \leq F \lor \neg 0 \leq L) \to S substr ⟨F, L⟩ = \emptyset))$
58	57	com23	$⊢ (F \in ℤ \land L \in ℤ) \to ((\neg 0 \leq F \lor \neg 0 \leq L) \to (S \in Word V \to S substr ⟨F, L⟩ = \emptyset))$
59	18 58	sylbir	$⊢ \neg \neg (F \in ℤ \land L \in ℤ) \to ((\neg 0 \leq F \lor \neg 0 \leq L) \to (S \in Word V \to S substr ⟨F, L⟩ = \emptyset))$
60	59	imp	$⊢ (\neg \neg (F \in ℤ \land L \in ℤ) \land (\neg 0 \leq F \lor \neg 0 \leq L)) \to (S \in Word V \to S substr ⟨F, L⟩ = \emptyset)$
61	17 60	jaoi3	$⊢ (\neg (F \in ℤ \land L \in ℤ) \lor (\neg 0 \leq F \lor \neg 0 \leq L)) \to (S \in Word V \to S substr ⟨F, L⟩ = \emptyset)$
62	15 61	sylbi	$⊢ \neg (F \in ℕ_{0} \land L \in ℕ_{0}) \to (S \in Word V \to S substr ⟨F, L⟩ = \emptyset)$
63	62	impcom	$⊢ (S \in Word V \land \neg (F \in ℕ_{0} \land L \in ℕ_{0})) \to S substr ⟨F, L⟩ = \emptyset$

Metamath Proof Explorer

Theorem swrdnnn0nd

Proof