Proof of Theorem swrdfv2
Step | Hyp | Ref
| Expression |
1 | | simp1 1081 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (#‘𝑆)) → 𝑆 ∈ Word 𝑉) |
2 | | simpl 472 |
. . . . . . . 8
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
(ℤ≥‘𝐹)) → 𝐹 ∈
ℕ0) |
3 | | eluznn0 11795 |
. . . . . . . 8
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
(ℤ≥‘𝐹)) → 𝐿 ∈
ℕ0) |
4 | | eluzle 11738 |
. . . . . . . . 9
⊢ (𝐿 ∈
(ℤ≥‘𝐹) → 𝐹 ≤ 𝐿) |
5 | 4 | adantl 481 |
. . . . . . . 8
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
(ℤ≥‘𝐹)) → 𝐹 ≤ 𝐿) |
6 | 2, 3, 5 | 3jca 1261 |
. . . . . . 7
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
(ℤ≥‘𝐹)) → (𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝐹 ≤ 𝐿)) |
7 | 6 | 3ad2ant2 1103 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (#‘𝑆)) → (𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝐹 ≤ 𝐿)) |
8 | | elfz2nn0 12469 |
. . . . . 6
⊢ (𝐹 ∈ (0...𝐿) ↔ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝐹 ≤ 𝐿)) |
9 | 7, 8 | sylibr 224 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (#‘𝑆)) → 𝐹 ∈ (0...𝐿)) |
10 | 3 | anim1i 591 |
. . . . . . 7
⊢ (((𝐹 ∈ ℕ0
∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (#‘𝑆)) → (𝐿 ∈ ℕ0 ∧ 𝐿 ≤ (#‘𝑆))) |
11 | 10 | 3adant1 1099 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (#‘𝑆)) → (𝐿 ∈ ℕ0 ∧ 𝐿 ≤ (#‘𝑆))) |
12 | | lencl 13356 |
. . . . . . . 8
⊢ (𝑆 ∈ Word 𝑉 → (#‘𝑆) ∈
ℕ0) |
13 | 12 | 3ad2ant1 1102 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (#‘𝑆)) → (#‘𝑆) ∈
ℕ0) |
14 | | fznn0 12470 |
. . . . . . 7
⊢
((#‘𝑆) ∈
ℕ0 → (𝐿 ∈ (0...(#‘𝑆)) ↔ (𝐿 ∈ ℕ0 ∧ 𝐿 ≤ (#‘𝑆)))) |
15 | 13, 14 | syl 17 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (#‘𝑆)) → (𝐿 ∈ (0...(#‘𝑆)) ↔ (𝐿 ∈ ℕ0 ∧ 𝐿 ≤ (#‘𝑆)))) |
16 | 11, 15 | mpbird 247 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (#‘𝑆)) → 𝐿 ∈ (0...(#‘𝑆))) |
17 | 1, 9, 16 | 3jca 1261 |
. . . 4
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (#‘𝑆)) → (𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(#‘𝑆)))) |
18 | 17 | adantr 480 |
. . 3
⊢ (((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (#‘𝑆)) ∧ 𝑋 ∈ (𝐹..^𝐿)) → (𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(#‘𝑆)))) |
19 | | nn0cn 11340 |
. . . . . . . . . 10
⊢ (𝐹 ∈ ℕ0
→ 𝐹 ∈
ℂ) |
20 | | eluzelcn 11737 |
. . . . . . . . . 10
⊢ (𝐿 ∈
(ℤ≥‘𝐹) → 𝐿 ∈ ℂ) |
21 | | pncan3 10327 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ ℂ ∧ 𝐿 ∈ ℂ) → (𝐹 + (𝐿 − 𝐹)) = 𝐿) |
22 | 19, 20, 21 | syl2an 493 |
. . . . . . . . 9
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
(ℤ≥‘𝐹)) → (𝐹 + (𝐿 − 𝐹)) = 𝐿) |
23 | 22 | eqcomd 2657 |
. . . . . . . 8
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
(ℤ≥‘𝐹)) → 𝐿 = (𝐹 + (𝐿 − 𝐹))) |
24 | 23 | 3ad2ant2 1103 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (#‘𝑆)) → 𝐿 = (𝐹 + (𝐿 − 𝐹))) |
25 | 24 | oveq2d 6706 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (#‘𝑆)) → (𝐹..^𝐿) = (𝐹..^(𝐹 + (𝐿 − 𝐹)))) |
26 | 25 | eleq2d 2716 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (#‘𝑆)) → (𝑋 ∈ (𝐹..^𝐿) ↔ 𝑋 ∈ (𝐹..^(𝐹 + (𝐿 − 𝐹))))) |
27 | 26 | biimpa 500 |
. . . 4
⊢ (((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (#‘𝑆)) ∧ 𝑋 ∈ (𝐹..^𝐿)) → 𝑋 ∈ (𝐹..^(𝐹 + (𝐿 − 𝐹)))) |
28 | | eluzelz 11735 |
. . . . . . . 8
⊢ (𝐿 ∈
(ℤ≥‘𝐹) → 𝐿 ∈ ℤ) |
29 | 28 | adantl 481 |
. . . . . . 7
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
(ℤ≥‘𝐹)) → 𝐿 ∈ ℤ) |
30 | | nn0z 11438 |
. . . . . . . 8
⊢ (𝐹 ∈ ℕ0
→ 𝐹 ∈
ℤ) |
31 | 30 | adantr 480 |
. . . . . . 7
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
(ℤ≥‘𝐹)) → 𝐹 ∈ ℤ) |
32 | 29, 31 | zsubcld 11525 |
. . . . . 6
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
(ℤ≥‘𝐹)) → (𝐿 − 𝐹) ∈ ℤ) |
33 | 32 | 3ad2ant2 1103 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (#‘𝑆)) → (𝐿 − 𝐹) ∈ ℤ) |
34 | 33 | adantr 480 |
. . . 4
⊢ (((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (#‘𝑆)) ∧ 𝑋 ∈ (𝐹..^𝐿)) → (𝐿 − 𝐹) ∈ ℤ) |
35 | | fzosubel3 12568 |
. . . 4
⊢ ((𝑋 ∈ (𝐹..^(𝐹 + (𝐿 − 𝐹))) ∧ (𝐿 − 𝐹) ∈ ℤ) → (𝑋 − 𝐹) ∈ (0..^(𝐿 − 𝐹))) |
36 | 27, 34, 35 | syl2anc 694 |
. . 3
⊢ (((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (#‘𝑆)) ∧ 𝑋 ∈ (𝐹..^𝐿)) → (𝑋 − 𝐹) ∈ (0..^(𝐿 − 𝐹))) |
37 | | swrdfv 13469 |
. . 3
⊢ (((𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(#‘𝑆))) ∧ (𝑋 − 𝐹) ∈ (0..^(𝐿 − 𝐹))) → ((𝑆 substr 〈𝐹, 𝐿〉)‘(𝑋 − 𝐹)) = (𝑆‘((𝑋 − 𝐹) + 𝐹))) |
38 | 18, 36, 37 | syl2anc 694 |
. 2
⊢ (((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (#‘𝑆)) ∧ 𝑋 ∈ (𝐹..^𝐿)) → ((𝑆 substr 〈𝐹, 𝐿〉)‘(𝑋 − 𝐹)) = (𝑆‘((𝑋 − 𝐹) + 𝐹))) |
39 | | elfzoelz 12509 |
. . . . 5
⊢ (𝑋 ∈ (𝐹..^𝐿) → 𝑋 ∈ ℤ) |
40 | 39 | zcnd 11521 |
. . . 4
⊢ (𝑋 ∈ (𝐹..^𝐿) → 𝑋 ∈ ℂ) |
41 | 19 | adantr 480 |
. . . . 5
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
(ℤ≥‘𝐹)) → 𝐹 ∈ ℂ) |
42 | 41 | 3ad2ant2 1103 |
. . . 4
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (#‘𝑆)) → 𝐹 ∈ ℂ) |
43 | | npcan 10328 |
. . . 4
⊢ ((𝑋 ∈ ℂ ∧ 𝐹 ∈ ℂ) → ((𝑋 − 𝐹) + 𝐹) = 𝑋) |
44 | 40, 42, 43 | syl2anr 494 |
. . 3
⊢ (((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (#‘𝑆)) ∧ 𝑋 ∈ (𝐹..^𝐿)) → ((𝑋 − 𝐹) + 𝐹) = 𝑋) |
45 | 44 | fveq2d 6233 |
. 2
⊢ (((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (#‘𝑆)) ∧ 𝑋 ∈ (𝐹..^𝐿)) → (𝑆‘((𝑋 − 𝐹) + 𝐹)) = (𝑆‘𝑋)) |
46 | 38, 45 | eqtrd 2685 |
1
⊢ (((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (#‘𝑆)) ∧ 𝑋 ∈ (𝐹..^𝐿)) → ((𝑆 substr 〈𝐹, 𝐿〉)‘(𝑋 − 𝐹)) = (𝑆‘𝑋)) |