| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 3orcomb 1093 | . . . 4
⊢ ((𝐹 < 0 ∨ 𝐿 ≤ 𝐹 ∨ (♯‘𝑊) < 𝐿) ↔ (𝐹 < 0 ∨ (♯‘𝑊) < 𝐿 ∨ 𝐿 ≤ 𝐹)) | 
| 2 |  | df-3or 1087 | . . . 4
⊢ ((𝐹 < 0 ∨
(♯‘𝑊) <
𝐿 ∨ 𝐿 ≤ 𝐹) ↔ ((𝐹 < 0 ∨ (♯‘𝑊) < 𝐿) ∨ 𝐿 ≤ 𝐹)) | 
| 3 | 1, 2 | bitri 275 | . . 3
⊢ ((𝐹 < 0 ∨ 𝐿 ≤ 𝐹 ∨ (♯‘𝑊) < 𝐿) ↔ ((𝐹 < 0 ∨ (♯‘𝑊) < 𝐿) ∨ 𝐿 ≤ 𝐹)) | 
| 4 |  | swrdlend 14692 | . . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝐿 ≤ 𝐹 → (𝑊 substr 〈𝐹, 𝐿〉) = ∅)) | 
| 5 | 4 | com12 32 | . . . . 5
⊢ (𝐿 ≤ 𝐹 → ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑊 substr 〈𝐹, 𝐿〉) = ∅)) | 
| 6 |  | swrdval 14682 | . . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑊 substr 〈𝐹, 𝐿〉) = if((𝐹..^𝐿) ⊆ dom 𝑊, (𝑖 ∈ (0..^(𝐿 − 𝐹)) ↦ (𝑊‘(𝑖 + 𝐹))), ∅)) | 
| 7 | 6 | adantl 481 | . . . . . . . 8
⊢ ((((𝐹 < 0 ∨
(♯‘𝑊) <
𝐿) ∧ ¬ 𝐿 ≤ 𝐹) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → (𝑊 substr 〈𝐹, 𝐿〉) = if((𝐹..^𝐿) ⊆ dom 𝑊, (𝑖 ∈ (0..^(𝐿 − 𝐹)) ↦ (𝑊‘(𝑖 + 𝐹))), ∅)) | 
| 8 |  | zre 12619 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐹 ∈ ℤ → 𝐹 ∈
ℝ) | 
| 9 |  | 0red 11265 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐹 ∈ ℤ → 0 ∈
ℝ) | 
| 10 | 8, 9 | ltnled 11409 | . . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ ℤ → (𝐹 < 0 ↔ ¬ 0 ≤
𝐹)) | 
| 11 | 10 | 3ad2ant2 1134 | . . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝐹 < 0 ↔ ¬ 0 ≤ 𝐹)) | 
| 12 |  | lencl 14572 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈
ℕ0) | 
| 13 | 12 | nn0red 12590 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ ℝ) | 
| 14 |  | zre 12619 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐿 ∈ ℤ → 𝐿 ∈
ℝ) | 
| 15 | 13, 14 | anim12i 613 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) →
((♯‘𝑊) ∈
ℝ ∧ 𝐿 ∈
ℝ)) | 
| 16 | 15 | 3adant2 1131 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) →
((♯‘𝑊) ∈
ℝ ∧ 𝐿 ∈
ℝ)) | 
| 17 |  | ltnle 11341 | . . . . . . . . . . . . . . . . 17
⊢
(((♯‘𝑊)
∈ ℝ ∧ 𝐿
∈ ℝ) → ((♯‘𝑊) < 𝐿 ↔ ¬ 𝐿 ≤ (♯‘𝑊))) | 
| 18 | 16, 17 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) →
((♯‘𝑊) <
𝐿 ↔ ¬ 𝐿 ≤ (♯‘𝑊))) | 
| 19 | 11, 18 | orbi12d 918 | . . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → ((𝐹 < 0 ∨ (♯‘𝑊) < 𝐿) ↔ (¬ 0 ≤ 𝐹 ∨ ¬ 𝐿 ≤ (♯‘𝑊)))) | 
| 20 | 19 | biimpcd 249 | . . . . . . . . . . . . . 14
⊢ ((𝐹 < 0 ∨
(♯‘𝑊) <
𝐿) → ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (¬ 0 ≤ 𝐹 ∨ ¬ 𝐿 ≤ (♯‘𝑊)))) | 
| 21 | 20 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝐹 < 0 ∨
(♯‘𝑊) <
𝐿) ∧ ¬ 𝐿 ≤ 𝐹) → ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (¬ 0 ≤ 𝐹 ∨ ¬ 𝐿 ≤ (♯‘𝑊)))) | 
| 22 | 21 | imp 406 | . . . . . . . . . . . 12
⊢ ((((𝐹 < 0 ∨
(♯‘𝑊) <
𝐿) ∧ ¬ 𝐿 ≤ 𝐹) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → (¬ 0 ≤ 𝐹 ∨ ¬ 𝐿 ≤ (♯‘𝑊))) | 
| 23 |  | ianor 983 | . . . . . . . . . . . 12
⊢ (¬ (0
≤ 𝐹 ∧ 𝐿 ≤ (♯‘𝑊)) ↔ (¬ 0 ≤ 𝐹 ∨ ¬ 𝐿 ≤ (♯‘𝑊))) | 
| 24 | 22, 23 | sylibr 234 | . . . . . . . . . . 11
⊢ ((((𝐹 < 0 ∨
(♯‘𝑊) <
𝐿) ∧ ¬ 𝐿 ≤ 𝐹) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → ¬ (0 ≤ 𝐹 ∧ 𝐿 ≤ (♯‘𝑊))) | 
| 25 |  | 3simpc 1150 | . . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) | 
| 26 | 12 | nn0zd 12641 | . . . . . . . . . . . . . 14
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈ ℤ) | 
| 27 |  | 0z 12626 | . . . . . . . . . . . . . 14
⊢ 0 ∈
ℤ | 
| 28 | 26, 27 | jctil 519 | . . . . . . . . . . . . 13
⊢ (𝑊 ∈ Word 𝑉 → (0 ∈ ℤ ∧
(♯‘𝑊) ∈
ℤ)) | 
| 29 | 28 | 3ad2ant1 1133 | . . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (0 ∈ ℤ
∧ (♯‘𝑊)
∈ ℤ)) | 
| 30 |  | ltnle 11341 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (𝐹 < 𝐿 ↔ ¬ 𝐿 ≤ 𝐹)) | 
| 31 | 8, 14, 30 | syl2an 596 | . . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝐹 < 𝐿 ↔ ¬ 𝐿 ≤ 𝐹)) | 
| 32 | 31 | 3adant1 1130 | . . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝐹 < 𝐿 ↔ ¬ 𝐿 ≤ 𝐹)) | 
| 33 | 32 | biimprcd 250 | . . . . . . . . . . . . . 14
⊢ (¬
𝐿 ≤ 𝐹 → ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → 𝐹 < 𝐿)) | 
| 34 | 33 | adantl 481 | . . . . . . . . . . . . 13
⊢ (((𝐹 < 0 ∨
(♯‘𝑊) <
𝐿) ∧ ¬ 𝐿 ≤ 𝐹) → ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → 𝐹 < 𝐿)) | 
| 35 | 34 | imp 406 | . . . . . . . . . . . 12
⊢ ((((𝐹 < 0 ∨
(♯‘𝑊) <
𝐿) ∧ ¬ 𝐿 ≤ 𝐹) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → 𝐹 < 𝐿) | 
| 36 |  | ssfzo12bi 13801 | . . . . . . . . . . . 12
⊢ (((𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (0 ∈
ℤ ∧ (♯‘𝑊) ∈ ℤ) ∧ 𝐹 < 𝐿) → ((𝐹..^𝐿) ⊆ (0..^(♯‘𝑊)) ↔ (0 ≤ 𝐹 ∧ 𝐿 ≤ (♯‘𝑊)))) | 
| 37 | 25, 29, 35, 36 | syl2an23an 1424 | . . . . . . . . . . 11
⊢ ((((𝐹 < 0 ∨
(♯‘𝑊) <
𝐿) ∧ ¬ 𝐿 ≤ 𝐹) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → ((𝐹..^𝐿) ⊆ (0..^(♯‘𝑊)) ↔ (0 ≤ 𝐹 ∧ 𝐿 ≤ (♯‘𝑊)))) | 
| 38 | 24, 37 | mtbird 325 | . . . . . . . . . 10
⊢ ((((𝐹 < 0 ∨
(♯‘𝑊) <
𝐿) ∧ ¬ 𝐿 ≤ 𝐹) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → ¬ (𝐹..^𝐿) ⊆ (0..^(♯‘𝑊))) | 
| 39 |  | wrddm 14560 | . . . . . . . . . . . . . 14
⊢ (𝑊 ∈ Word 𝑉 → dom 𝑊 = (0..^(♯‘𝑊))) | 
| 40 | 39 | sseq2d 4015 | . . . . . . . . . . . . 13
⊢ (𝑊 ∈ Word 𝑉 → ((𝐹..^𝐿) ⊆ dom 𝑊 ↔ (𝐹..^𝐿) ⊆ (0..^(♯‘𝑊)))) | 
| 41 | 40 | notbid 318 | . . . . . . . . . . . 12
⊢ (𝑊 ∈ Word 𝑉 → (¬ (𝐹..^𝐿) ⊆ dom 𝑊 ↔ ¬ (𝐹..^𝐿) ⊆ (0..^(♯‘𝑊)))) | 
| 42 | 41 | 3ad2ant1 1133 | . . . . . . . . . . 11
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (¬ (𝐹..^𝐿) ⊆ dom 𝑊 ↔ ¬ (𝐹..^𝐿) ⊆ (0..^(♯‘𝑊)))) | 
| 43 | 42 | adantl 481 | . . . . . . . . . 10
⊢ ((((𝐹 < 0 ∨
(♯‘𝑊) <
𝐿) ∧ ¬ 𝐿 ≤ 𝐹) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → (¬ (𝐹..^𝐿) ⊆ dom 𝑊 ↔ ¬ (𝐹..^𝐿) ⊆ (0..^(♯‘𝑊)))) | 
| 44 | 38, 43 | mpbird 257 | . . . . . . . . 9
⊢ ((((𝐹 < 0 ∨
(♯‘𝑊) <
𝐿) ∧ ¬ 𝐿 ≤ 𝐹) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → ¬ (𝐹..^𝐿) ⊆ dom 𝑊) | 
| 45 | 44 | iffalsed 4535 | . . . . . . . 8
⊢ ((((𝐹 < 0 ∨
(♯‘𝑊) <
𝐿) ∧ ¬ 𝐿 ≤ 𝐹) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → if((𝐹..^𝐿) ⊆ dom 𝑊, (𝑖 ∈ (0..^(𝐿 − 𝐹)) ↦ (𝑊‘(𝑖 + 𝐹))), ∅) = ∅) | 
| 46 | 7, 45 | eqtrd 2776 | . . . . . . 7
⊢ ((((𝐹 < 0 ∨
(♯‘𝑊) <
𝐿) ∧ ¬ 𝐿 ≤ 𝐹) ∧ (𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ)) → (𝑊 substr 〈𝐹, 𝐿〉) = ∅) | 
| 47 | 46 | exp31 419 | . . . . . 6
⊢ ((𝐹 < 0 ∨
(♯‘𝑊) <
𝐿) → (¬ 𝐿 ≤ 𝐹 → ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑊 substr 〈𝐹, 𝐿〉) = ∅))) | 
| 48 | 47 | impcom 407 | . . . . 5
⊢ ((¬
𝐿 ≤ 𝐹 ∧ (𝐹 < 0 ∨ (♯‘𝑊) < 𝐿)) → ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑊 substr 〈𝐹, 𝐿〉) = ∅)) | 
| 49 | 5, 48 | jaoi3 1060 | . . . 4
⊢ ((𝐿 ≤ 𝐹 ∨ (𝐹 < 0 ∨ (♯‘𝑊) < 𝐿)) → ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑊 substr 〈𝐹, 𝐿〉) = ∅)) | 
| 50 | 49 | orcoms 872 | . . 3
⊢ (((𝐹 < 0 ∨
(♯‘𝑊) <
𝐿) ∨ 𝐿 ≤ 𝐹) → ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑊 substr 〈𝐹, 𝐿〉) = ∅)) | 
| 51 | 3, 50 | sylbi 217 | . 2
⊢ ((𝐹 < 0 ∨ 𝐿 ≤ 𝐹 ∨ (♯‘𝑊) < 𝐿) → ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑊 substr 〈𝐹, 𝐿〉) = ∅)) | 
| 52 | 51 | com12 32 | 1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → ((𝐹 < 0 ∨ 𝐿 ≤ 𝐹 ∨ (♯‘𝑊) < 𝐿) → (𝑊 substr 〈𝐹, 𝐿〉) = ∅)) |