Step | Hyp | Ref
| Expression |
1 | | 3orcomb 1048 |
. . . 4
⊢ ((𝐹 < 0 ∨ 𝐿 ≤ 𝐹 ∨ (#‘𝑊) < 𝐿) ↔ (𝐹 < 0 ∨ (#‘𝑊) < 𝐿 ∨ 𝐿 ≤ 𝐹)) |
2 | | df-3or 1038 |
. . . 4
⊢ ((𝐹 < 0 ∨ (#‘𝑊) < 𝐿 ∨ 𝐿 ≤ 𝐹) ↔ ((𝐹 < 0 ∨ (#‘𝑊) < 𝐿) ∨ 𝐿 ≤ 𝐹)) |
3 | 1, 2 | bitri 264 |
. . 3
⊢ ((𝐹 < 0 ∨ 𝐿 ≤ 𝐹 ∨ (#‘𝑊) < 𝐿) ↔ ((𝐹 < 0 ∨ (#‘𝑊) < 𝐿) ∨ 𝐿 ≤ 𝐹)) |
4 | | swrdlend 13431 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝐿 ≤ 𝐹 → (𝑊 substr 〈𝐹, 𝐿〉) = ∅)) |
5 | 4 | com12 32 |
. . . . 5
⊢ (𝐿 ≤ 𝐹 → ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑊 substr 〈𝐹, 𝐿〉) = ∅)) |
6 | | swrdval 13417 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑊 substr 〈𝐹, 𝐿〉) = if((𝐹..^𝐿) ⊆ dom 𝑊, (𝑖 ∈ (0..^(𝐿 − 𝐹)) ↦ (𝑊‘(𝑖 + 𝐹))), ∅)) |
7 | 6 | adantl 482 |
. . . . . . . 8
⊢ ((((𝐹 < 0 ∨ (#‘𝑊) < 𝐿) ∧ ¬ 𝐿 ≤ 𝐹) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → (𝑊 substr 〈𝐹, 𝐿〉) = if((𝐹..^𝐿) ⊆ dom 𝑊, (𝑖 ∈ (0..^(𝐿 − 𝐹)) ↦ (𝑊‘(𝑖 + 𝐹))), ∅)) |
8 | | zre 11381 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 ∈ ℤ → 𝐹 ∈
ℝ) |
9 | | 0red 10041 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 ∈ ℤ → 0 ∈
ℝ) |
10 | 8, 9 | ltnled 10184 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ ℤ → (𝐹 < 0 ↔ ¬ 0 ≤
𝐹)) |
11 | 10 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝐹 < 0 ↔ ¬ 0 ≤ 𝐹)) |
12 | | lencl 13324 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑊 ∈ Word 𝑉 → (#‘𝑊) ∈
ℕ0) |
13 | 12 | nn0red 11352 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑊 ∈ Word 𝑉 → (#‘𝑊) ∈ ℝ) |
14 | | zre 11381 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐿 ∈ ℤ → 𝐿 ∈
ℝ) |
15 | 13, 14 | anim12i 590 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) → ((#‘𝑊) ∈ ℝ ∧ 𝐿 ∈
ℝ)) |
16 | 15 | 3adant2 1080 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → ((#‘𝑊) ∈ ℝ ∧ 𝐿 ∈
ℝ)) |
17 | | ltnle 10117 |
. . . . . . . . . . . . . . . . 17
⊢
(((#‘𝑊) ∈
ℝ ∧ 𝐿 ∈
ℝ) → ((#‘𝑊) < 𝐿 ↔ ¬ 𝐿 ≤ (#‘𝑊))) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → ((#‘𝑊) < 𝐿 ↔ ¬ 𝐿 ≤ (#‘𝑊))) |
19 | 11, 18 | orbi12d 746 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → ((𝐹 < 0 ∨ (#‘𝑊) < 𝐿) ↔ (¬ 0 ≤ 𝐹 ∨ ¬ 𝐿 ≤ (#‘𝑊)))) |
20 | 19 | biimpcd 239 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 < 0 ∨ (#‘𝑊) < 𝐿) → ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (¬ 0 ≤ 𝐹 ∨ ¬ 𝐿 ≤ (#‘𝑊)))) |
21 | 20 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝐹 < 0 ∨ (#‘𝑊) < 𝐿) ∧ ¬ 𝐿 ≤ 𝐹) → ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (¬ 0 ≤ 𝐹 ∨ ¬ 𝐿 ≤ (#‘𝑊)))) |
22 | 21 | imp 445 |
. . . . . . . . . . . 12
⊢ ((((𝐹 < 0 ∨ (#‘𝑊) < 𝐿) ∧ ¬ 𝐿 ≤ 𝐹) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → (¬ 0 ≤ 𝐹 ∨ ¬ 𝐿 ≤ (#‘𝑊))) |
23 | | ianor 509 |
. . . . . . . . . . . 12
⊢ (¬ (0
≤ 𝐹 ∧ 𝐿 ≤ (#‘𝑊)) ↔ (¬ 0 ≤ 𝐹 ∨ ¬ 𝐿 ≤ (#‘𝑊))) |
24 | 22, 23 | sylibr 224 |
. . . . . . . . . . 11
⊢ ((((𝐹 < 0 ∨ (#‘𝑊) < 𝐿) ∧ ¬ 𝐿 ≤ 𝐹) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → ¬ (0 ≤ 𝐹 ∧ 𝐿 ≤ (#‘𝑊))) |
25 | | 3simpc 1060 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) |
26 | 25 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((((𝐹 < 0 ∨ (#‘𝑊) < 𝐿) ∧ ¬ 𝐿 ≤ 𝐹) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → (𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) |
27 | 12 | nn0zd 11480 |
. . . . . . . . . . . . . . 15
⊢ (𝑊 ∈ Word 𝑉 → (#‘𝑊) ∈ ℤ) |
28 | | 0z 11388 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℤ |
29 | 27, 28 | jctil 560 |
. . . . . . . . . . . . . 14
⊢ (𝑊 ∈ Word 𝑉 → (0 ∈ ℤ ∧
(#‘𝑊) ∈
ℤ)) |
30 | 29 | 3ad2ant1 1082 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (0 ∈ ℤ
∧ (#‘𝑊) ∈
ℤ)) |
31 | 30 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((((𝐹 < 0 ∨ (#‘𝑊) < 𝐿) ∧ ¬ 𝐿 ≤ 𝐹) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → (0 ∈ ℤ
∧ (#‘𝑊) ∈
ℤ)) |
32 | | ltnle 10117 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (𝐹 < 𝐿 ↔ ¬ 𝐿 ≤ 𝐹)) |
33 | 8, 14, 32 | syl2an 494 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝐹 < 𝐿 ↔ ¬ 𝐿 ≤ 𝐹)) |
34 | 33 | 3adant1 1079 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝐹 < 𝐿 ↔ ¬ 𝐿 ≤ 𝐹)) |
35 | 34 | biimprcd 240 |
. . . . . . . . . . . . . 14
⊢ (¬
𝐿 ≤ 𝐹 → ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → 𝐹 < 𝐿)) |
36 | 35 | adantl 482 |
. . . . . . . . . . . . 13
⊢ (((𝐹 < 0 ∨ (#‘𝑊) < 𝐿) ∧ ¬ 𝐿 ≤ 𝐹) → ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → 𝐹 < 𝐿)) |
37 | 36 | imp 445 |
. . . . . . . . . . . 12
⊢ ((((𝐹 < 0 ∨ (#‘𝑊) < 𝐿) ∧ ¬ 𝐿 ≤ 𝐹) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → 𝐹 < 𝐿) |
38 | | ssfzo12bi 12563 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (0 ∈
ℤ ∧ (#‘𝑊)
∈ ℤ) ∧ 𝐹
< 𝐿) → ((𝐹..^𝐿) ⊆ (0..^(#‘𝑊)) ↔ (0 ≤ 𝐹 ∧ 𝐿 ≤ (#‘𝑊)))) |
39 | 26, 31, 37, 38 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ ((((𝐹 < 0 ∨ (#‘𝑊) < 𝐿) ∧ ¬ 𝐿 ≤ 𝐹) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → ((𝐹..^𝐿) ⊆ (0..^(#‘𝑊)) ↔ (0 ≤ 𝐹 ∧ 𝐿 ≤ (#‘𝑊)))) |
40 | 24, 39 | mtbird 315 |
. . . . . . . . . 10
⊢ ((((𝐹 < 0 ∨ (#‘𝑊) < 𝐿) ∧ ¬ 𝐿 ≤ 𝐹) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → ¬ (𝐹..^𝐿) ⊆ (0..^(#‘𝑊))) |
41 | | wrddm 13312 |
. . . . . . . . . . . . . 14
⊢ (𝑊 ∈ Word 𝑉 → dom 𝑊 = (0..^(#‘𝑊))) |
42 | 41 | sseq2d 3633 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ Word 𝑉 → ((𝐹..^𝐿) ⊆ dom 𝑊 ↔ (𝐹..^𝐿) ⊆ (0..^(#‘𝑊)))) |
43 | 42 | notbid 308 |
. . . . . . . . . . . 12
⊢ (𝑊 ∈ Word 𝑉 → (¬ (𝐹..^𝐿) ⊆ dom 𝑊 ↔ ¬ (𝐹..^𝐿) ⊆ (0..^(#‘𝑊)))) |
44 | 43 | 3ad2ant1 1082 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (¬ (𝐹..^𝐿) ⊆ dom 𝑊 ↔ ¬ (𝐹..^𝐿) ⊆ (0..^(#‘𝑊)))) |
45 | 44 | adantl 482 |
. . . . . . . . . 10
⊢ ((((𝐹 < 0 ∨ (#‘𝑊) < 𝐿) ∧ ¬ 𝐿 ≤ 𝐹) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → (¬ (𝐹..^𝐿) ⊆ dom 𝑊 ↔ ¬ (𝐹..^𝐿) ⊆ (0..^(#‘𝑊)))) |
46 | 40, 45 | mpbird 247 |
. . . . . . . . 9
⊢ ((((𝐹 < 0 ∨ (#‘𝑊) < 𝐿) ∧ ¬ 𝐿 ≤ 𝐹) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → ¬ (𝐹..^𝐿) ⊆ dom 𝑊) |
47 | 46 | iffalsed 4097 |
. . . . . . . 8
⊢ ((((𝐹 < 0 ∨ (#‘𝑊) < 𝐿) ∧ ¬ 𝐿 ≤ 𝐹) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → if((𝐹..^𝐿) ⊆ dom 𝑊, (𝑖 ∈ (0..^(𝐿 − 𝐹)) ↦ (𝑊‘(𝑖 + 𝐹))), ∅) = ∅) |
48 | 7, 47 | eqtrd 2656 |
. . . . . . 7
⊢ ((((𝐹 < 0 ∨ (#‘𝑊) < 𝐿) ∧ ¬ 𝐿 ≤ 𝐹) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → (𝑊 substr 〈𝐹, 𝐿〉) = ∅) |
49 | 48 | exp31 630 |
. . . . . 6
⊢ ((𝐹 < 0 ∨ (#‘𝑊) < 𝐿) → (¬ 𝐿 ≤ 𝐹 → ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑊 substr 〈𝐹, 𝐿〉) = ∅))) |
50 | 49 | impcom 446 |
. . . . 5
⊢ ((¬
𝐿 ≤ 𝐹 ∧ (𝐹 < 0 ∨ (#‘𝑊) < 𝐿)) → ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑊 substr 〈𝐹, 𝐿〉) = ∅)) |
51 | 5, 50 | jaoi3 1011 |
. . . 4
⊢ ((𝐿 ≤ 𝐹 ∨ (𝐹 < 0 ∨ (#‘𝑊) < 𝐿)) → ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑊 substr 〈𝐹, 𝐿〉) = ∅)) |
52 | 51 | orcoms 404 |
. . 3
⊢ (((𝐹 < 0 ∨ (#‘𝑊) < 𝐿) ∨ 𝐿 ≤ 𝐹) → ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑊 substr 〈𝐹, 𝐿〉) = ∅)) |
53 | 3, 52 | sylbi 207 |
. 2
⊢ ((𝐹 < 0 ∨ 𝐿 ≤ 𝐹 ∨ (#‘𝑊) < 𝐿) → ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑊 substr 〈𝐹, 𝐿〉) = ∅)) |
54 | 53 | com12 32 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → ((𝐹 < 0 ∨ 𝐿 ≤ 𝐹 ∨ (#‘𝑊) < 𝐿) → (𝑊 substr 〈𝐹, 𝐿〉) = ∅)) |