Proof of Theorem swrdfv2
Step | Hyp | Ref
| Expression |
1 | | simp1 1135 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) → 𝑆 ∈ Word 𝑉) |
2 | | simpl 483 |
. . . . . . . 8
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
(ℤ≥‘𝐹)) → 𝐹 ∈
ℕ0) |
3 | | eluznn0 12657 |
. . . . . . . 8
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
(ℤ≥‘𝐹)) → 𝐿 ∈
ℕ0) |
4 | | eluzle 12595 |
. . . . . . . . 9
⊢ (𝐿 ∈
(ℤ≥‘𝐹) → 𝐹 ≤ 𝐿) |
5 | 4 | adantl 482 |
. . . . . . . 8
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
(ℤ≥‘𝐹)) → 𝐹 ≤ 𝐿) |
6 | 2, 3, 5 | 3jca 1127 |
. . . . . . 7
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
(ℤ≥‘𝐹)) → (𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝐹 ≤ 𝐿)) |
7 | 6 | 3ad2ant2 1133 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) → (𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝐹 ≤ 𝐿)) |
8 | | elfz2nn0 13347 |
. . . . . 6
⊢ (𝐹 ∈ (0...𝐿) ↔ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0
∧ 𝐹 ≤ 𝐿)) |
9 | 7, 8 | sylibr 233 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) → 𝐹 ∈ (0...𝐿)) |
10 | 3 | anim1i 615 |
. . . . . . 7
⊢ (((𝐹 ∈ ℕ0
∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) → (𝐿 ∈ ℕ0 ∧ 𝐿 ≤ (♯‘𝑆))) |
11 | 10 | 3adant1 1129 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) → (𝐿 ∈ ℕ0 ∧ 𝐿 ≤ (♯‘𝑆))) |
12 | | lencl 14236 |
. . . . . . . 8
⊢ (𝑆 ∈ Word 𝑉 → (♯‘𝑆) ∈
ℕ0) |
13 | 12 | 3ad2ant1 1132 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) → (♯‘𝑆) ∈
ℕ0) |
14 | | fznn0 13348 |
. . . . . . 7
⊢
((♯‘𝑆)
∈ ℕ0 → (𝐿 ∈ (0...(♯‘𝑆)) ↔ (𝐿 ∈ ℕ0 ∧ 𝐿 ≤ (♯‘𝑆)))) |
15 | 13, 14 | syl 17 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) → (𝐿 ∈ (0...(♯‘𝑆)) ↔ (𝐿 ∈ ℕ0 ∧ 𝐿 ≤ (♯‘𝑆)))) |
16 | 11, 15 | mpbird 256 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) → 𝐿 ∈ (0...(♯‘𝑆))) |
17 | 1, 9, 16 | 3jca 1127 |
. . . 4
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) → (𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑆)))) |
18 | 17 | adantr 481 |
. . 3
⊢ (((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) ∧ 𝑋 ∈ (𝐹..^𝐿)) → (𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑆)))) |
19 | | nn0cn 12243 |
. . . . . . . . . 10
⊢ (𝐹 ∈ ℕ0
→ 𝐹 ∈
ℂ) |
20 | | eluzelcn 12594 |
. . . . . . . . . 10
⊢ (𝐿 ∈
(ℤ≥‘𝐹) → 𝐿 ∈ ℂ) |
21 | | pncan3 11229 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ ℂ ∧ 𝐿 ∈ ℂ) → (𝐹 + (𝐿 − 𝐹)) = 𝐿) |
22 | 19, 20, 21 | syl2an 596 |
. . . . . . . . 9
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
(ℤ≥‘𝐹)) → (𝐹 + (𝐿 − 𝐹)) = 𝐿) |
23 | 22 | eqcomd 2744 |
. . . . . . . 8
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
(ℤ≥‘𝐹)) → 𝐿 = (𝐹 + (𝐿 − 𝐹))) |
24 | 23 | 3ad2ant2 1133 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) → 𝐿 = (𝐹 + (𝐿 − 𝐹))) |
25 | 24 | oveq2d 7291 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) → (𝐹..^𝐿) = (𝐹..^(𝐹 + (𝐿 − 𝐹)))) |
26 | 25 | eleq2d 2824 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) → (𝑋 ∈ (𝐹..^𝐿) ↔ 𝑋 ∈ (𝐹..^(𝐹 + (𝐿 − 𝐹))))) |
27 | 26 | biimpa 477 |
. . . 4
⊢ (((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) ∧ 𝑋 ∈ (𝐹..^𝐿)) → 𝑋 ∈ (𝐹..^(𝐹 + (𝐿 − 𝐹)))) |
28 | | eluzelz 12592 |
. . . . . . . 8
⊢ (𝐿 ∈
(ℤ≥‘𝐹) → 𝐿 ∈ ℤ) |
29 | 28 | adantl 482 |
. . . . . . 7
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
(ℤ≥‘𝐹)) → 𝐿 ∈ ℤ) |
30 | | nn0z 12343 |
. . . . . . . 8
⊢ (𝐹 ∈ ℕ0
→ 𝐹 ∈
ℤ) |
31 | 30 | adantr 481 |
. . . . . . 7
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
(ℤ≥‘𝐹)) → 𝐹 ∈ ℤ) |
32 | 29, 31 | zsubcld 12431 |
. . . . . 6
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
(ℤ≥‘𝐹)) → (𝐿 − 𝐹) ∈ ℤ) |
33 | 32 | 3ad2ant2 1133 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) → (𝐿 − 𝐹) ∈ ℤ) |
34 | 33 | adantr 481 |
. . . 4
⊢ (((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) ∧ 𝑋 ∈ (𝐹..^𝐿)) → (𝐿 − 𝐹) ∈ ℤ) |
35 | | fzosubel3 13448 |
. . . 4
⊢ ((𝑋 ∈ (𝐹..^(𝐹 + (𝐿 − 𝐹))) ∧ (𝐿 − 𝐹) ∈ ℤ) → (𝑋 − 𝐹) ∈ (0..^(𝐿 − 𝐹))) |
36 | 27, 34, 35 | syl2anc 584 |
. . 3
⊢ (((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) ∧ 𝑋 ∈ (𝐹..^𝐿)) → (𝑋 − 𝐹) ∈ (0..^(𝐿 − 𝐹))) |
37 | | swrdfv 14361 |
. . 3
⊢ (((𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑆))) ∧ (𝑋 − 𝐹) ∈ (0..^(𝐿 − 𝐹))) → ((𝑆 substr 〈𝐹, 𝐿〉)‘(𝑋 − 𝐹)) = (𝑆‘((𝑋 − 𝐹) + 𝐹))) |
38 | 18, 36, 37 | syl2anc 584 |
. 2
⊢ (((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) ∧ 𝑋 ∈ (𝐹..^𝐿)) → ((𝑆 substr 〈𝐹, 𝐿〉)‘(𝑋 − 𝐹)) = (𝑆‘((𝑋 − 𝐹) + 𝐹))) |
39 | | elfzoelz 13387 |
. . . . 5
⊢ (𝑋 ∈ (𝐹..^𝐿) → 𝑋 ∈ ℤ) |
40 | 39 | zcnd 12427 |
. . . 4
⊢ (𝑋 ∈ (𝐹..^𝐿) → 𝑋 ∈ ℂ) |
41 | 19 | adantr 481 |
. . . . 5
⊢ ((𝐹 ∈ ℕ0
∧ 𝐿 ∈
(ℤ≥‘𝐹)) → 𝐹 ∈ ℂ) |
42 | 41 | 3ad2ant2 1133 |
. . . 4
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) → 𝐹 ∈ ℂ) |
43 | | npcan 11230 |
. . . 4
⊢ ((𝑋 ∈ ℂ ∧ 𝐹 ∈ ℂ) → ((𝑋 − 𝐹) + 𝐹) = 𝑋) |
44 | 40, 42, 43 | syl2anr 597 |
. . 3
⊢ (((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) ∧ 𝑋 ∈ (𝐹..^𝐿)) → ((𝑋 − 𝐹) + 𝐹) = 𝑋) |
45 | 44 | fveq2d 6778 |
. 2
⊢ (((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) ∧ 𝑋 ∈ (𝐹..^𝐿)) → (𝑆‘((𝑋 − 𝐹) + 𝐹)) = (𝑆‘𝑋)) |
46 | 38, 45 | eqtrd 2778 |
1
⊢ (((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈
(ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) ∧ 𝑋 ∈ (𝐹..^𝐿)) → ((𝑆 substr 〈𝐹, 𝐿〉)‘(𝑋 − 𝐹)) = (𝑆‘𝑋)) |