Proof of Theorem swrdfv2
| Step | Hyp | Ref
| Expression |
| 1 | | simp1 1137 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) → 𝑆 ∈ Word 𝑉) |
| 2 | | simpl 482 |
. . . . . . . 8
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
(ℤ≥‘𝐹)) → 𝐹 ∈
ℕ0) |
| 3 | | eluznn0 12959 |
. . . . . . . 8
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
(ℤ≥‘𝐹)) → 𝐿 ∈
ℕ0) |
| 4 | | eluzle 12891 |
. . . . . . . . 9
⊢ (𝐿 ∈
(ℤ≥‘𝐹) → 𝐹 ≤ 𝐿) |
| 5 | 4 | adantl 481 |
. . . . . . . 8
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
(ℤ≥‘𝐹)) → 𝐹 ≤ 𝐿) |
| 6 | 2, 3, 5 | 3jca 1129 |
. . . . . . 7
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
(ℤ≥‘𝐹)) → (𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝐹 ≤ 𝐿)) |
| 7 | 6 | 3ad2ant2 1135 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) → (𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝐹 ≤ 𝐿)) |
| 8 | | elfz2nn0 13658 |
. . . . . 6
⊢ (𝐹 ∈ (0...𝐿) ↔ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝐹 ≤ 𝐿)) |
| 9 | 7, 8 | sylibr 234 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) → 𝐹 ∈ (0...𝐿)) |
| 10 | 3 | anim1i 615 |
. . . . . . 7
⊢ (((𝐹 ∈ ℕ0
∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) → (𝐿 ∈ ℕ0 ∧ 𝐿 ≤ (♯‘𝑆))) |
| 11 | 10 | 3adant1 1131 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) → (𝐿 ∈ ℕ0 ∧ 𝐿 ≤ (♯‘𝑆))) |
| 12 | | lencl 14571 |
. . . . . . . 8
⊢ (𝑆 ∈ Word 𝑉 → (♯‘𝑆) ∈
ℕ0) |
| 13 | 12 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) → (♯‘𝑆) ∈
ℕ0) |
| 14 | | fznn0 13659 |
. . . . . . 7
⊢
((♯‘𝑆)
∈ ℕ0 → (𝐿 ∈ (0...(♯‘𝑆)) ↔ (𝐿 ∈ ℕ0 ∧ 𝐿 ≤ (♯‘𝑆)))) |
| 15 | 13, 14 | syl 17 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) → (𝐿 ∈ (0...(♯‘𝑆)) ↔ (𝐿 ∈ ℕ0 ∧ 𝐿 ≤ (♯‘𝑆)))) |
| 16 | 11, 15 | mpbird 257 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) → 𝐿 ∈ (0...(♯‘𝑆))) |
| 17 | 1, 9, 16 | 3jca 1129 |
. . . 4
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) → (𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑆)))) |
| 18 | 17 | adantr 480 |
. . 3
⊢ (((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) ∧ 𝑋 ∈ (𝐹..^𝐿)) → (𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑆)))) |
| 19 | | nn0cn 12536 |
. . . . . . . . . 10
⊢ (𝐹 ∈ ℕ0
→ 𝐹 ∈
ℂ) |
| 20 | | eluzelcn 12890 |
. . . . . . . . . 10
⊢ (𝐿 ∈
(ℤ≥‘𝐹) → 𝐿 ∈ ℂ) |
| 21 | | pncan3 11516 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ ℂ ∧ 𝐿 ∈ ℂ) → (𝐹 + (𝐿 − 𝐹)) = 𝐿) |
| 22 | 19, 20, 21 | syl2an 596 |
. . . . . . . . 9
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
(ℤ≥‘𝐹)) → (𝐹 + (𝐿 − 𝐹)) = 𝐿) |
| 23 | 22 | eqcomd 2743 |
. . . . . . . 8
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
(ℤ≥‘𝐹)) → 𝐿 = (𝐹 + (𝐿 − 𝐹))) |
| 24 | 23 | 3ad2ant2 1135 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) → 𝐿 = (𝐹 + (𝐿 − 𝐹))) |
| 25 | 24 | oveq2d 7447 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) → (𝐹..^𝐿) = (𝐹..^(𝐹 + (𝐿 − 𝐹)))) |
| 26 | 25 | eleq2d 2827 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) → (𝑋 ∈ (𝐹..^𝐿) ↔ 𝑋 ∈ (𝐹..^(𝐹 + (𝐿 − 𝐹))))) |
| 27 | 26 | biimpa 476 |
. . . 4
⊢ (((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) ∧ 𝑋 ∈ (𝐹..^𝐿)) → 𝑋 ∈ (𝐹..^(𝐹 + (𝐿 − 𝐹)))) |
| 28 | | eluzelz 12888 |
. . . . . . . 8
⊢ (𝐿 ∈
(ℤ≥‘𝐹) → 𝐿 ∈ ℤ) |
| 29 | 28 | adantl 481 |
. . . . . . 7
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
(ℤ≥‘𝐹)) → 𝐿 ∈ ℤ) |
| 30 | | nn0z 12638 |
. . . . . . . 8
⊢ (𝐹 ∈ ℕ0
→ 𝐹 ∈
ℤ) |
| 31 | 30 | adantr 480 |
. . . . . . 7
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
(ℤ≥‘𝐹)) → 𝐹 ∈ ℤ) |
| 32 | 29, 31 | zsubcld 12727 |
. . . . . 6
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
(ℤ≥‘𝐹)) → (𝐿 − 𝐹) ∈ ℤ) |
| 33 | 32 | 3ad2ant2 1135 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) → (𝐿 − 𝐹) ∈ ℤ) |
| 34 | 33 | adantr 480 |
. . . 4
⊢ (((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) ∧ 𝑋 ∈ (𝐹..^𝐿)) → (𝐿 − 𝐹) ∈ ℤ) |
| 35 | | fzosubel3 13765 |
. . . 4
⊢ ((𝑋 ∈ (𝐹..^(𝐹 + (𝐿 − 𝐹))) ∧ (𝐿 − 𝐹) ∈ ℤ) → (𝑋 − 𝐹) ∈ (0..^(𝐿 − 𝐹))) |
| 36 | 27, 34, 35 | syl2anc 584 |
. . 3
⊢ (((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) ∧ 𝑋 ∈ (𝐹..^𝐿)) → (𝑋 − 𝐹) ∈ (0..^(𝐿 − 𝐹))) |
| 37 | | swrdfv 14686 |
. . 3
⊢ (((𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑆))) ∧ (𝑋 − 𝐹) ∈ (0..^(𝐿 − 𝐹))) → ((𝑆 substr 〈𝐹, 𝐿〉)‘(𝑋 − 𝐹)) = (𝑆‘((𝑋 − 𝐹) + 𝐹))) |
| 38 | 18, 36, 37 | syl2anc 584 |
. 2
⊢ (((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) ∧ 𝑋 ∈ (𝐹..^𝐿)) → ((𝑆 substr 〈𝐹, 𝐿〉)‘(𝑋 − 𝐹)) = (𝑆‘((𝑋 − 𝐹) + 𝐹))) |
| 39 | | elfzoelz 13699 |
. . . . 5
⊢ (𝑋 ∈ (𝐹..^𝐿) → 𝑋 ∈ ℤ) |
| 40 | 39 | zcnd 12723 |
. . . 4
⊢ (𝑋 ∈ (𝐹..^𝐿) → 𝑋 ∈ ℂ) |
| 41 | 19 | adantr 480 |
. . . . 5
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
(ℤ≥‘𝐹)) → 𝐹 ∈ ℂ) |
| 42 | 41 | 3ad2ant2 1135 |
. . . 4
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) → 𝐹 ∈ ℂ) |
| 43 | | npcan 11517 |
. . . 4
⊢ ((𝑋 ∈ ℂ ∧ 𝐹 ∈ ℂ) → ((𝑋 − 𝐹) + 𝐹) = 𝑋) |
| 44 | 40, 42, 43 | syl2anr 597 |
. . 3
⊢ (((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) ∧ 𝑋 ∈ (𝐹..^𝐿)) → ((𝑋 − 𝐹) + 𝐹) = 𝑋) |
| 45 | 44 | fveq2d 6910 |
. 2
⊢ (((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) ∧ 𝑋 ∈ (𝐹..^𝐿)) → (𝑆‘((𝑋 − 𝐹) + 𝐹)) = (𝑆‘𝑋)) |
| 46 | 38, 45 | eqtrd 2777 |
1
⊢ (((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) ∧ 𝑋 ∈ (𝐹..^𝐿)) → ((𝑆 substr 〈𝐹, 𝐿〉)‘(𝑋 − 𝐹)) = (𝑆‘𝑋)) |