Step | Hyp | Ref
| Expression |
1 | | repswlen 14487 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
(♯‘(𝑆 repeatS
𝑁)) = 𝑁) |
2 | 1 | oveq2d 7287 |
. . . 4
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
(0..^(♯‘(𝑆
repeatS 𝑁))) = (0..^𝑁)) |
3 | 2 | mpteq1d 5174 |
. . 3
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑥 ∈
(0..^(♯‘(𝑆
repeatS 𝑁))) ↦
((𝑆 repeatS 𝑁)‘(((♯‘(𝑆 repeatS 𝑁)) − 1) − 𝑥))) = (𝑥 ∈ (0..^𝑁) ↦ ((𝑆 repeatS 𝑁)‘(((♯‘(𝑆 repeatS 𝑁)) − 1) − 𝑥)))) |
4 | | simpll 764 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (0..^𝑁)) → 𝑆 ∈ 𝑉) |
5 | | simplr 766 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (0..^𝑁)) → 𝑁 ∈
ℕ0) |
6 | 1 | adantr 481 |
. . . . . . . 8
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (0..^𝑁)) → (♯‘(𝑆 repeatS 𝑁)) = 𝑁) |
7 | 6 | oveq1d 7286 |
. . . . . . 7
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (0..^𝑁)) → ((♯‘(𝑆 repeatS 𝑁)) − 1) = (𝑁 − 1)) |
8 | 7 | oveq1d 7286 |
. . . . . 6
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (0..^𝑁)) → (((♯‘(𝑆 repeatS 𝑁)) − 1) − 𝑥) = ((𝑁 − 1) − 𝑥)) |
9 | | ubmelm1fzo 13481 |
. . . . . . . 8
⊢ (𝑥 ∈ (0..^𝑁) → ((𝑁 − 𝑥) − 1) ∈ (0..^𝑁)) |
10 | | elfzoelz 13386 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0..^𝑁) → 𝑥 ∈ ℤ) |
11 | | nn0cn 12243 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
12 | 11 | ad2antll 726 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 𝑁 ∈
ℂ) |
13 | | zcn 12324 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℂ) |
14 | 13 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 𝑥 ∈
ℂ) |
15 | | 1cnd 10971 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 1
∈ ℂ) |
16 | 12, 14, 15 | sub32d 11364 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((𝑁 − 𝑥) − 1) = ((𝑁 − 1) − 𝑥)) |
17 | 16 | eleq1d 2825 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) →
(((𝑁 − 𝑥) − 1) ∈ (0..^𝑁) ↔ ((𝑁 − 1) − 𝑥) ∈ (0..^𝑁))) |
18 | 17 | biimpd 228 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) →
(((𝑁 − 𝑥) − 1) ∈ (0..^𝑁) → ((𝑁 − 1) − 𝑥) ∈ (0..^𝑁))) |
19 | 18 | ex 413 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℤ → ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (((𝑁 − 𝑥) − 1) ∈ (0..^𝑁) → ((𝑁 − 1) − 𝑥) ∈ (0..^𝑁)))) |
20 | 10, 19 | syl 17 |
. . . . . . . 8
⊢ (𝑥 ∈ (0..^𝑁) → ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (((𝑁 − 𝑥) − 1) ∈ (0..^𝑁) → ((𝑁 − 1) − 𝑥) ∈ (0..^𝑁)))) |
21 | 9, 20 | mpid 44 |
. . . . . . 7
⊢ (𝑥 ∈ (0..^𝑁) → ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ((𝑁 − 1) − 𝑥) ∈ (0..^𝑁))) |
22 | 21 | impcom 408 |
. . . . . 6
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (0..^𝑁)) → ((𝑁 − 1) − 𝑥) ∈ (0..^𝑁)) |
23 | 8, 22 | eqeltrd 2841 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (0..^𝑁)) → (((♯‘(𝑆 repeatS 𝑁)) − 1) − 𝑥) ∈ (0..^𝑁)) |
24 | | repswsymb 14485 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧
(((♯‘(𝑆 repeatS
𝑁)) − 1) −
𝑥) ∈ (0..^𝑁)) → ((𝑆 repeatS 𝑁)‘(((♯‘(𝑆 repeatS 𝑁)) − 1) − 𝑥)) = 𝑆) |
25 | 4, 5, 23, 24 | syl3anc 1370 |
. . . 4
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (0..^𝑁)) → ((𝑆 repeatS 𝑁)‘(((♯‘(𝑆 repeatS 𝑁)) − 1) − 𝑥)) = 𝑆) |
26 | 25 | mpteq2dva 5179 |
. . 3
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑥 ∈ (0..^𝑁) ↦ ((𝑆 repeatS 𝑁)‘(((♯‘(𝑆 repeatS 𝑁)) − 1) − 𝑥))) = (𝑥 ∈ (0..^𝑁) ↦ 𝑆)) |
27 | 3, 26 | eqtrd 2780 |
. 2
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑥 ∈
(0..^(♯‘(𝑆
repeatS 𝑁))) ↦
((𝑆 repeatS 𝑁)‘(((♯‘(𝑆 repeatS 𝑁)) − 1) − 𝑥))) = (𝑥 ∈ (0..^𝑁) ↦ 𝑆)) |
28 | | ovex 7304 |
. . 3
⊢ (𝑆 repeatS 𝑁) ∈ V |
29 | | revval 14471 |
. . 3
⊢ ((𝑆 repeatS 𝑁) ∈ V → (reverse‘(𝑆 repeatS 𝑁)) = (𝑥 ∈ (0..^(♯‘(𝑆 repeatS 𝑁))) ↦ ((𝑆 repeatS 𝑁)‘(((♯‘(𝑆 repeatS 𝑁)) − 1) − 𝑥)))) |
30 | 28, 29 | mp1i 13 |
. 2
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
(reverse‘(𝑆 repeatS
𝑁)) = (𝑥 ∈ (0..^(♯‘(𝑆 repeatS 𝑁))) ↦ ((𝑆 repeatS 𝑁)‘(((♯‘(𝑆 repeatS 𝑁)) − 1) − 𝑥)))) |
31 | | reps 14481 |
. 2
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑆 repeatS 𝑁) = (𝑥 ∈ (0..^𝑁) ↦ 𝑆)) |
32 | 27, 30, 31 | 3eqtr4d 2790 |
1
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
(reverse‘(𝑆 repeatS
𝑁)) = (𝑆 repeatS 𝑁)) |