Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  circlemeth Structured version   Visualization version   GIF version

Theorem circlemeth 34328
Description: The Hardy, Littlewood and Ramanujan Circle Method, in a generic form, with different weighting / smoothing functions. (Contributed by Thierry Arnoux, 13-Dec-2021.)
Hypotheses
Ref Expression
circlemeth.n (πœ‘ β†’ 𝑁 ∈ β„•0)
circlemeth.s (πœ‘ β†’ 𝑆 ∈ β„•)
circlemeth.l (πœ‘ β†’ 𝐿:(0..^𝑆)⟢(β„‚ ↑m β„•))
Assertion
Ref Expression
circlemeth (πœ‘ β†’ Σ𝑐 ∈ (β„•(reprβ€˜π‘†)𝑁)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) = ∫(0(,)1)(βˆπ‘Ž ∈ (0..^𝑆)(((πΏβ€˜π‘Ž)vts𝑁)β€˜π‘₯) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)))) dπ‘₯)
Distinct variable groups:   𝐿,π‘Ž,𝑐,π‘₯   𝑁,π‘Ž,𝑐,π‘₯   𝑆,π‘Ž,𝑐,π‘₯   πœ‘,π‘Ž,𝑐,π‘₯

Proof of Theorem circlemeth
Dummy variable π‘š is distinct from all other variables.
StepHypRef Expression
1 circlemeth.n . . . . . . 7 (πœ‘ β†’ 𝑁 ∈ β„•0)
21adantr 479 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (0(,)1)) β†’ 𝑁 ∈ β„•0)
3 ioossre 13415 . . . . . . . . 9 (0(,)1) βŠ† ℝ
4 ax-resscn 11193 . . . . . . . . 9 ℝ βŠ† β„‚
53, 4sstri 3982 . . . . . . . 8 (0(,)1) βŠ† β„‚
65a1i 11 . . . . . . 7 (πœ‘ β†’ (0(,)1) βŠ† β„‚)
76sselda 3972 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (0(,)1)) β†’ π‘₯ ∈ β„‚)
8 circlemeth.s . . . . . . . 8 (πœ‘ β†’ 𝑆 ∈ β„•)
98nnnn0d 12560 . . . . . . 7 (πœ‘ β†’ 𝑆 ∈ β„•0)
109adantr 479 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (0(,)1)) β†’ 𝑆 ∈ β„•0)
11 circlemeth.l . . . . . . 7 (πœ‘ β†’ 𝐿:(0..^𝑆)⟢(β„‚ ↑m β„•))
1211adantr 479 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (0(,)1)) β†’ 𝐿:(0..^𝑆)⟢(β„‚ ↑m β„•))
132, 7, 10, 12vtsprod 34327 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ (0(,)1)) β†’ βˆπ‘Ž ∈ (0..^𝑆)(((πΏβ€˜π‘Ž)vts𝑁)β€˜π‘₯) = Ξ£π‘š ∈ (0...(𝑆 Β· 𝑁))Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯)))))
1413oveq1d 7430 . . . 4 ((πœ‘ ∧ π‘₯ ∈ (0(,)1)) β†’ (βˆπ‘Ž ∈ (0..^𝑆)(((πΏβ€˜π‘Ž)vts𝑁)β€˜π‘₯) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)))) = (Ξ£π‘š ∈ (0...(𝑆 Β· 𝑁))Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯)))) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)))))
15 fzfid 13968 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ (0(,)1)) β†’ (0...(𝑆 Β· 𝑁)) ∈ Fin)
16 ax-icn 11195 . . . . . . . . 9 i ∈ β„‚
17 2cn 12315 . . . . . . . . . 10 2 ∈ β„‚
18 picn 26410 . . . . . . . . . 10 Ο€ ∈ β„‚
1917, 18mulcli 11249 . . . . . . . . 9 (2 Β· Ο€) ∈ β„‚
2016, 19mulcli 11249 . . . . . . . 8 (i Β· (2 Β· Ο€)) ∈ β„‚
2120a1i 11 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (0(,)1)) β†’ (i Β· (2 Β· Ο€)) ∈ β„‚)
221nn0cnd 12562 . . . . . . . . . . 11 (πœ‘ β†’ 𝑁 ∈ β„‚)
2322negcld 11586 . . . . . . . . . 10 (πœ‘ β†’ -𝑁 ∈ β„‚)
2423ralrimivw 3140 . . . . . . . . 9 (πœ‘ β†’ βˆ€π‘₯ ∈ (0(,)1)-𝑁 ∈ β„‚)
2524r19.21bi 3239 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (0(,)1)) β†’ -𝑁 ∈ β„‚)
2625, 7mulcld 11262 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (0(,)1)) β†’ (-𝑁 Β· π‘₯) ∈ β„‚)
2721, 26mulcld 11262 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (0(,)1)) β†’ ((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)) ∈ β„‚)
2827efcld 16057 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ (0(,)1)) β†’ (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯))) ∈ β„‚)
29 fz1ssnn 13562 . . . . . . . 8 (1...𝑁) βŠ† β„•
3029a1i 11 . . . . . . 7 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (1...𝑁) βŠ† β„•)
31 simpr 483 . . . . . . . . 9 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ π‘š ∈ (0...(𝑆 Β· 𝑁)))
3231elfzelzd 13532 . . . . . . . 8 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ π‘š ∈ β„€)
3332adantlr 713 . . . . . . 7 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ π‘š ∈ β„€)
3410adantr 479 . . . . . . 7 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ 𝑆 ∈ β„•0)
35 fzfid 13968 . . . . . . 7 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (1...𝑁) ∈ Fin)
3630, 33, 34, 35reprfi 34304 . . . . . 6 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ ((1...𝑁)(reprβ€˜π‘†)π‘š) ∈ Fin)
37 fzofi 13969 . . . . . . . . 9 (0..^𝑆) ∈ Fin
3837a1i 11 . . . . . . . 8 ((((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ (0..^𝑆) ∈ Fin)
391ad3antrrr 728 . . . . . . . . . 10 ((((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ 𝑁 ∈ β„•0)
409ad3antrrr 728 . . . . . . . . . 10 ((((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ 𝑆 ∈ β„•0)
4132zcnd 12695 . . . . . . . . . . 11 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ π‘š ∈ β„‚)
4241ad2antrr 724 . . . . . . . . . 10 ((((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ π‘š ∈ β„‚)
4311ad3antrrr 728 . . . . . . . . . 10 ((((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ 𝐿:(0..^𝑆)⟢(β„‚ ↑m β„•))
44 simpr 483 . . . . . . . . . 10 ((((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ π‘Ž ∈ (0..^𝑆))
4529a1i 11 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ (1...𝑁) βŠ† β„•)
4632adantr 479 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ π‘š ∈ β„€)
479ad2antrr 724 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ 𝑆 ∈ β„•0)
48 simpr 483 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š))
4945, 46, 47, 48reprf 34300 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ 𝑐:(0..^𝑆)⟢(1...𝑁))
5049ffvelcdmda 7088 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ (π‘β€˜π‘Ž) ∈ (1...𝑁))
5129, 50sselid 3970 . . . . . . . . . 10 ((((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ (π‘β€˜π‘Ž) ∈ β„•)
5239, 40, 42, 43, 44, 51breprexplemb 34319 . . . . . . . . 9 ((((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ ((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) ∈ β„‚)
5352adantl3r 748 . . . . . . . 8 (((((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ ((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) ∈ β„‚)
5438, 53fprodcl 15926 . . . . . . 7 ((((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) ∈ β„‚)
5520a1i 11 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (i Β· (2 Β· Ο€)) ∈ β„‚)
5633zcnd 12695 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ π‘š ∈ β„‚)
577adantr 479 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ π‘₯ ∈ β„‚)
5856, 57mulcld 11262 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (π‘š Β· π‘₯) ∈ β„‚)
5955, 58mulcld 11262 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ ((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯)) ∈ β„‚)
6059efcld 16057 . . . . . . . 8 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯))) ∈ β„‚)
6160adantr 479 . . . . . . 7 ((((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ (expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯))) ∈ β„‚)
6254, 61mulcld 11262 . . . . . 6 ((((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ (βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯)))) ∈ β„‚)
6336, 62fsumcl 15709 . . . . 5 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯)))) ∈ β„‚)
6415, 28, 63fsummulc1 15761 . . . 4 ((πœ‘ ∧ π‘₯ ∈ (0(,)1)) β†’ (Ξ£π‘š ∈ (0...(𝑆 Β· 𝑁))Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯)))) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)))) = Ξ£π‘š ∈ (0...(𝑆 Β· 𝑁))(Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯)))) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)))))
6528adantr 479 . . . . . . 7 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯))) ∈ β„‚)
6636, 65, 62fsummulc1 15761 . . . . . 6 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯)))) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)))) = Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)((βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯)))) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)))))
6765adantr 479 . . . . . . . . 9 ((((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯))) ∈ β„‚)
6854, 61, 67mulassd 11265 . . . . . . . 8 ((((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ ((βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯)))) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)))) = (βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· ((expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯))) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯))))))
6927adantr 479 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ ((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)) ∈ β„‚)
70 efadd 16068 . . . . . . . . . . . 12 ((((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯)) ∈ β„‚ ∧ ((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)) ∈ β„‚) β†’ (expβ€˜(((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯)) + ((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)))) = ((expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯))) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)))))
7159, 69, 70syl2anc 582 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (expβ€˜(((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯)) + ((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)))) = ((expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯))) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)))))
7226adantr 479 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (-𝑁 Β· π‘₯) ∈ β„‚)
7355, 58, 72adddid 11266 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ ((i Β· (2 Β· Ο€)) Β· ((π‘š Β· π‘₯) + (-𝑁 Β· π‘₯))) = (((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯)) + ((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯))))
7425adantr 479 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ -𝑁 ∈ β„‚)
7556, 74, 57adddird 11267 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ ((π‘š + -𝑁) Β· π‘₯) = ((π‘š Β· π‘₯) + (-𝑁 Β· π‘₯)))
7622ad2antrr 724 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ 𝑁 ∈ β„‚)
7756, 76negsubd 11605 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (π‘š + -𝑁) = (π‘š βˆ’ 𝑁))
7877oveq1d 7430 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ ((π‘š + -𝑁) Β· π‘₯) = ((π‘š βˆ’ 𝑁) Β· π‘₯))
7975, 78eqtr3d 2767 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ ((π‘š Β· π‘₯) + (-𝑁 Β· π‘₯)) = ((π‘š βˆ’ 𝑁) Β· π‘₯))
8079oveq2d 7431 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ ((i Β· (2 Β· Ο€)) Β· ((π‘š Β· π‘₯) + (-𝑁 Β· π‘₯))) = ((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))
8173, 80eqtr3d 2767 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯)) + ((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯))) = ((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))
8281fveq2d 6895 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (expβ€˜(((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯)) + ((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)))) = (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯))))
8371, 82eqtr3d 2767 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ ((expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯))) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)))) = (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯))))
8483oveq2d 7431 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· ((expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯))) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯))))) = (βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))))
8584adantr 479 . . . . . . . 8 ((((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ (βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· ((expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯))) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯))))) = (βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))))
8668, 85eqtrd 2765 . . . . . . 7 ((((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ ((βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯)))) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)))) = (βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))))
8786sumeq2dv 15679 . . . . . 6 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)((βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯)))) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)))) = Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))))
8866, 87eqtrd 2765 . . . . 5 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯)))) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)))) = Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))))
8988sumeq2dv 15679 . . . 4 ((πœ‘ ∧ π‘₯ ∈ (0(,)1)) β†’ Ξ£π‘š ∈ (0...(𝑆 Β· 𝑁))(Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯)))) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)))) = Ξ£π‘š ∈ (0...(𝑆 Β· 𝑁))Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))))
9014, 64, 893eqtrd 2769 . . 3 ((πœ‘ ∧ π‘₯ ∈ (0(,)1)) β†’ (βˆπ‘Ž ∈ (0..^𝑆)(((πΏβ€˜π‘Ž)vts𝑁)β€˜π‘₯) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)))) = Ξ£π‘š ∈ (0...(𝑆 Β· 𝑁))Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))))
9190itgeq2dv 25727 . 2 (πœ‘ β†’ ∫(0(,)1)(βˆπ‘Ž ∈ (0..^𝑆)(((πΏβ€˜π‘Ž)vts𝑁)β€˜π‘₯) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)))) dπ‘₯ = ∫(0(,)1)Ξ£π‘š ∈ (0...(𝑆 Β· 𝑁))Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))) dπ‘₯)
92 ioombl 25510 . . . . 5 (0(,)1) ∈ dom vol
9392a1i 11 . . . 4 (πœ‘ β†’ (0(,)1) ∈ dom vol)
94 fzfid 13968 . . . 4 (πœ‘ β†’ (0...(𝑆 Β· 𝑁)) ∈ Fin)
95 sumex 15664 . . . . 5 Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))) ∈ V
9695a1i 11 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ (0(,)1) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁)))) β†’ Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))) ∈ V)
9793adantr 479 . . . . . 6 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (0(,)1) ∈ dom vol)
9829a1i 11 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (1...𝑁) βŠ† β„•)
999adantr 479 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ 𝑆 ∈ β„•0)
100 fzfid 13968 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (1...𝑁) ∈ Fin)
10198, 32, 99, 100reprfi 34304 . . . . . 6 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ ((1...𝑁)(reprβ€˜π‘†)π‘š) ∈ Fin)
10237a1i 11 . . . . . . . . 9 ((((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ π‘₯ ∈ (0(,)1)) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ (0..^𝑆) ∈ Fin)
10352adantllr 717 . . . . . . . . 9 (((((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ π‘₯ ∈ (0(,)1)) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ ((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) ∈ β„‚)
104102, 103fprodcl 15926 . . . . . . . 8 ((((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ π‘₯ ∈ (0(,)1)) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) ∈ β„‚)
10556, 76subcld 11599 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (π‘š βˆ’ 𝑁) ∈ β„‚)
106105, 57mulcld 11262 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ ((π‘š βˆ’ 𝑁) Β· π‘₯) ∈ β„‚)
10755, 106mulcld 11262 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ ((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)) ∈ β„‚)
108107an32s 650 . . . . . . . . . 10 (((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ π‘₯ ∈ (0(,)1)) β†’ ((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)) ∈ β„‚)
109108adantr 479 . . . . . . . . 9 ((((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ π‘₯ ∈ (0(,)1)) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ ((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)) ∈ β„‚)
110109efcld 16057 . . . . . . . 8 ((((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ π‘₯ ∈ (0(,)1)) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯))) ∈ β„‚)
111104, 110mulcld 11262 . . . . . . 7 ((((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ π‘₯ ∈ (0(,)1)) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ (βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))) ∈ β„‚)
112111anasss 465 . . . . . 6 (((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ (π‘₯ ∈ (0(,)1) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š))) β†’ (βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))) ∈ β„‚)
11337a1i 11 . . . . . . . 8 (((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ (0..^𝑆) ∈ Fin)
114113, 52fprodcl 15926 . . . . . . 7 (((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) ∈ β„‚)
115 fvex 6904 . . . . . . . 8 (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯))) ∈ V
116115a1i 11 . . . . . . 7 ((((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) ∧ π‘₯ ∈ (0(,)1)) β†’ (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯))) ∈ V)
117 ioossicc 13440 . . . . . . . . . 10 (0(,)1) βŠ† (0[,]1)
118117a1i 11 . . . . . . . . 9 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (0(,)1) βŠ† (0[,]1))
11992a1i 11 . . . . . . . . 9 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (0(,)1) ∈ dom vol)
120115a1i 11 . . . . . . . . 9 (((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ π‘₯ ∈ (0[,]1)) β†’ (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯))) ∈ V)
121 0red 11245 . . . . . . . . . 10 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ 0 ∈ ℝ)
122 1red 11243 . . . . . . . . . 10 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ 1 ∈ ℝ)
12322adantr 479 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ 𝑁 ∈ β„‚)
12441, 123subcld 11599 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (π‘š βˆ’ 𝑁) ∈ β„‚)
125 unitsscn 13507 . . . . . . . . . . . . . 14 (0[,]1) βŠ† β„‚
126125a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (0[,]1) βŠ† β„‚)
127 ssidd 3996 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ β„‚ βŠ† β„‚)
128 cncfmptc 24848 . . . . . . . . . . . . 13 (((π‘š βˆ’ 𝑁) ∈ β„‚ ∧ (0[,]1) βŠ† β„‚ ∧ β„‚ βŠ† β„‚) β†’ (π‘₯ ∈ (0[,]1) ↦ (π‘š βˆ’ 𝑁)) ∈ ((0[,]1)–cnβ†’β„‚))
129124, 126, 127, 128syl3anc 1368 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (π‘₯ ∈ (0[,]1) ↦ (π‘š βˆ’ 𝑁)) ∈ ((0[,]1)–cnβ†’β„‚))
130 cncfmptid 24849 . . . . . . . . . . . . 13 (((0[,]1) βŠ† β„‚ ∧ β„‚ βŠ† β„‚) β†’ (π‘₯ ∈ (0[,]1) ↦ π‘₯) ∈ ((0[,]1)–cnβ†’β„‚))
131126, 127, 130syl2anc 582 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (π‘₯ ∈ (0[,]1) ↦ π‘₯) ∈ ((0[,]1)–cnβ†’β„‚))
132129, 131mulcncf 25390 . . . . . . . . . . 11 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (π‘₯ ∈ (0[,]1) ↦ ((π‘š βˆ’ 𝑁) Β· π‘₯)) ∈ ((0[,]1)–cnβ†’β„‚))
133132efmul2picn 34284 . . . . . . . . . 10 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (π‘₯ ∈ (0[,]1) ↦ (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))) ∈ ((0[,]1)–cnβ†’β„‚))
134 cniccibl 25786 . . . . . . . . . 10 ((0 ∈ ℝ ∧ 1 ∈ ℝ ∧ (π‘₯ ∈ (0[,]1) ↦ (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))) ∈ ((0[,]1)–cnβ†’β„‚)) β†’ (π‘₯ ∈ (0[,]1) ↦ (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))) ∈ 𝐿1)
135121, 122, 133, 134syl3anc 1368 . . . . . . . . 9 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (π‘₯ ∈ (0[,]1) ↦ (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))) ∈ 𝐿1)
136118, 119, 120, 135iblss 25750 . . . . . . . 8 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (π‘₯ ∈ (0(,)1) ↦ (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))) ∈ 𝐿1)
137136adantr 479 . . . . . . 7 (((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ (π‘₯ ∈ (0(,)1) ↦ (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))) ∈ 𝐿1)
138114, 116, 137iblmulc2 25776 . . . . . 6 (((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ (π‘₯ ∈ (0(,)1) ↦ (βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯))))) ∈ 𝐿1)
13997, 101, 112, 138itgfsum 25772 . . . . 5 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ ((π‘₯ ∈ (0(,)1) ↦ Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯))))) ∈ 𝐿1 ∧ ∫(0(,)1)Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))) dπ‘₯ = Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)∫(0(,)1)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))) dπ‘₯))
140139simpld 493 . . . 4 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (π‘₯ ∈ (0(,)1) ↦ Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯))))) ∈ 𝐿1)
14193, 94, 96, 140itgfsum 25772 . . 3 (πœ‘ β†’ ((π‘₯ ∈ (0(,)1) ↦ Ξ£π‘š ∈ (0...(𝑆 Β· 𝑁))Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯))))) ∈ 𝐿1 ∧ ∫(0(,)1)Ξ£π‘š ∈ (0...(𝑆 Β· 𝑁))Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))) dπ‘₯ = Ξ£π‘š ∈ (0...(𝑆 Β· 𝑁))∫(0(,)1)Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))) dπ‘₯))
142141simprd 494 . 2 (πœ‘ β†’ ∫(0(,)1)Ξ£π‘š ∈ (0...(𝑆 Β· 𝑁))Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))) dπ‘₯ = Ξ£π‘š ∈ (0...(𝑆 Β· 𝑁))∫(0(,)1)Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))) dπ‘₯)
143 oveq2 7423 . . . . . . 7 (if((π‘š βˆ’ 𝑁) = 0, 1, 0) = 1 β†’ (Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· if((π‘š βˆ’ 𝑁) = 0, 1, 0)) = (Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· 1))
144 oveq2 7423 . . . . . . 7 (if((π‘š βˆ’ 𝑁) = 0, 1, 0) = 0 β†’ (Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· if((π‘š βˆ’ 𝑁) = 0, 1, 0)) = (Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· 0))
145101, 114fsumcl 15709 . . . . . . . 8 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) ∈ β„‚)
146145mulridd 11259 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· 1) = Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)))
147145mul01d 11441 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· 0) = 0)
148143, 144, 146, 147ifeq3da 32380 . . . . . 6 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ if((π‘š βˆ’ 𝑁) = 0, Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)), 0) = (Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· if((π‘š βˆ’ 𝑁) = 0, 1, 0)))
149 velsn 4640 . . . . . . . 8 (π‘š ∈ {𝑁} ↔ π‘š = 𝑁)
15041, 123subeq0ad 11609 . . . . . . . 8 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ ((π‘š βˆ’ 𝑁) = 0 ↔ π‘š = 𝑁))
151149, 150bitr4id 289 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (π‘š ∈ {𝑁} ↔ (π‘š βˆ’ 𝑁) = 0))
152151ifbid 4547 . . . . . 6 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ if(π‘š ∈ {𝑁}, Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)), 0) = if((π‘š βˆ’ 𝑁) = 0, Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)), 0))
1531nn0zd 12612 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑁 ∈ β„€)
154153ad2antrr 724 . . . . . . . . . . 11 (((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ 𝑁 ∈ β„€)
15546, 154zsubcld 12699 . . . . . . . . . 10 (((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ (π‘š βˆ’ 𝑁) ∈ β„€)
156 itgexpif 34294 . . . . . . . . . 10 ((π‘š βˆ’ 𝑁) ∈ β„€ β†’ ∫(0(,)1)(expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯))) dπ‘₯ = if((π‘š βˆ’ 𝑁) = 0, 1, 0))
157155, 156syl 17 . . . . . . . . 9 (((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ ∫(0(,)1)(expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯))) dπ‘₯ = if((π‘š βˆ’ 𝑁) = 0, 1, 0))
158157oveq2d 7431 . . . . . . . 8 (((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ (βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· ∫(0(,)1)(expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯))) dπ‘₯) = (βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· if((π‘š βˆ’ 𝑁) = 0, 1, 0)))
159158sumeq2dv 15679 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· ∫(0(,)1)(expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯))) dπ‘₯) = Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· if((π‘š βˆ’ 𝑁) = 0, 1, 0)))
160 1cnd 11237 . . . . . . . . 9 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ 1 ∈ β„‚)
161 0cnd 11235 . . . . . . . . 9 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ 0 ∈ β„‚)
162160, 161ifcld 4570 . . . . . . . 8 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ if((π‘š βˆ’ 𝑁) = 0, 1, 0) ∈ β„‚)
163101, 162, 114fsummulc1 15761 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· if((π‘š βˆ’ 𝑁) = 0, 1, 0)) = Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· if((π‘š βˆ’ 𝑁) = 0, 1, 0)))
164159, 163eqtr4d 2768 . . . . . 6 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· ∫(0(,)1)(expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯))) dπ‘₯) = (Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· if((π‘š βˆ’ 𝑁) = 0, 1, 0)))
165148, 152, 1643eqtr4rd 2776 . . . . 5 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· ∫(0(,)1)(expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯))) dπ‘₯) = if(π‘š ∈ {𝑁}, Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)), 0))
166165sumeq2dv 15679 . . . 4 (πœ‘ β†’ Ξ£π‘š ∈ (0...(𝑆 Β· 𝑁))Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· ∫(0(,)1)(expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯))) dπ‘₯) = Ξ£π‘š ∈ (0...(𝑆 Β· 𝑁))if(π‘š ∈ {𝑁}, Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)), 0))
167 0zd 12598 . . . . . . 7 (πœ‘ β†’ 0 ∈ β„€)
1689nn0zd 12612 . . . . . . . 8 (πœ‘ β†’ 𝑆 ∈ β„€)
169168, 153zmulcld 12700 . . . . . . 7 (πœ‘ β†’ (𝑆 Β· 𝑁) ∈ β„€)
1701nn0ge0d 12563 . . . . . . 7 (πœ‘ β†’ 0 ≀ 𝑁)
171 nnmulge 32563 . . . . . . . 8 ((𝑆 ∈ β„• ∧ 𝑁 ∈ β„•0) β†’ 𝑁 ≀ (𝑆 Β· 𝑁))
1728, 1, 171syl2anc 582 . . . . . . 7 (πœ‘ β†’ 𝑁 ≀ (𝑆 Β· 𝑁))
173167, 169, 153, 170, 172elfzd 13522 . . . . . 6 (πœ‘ β†’ 𝑁 ∈ (0...(𝑆 Β· 𝑁)))
174173snssd 4808 . . . . 5 (πœ‘ β†’ {𝑁} βŠ† (0...(𝑆 Β· 𝑁)))
175174sselda 3972 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ {𝑁}) β†’ π‘š ∈ (0...(𝑆 Β· 𝑁)))
176175, 145syldan 589 . . . . . 6 ((πœ‘ ∧ π‘š ∈ {𝑁}) β†’ Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) ∈ β„‚)
177176ralrimiva 3136 . . . . 5 (πœ‘ β†’ βˆ€π‘š ∈ {𝑁}Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) ∈ β„‚)
17894olcd 872 . . . . 5 (πœ‘ β†’ ((0...(𝑆 Β· 𝑁)) βŠ† (β„€β‰₯β€˜0) ∨ (0...(𝑆 Β· 𝑁)) ∈ Fin))
179 sumss2 15702 . . . . 5 ((({𝑁} βŠ† (0...(𝑆 Β· 𝑁)) ∧ βˆ€π‘š ∈ {𝑁}Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) ∈ β„‚) ∧ ((0...(𝑆 Β· 𝑁)) βŠ† (β„€β‰₯β€˜0) ∨ (0...(𝑆 Β· 𝑁)) ∈ Fin)) β†’ Ξ£π‘š ∈ {𝑁}Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) = Ξ£π‘š ∈ (0...(𝑆 Β· 𝑁))if(π‘š ∈ {𝑁}, Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)), 0))
180174, 177, 178, 179syl21anc 836 . . . 4 (πœ‘ β†’ Ξ£π‘š ∈ {𝑁}Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) = Ξ£π‘š ∈ (0...(𝑆 Β· 𝑁))if(π‘š ∈ {𝑁}, Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)), 0))
18129a1i 11 . . . . . . 7 (πœ‘ β†’ (1...𝑁) βŠ† β„•)
182 fzfid 13968 . . . . . . 7 (πœ‘ β†’ (1...𝑁) ∈ Fin)
183181, 153, 9, 182reprfi 34304 . . . . . 6 (πœ‘ β†’ ((1...𝑁)(reprβ€˜π‘†)𝑁) ∈ Fin)
18437a1i 11 . . . . . . 7 ((πœ‘ ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)) β†’ (0..^𝑆) ∈ Fin)
1851ad2antrr 724 . . . . . . . 8 (((πœ‘ ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ 𝑁 ∈ β„•0)
1869ad2antrr 724 . . . . . . . 8 (((πœ‘ ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ 𝑆 ∈ β„•0)
18722ad2antrr 724 . . . . . . . 8 (((πœ‘ ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ 𝑁 ∈ β„‚)
18811ad2antrr 724 . . . . . . . 8 (((πœ‘ ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ 𝐿:(0..^𝑆)⟢(β„‚ ↑m β„•))
189 simpr 483 . . . . . . . 8 (((πœ‘ ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ π‘Ž ∈ (0..^𝑆))
19029a1i 11 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)) β†’ (1...𝑁) βŠ† β„•)
191153adantr 479 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)) β†’ 𝑁 ∈ β„€)
1929adantr 479 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)) β†’ 𝑆 ∈ β„•0)
193 simpr 483 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)) β†’ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁))
194190, 191, 192, 193reprf 34300 . . . . . . . . . 10 ((πœ‘ ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)) β†’ 𝑐:(0..^𝑆)⟢(1...𝑁))
195194ffvelcdmda 7088 . . . . . . . . 9 (((πœ‘ ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ (π‘β€˜π‘Ž) ∈ (1...𝑁))
19629, 195sselid 3970 . . . . . . . 8 (((πœ‘ ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ (π‘β€˜π‘Ž) ∈ β„•)
197185, 186, 187, 188, 189, 196breprexplemb 34319 . . . . . . 7 (((πœ‘ ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ ((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) ∈ β„‚)
198184, 197fprodcl 15926 . . . . . 6 ((πœ‘ ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)) β†’ βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) ∈ β„‚)
199183, 198fsumcl 15709 . . . . 5 (πœ‘ β†’ Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) ∈ β„‚)
200 oveq2 7423 . . . . . . 7 (π‘š = 𝑁 β†’ ((1...𝑁)(reprβ€˜π‘†)π‘š) = ((1...𝑁)(reprβ€˜π‘†)𝑁))
201200sumeq1d 15677 . . . . . 6 (π‘š = 𝑁 β†’ Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) = Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)))
202201sumsn 15722 . . . . 5 ((𝑁 ∈ β„•0 ∧ Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) ∈ β„‚) β†’ Ξ£π‘š ∈ {𝑁}Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) = Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)))
2031, 199, 202syl2anc 582 . . . 4 (πœ‘ β†’ Ξ£π‘š ∈ {𝑁}Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) = Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)))
204166, 180, 2033eqtr2d 2771 . . 3 (πœ‘ β†’ Ξ£π‘š ∈ (0...(𝑆 Β· 𝑁))Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· ∫(0(,)1)(expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯))) dπ‘₯) = Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)))
205139simprd 494 . . . . 5 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ ∫(0(,)1)Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))) dπ‘₯ = Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)∫(0(,)1)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))) dπ‘₯)
206110an32s 650 . . . . . . 7 ((((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) ∧ π‘₯ ∈ (0(,)1)) β†’ (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯))) ∈ β„‚)
207114, 206, 137itgmulc2 25779 . . . . . 6 (((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ (βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· ∫(0(,)1)(expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯))) dπ‘₯) = ∫(0(,)1)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))) dπ‘₯)
208207sumeq2dv 15679 . . . . 5 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· ∫(0(,)1)(expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯))) dπ‘₯) = Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)∫(0(,)1)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))) dπ‘₯)
209205, 208eqtr4d 2768 . . . 4 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ ∫(0(,)1)Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))) dπ‘₯ = Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· ∫(0(,)1)(expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯))) dπ‘₯))
210209sumeq2dv 15679 . . 3 (πœ‘ β†’ Ξ£π‘š ∈ (0...(𝑆 Β· 𝑁))∫(0(,)1)Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))) dπ‘₯ = Ξ£π‘š ∈ (0...(𝑆 Β· 𝑁))Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· ∫(0(,)1)(expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯))) dπ‘₯))
2111, 9reprfz1 34312 . . . 4 (πœ‘ β†’ (β„•(reprβ€˜π‘†)𝑁) = ((1...𝑁)(reprβ€˜π‘†)𝑁))
212211sumeq1d 15677 . . 3 (πœ‘ β†’ Σ𝑐 ∈ (β„•(reprβ€˜π‘†)𝑁)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) = Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)))
213204, 210, 2123eqtr4d 2775 . 2 (πœ‘ β†’ Ξ£π‘š ∈ (0...(𝑆 Β· 𝑁))∫(0(,)1)Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))) dπ‘₯ = Σ𝑐 ∈ (β„•(reprβ€˜π‘†)𝑁)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)))
21491, 142, 2133eqtrrd 2770 1 (πœ‘ β†’ Σ𝑐 ∈ (β„•(reprβ€˜π‘†)𝑁)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) = ∫(0(,)1)(βˆπ‘Ž ∈ (0..^𝑆)(((πΏβ€˜π‘Ž)vts𝑁)β€˜π‘₯) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)))) dπ‘₯)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 394   ∨ wo 845   = wceq 1533   ∈ wcel 2098  βˆ€wral 3051  Vcvv 3463   βŠ† wss 3940  ifcif 4524  {csn 4624   class class class wbr 5143   ↦ cmpt 5226  dom cdm 5672  βŸΆwf 6538  β€˜cfv 6542  (class class class)co 7415   ↑m cmap 8841  Fincfn 8960  β„‚cc 11134  β„cr 11135  0cc0 11136  1c1 11137  ici 11138   + caddc 11139   Β· cmul 11141   ≀ cle 11277   βˆ’ cmin 11472  -cneg 11473  β„•cn 12240  2c2 12295  β„•0cn0 12500  β„€cz 12586  β„€β‰₯cuz 12850  (,)cioo 13354  [,]cicc 13357  ...cfz 13514  ..^cfzo 13657  Ξ£csu 15662  βˆcprod 15879  expce 16035  Ο€cpi 16040  β€“cnβ†’ccncf 24812  volcvol 25408  πΏ1cibl 25562  βˆ«citg 25563  reprcrepr 34296  vtscvts 34323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5280  ax-sep 5294  ax-nul 5301  ax-pow 5359  ax-pr 5423  ax-un 7737  ax-inf2 9662  ax-cc 10456  ax-cnex 11192  ax-resscn 11193  ax-1cn 11194  ax-icn 11195  ax-addcl 11196  ax-addrcl 11197  ax-mulcl 11198  ax-mulrcl 11199  ax-mulcom 11200  ax-addass 11201  ax-mulass 11202  ax-distr 11203  ax-i2m1 11204  ax-1ne0 11205  ax-1rid 11206  ax-rnegex 11207  ax-rrecex 11208  ax-cnre 11209  ax-pre-lttri 11210  ax-pre-lttrn 11211  ax-pre-ltadd 11212  ax-pre-mulgt0 11213  ax-pre-sup 11214  ax-addf 11215
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3960  df-symdif 4237  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-tp 4629  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-iin 4994  df-disj 5109  df-br 5144  df-opab 5206  df-mpt 5227  df-tr 5261  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7371  df-ov 7418  df-oprab 7419  df-mpo 7420  df-of 7681  df-ofr 7682  df-om 7868  df-1st 7989  df-2nd 7990  df-supp 8162  df-frecs 8283  df-wrecs 8314  df-recs 8388  df-rdg 8427  df-1o 8483  df-2o 8484  df-oadd 8487  df-omul 8488  df-er 8721  df-map 8843  df-pm 8844  df-ixp 8913  df-en 8961  df-dom 8962  df-sdom 8963  df-fin 8964  df-fsupp 9384  df-fi 9432  df-sup 9463  df-inf 9464  df-oi 9531  df-dju 9922  df-card 9960  df-acn 9963  df-pnf 11278  df-mnf 11279  df-xr 11280  df-ltxr 11281  df-le 11282  df-sub 11474  df-neg 11475  df-div 11900  df-nn 12241  df-2 12303  df-3 12304  df-4 12305  df-5 12306  df-6 12307  df-7 12308  df-8 12309  df-9 12310  df-n0 12501  df-z 12587  df-dec 12706  df-uz 12851  df-q 12961  df-rp 13005  df-xneg 13122  df-xadd 13123  df-xmul 13124  df-ioo 13358  df-ioc 13359  df-ico 13360  df-icc 13361  df-fz 13515  df-fzo 13658  df-fl 13787  df-mod 13865  df-seq 13997  df-exp 14057  df-fac 14263  df-bc 14292  df-hash 14320  df-shft 15044  df-cj 15076  df-re 15077  df-im 15078  df-sqrt 15212  df-abs 15213  df-limsup 15445  df-clim 15462  df-rlim 15463  df-sum 15663  df-prod 15880  df-ef 16041  df-sin 16043  df-cos 16044  df-pi 16046  df-struct 17113  df-sets 17130  df-slot 17148  df-ndx 17160  df-base 17178  df-ress 17207  df-plusg 17243  df-mulr 17244  df-starv 17245  df-sca 17246  df-vsca 17247  df-ip 17248  df-tset 17249  df-ple 17250  df-ds 17252  df-unif 17253  df-hom 17254  df-cco 17255  df-rest 17401  df-topn 17402  df-0g 17420  df-gsum 17421  df-topgen 17422  df-pt 17423  df-prds 17426  df-xrs 17481  df-qtop 17486  df-imas 17487  df-xps 17489  df-mre 17563  df-mrc 17564  df-acs 17566  df-mgm 18597  df-sgrp 18676  df-mnd 18692  df-submnd 18738  df-mulg 19026  df-cntz 19270  df-cmn 19739  df-psmet 21273  df-xmet 21274  df-met 21275  df-bl 21276  df-mopn 21277  df-fbas 21278  df-fg 21279  df-cnfld 21282  df-top 22812  df-topon 22829  df-topsp 22851  df-bases 22865  df-cld 22939  df-ntr 22940  df-cls 22941  df-nei 23018  df-lp 23056  df-perf 23057  df-cn 23147  df-cnp 23148  df-haus 23235  df-cmp 23307  df-tx 23482  df-hmeo 23675  df-fil 23766  df-fm 23858  df-flim 23859  df-flf 23860  df-xms 24242  df-ms 24243  df-tms 24244  df-cncf 24814  df-ovol 25409  df-vol 25410  df-mbf 25564  df-itg1 25565  df-itg2 25566  df-ibl 25567  df-itg 25568  df-0p 25615  df-limc 25811  df-dv 25812  df-repr 34297  df-vts 34324
This theorem is referenced by:  circlemethnat  34329  circlevma  34330  circlemethhgt  34331
  Copyright terms: Public domain W3C validator