Step | Hyp | Ref
| Expression |
1 | | 3orass 1089 |
. . 3
⊢ ((𝐵 ≤ 𝐴 ∨ (♯‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0) ↔ (𝐵 ≤ 𝐴 ∨ ((♯‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0))) |
2 | | pm2.24 124 |
. . . . 5
⊢ (𝐵 ≤ 𝐴 → (¬ 𝐵 ≤ 𝐴 → ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑊 substr 〈𝐴, 𝐵〉) = ∅))) |
3 | | swrdval 14345 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑊 substr 〈𝐴, 𝐵〉) = if((𝐴..^𝐵) ⊆ dom 𝑊, (𝑥 ∈ (0..^(𝐵 − 𝐴)) ↦ (𝑊‘(𝑥 + 𝐴))), ∅)) |
4 | 3 | ad2antrr 723 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ((♯‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0)) ∧ ¬ 𝐵 ≤ 𝐴) → (𝑊 substr 〈𝐴, 𝐵〉) = if((𝐴..^𝐵) ⊆ dom 𝑊, (𝑥 ∈ (0..^(𝐵 − 𝐴)) ↦ (𝑊‘(𝑥 + 𝐴))), ∅)) |
5 | | wrddm 14213 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ Word 𝑉 → dom 𝑊 = (0..^(♯‘𝑊))) |
6 | | lencl 14225 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈
ℕ0) |
7 | | 3anass 1094 |
. . . . . . . . . . . . . . . . 17
⊢
(((♯‘𝑊)
∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ↔
((♯‘𝑊) ∈
ℕ0 ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ))) |
8 | | ssfzoulel 13470 |
. . . . . . . . . . . . . . . . . 18
⊢
(((♯‘𝑊)
∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) →
(((♯‘𝑊) ≤
𝐴 ∨ 𝐵 ≤ 0) → ((𝐴..^𝐵) ⊆ (0..^(♯‘𝑊)) → 𝐵 ≤ 𝐴))) |
9 | 8 | imp 407 |
. . . . . . . . . . . . . . . . 17
⊢
((((♯‘𝑊)
∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ((♯‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0)) → ((𝐴..^𝐵) ⊆ (0..^(♯‘𝑊)) → 𝐵 ≤ 𝐴)) |
10 | 7, 9 | sylanbr 582 |
. . . . . . . . . . . . . . . 16
⊢
((((♯‘𝑊)
∈ ℕ0 ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) ∧
((♯‘𝑊) ≤
𝐴 ∨ 𝐵 ≤ 0)) → ((𝐴..^𝐵) ⊆ (0..^(♯‘𝑊)) → 𝐵 ≤ 𝐴)) |
11 | 10 | con3dimp 409 |
. . . . . . . . . . . . . . 15
⊢
(((((♯‘𝑊) ∈ ℕ0 ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) ∧
((♯‘𝑊) ≤
𝐴 ∨ 𝐵 ≤ 0)) ∧ ¬ 𝐵 ≤ 𝐴) → ¬ (𝐴..^𝐵) ⊆ (0..^(♯‘𝑊))) |
12 | | sseq2 3948 |
. . . . . . . . . . . . . . . 16
⊢ (dom
𝑊 =
(0..^(♯‘𝑊))
→ ((𝐴..^𝐵) ⊆ dom 𝑊 ↔ (𝐴..^𝐵) ⊆ (0..^(♯‘𝑊)))) |
13 | 12 | notbid 318 |
. . . . . . . . . . . . . . 15
⊢ (dom
𝑊 =
(0..^(♯‘𝑊))
→ (¬ (𝐴..^𝐵) ⊆ dom 𝑊 ↔ ¬ (𝐴..^𝐵) ⊆ (0..^(♯‘𝑊)))) |
14 | 11, 13 | syl5ibr 245 |
. . . . . . . . . . . . . 14
⊢ (dom
𝑊 =
(0..^(♯‘𝑊))
→ (((((♯‘𝑊) ∈ ℕ0 ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) ∧
((♯‘𝑊) ≤
𝐴 ∨ 𝐵 ≤ 0)) ∧ ¬ 𝐵 ≤ 𝐴) → ¬ (𝐴..^𝐵) ⊆ dom 𝑊)) |
15 | 14 | exp5j 446 |
. . . . . . . . . . . . 13
⊢ (dom
𝑊 =
(0..^(♯‘𝑊))
→ ((♯‘𝑊)
∈ ℕ0 → ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) →
(((♯‘𝑊) ≤
𝐴 ∨ 𝐵 ≤ 0) → (¬ 𝐵 ≤ 𝐴 → ¬ (𝐴..^𝐵) ⊆ dom 𝑊))))) |
16 | 5, 6, 15 | sylc 65 |
. . . . . . . . . . . 12
⊢ (𝑊 ∈ Word 𝑉 → ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) →
(((♯‘𝑊) ≤
𝐴 ∨ 𝐵 ≤ 0) → (¬ 𝐵 ≤ 𝐴 → ¬ (𝐴..^𝐵) ⊆ dom 𝑊)))) |
17 | 16 | 3impib 1115 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) →
(((♯‘𝑊) ≤
𝐴 ∨ 𝐵 ≤ 0) → (¬ 𝐵 ≤ 𝐴 → ¬ (𝐴..^𝐵) ⊆ dom 𝑊))) |
18 | 17 | imp31 418 |
. . . . . . . . . 10
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ((♯‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0)) ∧ ¬ 𝐵 ≤ 𝐴) → ¬ (𝐴..^𝐵) ⊆ dom 𝑊) |
19 | 18 | iffalsed 4472 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ((♯‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0)) ∧ ¬ 𝐵 ≤ 𝐴) → if((𝐴..^𝐵) ⊆ dom 𝑊, (𝑥 ∈ (0..^(𝐵 − 𝐴)) ↦ (𝑊‘(𝑥 + 𝐴))), ∅) = ∅) |
20 | 4, 19 | eqtrd 2778 |
. . . . . . . 8
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ((♯‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0)) ∧ ¬ 𝐵 ≤ 𝐴) → (𝑊 substr 〈𝐴, 𝐵〉) = ∅) |
21 | 20 | ex 413 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ((♯‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0)) → (¬ 𝐵 ≤ 𝐴 → (𝑊 substr 〈𝐴, 𝐵〉) = ∅)) |
22 | 21 | expcom 414 |
. . . . . 6
⊢
(((♯‘𝑊)
≤ 𝐴 ∨ 𝐵 ≤ 0) → ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (¬ 𝐵 ≤ 𝐴 → (𝑊 substr 〈𝐴, 𝐵〉) = ∅))) |
23 | 22 | com23 86 |
. . . . 5
⊢
(((♯‘𝑊)
≤ 𝐴 ∨ 𝐵 ≤ 0) → (¬ 𝐵 ≤ 𝐴 → ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑊 substr 〈𝐴, 𝐵〉) = ∅))) |
24 | 2, 23 | jaoi 854 |
. . . 4
⊢ ((𝐵 ≤ 𝐴 ∨ ((♯‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0)) → (¬ 𝐵 ≤ 𝐴 → ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑊 substr 〈𝐴, 𝐵〉) = ∅))) |
25 | | swrdlend 14355 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐵 ≤ 𝐴 → (𝑊 substr 〈𝐴, 𝐵〉) = ∅)) |
26 | 25 | com12 32 |
. . . 4
⊢ (𝐵 ≤ 𝐴 → ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑊 substr 〈𝐴, 𝐵〉) = ∅)) |
27 | 24, 26 | pm2.61d2 181 |
. . 3
⊢ ((𝐵 ≤ 𝐴 ∨ ((♯‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0)) → ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑊 substr 〈𝐴, 𝐵〉) = ∅)) |
28 | 1, 27 | sylbi 216 |
. 2
⊢ ((𝐵 ≤ 𝐴 ∨ (♯‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0) → ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑊 substr 〈𝐴, 𝐵〉) = ∅)) |
29 | 28 | com12 32 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐵 ≤ 𝐴 ∨ (♯‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0) → (𝑊 substr 〈𝐴, 𝐵〉) = ∅)) |