Metamath Proof Explorer


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

Proof

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