Step | Hyp | Ref
| Expression |
1 | | 3orass 1034 |
. . 3
⊢ ((𝐵 ≤ 𝐴 ∨ (#‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0) ↔ (𝐵 ≤ 𝐴 ∨ ((#‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0))) |
2 | | pm2.24 120 |
. . . . 5
⊢ (𝐵 ≤ 𝐴 → (¬ 𝐵 ≤ 𝐴 → ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑊 substr 〈𝐴, 𝐵〉) = ∅))) |
3 | | swrdval 13269 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑊 substr 〈𝐴, 𝐵〉) = if((𝐴..^𝐵) ⊆ dom 𝑊, (𝑥 ∈ (0..^(𝐵 − 𝐴)) ↦ (𝑊‘(𝑥 + 𝐴))), ∅)) |
4 | 3 | ad2antrr 758 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ((#‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0)) ∧ ¬ 𝐵 ≤ 𝐴) → (𝑊 substr 〈𝐴, 𝐵〉) = if((𝐴..^𝐵) ⊆ dom 𝑊, (𝑥 ∈ (0..^(𝐵 − 𝐴)) ↦ (𝑊‘(𝑥 + 𝐴))), ∅)) |
5 | | wrdf 13165 |
. . . . . . . . . . . . . . 15
⊢ (𝑊 ∈ Word 𝑉 → 𝑊:(0..^(#‘𝑊))⟶𝑉) |
6 | | fdm 5964 |
. . . . . . . . . . . . . . 15
⊢ (𝑊:(0..^(#‘𝑊))⟶𝑉 → dom 𝑊 = (0..^(#‘𝑊))) |
7 | 5, 6 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑊 ∈ Word 𝑉 → dom 𝑊 = (0..^(#‘𝑊))) |
8 | | lencl 13179 |
. . . . . . . . . . . . . 14
⊢ (𝑊 ∈ Word 𝑉 → (#‘𝑊) ∈
ℕ0) |
9 | | 3anass 1035 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((#‘𝑊) ∈
ℕ0 ∧ 𝐴
∈ ℤ ∧ 𝐵
∈ ℤ) ↔ ((#‘𝑊) ∈ ℕ0 ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈
ℤ))) |
10 | | ssfzoulel 12428 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((#‘𝑊) ∈
ℕ0 ∧ 𝐴
∈ ℤ ∧ 𝐵
∈ ℤ) → (((#‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0) → ((𝐴..^𝐵) ⊆ (0..^(#‘𝑊)) → 𝐵 ≤ 𝐴))) |
11 | 10 | imp 444 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((#‘𝑊)
∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ((#‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0)) → ((𝐴..^𝐵) ⊆ (0..^(#‘𝑊)) → 𝐵 ≤ 𝐴)) |
12 | 9, 11 | sylanbr 489 |
. . . . . . . . . . . . . . . . . 18
⊢
((((#‘𝑊)
∈ ℕ0 ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) ∧ ((#‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0)) → ((𝐴..^𝐵) ⊆ (0..^(#‘𝑊)) → 𝐵 ≤ 𝐴)) |
13 | 12 | con3dimp 456 |
. . . . . . . . . . . . . . . . 17
⊢
(((((#‘𝑊)
∈ ℕ0 ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) ∧ ((#‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0)) ∧ ¬ 𝐵 ≤ 𝐴) → ¬ (𝐴..^𝐵) ⊆ (0..^(#‘𝑊))) |
14 | | sseq2 3590 |
. . . . . . . . . . . . . . . . . 18
⊢ (dom
𝑊 = (0..^(#‘𝑊)) → ((𝐴..^𝐵) ⊆ dom 𝑊 ↔ (𝐴..^𝐵) ⊆ (0..^(#‘𝑊)))) |
15 | 14 | notbid 307 |
. . . . . . . . . . . . . . . . 17
⊢ (dom
𝑊 = (0..^(#‘𝑊)) → (¬ (𝐴..^𝐵) ⊆ dom 𝑊 ↔ ¬ (𝐴..^𝐵) ⊆ (0..^(#‘𝑊)))) |
16 | 13, 15 | syl5ibr 235 |
. . . . . . . . . . . . . . . 16
⊢ (dom
𝑊 = (0..^(#‘𝑊)) → (((((#‘𝑊) ∈ ℕ0
∧ (𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ))
∧ ((#‘𝑊) ≤
𝐴 ∨ 𝐵 ≤ 0)) ∧ ¬ 𝐵 ≤ 𝐴) → ¬ (𝐴..^𝐵) ⊆ dom 𝑊)) |
17 | 16 | expd 451 |
. . . . . . . . . . . . . . 15
⊢ (dom
𝑊 = (0..^(#‘𝑊)) → ((((#‘𝑊) ∈ ℕ0
∧ (𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ))
∧ ((#‘𝑊) ≤
𝐴 ∨ 𝐵 ≤ 0)) → (¬ 𝐵 ≤ 𝐴 → ¬ (𝐴..^𝐵) ⊆ dom 𝑊))) |
18 | 17 | exp4c 634 |
. . . . . . . . . . . . . 14
⊢ (dom
𝑊 = (0..^(#‘𝑊)) → ((#‘𝑊) ∈ ℕ0
→ ((𝐴 ∈ ℤ
∧ 𝐵 ∈ ℤ)
→ (((#‘𝑊) ≤
𝐴 ∨ 𝐵 ≤ 0) → (¬ 𝐵 ≤ 𝐴 → ¬ (𝐴..^𝐵) ⊆ dom 𝑊))))) |
19 | 7, 8, 18 | sylc 63 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ Word 𝑉 → ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (((#‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0) → (¬ 𝐵 ≤ 𝐴 → ¬ (𝐴..^𝐵) ⊆ dom 𝑊)))) |
20 | 19 | 3impib 1254 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (((#‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0) → (¬ 𝐵 ≤ 𝐴 → ¬ (𝐴..^𝐵) ⊆ dom 𝑊))) |
21 | 20 | imp 444 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ((#‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0)) → (¬ 𝐵 ≤ 𝐴 → ¬ (𝐴..^𝐵) ⊆ dom 𝑊)) |
22 | 21 | imp 444 |
. . . . . . . . . 10
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ((#‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0)) ∧ ¬ 𝐵 ≤ 𝐴) → ¬ (𝐴..^𝐵) ⊆ dom 𝑊) |
23 | 22 | iffalsed 4047 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ((#‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0)) ∧ ¬ 𝐵 ≤ 𝐴) → if((𝐴..^𝐵) ⊆ dom 𝑊, (𝑥 ∈ (0..^(𝐵 − 𝐴)) ↦ (𝑊‘(𝑥 + 𝐴))), ∅) = ∅) |
24 | 4, 23 | eqtrd 2644 |
. . . . . . . 8
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ((#‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0)) ∧ ¬ 𝐵 ≤ 𝐴) → (𝑊 substr 〈𝐴, 𝐵〉) = ∅) |
25 | 24 | ex 449 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ((#‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0)) → (¬ 𝐵 ≤ 𝐴 → (𝑊 substr 〈𝐴, 𝐵〉) = ∅)) |
26 | 25 | expcom 450 |
. . . . . 6
⊢
(((#‘𝑊) ≤
𝐴 ∨ 𝐵 ≤ 0) → ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (¬ 𝐵 ≤ 𝐴 → (𝑊 substr 〈𝐴, 𝐵〉) = ∅))) |
27 | 26 | com23 84 |
. . . . 5
⊢
(((#‘𝑊) ≤
𝐴 ∨ 𝐵 ≤ 0) → (¬ 𝐵 ≤ 𝐴 → ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑊 substr 〈𝐴, 𝐵〉) = ∅))) |
28 | 2, 27 | jaoi 393 |
. . . 4
⊢ ((𝐵 ≤ 𝐴 ∨ ((#‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0)) → (¬ 𝐵 ≤ 𝐴 → ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑊 substr 〈𝐴, 𝐵〉) = ∅))) |
29 | | swrdlend 13283 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐵 ≤ 𝐴 → (𝑊 substr 〈𝐴, 𝐵〉) = ∅)) |
30 | 29 | com12 32 |
. . . 4
⊢ (𝐵 ≤ 𝐴 → ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑊 substr 〈𝐴, 𝐵〉) = ∅)) |
31 | 28, 30 | pm2.61d2 171 |
. . 3
⊢ ((𝐵 ≤ 𝐴 ∨ ((#‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0)) → ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑊 substr 〈𝐴, 𝐵〉) = ∅)) |
32 | 1, 31 | sylbi 206 |
. 2
⊢ ((𝐵 ≤ 𝐴 ∨ (#‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0) → ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑊 substr 〈𝐴, 𝐵〉) = ∅)) |
33 | 32 | com12 32 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐵 ≤ 𝐴 ∨ (#‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0) → (𝑊 substr 〈𝐴, 𝐵〉) = ∅)) |