Step | Hyp | Ref
| Expression |
1 | | ccatcl 13212 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (𝑆 ++ 𝑇) ∈ Word 𝐵) |
2 | | ccatcl 13212 |
. . . . 5
⊢ (((𝑆 ++ 𝑇) ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) ++ 𝑈) ∈ Word 𝐵) |
3 | 1, 2 | stoic3 1692 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) ++ 𝑈) ∈ Word 𝐵) |
4 | | wrdf 13165 |
. . . 4
⊢ (((𝑆 ++ 𝑇) ++ 𝑈) ∈ Word 𝐵 → ((𝑆 ++ 𝑇) ++ 𝑈):(0..^(#‘((𝑆 ++ 𝑇) ++ 𝑈)))⟶𝐵) |
5 | | ffn 5958 |
. . . 4
⊢ (((𝑆 ++ 𝑇) ++ 𝑈):(0..^(#‘((𝑆 ++ 𝑇) ++ 𝑈)))⟶𝐵 → ((𝑆 ++ 𝑇) ++ 𝑈) Fn (0..^(#‘((𝑆 ++ 𝑇) ++ 𝑈)))) |
6 | 3, 4, 5 | 3syl 18 |
. . 3
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) ++ 𝑈) Fn (0..^(#‘((𝑆 ++ 𝑇) ++ 𝑈)))) |
7 | | ccatlen 13213 |
. . . . . . 7
⊢ (((𝑆 ++ 𝑇) ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → (#‘((𝑆 ++ 𝑇) ++ 𝑈)) = ((#‘(𝑆 ++ 𝑇)) + (#‘𝑈))) |
8 | 1, 7 | stoic3 1692 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → (#‘((𝑆 ++ 𝑇) ++ 𝑈)) = ((#‘(𝑆 ++ 𝑇)) + (#‘𝑈))) |
9 | | ccatlen 13213 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (#‘(𝑆 ++ 𝑇)) = ((#‘𝑆) + (#‘𝑇))) |
10 | 9 | 3adant3 1074 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → (#‘(𝑆 ++ 𝑇)) = ((#‘𝑆) + (#‘𝑇))) |
11 | 10 | oveq1d 6564 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → ((#‘(𝑆 ++ 𝑇)) + (#‘𝑈)) = (((#‘𝑆) + (#‘𝑇)) + (#‘𝑈))) |
12 | 8, 11 | eqtrd 2644 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → (#‘((𝑆 ++ 𝑇) ++ 𝑈)) = (((#‘𝑆) + (#‘𝑇)) + (#‘𝑈))) |
13 | 12 | oveq2d 6565 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → (0..^(#‘((𝑆 ++ 𝑇) ++ 𝑈))) = (0..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈)))) |
14 | 13 | fneq2d 5896 |
. . 3
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → (((𝑆 ++ 𝑇) ++ 𝑈) Fn (0..^(#‘((𝑆 ++ 𝑇) ++ 𝑈))) ↔ ((𝑆 ++ 𝑇) ++ 𝑈) Fn (0..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈))))) |
15 | 6, 14 | mpbid 221 |
. 2
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) ++ 𝑈) Fn (0..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈)))) |
16 | | simp1 1054 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → 𝑆 ∈ Word 𝐵) |
17 | | ccatcl 13212 |
. . . . . 6
⊢ ((𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → (𝑇 ++ 𝑈) ∈ Word 𝐵) |
18 | 17 | 3adant1 1072 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → (𝑇 ++ 𝑈) ∈ Word 𝐵) |
19 | | ccatcl 13212 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐵 ∧ (𝑇 ++ 𝑈) ∈ Word 𝐵) → (𝑆 ++ (𝑇 ++ 𝑈)) ∈ Word 𝐵) |
20 | 16, 18, 19 | syl2anc 691 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → (𝑆 ++ (𝑇 ++ 𝑈)) ∈ Word 𝐵) |
21 | | wrdf 13165 |
. . . 4
⊢ ((𝑆 ++ (𝑇 ++ 𝑈)) ∈ Word 𝐵 → (𝑆 ++ (𝑇 ++ 𝑈)):(0..^(#‘(𝑆 ++ (𝑇 ++ 𝑈))))⟶𝐵) |
22 | | ffn 5958 |
. . . 4
⊢ ((𝑆 ++ (𝑇 ++ 𝑈)):(0..^(#‘(𝑆 ++ (𝑇 ++ 𝑈))))⟶𝐵 → (𝑆 ++ (𝑇 ++ 𝑈)) Fn (0..^(#‘(𝑆 ++ (𝑇 ++ 𝑈))))) |
23 | 20, 21, 22 | 3syl 18 |
. . 3
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → (𝑆 ++ (𝑇 ++ 𝑈)) Fn (0..^(#‘(𝑆 ++ (𝑇 ++ 𝑈))))) |
24 | | ccatlen 13213 |
. . . . . . . 8
⊢ ((𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → (#‘(𝑇 ++ 𝑈)) = ((#‘𝑇) + (#‘𝑈))) |
25 | 24 | 3adant1 1072 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → (#‘(𝑇 ++ 𝑈)) = ((#‘𝑇) + (#‘𝑈))) |
26 | 25 | oveq2d 6565 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → ((#‘𝑆) + (#‘(𝑇 ++ 𝑈))) = ((#‘𝑆) + ((#‘𝑇) + (#‘𝑈)))) |
27 | | ccatlen 13213 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐵 ∧ (𝑇 ++ 𝑈) ∈ Word 𝐵) → (#‘(𝑆 ++ (𝑇 ++ 𝑈))) = ((#‘𝑆) + (#‘(𝑇 ++ 𝑈)))) |
28 | 16, 18, 27 | syl2anc 691 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → (#‘(𝑆 ++ (𝑇 ++ 𝑈))) = ((#‘𝑆) + (#‘(𝑇 ++ 𝑈)))) |
29 | | lencl 13179 |
. . . . . . . . 9
⊢ (𝑆 ∈ Word 𝐵 → (#‘𝑆) ∈
ℕ0) |
30 | 29 | 3ad2ant1 1075 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → (#‘𝑆) ∈
ℕ0) |
31 | 30 | nn0cnd 11230 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → (#‘𝑆) ∈ ℂ) |
32 | | lencl 13179 |
. . . . . . . . 9
⊢ (𝑇 ∈ Word 𝐵 → (#‘𝑇) ∈
ℕ0) |
33 | 32 | 3ad2ant2 1076 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → (#‘𝑇) ∈
ℕ0) |
34 | 33 | nn0cnd 11230 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → (#‘𝑇) ∈ ℂ) |
35 | | lencl 13179 |
. . . . . . . . 9
⊢ (𝑈 ∈ Word 𝐵 → (#‘𝑈) ∈
ℕ0) |
36 | 35 | 3ad2ant3 1077 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → (#‘𝑈) ∈
ℕ0) |
37 | 36 | nn0cnd 11230 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → (#‘𝑈) ∈ ℂ) |
38 | 31, 34, 37 | addassd 9941 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → (((#‘𝑆) + (#‘𝑇)) + (#‘𝑈)) = ((#‘𝑆) + ((#‘𝑇) + (#‘𝑈)))) |
39 | 26, 28, 38 | 3eqtr4d 2654 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → (#‘(𝑆 ++ (𝑇 ++ 𝑈))) = (((#‘𝑆) + (#‘𝑇)) + (#‘𝑈))) |
40 | 39 | oveq2d 6565 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → (0..^(#‘(𝑆 ++ (𝑇 ++ 𝑈)))) = (0..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈)))) |
41 | 40 | fneq2d 5896 |
. . 3
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → ((𝑆 ++ (𝑇 ++ 𝑈)) Fn (0..^(#‘(𝑆 ++ (𝑇 ++ 𝑈)))) ↔ (𝑆 ++ (𝑇 ++ 𝑈)) Fn (0..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈))))) |
42 | 23, 41 | mpbid 221 |
. 2
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → (𝑆 ++ (𝑇 ++ 𝑈)) Fn (0..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈)))) |
43 | 30 | nn0zd 11356 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → (#‘𝑆) ∈ ℤ) |
44 | | fzospliti 12369 |
. . . . 5
⊢ ((𝑥 ∈ (0..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈))) ∧ (#‘𝑆) ∈ ℤ) → (𝑥 ∈ (0..^(#‘𝑆)) ∨ 𝑥 ∈ ((#‘𝑆)..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈))))) |
45 | 44 | ancoms 468 |
. . . 4
⊢
(((#‘𝑆) ∈
ℤ ∧ 𝑥 ∈
(0..^(((#‘𝑆) +
(#‘𝑇)) +
(#‘𝑈)))) →
(𝑥 ∈
(0..^(#‘𝑆)) ∨
𝑥 ∈ ((#‘𝑆)..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈))))) |
46 | 43, 45 | sylan 487 |
. . 3
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈)))) → (𝑥 ∈ (0..^(#‘𝑆)) ∨ 𝑥 ∈ ((#‘𝑆)..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈))))) |
47 | | simpl1 1057 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑆))) → 𝑆 ∈ Word 𝐵) |
48 | | simpl2 1058 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑆))) → 𝑇 ∈ Word 𝐵) |
49 | | simpr 476 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑆))) → 𝑥 ∈ (0..^(#‘𝑆))) |
50 | | ccatval1 13214 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑥 ∈ (0..^(#‘𝑆))) → ((𝑆 ++ 𝑇)‘𝑥) = (𝑆‘𝑥)) |
51 | 47, 48, 49, 50 | syl3anc 1318 |
. . . . 5
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑆))) → ((𝑆 ++ 𝑇)‘𝑥) = (𝑆‘𝑥)) |
52 | 1 | 3adant3 1074 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → (𝑆 ++ 𝑇) ∈ Word 𝐵) |
53 | 52 | adantr 480 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑆))) → (𝑆 ++ 𝑇) ∈ Word 𝐵) |
54 | | simpl3 1059 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑆))) → 𝑈 ∈ Word 𝐵) |
55 | | uzid 11578 |
. . . . . . . . . . 11
⊢
((#‘𝑆) ∈
ℤ → (#‘𝑆)
∈ (ℤ≥‘(#‘𝑆))) |
56 | 43, 55 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → (#‘𝑆) ∈
(ℤ≥‘(#‘𝑆))) |
57 | | uzaddcl 11620 |
. . . . . . . . . 10
⊢
(((#‘𝑆) ∈
(ℤ≥‘(#‘𝑆)) ∧ (#‘𝑇) ∈ ℕ0) →
((#‘𝑆) +
(#‘𝑇)) ∈
(ℤ≥‘(#‘𝑆))) |
58 | 56, 33, 57 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → ((#‘𝑆) + (#‘𝑇)) ∈
(ℤ≥‘(#‘𝑆))) |
59 | | fzoss2 12365 |
. . . . . . . . 9
⊢
(((#‘𝑆) +
(#‘𝑇)) ∈
(ℤ≥‘(#‘𝑆)) → (0..^(#‘𝑆)) ⊆ (0..^((#‘𝑆) + (#‘𝑇)))) |
60 | 58, 59 | syl 17 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → (0..^(#‘𝑆)) ⊆ (0..^((#‘𝑆) + (#‘𝑇)))) |
61 | 10 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → (0..^(#‘(𝑆 ++ 𝑇))) = (0..^((#‘𝑆) + (#‘𝑇)))) |
62 | 60, 61 | sseqtr4d 3605 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → (0..^(#‘𝑆)) ⊆ (0..^(#‘(𝑆 ++ 𝑇)))) |
63 | 62 | sselda 3568 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑆))) → 𝑥 ∈ (0..^(#‘(𝑆 ++ 𝑇)))) |
64 | | ccatval1 13214 |
. . . . . 6
⊢ (((𝑆 ++ 𝑇) ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ∧ 𝑥 ∈ (0..^(#‘(𝑆 ++ 𝑇)))) → (((𝑆 ++ 𝑇) ++ 𝑈)‘𝑥) = ((𝑆 ++ 𝑇)‘𝑥)) |
65 | 53, 54, 63, 64 | syl3anc 1318 |
. . . . 5
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑆))) → (((𝑆 ++ 𝑇) ++ 𝑈)‘𝑥) = ((𝑆 ++ 𝑇)‘𝑥)) |
66 | 18 | adantr 480 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑆))) → (𝑇 ++ 𝑈) ∈ Word 𝐵) |
67 | | ccatval1 13214 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐵 ∧ (𝑇 ++ 𝑈) ∈ Word 𝐵 ∧ 𝑥 ∈ (0..^(#‘𝑆))) → ((𝑆 ++ (𝑇 ++ 𝑈))‘𝑥) = (𝑆‘𝑥)) |
68 | 47, 66, 49, 67 | syl3anc 1318 |
. . . . 5
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑆))) → ((𝑆 ++ (𝑇 ++ 𝑈))‘𝑥) = (𝑆‘𝑥)) |
69 | 51, 65, 68 | 3eqtr4d 2654 |
. . . 4
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(#‘𝑆))) → (((𝑆 ++ 𝑇) ++ 𝑈)‘𝑥) = ((𝑆 ++ (𝑇 ++ 𝑈))‘𝑥)) |
70 | 33 | nn0zd 11356 |
. . . . . . 7
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → (#‘𝑇) ∈ ℤ) |
71 | 43, 70 | zaddcld 11362 |
. . . . . 6
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → ((#‘𝑆) + (#‘𝑇)) ∈ ℤ) |
72 | | fzospliti 12369 |
. . . . . . 7
⊢ ((𝑥 ∈ ((#‘𝑆)..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈))) ∧ ((#‘𝑆) + (#‘𝑇)) ∈ ℤ) → (𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇))) ∨ 𝑥 ∈ (((#‘𝑆) + (#‘𝑇))..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈))))) |
73 | 72 | ancoms 468 |
. . . . . 6
⊢
((((#‘𝑆) +
(#‘𝑇)) ∈ ℤ
∧ 𝑥 ∈
((#‘𝑆)..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈)))) → (𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇))) ∨ 𝑥 ∈ (((#‘𝑆) + (#‘𝑇))..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈))))) |
74 | 71, 73 | sylan 487 |
. . . . 5
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ ((#‘𝑆)..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈)))) → (𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇))) ∨ 𝑥 ∈ (((#‘𝑆) + (#‘𝑇))..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈))))) |
75 | | simpl1 1057 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))) → 𝑆 ∈ Word 𝐵) |
76 | | simpl2 1058 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))) → 𝑇 ∈ Word 𝐵) |
77 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))) → 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))) |
78 | | ccatval2 13215 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))) → ((𝑆 ++ 𝑇)‘𝑥) = (𝑇‘(𝑥 − (#‘𝑆)))) |
79 | 75, 76, 77, 78 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))) → ((𝑆 ++ 𝑇)‘𝑥) = (𝑇‘(𝑥 − (#‘𝑆)))) |
80 | | simpl3 1059 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))) → 𝑈 ∈ Word 𝐵) |
81 | | fzosubel3 12396 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇))) ∧ (#‘𝑇) ∈ ℤ) → (𝑥 − (#‘𝑆)) ∈ (0..^(#‘𝑇))) |
82 | 81 | ancoms 468 |
. . . . . . . . . 10
⊢
(((#‘𝑇) ∈
ℤ ∧ 𝑥 ∈
((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))) → (𝑥 − (#‘𝑆)) ∈ (0..^(#‘𝑇))) |
83 | 70, 82 | sylan 487 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))) → (𝑥 − (#‘𝑆)) ∈ (0..^(#‘𝑇))) |
84 | | ccatval1 13214 |
. . . . . . . . 9
⊢ ((𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ∧ (𝑥 − (#‘𝑆)) ∈ (0..^(#‘𝑇))) → ((𝑇 ++ 𝑈)‘(𝑥 − (#‘𝑆))) = (𝑇‘(𝑥 − (#‘𝑆)))) |
85 | 76, 80, 83, 84 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))) → ((𝑇 ++ 𝑈)‘(𝑥 − (#‘𝑆))) = (𝑇‘(𝑥 − (#‘𝑆)))) |
86 | 79, 85 | eqtr4d 2647 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))) → ((𝑆 ++ 𝑇)‘𝑥) = ((𝑇 ++ 𝑈)‘(𝑥 − (#‘𝑆)))) |
87 | 52 | adantr 480 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))) → (𝑆 ++ 𝑇) ∈ Word 𝐵) |
88 | | fzoss1 12364 |
. . . . . . . . . . . 12
⊢
((#‘𝑆) ∈
(ℤ≥‘0) → ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇))) ⊆ (0..^((#‘𝑆) + (#‘𝑇)))) |
89 | | nn0uz 11598 |
. . . . . . . . . . . 12
⊢
ℕ0 = (ℤ≥‘0) |
90 | 88, 89 | eleq2s 2706 |
. . . . . . . . . . 11
⊢
((#‘𝑆) ∈
ℕ0 → ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇))) ⊆ (0..^((#‘𝑆) + (#‘𝑇)))) |
91 | 30, 90 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇))) ⊆ (0..^((#‘𝑆) + (#‘𝑇)))) |
92 | 91, 61 | sseqtr4d 3605 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇))) ⊆ (0..^(#‘(𝑆 ++ 𝑇)))) |
93 | 92 | sselda 3568 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))) → 𝑥 ∈ (0..^(#‘(𝑆 ++ 𝑇)))) |
94 | 87, 80, 93, 64 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))) → (((𝑆 ++ 𝑇) ++ 𝑈)‘𝑥) = ((𝑆 ++ 𝑇)‘𝑥)) |
95 | 18 | adantr 480 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))) → (𝑇 ++ 𝑈) ∈ Word 𝐵) |
96 | | uzid 11578 |
. . . . . . . . . . . . 13
⊢
(((#‘𝑆) +
(#‘𝑇)) ∈ ℤ
→ ((#‘𝑆) +
(#‘𝑇)) ∈
(ℤ≥‘((#‘𝑆) + (#‘𝑇)))) |
97 | 71, 96 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → ((#‘𝑆) + (#‘𝑇)) ∈
(ℤ≥‘((#‘𝑆) + (#‘𝑇)))) |
98 | | uzaddcl 11620 |
. . . . . . . . . . . 12
⊢
((((#‘𝑆) +
(#‘𝑇)) ∈
(ℤ≥‘((#‘𝑆) + (#‘𝑇))) ∧ (#‘𝑈) ∈ ℕ0) →
(((#‘𝑆) +
(#‘𝑇)) +
(#‘𝑈)) ∈
(ℤ≥‘((#‘𝑆) + (#‘𝑇)))) |
99 | 97, 36, 98 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → (((#‘𝑆) + (#‘𝑇)) + (#‘𝑈)) ∈
(ℤ≥‘((#‘𝑆) + (#‘𝑇)))) |
100 | | fzoss2 12365 |
. . . . . . . . . . 11
⊢
((((#‘𝑆) +
(#‘𝑇)) +
(#‘𝑈)) ∈
(ℤ≥‘((#‘𝑆) + (#‘𝑇))) → ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇))) ⊆ ((#‘𝑆)..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈)))) |
101 | 99, 100 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇))) ⊆ ((#‘𝑆)..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈)))) |
102 | 26, 38 | eqtr4d 2647 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → ((#‘𝑆) + (#‘(𝑇 ++ 𝑈))) = (((#‘𝑆) + (#‘𝑇)) + (#‘𝑈))) |
103 | 102 | oveq2d 6565 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → ((#‘𝑆)..^((#‘𝑆) + (#‘(𝑇 ++ 𝑈)))) = ((#‘𝑆)..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈)))) |
104 | 101, 103 | sseqtr4d 3605 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇))) ⊆ ((#‘𝑆)..^((#‘𝑆) + (#‘(𝑇 ++ 𝑈))))) |
105 | 104 | sselda 3568 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))) → 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘(𝑇 ++ 𝑈))))) |
106 | | ccatval2 13215 |
. . . . . . . 8
⊢ ((𝑆 ∈ Word 𝐵 ∧ (𝑇 ++ 𝑈) ∈ Word 𝐵 ∧ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘(𝑇 ++ 𝑈))))) → ((𝑆 ++ (𝑇 ++ 𝑈))‘𝑥) = ((𝑇 ++ 𝑈)‘(𝑥 − (#‘𝑆)))) |
107 | 75, 95, 105, 106 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))) → ((𝑆 ++ (𝑇 ++ 𝑈))‘𝑥) = ((𝑇 ++ 𝑈)‘(𝑥 − (#‘𝑆)))) |
108 | 86, 94, 107 | 3eqtr4d 2654 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇)))) → (((𝑆 ++ 𝑇) ++ 𝑈)‘𝑥) = ((𝑆 ++ (𝑇 ++ 𝑈))‘𝑥)) |
109 | 10 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → (𝑥 − (#‘(𝑆 ++ 𝑇))) = (𝑥 − ((#‘𝑆) + (#‘𝑇)))) |
110 | 109 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((#‘𝑆) + (#‘𝑇))..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈)))) → (𝑥 − (#‘(𝑆 ++ 𝑇))) = (𝑥 − ((#‘𝑆) + (#‘𝑇)))) |
111 | | elfzoelz 12339 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (((#‘𝑆) + (#‘𝑇))..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈))) → 𝑥 ∈ ℤ) |
112 | 111 | zcnd 11359 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (((#‘𝑆) + (#‘𝑇))..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈))) → 𝑥 ∈ ℂ) |
113 | 112 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((#‘𝑆) + (#‘𝑇))..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈)))) → 𝑥 ∈ ℂ) |
114 | 31 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((#‘𝑆) + (#‘𝑇))..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈)))) → (#‘𝑆) ∈ ℂ) |
115 | 34 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((#‘𝑆) + (#‘𝑇))..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈)))) → (#‘𝑇) ∈ ℂ) |
116 | 113, 114,
115 | subsub4d 10302 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((#‘𝑆) + (#‘𝑇))..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈)))) → ((𝑥 − (#‘𝑆)) − (#‘𝑇)) = (𝑥 − ((#‘𝑆) + (#‘𝑇)))) |
117 | 110, 116 | eqtr4d 2647 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((#‘𝑆) + (#‘𝑇))..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈)))) → (𝑥 − (#‘(𝑆 ++ 𝑇))) = ((𝑥 − (#‘𝑆)) − (#‘𝑇))) |
118 | 117 | fveq2d 6107 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((#‘𝑆) + (#‘𝑇))..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈)))) → (𝑈‘(𝑥 − (#‘(𝑆 ++ 𝑇)))) = (𝑈‘((𝑥 − (#‘𝑆)) − (#‘𝑇)))) |
119 | | simpl2 1058 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((#‘𝑆) + (#‘𝑇))..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈)))) → 𝑇 ∈ Word 𝐵) |
120 | | simpl3 1059 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((#‘𝑆) + (#‘𝑇))..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈)))) → 𝑈 ∈ Word 𝐵) |
121 | 38 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → (((#‘𝑆) + (#‘𝑇))..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈))) = (((#‘𝑆) + (#‘𝑇))..^((#‘𝑆) + ((#‘𝑇) + (#‘𝑈))))) |
122 | 121 | eleq2d 2673 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → (𝑥 ∈ (((#‘𝑆) + (#‘𝑇))..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈))) ↔ 𝑥 ∈ (((#‘𝑆) + (#‘𝑇))..^((#‘𝑆) + ((#‘𝑇) + (#‘𝑈)))))) |
123 | 122 | biimpa 500 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((#‘𝑆) + (#‘𝑇))..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈)))) → 𝑥 ∈ (((#‘𝑆) + (#‘𝑇))..^((#‘𝑆) + ((#‘𝑇) + (#‘𝑈))))) |
124 | 43 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((#‘𝑆) + (#‘𝑇))..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈)))) → (#‘𝑆) ∈ ℤ) |
125 | 70 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((#‘𝑆) + (#‘𝑇))..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈)))) → (#‘𝑇) ∈ ℤ) |
126 | 36 | nn0zd 11356 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → (#‘𝑈) ∈ ℤ) |
127 | 70, 126 | zaddcld 11362 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → ((#‘𝑇) + (#‘𝑈)) ∈ ℤ) |
128 | 127 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((#‘𝑆) + (#‘𝑇))..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈)))) → ((#‘𝑇) + (#‘𝑈)) ∈ ℤ) |
129 | | fzosubel2 12395 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (((#‘𝑆) + (#‘𝑇))..^((#‘𝑆) + ((#‘𝑇) + (#‘𝑈)))) ∧ ((#‘𝑆) ∈ ℤ ∧ (#‘𝑇) ∈ ℤ ∧
((#‘𝑇) +
(#‘𝑈)) ∈
ℤ)) → (𝑥 −
(#‘𝑆)) ∈
((#‘𝑇)..^((#‘𝑇) + (#‘𝑈)))) |
130 | 123, 124,
125, 128, 129 | syl13anc 1320 |
. . . . . . . . 9
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((#‘𝑆) + (#‘𝑇))..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈)))) → (𝑥 − (#‘𝑆)) ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑈)))) |
131 | | ccatval2 13215 |
. . . . . . . . 9
⊢ ((𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ∧ (𝑥 − (#‘𝑆)) ∈ ((#‘𝑇)..^((#‘𝑇) + (#‘𝑈)))) → ((𝑇 ++ 𝑈)‘(𝑥 − (#‘𝑆))) = (𝑈‘((𝑥 − (#‘𝑆)) − (#‘𝑇)))) |
132 | 119, 120,
130, 131 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((#‘𝑆) + (#‘𝑇))..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈)))) → ((𝑇 ++ 𝑈)‘(𝑥 − (#‘𝑆))) = (𝑈‘((𝑥 − (#‘𝑆)) − (#‘𝑇)))) |
133 | 118, 132 | eqtr4d 2647 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((#‘𝑆) + (#‘𝑇))..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈)))) → (𝑈‘(𝑥 − (#‘(𝑆 ++ 𝑇)))) = ((𝑇 ++ 𝑈)‘(𝑥 − (#‘𝑆)))) |
134 | 52 | adantr 480 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((#‘𝑆) + (#‘𝑇))..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈)))) → (𝑆 ++ 𝑇) ∈ Word 𝐵) |
135 | 10, 11 | oveq12d 6567 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → ((#‘(𝑆 ++ 𝑇))..^((#‘(𝑆 ++ 𝑇)) + (#‘𝑈))) = (((#‘𝑆) + (#‘𝑇))..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈)))) |
136 | 135 | eleq2d 2673 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → (𝑥 ∈ ((#‘(𝑆 ++ 𝑇))..^((#‘(𝑆 ++ 𝑇)) + (#‘𝑈))) ↔ 𝑥 ∈ (((#‘𝑆) + (#‘𝑇))..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈))))) |
137 | 136 | biimpar 501 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((#‘𝑆) + (#‘𝑇))..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈)))) → 𝑥 ∈ ((#‘(𝑆 ++ 𝑇))..^((#‘(𝑆 ++ 𝑇)) + (#‘𝑈)))) |
138 | | ccatval2 13215 |
. . . . . . . 8
⊢ (((𝑆 ++ 𝑇) ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵 ∧ 𝑥 ∈ ((#‘(𝑆 ++ 𝑇))..^((#‘(𝑆 ++ 𝑇)) + (#‘𝑈)))) → (((𝑆 ++ 𝑇) ++ 𝑈)‘𝑥) = (𝑈‘(𝑥 − (#‘(𝑆 ++ 𝑇))))) |
139 | 134, 120,
137, 138 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((#‘𝑆) + (#‘𝑇))..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈)))) → (((𝑆 ++ 𝑇) ++ 𝑈)‘𝑥) = (𝑈‘(𝑥 − (#‘(𝑆 ++ 𝑇))))) |
140 | | simpl1 1057 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((#‘𝑆) + (#‘𝑇))..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈)))) → 𝑆 ∈ Word 𝐵) |
141 | 18 | adantr 480 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((#‘𝑆) + (#‘𝑇))..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈)))) → (𝑇 ++ 𝑈) ∈ Word 𝐵) |
142 | | fzoss1 12364 |
. . . . . . . . . . 11
⊢
(((#‘𝑆) +
(#‘𝑇)) ∈
(ℤ≥‘(#‘𝑆)) → (((#‘𝑆) + (#‘𝑇))..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈))) ⊆ ((#‘𝑆)..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈)))) |
143 | 58, 142 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → (((#‘𝑆) + (#‘𝑇))..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈))) ⊆ ((#‘𝑆)..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈)))) |
144 | 143, 103 | sseqtr4d 3605 |
. . . . . . . . 9
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → (((#‘𝑆) + (#‘𝑇))..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈))) ⊆ ((#‘𝑆)..^((#‘𝑆) + (#‘(𝑇 ++ 𝑈))))) |
145 | 144 | sselda 3568 |
. . . . . . . 8
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((#‘𝑆) + (#‘𝑇))..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈)))) → 𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘(𝑇 ++ 𝑈))))) |
146 | 140, 141,
145, 106 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((#‘𝑆) + (#‘𝑇))..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈)))) → ((𝑆 ++ (𝑇 ++ 𝑈))‘𝑥) = ((𝑇 ++ 𝑈)‘(𝑥 − (#‘𝑆)))) |
147 | 133, 139,
146 | 3eqtr4d 2654 |
. . . . . 6
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (((#‘𝑆) + (#‘𝑇))..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈)))) → (((𝑆 ++ 𝑇) ++ 𝑈)‘𝑥) = ((𝑆 ++ (𝑇 ++ 𝑈))‘𝑥)) |
148 | 108, 147 | jaodan 822 |
. . . . 5
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ (𝑥 ∈ ((#‘𝑆)..^((#‘𝑆) + (#‘𝑇))) ∨ 𝑥 ∈ (((#‘𝑆) + (#‘𝑇))..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈))))) → (((𝑆 ++ 𝑇) ++ 𝑈)‘𝑥) = ((𝑆 ++ (𝑇 ++ 𝑈))‘𝑥)) |
149 | 74, 148 | syldan 486 |
. . . 4
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ ((#‘𝑆)..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈)))) → (((𝑆 ++ 𝑇) ++ 𝑈)‘𝑥) = ((𝑆 ++ (𝑇 ++ 𝑈))‘𝑥)) |
150 | 69, 149 | jaodan 822 |
. . 3
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ (𝑥 ∈ (0..^(#‘𝑆)) ∨ 𝑥 ∈ ((#‘𝑆)..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈))))) → (((𝑆 ++ 𝑇) ++ 𝑈)‘𝑥) = ((𝑆 ++ (𝑇 ++ 𝑈))‘𝑥)) |
151 | 46, 150 | syldan 486 |
. 2
⊢ (((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) ∧ 𝑥 ∈ (0..^(((#‘𝑆) + (#‘𝑇)) + (#‘𝑈)))) → (((𝑆 ++ 𝑇) ++ 𝑈)‘𝑥) = ((𝑆 ++ (𝑇 ++ 𝑈))‘𝑥)) |
152 | 15, 42, 151 | eqfnfvd 6222 |
1
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) ++ 𝑈) = (𝑆 ++ (𝑇 ++ 𝑈))) |