Step | Hyp | Ref
| Expression |
1 | | repswlen 14341 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
(♯‘(𝑆 repeatS
𝑁)) = 𝑁) |
2 | 1 | 3adant3 1134 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
→ (♯‘(𝑆
repeatS 𝑁)) = 𝑁) |
3 | | repswlen 14341 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ ℕ0) →
(♯‘(𝑆 repeatS
𝑀)) = 𝑀) |
4 | 3 | 3adant2 1133 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
→ (♯‘(𝑆
repeatS 𝑀)) = 𝑀) |
5 | 2, 4 | oveq12d 7231 |
. . . 4
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
→ ((♯‘(𝑆
repeatS 𝑁)) +
(♯‘(𝑆 repeatS
𝑀))) = (𝑁 + 𝑀)) |
6 | 5 | oveq2d 7229 |
. . 3
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
→ (0..^((♯‘(𝑆 repeatS 𝑁)) + (♯‘(𝑆 repeatS 𝑀)))) = (0..^(𝑁 + 𝑀))) |
7 | | simp1 1138 |
. . . . . . . 8
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
→ 𝑆 ∈ 𝑉) |
8 | 7 | adantr 484 |
. . . . . . 7
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
(0..^(♯‘(𝑆
repeatS 𝑁)))) → 𝑆 ∈ 𝑉) |
9 | | simpl2 1194 |
. . . . . . 7
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
(0..^(♯‘(𝑆
repeatS 𝑁)))) → 𝑁 ∈
ℕ0) |
10 | 2 | oveq2d 7229 |
. . . . . . . . 9
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
→ (0..^(♯‘(𝑆 repeatS 𝑁))) = (0..^𝑁)) |
11 | 10 | eleq2d 2823 |
. . . . . . . 8
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
→ (𝑥 ∈
(0..^(♯‘(𝑆
repeatS 𝑁))) ↔ 𝑥 ∈ (0..^𝑁))) |
12 | 11 | biimpa 480 |
. . . . . . 7
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
(0..^(♯‘(𝑆
repeatS 𝑁)))) → 𝑥 ∈ (0..^𝑁)) |
13 | 8, 9, 12 | 3jca 1130 |
. . . . . 6
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
(0..^(♯‘(𝑆
repeatS 𝑁)))) → (𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ (0..^𝑁))) |
14 | 13 | adantlr 715 |
. . . . 5
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
(0..^((♯‘(𝑆
repeatS 𝑁)) +
(♯‘(𝑆 repeatS
𝑀))))) ∧ 𝑥 ∈
(0..^(♯‘(𝑆
repeatS 𝑁)))) → (𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ (0..^𝑁))) |
15 | | repswsymb 14339 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝑆 repeatS 𝑁)‘𝑥) = 𝑆) |
16 | 14, 15 | syl 17 |
. . . 4
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
(0..^((♯‘(𝑆
repeatS 𝑁)) +
(♯‘(𝑆 repeatS
𝑀))))) ∧ 𝑥 ∈
(0..^(♯‘(𝑆
repeatS 𝑁)))) →
((𝑆 repeatS 𝑁)‘𝑥) = 𝑆) |
17 | 7 | ad2antrr 726 |
. . . . 5
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
(0..^((♯‘(𝑆
repeatS 𝑁)) +
(♯‘(𝑆 repeatS
𝑀))))) ∧ ¬ 𝑥 ∈
(0..^(♯‘(𝑆
repeatS 𝑁)))) → 𝑆 ∈ 𝑉) |
18 | | simpll3 1216 |
. . . . 5
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
(0..^((♯‘(𝑆
repeatS 𝑁)) +
(♯‘(𝑆 repeatS
𝑀))))) ∧ ¬ 𝑥 ∈
(0..^(♯‘(𝑆
repeatS 𝑁)))) → 𝑀 ∈
ℕ0) |
19 | 2, 4 | jca 515 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
→ ((♯‘(𝑆
repeatS 𝑁)) = 𝑁 ∧ (♯‘(𝑆 repeatS 𝑀)) = 𝑀)) |
20 | | simpr 488 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ 𝑥 ∈ (0..^(𝑁 + 𝑀))) → 𝑥 ∈ (0..^(𝑁 + 𝑀))) |
21 | 20 | anim1i 618 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ 𝑥 ∈ (0..^(𝑁 + 𝑀))) ∧ ¬ 𝑥 ∈ (0..^𝑁)) → (𝑥 ∈ (0..^(𝑁 + 𝑀)) ∧ ¬ 𝑥 ∈ (0..^𝑁))) |
22 | | nn0z 12200 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
23 | | nn0z 12200 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℤ) |
24 | 22, 23 | anim12i 616 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) |
25 | 24 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ 𝑥 ∈ (0..^(𝑁 + 𝑀))) ∧ ¬ 𝑥 ∈ (0..^𝑁)) → (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) |
26 | | fzocatel 13306 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ (0..^(𝑁 + 𝑀)) ∧ ¬ 𝑥 ∈ (0..^𝑁)) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (𝑥 − 𝑁) ∈ (0..^𝑀)) |
27 | 21, 25, 26 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ 𝑥 ∈ (0..^(𝑁 + 𝑀))) ∧ ¬ 𝑥 ∈ (0..^𝑁)) → (𝑥 − 𝑁) ∈ (0..^𝑀)) |
28 | 27 | exp31 423 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (𝑥 ∈ (0..^(𝑁 + 𝑀)) → (¬ 𝑥 ∈ (0..^𝑁) → (𝑥 − 𝑁) ∈ (0..^𝑀)))) |
29 | 28 | 3adant1 1132 |
. . . . . . . 8
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
→ (𝑥 ∈
(0..^(𝑁 + 𝑀)) → (¬ 𝑥 ∈ (0..^𝑁) → (𝑥 − 𝑁) ∈ (0..^𝑀)))) |
30 | | oveq12 7222 |
. . . . . . . . . . 11
⊢
(((♯‘(𝑆
repeatS 𝑁)) = 𝑁 ∧ (♯‘(𝑆 repeatS 𝑀)) = 𝑀) → ((♯‘(𝑆 repeatS 𝑁)) + (♯‘(𝑆 repeatS 𝑀))) = (𝑁 + 𝑀)) |
31 | 30 | oveq2d 7229 |
. . . . . . . . . 10
⊢
(((♯‘(𝑆
repeatS 𝑁)) = 𝑁 ∧ (♯‘(𝑆 repeatS 𝑀)) = 𝑀) → (0..^((♯‘(𝑆 repeatS 𝑁)) + (♯‘(𝑆 repeatS 𝑀)))) = (0..^(𝑁 + 𝑀))) |
32 | 31 | eleq2d 2823 |
. . . . . . . . 9
⊢
(((♯‘(𝑆
repeatS 𝑁)) = 𝑁 ∧ (♯‘(𝑆 repeatS 𝑀)) = 𝑀) → (𝑥 ∈ (0..^((♯‘(𝑆 repeatS 𝑁)) + (♯‘(𝑆 repeatS 𝑀)))) ↔ 𝑥 ∈ (0..^(𝑁 + 𝑀)))) |
33 | | oveq2 7221 |
. . . . . . . . . . . . 13
⊢
((♯‘(𝑆
repeatS 𝑁)) = 𝑁 →
(0..^(♯‘(𝑆
repeatS 𝑁))) = (0..^𝑁)) |
34 | 33 | eleq2d 2823 |
. . . . . . . . . . . 12
⊢
((♯‘(𝑆
repeatS 𝑁)) = 𝑁 → (𝑥 ∈ (0..^(♯‘(𝑆 repeatS 𝑁))) ↔ 𝑥 ∈ (0..^𝑁))) |
35 | 34 | notbid 321 |
. . . . . . . . . . 11
⊢
((♯‘(𝑆
repeatS 𝑁)) = 𝑁 → (¬ 𝑥 ∈
(0..^(♯‘(𝑆
repeatS 𝑁))) ↔ ¬
𝑥 ∈ (0..^𝑁))) |
36 | 35 | adantr 484 |
. . . . . . . . . 10
⊢
(((♯‘(𝑆
repeatS 𝑁)) = 𝑁 ∧ (♯‘(𝑆 repeatS 𝑀)) = 𝑀) → (¬ 𝑥 ∈ (0..^(♯‘(𝑆 repeatS 𝑁))) ↔ ¬ 𝑥 ∈ (0..^𝑁))) |
37 | | oveq2 7221 |
. . . . . . . . . . . 12
⊢
((♯‘(𝑆
repeatS 𝑁)) = 𝑁 → (𝑥 − (♯‘(𝑆 repeatS 𝑁))) = (𝑥 − 𝑁)) |
38 | 37 | eleq1d 2822 |
. . . . . . . . . . 11
⊢
((♯‘(𝑆
repeatS 𝑁)) = 𝑁 → ((𝑥 − (♯‘(𝑆 repeatS 𝑁))) ∈ (0..^𝑀) ↔ (𝑥 − 𝑁) ∈ (0..^𝑀))) |
39 | 38 | adantr 484 |
. . . . . . . . . 10
⊢
(((♯‘(𝑆
repeatS 𝑁)) = 𝑁 ∧ (♯‘(𝑆 repeatS 𝑀)) = 𝑀) → ((𝑥 − (♯‘(𝑆 repeatS 𝑁))) ∈ (0..^𝑀) ↔ (𝑥 − 𝑁) ∈ (0..^𝑀))) |
40 | 36, 39 | imbi12d 348 |
. . . . . . . . 9
⊢
(((♯‘(𝑆
repeatS 𝑁)) = 𝑁 ∧ (♯‘(𝑆 repeatS 𝑀)) = 𝑀) → ((¬ 𝑥 ∈ (0..^(♯‘(𝑆 repeatS 𝑁))) → (𝑥 − (♯‘(𝑆 repeatS 𝑁))) ∈ (0..^𝑀)) ↔ (¬ 𝑥 ∈ (0..^𝑁) → (𝑥 − 𝑁) ∈ (0..^𝑀)))) |
41 | 32, 40 | imbi12d 348 |
. . . . . . . 8
⊢
(((♯‘(𝑆
repeatS 𝑁)) = 𝑁 ∧ (♯‘(𝑆 repeatS 𝑀)) = 𝑀) → ((𝑥 ∈ (0..^((♯‘(𝑆 repeatS 𝑁)) + (♯‘(𝑆 repeatS 𝑀)))) → (¬ 𝑥 ∈ (0..^(♯‘(𝑆 repeatS 𝑁))) → (𝑥 − (♯‘(𝑆 repeatS 𝑁))) ∈ (0..^𝑀))) ↔ (𝑥 ∈ (0..^(𝑁 + 𝑀)) → (¬ 𝑥 ∈ (0..^𝑁) → (𝑥 − 𝑁) ∈ (0..^𝑀))))) |
42 | 29, 41 | syl5ibr 249 |
. . . . . . 7
⊢
(((♯‘(𝑆
repeatS 𝑁)) = 𝑁 ∧ (♯‘(𝑆 repeatS 𝑀)) = 𝑀) → ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
→ (𝑥 ∈
(0..^((♯‘(𝑆
repeatS 𝑁)) +
(♯‘(𝑆 repeatS
𝑀)))) → (¬ 𝑥 ∈
(0..^(♯‘(𝑆
repeatS 𝑁))) → (𝑥 − (♯‘(𝑆 repeatS 𝑁))) ∈ (0..^𝑀))))) |
43 | 19, 42 | mpcom 38 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
→ (𝑥 ∈
(0..^((♯‘(𝑆
repeatS 𝑁)) +
(♯‘(𝑆 repeatS
𝑀)))) → (¬ 𝑥 ∈
(0..^(♯‘(𝑆
repeatS 𝑁))) → (𝑥 − (♯‘(𝑆 repeatS 𝑁))) ∈ (0..^𝑀)))) |
44 | 43 | imp31 421 |
. . . . 5
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
(0..^((♯‘(𝑆
repeatS 𝑁)) +
(♯‘(𝑆 repeatS
𝑀))))) ∧ ¬ 𝑥 ∈
(0..^(♯‘(𝑆
repeatS 𝑁)))) → (𝑥 − (♯‘(𝑆 repeatS 𝑁))) ∈ (0..^𝑀)) |
45 | | repswsymb 14339 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑀 ∈ ℕ0 ∧ (𝑥 − (♯‘(𝑆 repeatS 𝑁))) ∈ (0..^𝑀)) → ((𝑆 repeatS 𝑀)‘(𝑥 − (♯‘(𝑆 repeatS 𝑁)))) = 𝑆) |
46 | 17, 18, 44, 45 | syl3anc 1373 |
. . . 4
⊢ ((((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
(0..^((♯‘(𝑆
repeatS 𝑁)) +
(♯‘(𝑆 repeatS
𝑀))))) ∧ ¬ 𝑥 ∈
(0..^(♯‘(𝑆
repeatS 𝑁)))) →
((𝑆 repeatS 𝑀)‘(𝑥 − (♯‘(𝑆 repeatS 𝑁)))) = 𝑆) |
47 | 16, 46 | ifeqda 4475 |
. . 3
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈
(0..^((♯‘(𝑆
repeatS 𝑁)) +
(♯‘(𝑆 repeatS
𝑀))))) → if(𝑥 ∈
(0..^(♯‘(𝑆
repeatS 𝑁))), ((𝑆 repeatS 𝑁)‘𝑥), ((𝑆 repeatS 𝑀)‘(𝑥 − (♯‘(𝑆 repeatS 𝑁))))) = 𝑆) |
48 | 6, 47 | mpteq12dva 5139 |
. 2
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
→ (𝑥 ∈
(0..^((♯‘(𝑆
repeatS 𝑁)) +
(♯‘(𝑆 repeatS
𝑀)))) ↦ if(𝑥 ∈
(0..^(♯‘(𝑆
repeatS 𝑁))), ((𝑆 repeatS 𝑁)‘𝑥), ((𝑆 repeatS 𝑀)‘(𝑥 − (♯‘(𝑆 repeatS 𝑁)))))) = (𝑥 ∈ (0..^(𝑁 + 𝑀)) ↦ 𝑆)) |
49 | | ovex 7246 |
. . . 4
⊢ (𝑆 repeatS 𝑁) ∈ V |
50 | | ovex 7246 |
. . . 4
⊢ (𝑆 repeatS 𝑀) ∈ V |
51 | 49, 50 | pm3.2i 474 |
. . 3
⊢ ((𝑆 repeatS 𝑁) ∈ V ∧ (𝑆 repeatS 𝑀) ∈ V) |
52 | | ccatfval 14128 |
. . 3
⊢ (((𝑆 repeatS 𝑁) ∈ V ∧ (𝑆 repeatS 𝑀) ∈ V) → ((𝑆 repeatS 𝑁) ++ (𝑆 repeatS 𝑀)) = (𝑥 ∈ (0..^((♯‘(𝑆 repeatS 𝑁)) + (♯‘(𝑆 repeatS 𝑀)))) ↦ if(𝑥 ∈ (0..^(♯‘(𝑆 repeatS 𝑁))), ((𝑆 repeatS 𝑁)‘𝑥), ((𝑆 repeatS 𝑀)‘(𝑥 − (♯‘(𝑆 repeatS 𝑁))))))) |
53 | 51, 52 | mp1i 13 |
. 2
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
→ ((𝑆 repeatS 𝑁) ++ (𝑆 repeatS 𝑀)) = (𝑥 ∈ (0..^((♯‘(𝑆 repeatS 𝑁)) + (♯‘(𝑆 repeatS 𝑀)))) ↦ if(𝑥 ∈ (0..^(♯‘(𝑆 repeatS 𝑁))), ((𝑆 repeatS 𝑁)‘𝑥), ((𝑆 repeatS 𝑀)‘(𝑥 − (♯‘(𝑆 repeatS 𝑁))))))) |
54 | | nn0addcl 12125 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (𝑁 + 𝑀) ∈
ℕ0) |
55 | 54 | 3adant1 1132 |
. . 3
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
→ (𝑁 + 𝑀) ∈
ℕ0) |
56 | | reps 14335 |
. . 3
⊢ ((𝑆 ∈ 𝑉 ∧ (𝑁 + 𝑀) ∈ ℕ0) → (𝑆 repeatS (𝑁 + 𝑀)) = (𝑥 ∈ (0..^(𝑁 + 𝑀)) ↦ 𝑆)) |
57 | 7, 55, 56 | syl2anc 587 |
. 2
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
→ (𝑆 repeatS (𝑁 + 𝑀)) = (𝑥 ∈ (0..^(𝑁 + 𝑀)) ↦ 𝑆)) |
58 | 48, 53, 57 | 3eqtr4d 2787 |
1
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0)
→ ((𝑆 repeatS 𝑁) ++ (𝑆 repeatS 𝑀)) = (𝑆 repeatS (𝑁 + 𝑀))) |