Step | Hyp | Ref
| Expression |
1 | | 3orass 1111 |
. . 3
⊢ ((𝐵 ≤ 𝐴 ∨ (♯‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0) ↔ (𝐵 ≤ 𝐴 ∨ ((♯‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0))) |
2 | | pm2.24 122 |
. . . . 5
⊢ (𝐵 ≤ 𝐴 → (¬ 𝐵 ≤ 𝐴 → ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑊 substr 〈𝐴, 𝐵〉) = ∅))) |
3 | | swrdval 13664 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑊 substr 〈𝐴, 𝐵〉) = if((𝐴..^𝐵) ⊆ dom 𝑊, (𝑥 ∈ (0..^(𝐵 − 𝐴)) ↦ (𝑊‘(𝑥 + 𝐴))), ∅)) |
4 | 3 | ad2antrr 718 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ((♯‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0)) ∧ ¬ 𝐵 ≤ 𝐴) → (𝑊 substr 〈𝐴, 𝐵〉) = if((𝐴..^𝐵) ⊆ dom 𝑊, (𝑥 ∈ (0..^(𝐵 − 𝐴)) ↦ (𝑊‘(𝑥 + 𝐴))), ∅)) |
5 | | wrdf 13535 |
. . . . . . . . . . . . . . 15
⊢ (𝑊 ∈ Word 𝑉 → 𝑊:(0..^(♯‘𝑊))⟶𝑉) |
6 | 5 | fdmd 6263 |
. . . . . . . . . . . . . 14
⊢ (𝑊 ∈ Word 𝑉 → dom 𝑊 = (0..^(♯‘𝑊))) |
7 | | lencl 13549 |
. . . . . . . . . . . . . 14
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈
ℕ0) |
8 | | 3anass 1117 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((♯‘𝑊)
∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ↔
((♯‘𝑊) ∈
ℕ0 ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ))) |
9 | | ssfzoulel 12813 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((♯‘𝑊)
∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) →
(((♯‘𝑊) ≤
𝐴 ∨ 𝐵 ≤ 0) → ((𝐴..^𝐵) ⊆ (0..^(♯‘𝑊)) → 𝐵 ≤ 𝐴))) |
10 | 9 | imp 396 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((♯‘𝑊)
∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ((♯‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0)) → ((𝐴..^𝐵) ⊆ (0..^(♯‘𝑊)) → 𝐵 ≤ 𝐴)) |
11 | 8, 10 | sylanbr 578 |
. . . . . . . . . . . . . . . . . 18
⊢
((((♯‘𝑊)
∈ ℕ0 ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) ∧
((♯‘𝑊) ≤
𝐴 ∨ 𝐵 ≤ 0)) → ((𝐴..^𝐵) ⊆ (0..^(♯‘𝑊)) → 𝐵 ≤ 𝐴)) |
12 | 11 | con3dimp 398 |
. . . . . . . . . . . . . . . . 17
⊢
(((((♯‘𝑊) ∈ ℕ0 ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) ∧
((♯‘𝑊) ≤
𝐴 ∨ 𝐵 ≤ 0)) ∧ ¬ 𝐵 ≤ 𝐴) → ¬ (𝐴..^𝐵) ⊆ (0..^(♯‘𝑊))) |
13 | | sseq2 3821 |
. . . . . . . . . . . . . . . . . 18
⊢ (dom
𝑊 =
(0..^(♯‘𝑊))
→ ((𝐴..^𝐵) ⊆ dom 𝑊 ↔ (𝐴..^𝐵) ⊆ (0..^(♯‘𝑊)))) |
14 | 13 | notbid 310 |
. . . . . . . . . . . . . . . . 17
⊢ (dom
𝑊 =
(0..^(♯‘𝑊))
→ (¬ (𝐴..^𝐵) ⊆ dom 𝑊 ↔ ¬ (𝐴..^𝐵) ⊆ (0..^(♯‘𝑊)))) |
15 | 12, 14 | syl5ibr 238 |
. . . . . . . . . . . . . . . 16
⊢ (dom
𝑊 =
(0..^(♯‘𝑊))
→ (((((♯‘𝑊) ∈ ℕ0 ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) ∧
((♯‘𝑊) ≤
𝐴 ∨ 𝐵 ≤ 0)) ∧ ¬ 𝐵 ≤ 𝐴) → ¬ (𝐴..^𝐵) ⊆ dom 𝑊)) |
16 | 15 | expd 405 |
. . . . . . . . . . . . . . 15
⊢ (dom
𝑊 =
(0..^(♯‘𝑊))
→ ((((♯‘𝑊)
∈ ℕ0 ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ)) ∧
((♯‘𝑊) ≤
𝐴 ∨ 𝐵 ≤ 0)) → (¬ 𝐵 ≤ 𝐴 → ¬ (𝐴..^𝐵) ⊆ dom 𝑊))) |
17 | 16 | exp4c 424 |
. . . . . . . . . . . . . 14
⊢ (dom
𝑊 =
(0..^(♯‘𝑊))
→ ((♯‘𝑊)
∈ ℕ0 → ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) →
(((♯‘𝑊) ≤
𝐴 ∨ 𝐵 ≤ 0) → (¬ 𝐵 ≤ 𝐴 → ¬ (𝐴..^𝐵) ⊆ dom 𝑊))))) |
18 | 6, 7, 17 | sylc 65 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ Word 𝑉 → ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) →
(((♯‘𝑊) ≤
𝐴 ∨ 𝐵 ≤ 0) → (¬ 𝐵 ≤ 𝐴 → ¬ (𝐴..^𝐵) ⊆ dom 𝑊)))) |
19 | 18 | 3impib 1145 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) →
(((♯‘𝑊) ≤
𝐴 ∨ 𝐵 ≤ 0) → (¬ 𝐵 ≤ 𝐴 → ¬ (𝐴..^𝐵) ⊆ dom 𝑊))) |
20 | 19 | imp 396 |
. . . . . . . . . . 11
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ((♯‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0)) → (¬ 𝐵 ≤ 𝐴 → ¬ (𝐴..^𝐵) ⊆ dom 𝑊)) |
21 | 20 | imp 396 |
. . . . . . . . . 10
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ((♯‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0)) ∧ ¬ 𝐵 ≤ 𝐴) → ¬ (𝐴..^𝐵) ⊆ dom 𝑊) |
22 | 21 | iffalsed 4286 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ((♯‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0)) ∧ ¬ 𝐵 ≤ 𝐴) → if((𝐴..^𝐵) ⊆ dom 𝑊, (𝑥 ∈ (0..^(𝐵 − 𝐴)) ↦ (𝑊‘(𝑥 + 𝐴))), ∅) = ∅) |
23 | 4, 22 | eqtrd 2831 |
. . . . . . . 8
⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ((♯‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0)) ∧ ¬ 𝐵 ≤ 𝐴) → (𝑊 substr 〈𝐴, 𝐵〉) = ∅) |
24 | 23 | ex 402 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ((♯‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0)) → (¬ 𝐵 ≤ 𝐴 → (𝑊 substr 〈𝐴, 𝐵〉) = ∅)) |
25 | 24 | expcom 403 |
. . . . . 6
⊢
(((♯‘𝑊)
≤ 𝐴 ∨ 𝐵 ≤ 0) → ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (¬ 𝐵 ≤ 𝐴 → (𝑊 substr 〈𝐴, 𝐵〉) = ∅))) |
26 | 25 | com23 86 |
. . . . 5
⊢
(((♯‘𝑊)
≤ 𝐴 ∨ 𝐵 ≤ 0) → (¬ 𝐵 ≤ 𝐴 → ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑊 substr 〈𝐴, 𝐵〉) = ∅))) |
27 | 2, 26 | jaoi 884 |
. . . 4
⊢ ((𝐵 ≤ 𝐴 ∨ ((♯‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0)) → (¬ 𝐵 ≤ 𝐴 → ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑊 substr 〈𝐴, 𝐵〉) = ∅))) |
28 | | swrdlend 13679 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐵 ≤ 𝐴 → (𝑊 substr 〈𝐴, 𝐵〉) = ∅)) |
29 | 28 | com12 32 |
. . . 4
⊢ (𝐵 ≤ 𝐴 → ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑊 substr 〈𝐴, 𝐵〉) = ∅)) |
30 | 27, 29 | pm2.61d2 174 |
. . 3
⊢ ((𝐵 ≤ 𝐴 ∨ ((♯‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0)) → ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑊 substr 〈𝐴, 𝐵〉) = ∅)) |
31 | 1, 30 | sylbi 209 |
. 2
⊢ ((𝐵 ≤ 𝐴 ∨ (♯‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0) → ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑊 substr 〈𝐴, 𝐵〉) = ∅)) |
32 | 31 | com12 32 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐵 ≤ 𝐴 ∨ (♯‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0) → (𝑊 substr 〈𝐴, 𝐵〉) = ∅)) |