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 〈 𝐹 , 𝐿 〉 ) = ∅ ) ) |