Step | Hyp | Ref
| Expression |
1 | | repswlen 14725 |
. . . . 5
β’ ((π β π β§ π β β0) β
(β―β(π repeatS
π)) = π) |
2 | 1 | oveq2d 7424 |
. . . 4
β’ ((π β π β§ π β β0) β
(0..^(β―β(π
repeatS π))) = (0..^π)) |
3 | 2 | mpteq1d 5243 |
. . 3
β’ ((π β π β§ π β β0) β (π₯ β
(0..^(β―β(π
repeatS π))) β¦
((π repeatS π)β(((β―β(π repeatS π)) β 1) β π₯))) = (π₯ β (0..^π) β¦ ((π repeatS π)β(((β―β(π repeatS π)) β 1) β π₯)))) |
4 | | simpll 765 |
. . . . 5
β’ (((π β π β§ π β β0) β§ π₯ β (0..^π)) β π β π) |
5 | | simplr 767 |
. . . . 5
β’ (((π β π β§ π β β0) β§ π₯ β (0..^π)) β π β
β0) |
6 | 1 | adantr 481 |
. . . . . . . 8
β’ (((π β π β§ π β β0) β§ π₯ β (0..^π)) β (β―β(π repeatS π)) = π) |
7 | 6 | oveq1d 7423 |
. . . . . . 7
β’ (((π β π β§ π β β0) β§ π₯ β (0..^π)) β ((β―β(π repeatS π)) β 1) = (π β 1)) |
8 | 7 | oveq1d 7423 |
. . . . . 6
β’ (((π β π β§ π β β0) β§ π₯ β (0..^π)) β (((β―β(π repeatS π)) β 1) β π₯) = ((π β 1) β π₯)) |
9 | | ubmelm1fzo 13727 |
. . . . . . . 8
β’ (π₯ β (0..^π) β ((π β π₯) β 1) β (0..^π)) |
10 | | elfzoelz 13631 |
. . . . . . . . 9
β’ (π₯ β (0..^π) β π₯ β β€) |
11 | | nn0cn 12481 |
. . . . . . . . . . . . . 14
β’ (π β β0
β π β
β) |
12 | 11 | ad2antll 727 |
. . . . . . . . . . . . 13
β’ ((π₯ β β€ β§ (π β π β§ π β β0)) β π β
β) |
13 | | zcn 12562 |
. . . . . . . . . . . . . 14
β’ (π₯ β β€ β π₯ β
β) |
14 | 13 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((π₯ β β€ β§ (π β π β§ π β β0)) β π₯ β
β) |
15 | | 1cnd 11208 |
. . . . . . . . . . . . 13
β’ ((π₯ β β€ β§ (π β π β§ π β β0)) β 1
β β) |
16 | 12, 14, 15 | sub32d 11602 |
. . . . . . . . . . . 12
β’ ((π₯ β β€ β§ (π β π β§ π β β0)) β ((π β π₯) β 1) = ((π β 1) β π₯)) |
17 | 16 | eleq1d 2818 |
. . . . . . . . . . 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 2833 |
. . . . 5
β’ (((π β π β§ π β β0) β§ π₯ β (0..^π)) β (((β―β(π repeatS π)) β 1) β π₯) β (0..^π)) |
24 | | repswsymb 14723 |
. . . . 5
β’ ((π β π β§ π β β0 β§
(((β―β(π repeatS
π)) β 1) β
π₯) β (0..^π)) β ((π repeatS π)β(((β―β(π repeatS π)) β 1) β π₯)) = π) |
25 | 4, 5, 23, 24 | syl3anc 1371 |
. . . 4
β’ (((π β π β§ π β β0) β§ π₯ β (0..^π)) β ((π repeatS π)β(((β―β(π repeatS π)) β 1) β π₯)) = π) |
26 | 25 | mpteq2dva 5248 |
. . 3
β’ ((π β π β§ π β β0) β (π₯ β (0..^π) β¦ ((π repeatS π)β(((β―β(π repeatS π)) β 1) β π₯))) = (π₯ β (0..^π) β¦ π)) |
27 | 3, 26 | eqtrd 2772 |
. 2
β’ ((π β π β§ π β β0) β (π₯ β
(0..^(β―β(π
repeatS π))) β¦
((π repeatS π)β(((β―β(π repeatS π)) β 1) β π₯))) = (π₯ β (0..^π) β¦ π)) |
28 | | ovex 7441 |
. . 3
β’ (π repeatS π) β V |
29 | | revval 14709 |
. . 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 14719 |
. 2
β’ ((π β π β§ π β β0) β (π repeatS π) = (π₯ β (0..^π) β¦ π)) |
32 | 27, 30, 31 | 3eqtr4d 2782 |
1
β’ ((π β π β§ π β β0) β
(reverseβ(π repeatS
π)) = (π repeatS π)) |