Step | Hyp | Ref
| Expression |
1 | | vtsval.n |
. . 3
β’ (π β π β
β0) |
2 | | vtsprod.s |
. . 3
β’ (π β π β
β0) |
3 | | ax-icn 11169 |
. . . . . . 7
β’ i β
β |
4 | 3 | a1i 11 |
. . . . . 6
β’ (π β i β
β) |
5 | | 2cnd 12290 |
. . . . . . 7
β’ (π β 2 β
β) |
6 | | picn 25969 |
. . . . . . . 8
β’ Ο
β β |
7 | 6 | a1i 11 |
. . . . . . 7
β’ (π β Ο β
β) |
8 | 5, 7 | mulcld 11234 |
. . . . . 6
β’ (π β (2 Β· Ο) β
β) |
9 | 4, 8 | mulcld 11234 |
. . . . 5
β’ (π β (i Β· (2 Β·
Ο)) β β) |
10 | | vtsval.x |
. . . . 5
β’ (π β π β β) |
11 | 9, 10 | mulcld 11234 |
. . . 4
β’ (π β ((i Β· (2 Β·
Ο)) Β· π) β
β) |
12 | 11 | efcld 33603 |
. . 3
β’ (π β (expβ((i Β· (2
Β· Ο)) Β· π)) β β) |
13 | | vtsprod.l |
. . 3
β’ (π β πΏ:(0..^π)βΆ(β βm
β)) |
14 | 1, 2, 12, 13 | breprexp 33645 |
. 2
β’ (π β βπ β (0..^π)Ξ£π β (1...π)(((πΏβπ)βπ) Β· ((expβ((i Β· (2
Β· Ο)) Β· π))βπ)) = Ξ£π β (0...(π Β· π))Ξ£π β ((1...π)(reprβπ)π)(βπ β (0..^π)((πΏβπ)β(πβπ)) Β· ((expβ((i Β· (2
Β· Ο)) Β· π))βπ))) |
15 | 1 | adantr 482 |
. . . . 5
β’ ((π β§ π β (0..^π)) β π β
β0) |
16 | 10 | adantr 482 |
. . . . 5
β’ ((π β§ π β (0..^π)) β π β β) |
17 | 13 | ffvelcdmda 7087 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β (πΏβπ) β (β βm
β)) |
18 | | elmapi 8843 |
. . . . . 6
β’ ((πΏβπ) β (β βm β)
β (πΏβπ):ββΆβ) |
19 | 17, 18 | syl 17 |
. . . . 5
β’ ((π β§ π β (0..^π)) β (πΏβπ):ββΆβ) |
20 | 15, 16, 19 | vtsval 33649 |
. . . 4
β’ ((π β§ π β (0..^π)) β (((πΏβπ)vtsπ)βπ) = Ξ£π β (1...π)(((πΏβπ)βπ) Β· (expβ((i Β· (2
Β· Ο)) Β· (π
Β· π))))) |
21 | | fzssz 13503 |
. . . . . . . . . . 11
β’
(1...π) β
β€ |
22 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β§ π β (0..^π)) β§ π β (1...π)) β π β (1...π)) |
23 | 21, 22 | sselid 3981 |
. . . . . . . . . 10
β’ (((π β§ π β (0..^π)) β§ π β (1...π)) β π β β€) |
24 | 23 | zcnd 12667 |
. . . . . . . . 9
β’ (((π β§ π β (0..^π)) β§ π β (1...π)) β π β β) |
25 | 9 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π β (0..^π)) β§ π β (1...π)) β (i Β· (2 Β· Ο))
β β) |
26 | 16 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π β (0..^π)) β§ π β (1...π)) β π β β) |
27 | 24, 25, 26 | mul12d 11423 |
. . . . . . . 8
β’ (((π β§ π β (0..^π)) β§ π β (1...π)) β (π Β· ((i Β· (2 Β· Ο))
Β· π)) = ((i Β·
(2 Β· Ο)) Β· (π Β· π))) |
28 | 27 | fveq2d 6896 |
. . . . . . 7
β’ (((π β§ π β (0..^π)) β§ π β (1...π)) β (expβ(π Β· ((i Β· (2 Β· Ο))
Β· π))) =
(expβ((i Β· (2 Β· Ο)) Β· (π Β· π)))) |
29 | 11 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β (0..^π)) β§ π β (1...π)) β ((i Β· (2 Β· Ο))
Β· π) β
β) |
30 | | efexp 16044 |
. . . . . . . 8
β’ ((((i
Β· (2 Β· Ο)) Β· π) β β β§ π β β€) β (expβ(π Β· ((i Β· (2
Β· Ο)) Β· π))) = ((expβ((i Β· (2 Β·
Ο)) Β· π))βπ)) |
31 | 29, 23, 30 | syl2anc 585 |
. . . . . . 7
β’ (((π β§ π β (0..^π)) β§ π β (1...π)) β (expβ(π Β· ((i Β· (2 Β· Ο))
Β· π))) =
((expβ((i Β· (2 Β· Ο)) Β· π))βπ)) |
32 | 28, 31 | eqtr3d 2775 |
. . . . . 6
β’ (((π β§ π β (0..^π)) β§ π β (1...π)) β (expβ((i Β· (2
Β· Ο)) Β· (π
Β· π))) =
((expβ((i Β· (2 Β· Ο)) Β· π))βπ)) |
33 | 32 | oveq2d 7425 |
. . . . 5
β’ (((π β§ π β (0..^π)) β§ π β (1...π)) β (((πΏβπ)βπ) Β· (expβ((i Β· (2
Β· Ο)) Β· (π
Β· π)))) = (((πΏβπ)βπ) Β· ((expβ((i Β· (2
Β· Ο)) Β· π))βπ))) |
34 | 33 | sumeq2dv 15649 |
. . . 4
β’ ((π β§ π β (0..^π)) β Ξ£π β (1...π)(((πΏβπ)βπ) Β· (expβ((i Β· (2
Β· Ο)) Β· (π
Β· π)))) =
Ξ£π β (1...π)(((πΏβπ)βπ) Β· ((expβ((i Β· (2
Β· Ο)) Β· π))βπ))) |
35 | 20, 34 | eqtrd 2773 |
. . 3
β’ ((π β§ π β (0..^π)) β (((πΏβπ)vtsπ)βπ) = Ξ£π β (1...π)(((πΏβπ)βπ) Β· ((expβ((i Β· (2
Β· Ο)) Β· π))βπ))) |
36 | 35 | prodeq2dv 15867 |
. 2
β’ (π β βπ β (0..^π)(((πΏβπ)vtsπ)βπ) = βπ β (0..^π)Ξ£π β (1...π)(((πΏβπ)βπ) Β· ((expβ((i Β· (2
Β· Ο)) Β· π))βπ))) |
37 | | fzssz 13503 |
. . . . . . . . . . 11
β’
(0...(π Β·
π)) β
β€ |
38 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β§ π β (0...(π Β· π))) β π β (0...(π Β· π))) |
39 | 37, 38 | sselid 3981 |
. . . . . . . . . 10
β’ ((π β§ π β (0...(π Β· π))) β π β β€) |
40 | 39 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π β (0...(π Β· π))) β§ π β ((1...π)(reprβπ)π)) β π β β€) |
41 | 40 | zcnd 12667 |
. . . . . . . 8
β’ (((π β§ π β (0...(π Β· π))) β§ π β ((1...π)(reprβπ)π)) β π β β) |
42 | 9 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β (0...(π Β· π))) β§ π β ((1...π)(reprβπ)π)) β (i Β· (2 Β· Ο))
β β) |
43 | 10 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β (0...(π Β· π))) β§ π β ((1...π)(reprβπ)π)) β π β β) |
44 | 41, 42, 43 | mul12d 11423 |
. . . . . . 7
β’ (((π β§ π β (0...(π Β· π))) β§ π β ((1...π)(reprβπ)π)) β (π Β· ((i Β· (2 Β· Ο))
Β· π)) = ((i Β·
(2 Β· Ο)) Β· (π Β· π))) |
45 | 44 | fveq2d 6896 |
. . . . . 6
β’ (((π β§ π β (0...(π Β· π))) β§ π β ((1...π)(reprβπ)π)) β (expβ(π Β· ((i Β· (2 Β· Ο))
Β· π))) =
(expβ((i Β· (2 Β· Ο)) Β· (π Β· π)))) |
46 | 11 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π β (0...(π Β· π))) β§ π β ((1...π)(reprβπ)π)) β ((i Β· (2 Β· Ο))
Β· π) β
β) |
47 | | efexp 16044 |
. . . . . . 7
β’ ((((i
Β· (2 Β· Ο)) Β· π) β β β§ π β β€) β (expβ(π Β· ((i Β· (2
Β· Ο)) Β· π))) = ((expβ((i Β· (2 Β·
Ο)) Β· π))βπ)) |
48 | 46, 40, 47 | syl2anc 585 |
. . . . . 6
β’ (((π β§ π β (0...(π Β· π))) β§ π β ((1...π)(reprβπ)π)) β (expβ(π Β· ((i Β· (2 Β· Ο))
Β· π))) =
((expβ((i Β· (2 Β· Ο)) Β· π))βπ)) |
49 | 45, 48 | eqtr3d 2775 |
. . . . 5
β’ (((π β§ π β (0...(π Β· π))) β§ π β ((1...π)(reprβπ)π)) β (expβ((i Β· (2 Β·
Ο)) Β· (π Β·
π))) = ((expβ((i
Β· (2 Β· Ο)) Β· π))βπ)) |
50 | 49 | oveq2d 7425 |
. . . 4
β’ (((π β§ π β (0...(π Β· π))) β§ π β ((1...π)(reprβπ)π)) β (βπ β (0..^π)((πΏβπ)β(πβπ)) Β· (expβ((i Β· (2
Β· Ο)) Β· (π
Β· π)))) =
(βπ β (0..^π)((πΏβπ)β(πβπ)) Β· ((expβ((i Β· (2
Β· Ο)) Β· π))βπ))) |
51 | 50 | sumeq2dv 15649 |
. . 3
β’ ((π β§ π β (0...(π Β· π))) β Ξ£π β ((1...π)(reprβπ)π)(βπ β (0..^π)((πΏβπ)β(πβπ)) Β· (expβ((i Β· (2
Β· Ο)) Β· (π
Β· π)))) =
Ξ£π β ((1...π)(reprβπ)π)(βπ β (0..^π)((πΏβπ)β(πβπ)) Β· ((expβ((i Β· (2
Β· Ο)) Β· π))βπ))) |
52 | 51 | sumeq2dv 15649 |
. 2
β’ (π β Ξ£π β (0...(π Β· π))Ξ£π β ((1...π)(reprβπ)π)(βπ β (0..^π)((πΏβπ)β(πβπ)) Β· (expβ((i Β· (2
Β· Ο)) Β· (π
Β· π)))) =
Ξ£π β (0...(π Β· π))Ξ£π β ((1...π)(reprβπ)π)(βπ β (0..^π)((πΏβπ)β(πβπ)) Β· ((expβ((i Β· (2
Β· Ο)) Β· π))βπ))) |
53 | 14, 36, 52 | 3eqtr4d 2783 |
1
β’ (π β βπ β (0..^π)(((πΏβπ)vtsπ)βπ) = Ξ£π β (0...(π Β· π))Ξ£π β ((1...π)(reprβπ)π)(βπ β (0..^π)((πΏβπ)β(πβπ)) Β· (expβ((i Β· (2
Β· Ο)) Β· (π
Β· π))))) |