Metamath Proof Explorer

Theorem 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 ( ( 𝑆 ∈ Word 𝑉 ∧ ¬ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ )

Proof

Step Hyp Ref Expression
1 ianor ⊢ ( ¬ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) ↔ ( ¬ 𝐹 ∈ ℕ0 ∨ ¬ 𝐿 ∈ ℕ0 ) )
2 ianor ⊢ ( ¬ ( 𝐹 ∈ ℤ ∧ 0 ≤ 𝐹 ) ↔ ( ¬ 𝐹 ∈ ℤ ∨ ¬ 0 ≤ 𝐹 ) )
3 elnn0z ⊢ ( 𝐹 ∈ ℕ0 ↔ ( 𝐹 ∈ ℤ ∧ 0 ≤ 𝐹 ) )
4 2 3 xchnxbir ⊢ ( ¬ 𝐹 ∈ ℕ0 ↔ ( ¬ 𝐹 ∈ ℤ ∨ ¬ 0 ≤ 𝐹 ) )
5 ianor ⊢ ( ¬ ( 𝐿 ∈ ℤ ∧ 0 ≤ 𝐿 ) ↔ ( ¬ 𝐿 ∈ ℤ ∨ ¬ 0 ≤ 𝐿 ) )
6 elnn0z ⊢ ( 𝐿 ∈ ℕ0 ↔ ( 𝐿 ∈ ℤ ∧ 0 ≤ 𝐿 ) )
7 5 6 xchnxbir ⊢ ( ¬ 𝐿 ∈ ℕ0 ↔ ( ¬ 𝐿 ∈ ℤ ∨ ¬ 0 ≤ 𝐿 ) )
8 4 7 orbi12i ⊢ ( ( ¬ 𝐹 ∈ ℕ0 ∨ ¬ 𝐿 ∈ ℕ0 ) ↔ ( ( ¬ 𝐹 ∈ ℤ ∨ ¬ 0 ≤ 𝐹 ) ∨ ( ¬ 𝐿 ∈ ℤ ∨ ¬ 0 ≤ 𝐿 ) ) )
9 or4 ⊢ ( ( ( ¬ 𝐹 ∈ ℤ ∨ ¬ 0 ≤ 𝐹 ) ∨ ( ¬ 𝐿 ∈ ℤ ∨ ¬ 0 ≤ 𝐿 ) ) ↔ ( ( ¬ 𝐹 ∈ ℤ ∨ ¬ 𝐿 ∈ ℤ ) ∨ ( ¬ 0 ≤ 𝐹 ∨ ¬ 0 ≤ 𝐿 ) ) )
10 ianor ⊢ ( ¬ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ↔ ( ¬ 𝐹 ∈ ℤ ∨ ¬ 𝐿 ∈ ℤ ) )
11 10 bicomi ⊢ ( ( ¬ 𝐹 ∈ ℤ ∨ ¬ 𝐿 ∈ ℤ ) ↔ ¬ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) )
12 11 orbi1i ⊢ ( ( ( ¬ 𝐹 ∈ ℤ ∨ ¬ 𝐿 ∈ ℤ ) ∨ ( ¬ 0 ≤ 𝐹 ∨ ¬ 0 ≤ 𝐿 ) ) ↔ ( ¬ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∨ ( ¬ 0 ≤ 𝐹 ∨ ¬ 0 ≤ 𝐿 ) ) )
13 9 12 bitri ⊢ ( ( ( ¬ 𝐹 ∈ ℤ ∨ ¬ 0 ≤ 𝐹 ) ∨ ( ¬ 𝐿 ∈ ℤ ∨ ¬ 0 ≤ 𝐿 ) ) ↔ ( ¬ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∨ ( ¬ 0 ≤ 𝐹 ∨ ¬ 0 ≤ 𝐿 ) ) )
14 8 13 bitri ⊢ ( ( ¬ 𝐹 ∈ ℕ0 ∨ ¬ 𝐿 ∈ ℕ0 ) ↔ ( ¬ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∨ ( ¬ 0 ≤ 𝐹 ∨ ¬ 0 ≤ 𝐿 ) ) )
15 1 14 bitri ⊢ ( ¬ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) ↔ ( ¬ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∨ ( ¬ 0 ≤ 𝐹 ∨ ¬ 0 ≤ 𝐿 ) ) )
16 swrdnznd ⊢ ( ¬ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ )
17 16 a1d ⊢ ( ¬ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝑆 ∈ Word 𝑉 → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) )
18 notnotb ⊢ ( ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ↔ ¬ ¬ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) )
19 zre ⊢ ( 𝐹 ∈ ℤ → 𝐹 ∈ ℝ )
20 0red ⊢ ( 𝐹 ∈ ℤ → 0 ∈ ℝ )
21 19 20 jca ⊢ ( 𝐹 ∈ ℤ → ( 𝐹 ∈ ℝ ∧ 0 ∈ ℝ ) )
22 21 3ad2ant2 ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝐹 ∈ ℝ ∧ 0 ∈ ℝ ) )
23 ltnle ⊢ ( ( 𝐹 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝐹 < 0 ↔ ¬ 0 ≤ 𝐹 ) )
24 22 23 syl ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝐹 < 0 ↔ ¬ 0 ≤ 𝐹 ) )
25 orc ⊢ ( 𝐹 < 0 → ( 𝐹 < 0 ∨ 𝐿 ≤ 𝐹 ) )
26 24 25 biimtrrdi ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ¬ 0 ≤ 𝐹 → ( 𝐹 < 0 ∨ 𝐿 ≤ 𝐹 ) ) )
27 26 com12 ⊢ ( ¬ 0 ≤ 𝐹 → ( ( 𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝐹 < 0 ∨ 𝐿 ≤ 𝐹 ) ) )
28 notnotb ⊢ ( 0 ≤ 𝐹 ↔ ¬ ¬ 0 ≤ 𝐹 )
29 28 a1i ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 0 ≤ 𝐹 ↔ ¬ ¬ 0 ≤ 𝐹 ) )
30 zre ⊢ ( 𝐿 ∈ ℤ → 𝐿 ∈ ℝ )
31 0red ⊢ ( 𝐿 ∈ ℤ → 0 ∈ ℝ )
32 30 31 jca ⊢ ( 𝐿 ∈ ℤ → ( 𝐿 ∈ ℝ ∧ 0 ∈ ℝ ) )
33 32 3ad2ant3 ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝐿 ∈ ℝ ∧ 0 ∈ ℝ ) )
34 ltnle ⊢ ( ( 𝐿 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝐿 < 0 ↔ ¬ 0 ≤ 𝐿 ) )
35 33 34 syl ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝐿 < 0 ↔ ¬ 0 ≤ 𝐿 ) )
36 29 35 anbi12d ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ( 0 ≤ 𝐹 ∧ 𝐿 < 0 ) ↔ ( ¬ ¬ 0 ≤ 𝐹 ∧ ¬ 0 ≤ 𝐿 ) ) )
37 30 3ad2ant3 ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → 𝐿 ∈ ℝ )
38 0red ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → 0 ∈ ℝ )
39 19 3ad2ant2 ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → 𝐹 ∈ ℝ )
40 ltleletr ⊢ ( ( 𝐿 ∈ ℝ ∧ 0 ∈ ℝ ∧ 𝐹 ∈ ℝ ) → ( ( 𝐿 < 0 ∧ 0 ≤ 𝐹 ) → 𝐿 ≤ 𝐹 ) )
41 37 38 39 40 syl3anc ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ( 𝐿 < 0 ∧ 0 ≤ 𝐹 ) → 𝐿 ≤ 𝐹 ) )
42 olc ⊢ ( 𝐿 ≤ 𝐹 → ( 𝐹 < 0 ∨ 𝐿 ≤ 𝐹 ) )
43 41 42 syl6 ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ( 𝐿 < 0 ∧ 0 ≤ 𝐹 ) → ( 𝐹 < 0 ∨ 𝐿 ≤ 𝐹 ) ) )
44 43 ancomsd ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ( 0 ≤ 𝐹 ∧ 𝐿 < 0 ) → ( 𝐹 < 0 ∨ 𝐿 ≤ 𝐹 ) ) )
45 36 44 sylbird ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ( ¬ ¬ 0 ≤ 𝐹 ∧ ¬ 0 ≤ 𝐿 ) → ( 𝐹 < 0 ∨ 𝐿 ≤ 𝐹 ) ) )
46 45 com12 ⊢ ( ( ¬ ¬ 0 ≤ 𝐹 ∧ ¬ 0 ≤ 𝐿 ) → ( ( 𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝐹 < 0 ∨ 𝐿 ≤ 𝐹 ) ) )
47 27 46 jaoi3 ⊢ ( ( ¬ 0 ≤ 𝐹 ∨ ¬ 0 ≤ 𝐿 ) → ( ( 𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝐹 < 0 ∨ 𝐿 ≤ 𝐹 ) ) )
48 47 impcom ⊢ ( ( ( 𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( ¬ 0 ≤ 𝐹 ∨ ¬ 0 ≤ 𝐿 ) ) → ( 𝐹 < 0 ∨ 𝐿 ≤ 𝐹 ) )
49 48 orcd ⊢ ( ( ( 𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( ¬ 0 ≤ 𝐹 ∨ ¬ 0 ≤ 𝐿 ) ) → ( ( 𝐹 < 0 ∨ 𝐿 ≤ 𝐹 ) ∨ ( ♯ ‘ 𝑆 ) < 𝐿 ) )
50 df-3or ⊢ ( ( 𝐹 < 0 ∨ 𝐿 ≤ 𝐹 ∨ ( ♯ ‘ 𝑆 ) < 𝐿 ) ↔ ( ( 𝐹 < 0 ∨ 𝐿 ≤ 𝐹 ) ∨ ( ♯ ‘ 𝑆 ) < 𝐿 ) )
51 49 50 sylibr ⊢ ( ( ( 𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( ¬ 0 ≤ 𝐹 ∨ ¬ 0 ≤ 𝐿 ) ) → ( 𝐹 < 0 ∨ 𝐿 ≤ 𝐹 ∨ ( ♯ ‘ 𝑆 ) < 𝐿 ) )
52 swrdnd ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ( 𝐹 < 0 ∨ 𝐿 ≤ 𝐹 ∨ ( ♯ ‘ 𝑆 ) < 𝐿 ) → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) )
53 52 imp ⊢ ( ( ( 𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝐹 < 0 ∨ 𝐿 ≤ 𝐹 ∨ ( ♯ ‘ 𝑆 ) < 𝐿 ) ) → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ )
54 51 53 syldan ⊢ ( ( ( 𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( ¬ 0 ≤ 𝐹 ∨ ¬ 0 ≤ 𝐿 ) ) → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ )
55 54 ex ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ( ¬ 0 ≤ 𝐹 ∨ ¬ 0 ≤ 𝐿 ) → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) )
56 55 3expb ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ) → ( ( ¬ 0 ≤ 𝐹 ∨ ¬ 0 ≤ 𝐿 ) → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) )
57 56 expcom ⊢ ( ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝑆 ∈ Word 𝑉 → ( ( ¬ 0 ≤ 𝐹 ∨ ¬ 0 ≤ 𝐿 ) → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) ) )
58 57 com23 ⊢ ( ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ( ¬ 0 ≤ 𝐹 ∨ ¬ 0 ≤ 𝐿 ) → ( 𝑆 ∈ Word 𝑉 → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) ) )
59 18 58 sylbir ⊢ ( ¬ ¬ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ( ¬ 0 ≤ 𝐹 ∨ ¬ 0 ≤ 𝐿 ) → ( 𝑆 ∈ Word 𝑉 → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) ) )
60 59 imp ⊢ ( ( ¬ ¬ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( ¬ 0 ≤ 𝐹 ∨ ¬ 0 ≤ 𝐿 ) ) → ( 𝑆 ∈ Word 𝑉 → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) )
61 17 60 jaoi3 ⊢ ( ( ¬ ( 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∨ ( ¬ 0 ≤ 𝐹 ∨ ¬ 0 ≤ 𝐿 ) ) → ( 𝑆 ∈ Word 𝑉 → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) )
62 15 61 sylbi ⊢ ( ¬ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( 𝑆 ∈ Word 𝑉 → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ ) )
63 62 impcom ⊢ ( ( 𝑆 ∈ Word 𝑉 ∧ ¬ ( 𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝑆 substr ⟨ 𝐹 , 𝐿 ⟩ ) = ∅ )