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 34181
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 480 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (0(,)1)) β†’ 𝑁 ∈ β„•0)
3 ioossre 13391 . . . . . . . . 9 (0(,)1) βŠ† ℝ
4 ax-resscn 11169 . . . . . . . . 9 ℝ βŠ† β„‚
53, 4sstri 3986 . . . . . . . 8 (0(,)1) βŠ† β„‚
65a1i 11 . . . . . . 7 (πœ‘ β†’ (0(,)1) βŠ† β„‚)
76sselda 3977 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (0(,)1)) β†’ π‘₯ ∈ β„‚)
8 circlemeth.s . . . . . . . 8 (πœ‘ β†’ 𝑆 ∈ β„•)
98nnnn0d 12536 . . . . . . 7 (πœ‘ β†’ 𝑆 ∈ β„•0)
109adantr 480 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (0(,)1)) β†’ 𝑆 ∈ β„•0)
11 circlemeth.l . . . . . . 7 (πœ‘ β†’ 𝐿:(0..^𝑆)⟢(β„‚ ↑m β„•))
1211adantr 480 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (0(,)1)) β†’ 𝐿:(0..^𝑆)⟢(β„‚ ↑m β„•))
132, 7, 10, 12vtsprod 34180 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ (0(,)1)) β†’ βˆπ‘Ž ∈ (0..^𝑆)(((πΏβ€˜π‘Ž)vts𝑁)β€˜π‘₯) = Ξ£π‘š ∈ (0...(𝑆 Β· 𝑁))Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯)))))
1413oveq1d 7420 . . . 4 ((πœ‘ ∧ π‘₯ ∈ (0(,)1)) β†’ (βˆπ‘Ž ∈ (0..^𝑆)(((πΏβ€˜π‘Ž)vts𝑁)β€˜π‘₯) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)))) = (Ξ£π‘š ∈ (0...(𝑆 Β· 𝑁))Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯)))) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)))))
15 fzfid 13944 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ (0(,)1)) β†’ (0...(𝑆 Β· 𝑁)) ∈ Fin)
16 ax-icn 11171 . . . . . . . . 9 i ∈ β„‚
17 2cn 12291 . . . . . . . . . 10 2 ∈ β„‚
18 picn 26349 . . . . . . . . . 10 Ο€ ∈ β„‚
1917, 18mulcli 11225 . . . . . . . . 9 (2 Β· Ο€) ∈ β„‚
2016, 19mulcli 11225 . . . . . . . 8 (i Β· (2 Β· Ο€)) ∈ β„‚
2120a1i 11 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (0(,)1)) β†’ (i Β· (2 Β· Ο€)) ∈ β„‚)
221nn0cnd 12538 . . . . . . . . . . 11 (πœ‘ β†’ 𝑁 ∈ β„‚)
2322negcld 11562 . . . . . . . . . 10 (πœ‘ β†’ -𝑁 ∈ β„‚)
2423ralrimivw 3144 . . . . . . . . 9 (πœ‘ β†’ βˆ€π‘₯ ∈ (0(,)1)-𝑁 ∈ β„‚)
2524r19.21bi 3242 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (0(,)1)) β†’ -𝑁 ∈ β„‚)
2625, 7mulcld 11238 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (0(,)1)) β†’ (-𝑁 Β· π‘₯) ∈ β„‚)
2721, 26mulcld 11238 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (0(,)1)) β†’ ((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)) ∈ β„‚)
2827efcld 16033 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ (0(,)1)) β†’ (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯))) ∈ β„‚)
29 fz1ssnn 13538 . . . . . . . 8 (1...𝑁) βŠ† β„•
3029a1i 11 . . . . . . 7 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (1...𝑁) βŠ† β„•)
31 simpr 484 . . . . . . . . 9 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ π‘š ∈ (0...(𝑆 Β· 𝑁)))
3231elfzelzd 13508 . . . . . . . 8 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ π‘š ∈ β„€)
3332adantlr 712 . . . . . . 7 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ π‘š ∈ β„€)
3410adantr 480 . . . . . . 7 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ 𝑆 ∈ β„•0)
35 fzfid 13944 . . . . . . 7 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (1...𝑁) ∈ Fin)
3630, 33, 34, 35reprfi 34157 . . . . . 6 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ ((1...𝑁)(reprβ€˜π‘†)π‘š) ∈ Fin)
37 fzofi 13945 . . . . . . . . 9 (0..^𝑆) ∈ Fin
3837a1i 11 . . . . . . . 8 ((((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ (0..^𝑆) ∈ Fin)
391ad3antrrr 727 . . . . . . . . . 10 ((((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ 𝑁 ∈ β„•0)
409ad3antrrr 727 . . . . . . . . . 10 ((((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ 𝑆 ∈ β„•0)
4132zcnd 12671 . . . . . . . . . . 11 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ π‘š ∈ β„‚)
4241ad2antrr 723 . . . . . . . . . 10 ((((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ π‘š ∈ β„‚)
4311ad3antrrr 727 . . . . . . . . . 10 ((((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ 𝐿:(0..^𝑆)⟢(β„‚ ↑m β„•))
44 simpr 484 . . . . . . . . . 10 ((((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ π‘Ž ∈ (0..^𝑆))
4529a1i 11 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ (1...𝑁) βŠ† β„•)
4632adantr 480 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ π‘š ∈ β„€)
479ad2antrr 723 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ 𝑆 ∈ β„•0)
48 simpr 484 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š))
4945, 46, 47, 48reprf 34153 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ 𝑐:(0..^𝑆)⟢(1...𝑁))
5049ffvelcdmda 7080 . . . . . . . . . . 11 ((((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ (π‘β€˜π‘Ž) ∈ (1...𝑁))
5129, 50sselid 3975 . . . . . . . . . 10 ((((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ (π‘β€˜π‘Ž) ∈ β„•)
5239, 40, 42, 43, 44, 51breprexplemb 34172 . . . . . . . . 9 ((((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ ((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) ∈ β„‚)
5352adantl3r 747 . . . . . . . 8 (((((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ ((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) ∈ β„‚)
5438, 53fprodcl 15902 . . . . . . 7 ((((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) ∈ β„‚)
5520a1i 11 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (i Β· (2 Β· Ο€)) ∈ β„‚)
5633zcnd 12671 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ π‘š ∈ β„‚)
577adantr 480 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ π‘₯ ∈ β„‚)
5856, 57mulcld 11238 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (π‘š Β· π‘₯) ∈ β„‚)
5955, 58mulcld 11238 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ ((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯)) ∈ β„‚)
6059efcld 16033 . . . . . . . 8 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯))) ∈ β„‚)
6160adantr 480 . . . . . . 7 ((((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ (expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯))) ∈ β„‚)
6254, 61mulcld 11238 . . . . . 6 ((((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ (βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯)))) ∈ β„‚)
6336, 62fsumcl 15685 . . . . 5 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯)))) ∈ β„‚)
6415, 28, 63fsummulc1 15737 . . . 4 ((πœ‘ ∧ π‘₯ ∈ (0(,)1)) β†’ (Ξ£π‘š ∈ (0...(𝑆 Β· 𝑁))Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯)))) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)))) = Ξ£π‘š ∈ (0...(𝑆 Β· 𝑁))(Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯)))) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)))))
6528adantr 480 . . . . . . 7 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯))) ∈ β„‚)
6636, 65, 62fsummulc1 15737 . . . . . 6 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯)))) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)))) = Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)((βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯)))) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)))))
6765adantr 480 . . . . . . . . 9 ((((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯))) ∈ β„‚)
6854, 61, 67mulassd 11241 . . . . . . . 8 ((((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ ((βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯)))) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)))) = (βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· ((expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯))) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯))))))
6927adantr 480 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ ((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)) ∈ β„‚)
70 efadd 16044 . . . . . . . . . . . 12 ((((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯)) ∈ β„‚ ∧ ((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)) ∈ β„‚) β†’ (expβ€˜(((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯)) + ((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)))) = ((expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯))) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)))))
7159, 69, 70syl2anc 583 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (expβ€˜(((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯)) + ((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)))) = ((expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯))) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)))))
7226adantr 480 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (-𝑁 Β· π‘₯) ∈ β„‚)
7355, 58, 72adddid 11242 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ ((i Β· (2 Β· Ο€)) Β· ((π‘š Β· π‘₯) + (-𝑁 Β· π‘₯))) = (((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯)) + ((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯))))
7425adantr 480 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ -𝑁 ∈ β„‚)
7556, 74, 57adddird 11243 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ ((π‘š + -𝑁) Β· π‘₯) = ((π‘š Β· π‘₯) + (-𝑁 Β· π‘₯)))
7622ad2antrr 723 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ 𝑁 ∈ β„‚)
7756, 76negsubd 11581 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (π‘š + -𝑁) = (π‘š βˆ’ 𝑁))
7877oveq1d 7420 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ ((π‘š + -𝑁) Β· π‘₯) = ((π‘š βˆ’ 𝑁) Β· π‘₯))
7975, 78eqtr3d 2768 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ ((π‘š Β· π‘₯) + (-𝑁 Β· π‘₯)) = ((π‘š βˆ’ 𝑁) Β· π‘₯))
8079oveq2d 7421 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ ((i Β· (2 Β· Ο€)) Β· ((π‘š Β· π‘₯) + (-𝑁 Β· π‘₯))) = ((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))
8173, 80eqtr3d 2768 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯)) + ((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯))) = ((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))
8281fveq2d 6889 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (expβ€˜(((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯)) + ((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)))) = (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯))))
8371, 82eqtr3d 2768 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ ((expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯))) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)))) = (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯))))
8483oveq2d 7421 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· ((expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯))) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯))))) = (βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))))
8584adantr 480 . . . . . . . 8 ((((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ (βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· ((expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯))) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯))))) = (βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))))
8668, 85eqtrd 2766 . . . . . . 7 ((((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ ((βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯)))) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)))) = (βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))))
8786sumeq2dv 15655 . . . . . 6 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)((βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯)))) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)))) = Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))))
8866, 87eqtrd 2766 . . . . 5 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯)))) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)))) = Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))))
8988sumeq2dv 15655 . . . 4 ((πœ‘ ∧ π‘₯ ∈ (0(,)1)) β†’ Ξ£π‘š ∈ (0...(𝑆 Β· 𝑁))(Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (π‘š Β· π‘₯)))) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)))) = Ξ£π‘š ∈ (0...(𝑆 Β· 𝑁))Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))))
9014, 64, 893eqtrd 2770 . . 3 ((πœ‘ ∧ π‘₯ ∈ (0(,)1)) β†’ (βˆπ‘Ž ∈ (0..^𝑆)(((πΏβ€˜π‘Ž)vts𝑁)β€˜π‘₯) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)))) = Ξ£π‘š ∈ (0...(𝑆 Β· 𝑁))Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))))
9190itgeq2dv 25666 . 2 (πœ‘ β†’ ∫(0(,)1)(βˆπ‘Ž ∈ (0..^𝑆)(((πΏβ€˜π‘Ž)vts𝑁)β€˜π‘₯) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)))) dπ‘₯ = ∫(0(,)1)Ξ£π‘š ∈ (0...(𝑆 Β· 𝑁))Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))) dπ‘₯)
92 ioombl 25449 . . . . 5 (0(,)1) ∈ dom vol
9392a1i 11 . . . 4 (πœ‘ β†’ (0(,)1) ∈ dom vol)
94 fzfid 13944 . . . 4 (πœ‘ β†’ (0...(𝑆 Β· 𝑁)) ∈ Fin)
95 sumex 15640 . . . . 5 Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))) ∈ V
9695a1i 11 . . . 4 ((πœ‘ ∧ (π‘₯ ∈ (0(,)1) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁)))) β†’ Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))) ∈ V)
9793adantr 480 . . . . . 6 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (0(,)1) ∈ dom vol)
9829a1i 11 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (1...𝑁) βŠ† β„•)
999adantr 480 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ 𝑆 ∈ β„•0)
100 fzfid 13944 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (1...𝑁) ∈ Fin)
10198, 32, 99, 100reprfi 34157 . . . . . 6 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ ((1...𝑁)(reprβ€˜π‘†)π‘š) ∈ Fin)
10237a1i 11 . . . . . . . . 9 ((((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ π‘₯ ∈ (0(,)1)) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ (0..^𝑆) ∈ Fin)
10352adantllr 716 . . . . . . . . 9 (((((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ π‘₯ ∈ (0(,)1)) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ ((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) ∈ β„‚)
104102, 103fprodcl 15902 . . . . . . . 8 ((((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ π‘₯ ∈ (0(,)1)) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) ∈ β„‚)
10556, 76subcld 11575 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (π‘š βˆ’ 𝑁) ∈ β„‚)
106105, 57mulcld 11238 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ ((π‘š βˆ’ 𝑁) Β· π‘₯) ∈ β„‚)
10755, 106mulcld 11238 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ (0(,)1)) ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ ((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)) ∈ β„‚)
108107an32s 649 . . . . . . . . . 10 (((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ π‘₯ ∈ (0(,)1)) β†’ ((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)) ∈ β„‚)
109108adantr 480 . . . . . . . . 9 ((((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ π‘₯ ∈ (0(,)1)) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ ((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)) ∈ β„‚)
110109efcld 16033 . . . . . . . 8 ((((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ π‘₯ ∈ (0(,)1)) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯))) ∈ β„‚)
111104, 110mulcld 11238 . . . . . . 7 ((((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ π‘₯ ∈ (0(,)1)) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ (βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))) ∈ β„‚)
112111anasss 466 . . . . . 6 (((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ (π‘₯ ∈ (0(,)1) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š))) β†’ (βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))) ∈ β„‚)
11337a1i 11 . . . . . . . 8 (((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ (0..^𝑆) ∈ Fin)
114113, 52fprodcl 15902 . . . . . . 7 (((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) ∈ β„‚)
115 fvex 6898 . . . . . . . 8 (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯))) ∈ V
116115a1i 11 . . . . . . 7 ((((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) ∧ π‘₯ ∈ (0(,)1)) β†’ (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯))) ∈ V)
117 ioossicc 13416 . . . . . . . . . 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 11221 . . . . . . . . . 10 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ 0 ∈ ℝ)
122 1red 11219 . . . . . . . . . 10 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ 1 ∈ ℝ)
12322adantr 480 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ 𝑁 ∈ β„‚)
12441, 123subcld 11575 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (π‘š βˆ’ 𝑁) ∈ β„‚)
125 unitsscn 13483 . . . . . . . . . . . . . 14 (0[,]1) βŠ† β„‚
126125a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (0[,]1) βŠ† β„‚)
127 ssidd 4000 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ β„‚ βŠ† β„‚)
128 cncfmptc 24787 . . . . . . . . . . . . 13 (((π‘š βˆ’ 𝑁) ∈ β„‚ ∧ (0[,]1) βŠ† β„‚ ∧ β„‚ βŠ† β„‚) β†’ (π‘₯ ∈ (0[,]1) ↦ (π‘š βˆ’ 𝑁)) ∈ ((0[,]1)–cnβ†’β„‚))
129124, 126, 127, 128syl3anc 1368 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (π‘₯ ∈ (0[,]1) ↦ (π‘š βˆ’ 𝑁)) ∈ ((0[,]1)–cnβ†’β„‚))
130 cncfmptid 24788 . . . . . . . . . . . . 13 (((0[,]1) βŠ† β„‚ ∧ β„‚ βŠ† β„‚) β†’ (π‘₯ ∈ (0[,]1) ↦ π‘₯) ∈ ((0[,]1)–cnβ†’β„‚))
131126, 127, 130syl2anc 583 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (π‘₯ ∈ (0[,]1) ↦ π‘₯) ∈ ((0[,]1)–cnβ†’β„‚))
132129, 131mulcncf 25329 . . . . . . . . . . 11 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (π‘₯ ∈ (0[,]1) ↦ ((π‘š βˆ’ 𝑁) Β· π‘₯)) ∈ ((0[,]1)–cnβ†’β„‚))
133132efmul2picn 34137 . . . . . . . . . 10 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (π‘₯ ∈ (0[,]1) ↦ (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))) ∈ ((0[,]1)–cnβ†’β„‚))
134 cniccibl 25725 . . . . . . . . . 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 25689 . . . . . . . 8 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (π‘₯ ∈ (0(,)1) ↦ (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))) ∈ 𝐿1)
137136adantr 480 . . . . . . 7 (((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ (π‘₯ ∈ (0(,)1) ↦ (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))) ∈ 𝐿1)
138114, 116, 137iblmulc2 25715 . . . . . 6 (((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ (π‘₯ ∈ (0(,)1) ↦ (βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯))))) ∈ 𝐿1)
13997, 101, 112, 138itgfsum 25711 . . . . 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 494 . . . 4 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (π‘₯ ∈ (0(,)1) ↦ Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯))))) ∈ 𝐿1)
14193, 94, 96, 140itgfsum 25711 . . 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 495 . 2 (πœ‘ β†’ ∫(0(,)1)Ξ£π‘š ∈ (0...(𝑆 Β· 𝑁))Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))) dπ‘₯ = Ξ£π‘š ∈ (0...(𝑆 Β· 𝑁))∫(0(,)1)Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))) dπ‘₯)
143 oveq2 7413 . . . . . . 7 (if((π‘š βˆ’ 𝑁) = 0, 1, 0) = 1 β†’ (Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· if((π‘š βˆ’ 𝑁) = 0, 1, 0)) = (Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· 1))
144 oveq2 7413 . . . . . . 7 (if((π‘š βˆ’ 𝑁) = 0, 1, 0) = 0 β†’ (Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· if((π‘š βˆ’ 𝑁) = 0, 1, 0)) = (Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· 0))
145101, 114fsumcl 15685 . . . . . . . 8 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) ∈ β„‚)
146145mulridd 11235 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· 1) = Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)))
147145mul01d 11417 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· 0) = 0)
148143, 144, 146, 147ifeq3da 32287 . . . . . 6 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ if((π‘š βˆ’ 𝑁) = 0, Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)), 0) = (Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· if((π‘š βˆ’ 𝑁) = 0, 1, 0)))
149 velsn 4639 . . . . . . . 8 (π‘š ∈ {𝑁} ↔ π‘š = 𝑁)
15041, 123subeq0ad 11585 . . . . . . . 8 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ ((π‘š βˆ’ 𝑁) = 0 ↔ π‘š = 𝑁))
151149, 150bitr4id 290 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (π‘š ∈ {𝑁} ↔ (π‘š βˆ’ 𝑁) = 0))
152151ifbid 4546 . . . . . 6 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ if(π‘š ∈ {𝑁}, Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)), 0) = if((π‘š βˆ’ 𝑁) = 0, Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)), 0))
1531nn0zd 12588 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑁 ∈ β„€)
154153ad2antrr 723 . . . . . . . . . . 11 (((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ 𝑁 ∈ β„€)
15546, 154zsubcld 12675 . . . . . . . . . 10 (((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ (π‘š βˆ’ 𝑁) ∈ β„€)
156 itgexpif 34147 . . . . . . . . . 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 7421 . . . . . . . 8 (((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ (βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· ∫(0(,)1)(expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯))) dπ‘₯) = (βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· if((π‘š βˆ’ 𝑁) = 0, 1, 0)))
159158sumeq2dv 15655 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· ∫(0(,)1)(expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯))) dπ‘₯) = Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· if((π‘š βˆ’ 𝑁) = 0, 1, 0)))
160 1cnd 11213 . . . . . . . . 9 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ 1 ∈ β„‚)
161 0cnd 11211 . . . . . . . . 9 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ 0 ∈ β„‚)
162160, 161ifcld 4569 . . . . . . . 8 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ if((π‘š βˆ’ 𝑁) = 0, 1, 0) ∈ β„‚)
163101, 162, 114fsummulc1 15737 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ (Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· if((π‘š βˆ’ 𝑁) = 0, 1, 0)) = Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· if((π‘š βˆ’ 𝑁) = 0, 1, 0)))
164159, 163eqtr4d 2769 . . . . . 6 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· ∫(0(,)1)(expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯))) dπ‘₯) = (Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· if((π‘š βˆ’ 𝑁) = 0, 1, 0)))
165148, 152, 1643eqtr4rd 2777 . . . . 5 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· ∫(0(,)1)(expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯))) dπ‘₯) = if(π‘š ∈ {𝑁}, Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)), 0))
166165sumeq2dv 15655 . . . 4 (πœ‘ β†’ Ξ£π‘š ∈ (0...(𝑆 Β· 𝑁))Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· ∫(0(,)1)(expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯))) dπ‘₯) = Ξ£π‘š ∈ (0...(𝑆 Β· 𝑁))if(π‘š ∈ {𝑁}, Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)), 0))
167 0zd 12574 . . . . . . 7 (πœ‘ β†’ 0 ∈ β„€)
1689nn0zd 12588 . . . . . . . 8 (πœ‘ β†’ 𝑆 ∈ β„€)
169168, 153zmulcld 12676 . . . . . . 7 (πœ‘ β†’ (𝑆 Β· 𝑁) ∈ β„€)
1701nn0ge0d 12539 . . . . . . 7 (πœ‘ β†’ 0 ≀ 𝑁)
171 nnmulge 32470 . . . . . . . 8 ((𝑆 ∈ β„• ∧ 𝑁 ∈ β„•0) β†’ 𝑁 ≀ (𝑆 Β· 𝑁))
1728, 1, 171syl2anc 583 . . . . . . 7 (πœ‘ β†’ 𝑁 ≀ (𝑆 Β· 𝑁))
173167, 169, 153, 170, 172elfzd 13498 . . . . . 6 (πœ‘ β†’ 𝑁 ∈ (0...(𝑆 Β· 𝑁)))
174173snssd 4807 . . . . 5 (πœ‘ β†’ {𝑁} βŠ† (0...(𝑆 Β· 𝑁)))
175174sselda 3977 . . . . . . 7 ((πœ‘ ∧ π‘š ∈ {𝑁}) β†’ π‘š ∈ (0...(𝑆 Β· 𝑁)))
176175, 145syldan 590 . . . . . 6 ((πœ‘ ∧ π‘š ∈ {𝑁}) β†’ Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) ∈ β„‚)
177176ralrimiva 3140 . . . . 5 (πœ‘ β†’ βˆ€π‘š ∈ {𝑁}Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) ∈ β„‚)
17894olcd 871 . . . . 5 (πœ‘ β†’ ((0...(𝑆 Β· 𝑁)) βŠ† (β„€β‰₯β€˜0) ∨ (0...(𝑆 Β· 𝑁)) ∈ Fin))
179 sumss2 15678 . . . . 5 ((({𝑁} βŠ† (0...(𝑆 Β· 𝑁)) ∧ βˆ€π‘š ∈ {𝑁}Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) ∈ β„‚) ∧ ((0...(𝑆 Β· 𝑁)) βŠ† (β„€β‰₯β€˜0) ∨ (0...(𝑆 Β· 𝑁)) ∈ Fin)) β†’ Ξ£π‘š ∈ {𝑁}Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) = Ξ£π‘š ∈ (0...(𝑆 Β· 𝑁))if(π‘š ∈ {𝑁}, Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)), 0))
180174, 177, 178, 179syl21anc 835 . . . 4 (πœ‘ β†’ Ξ£π‘š ∈ {𝑁}Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) = Ξ£π‘š ∈ (0...(𝑆 Β· 𝑁))if(π‘š ∈ {𝑁}, Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)), 0))
18129a1i 11 . . . . . . 7 (πœ‘ β†’ (1...𝑁) βŠ† β„•)
182 fzfid 13944 . . . . . . 7 (πœ‘ β†’ (1...𝑁) ∈ Fin)
183181, 153, 9, 182reprfi 34157 . . . . . 6 (πœ‘ β†’ ((1...𝑁)(reprβ€˜π‘†)𝑁) ∈ Fin)
18437a1i 11 . . . . . . 7 ((πœ‘ ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)) β†’ (0..^𝑆) ∈ Fin)
1851ad2antrr 723 . . . . . . . 8 (((πœ‘ ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ 𝑁 ∈ β„•0)
1869ad2antrr 723 . . . . . . . 8 (((πœ‘ ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ 𝑆 ∈ β„•0)
18722ad2antrr 723 . . . . . . . 8 (((πœ‘ ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ 𝑁 ∈ β„‚)
18811ad2antrr 723 . . . . . . . 8 (((πœ‘ ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ 𝐿:(0..^𝑆)⟢(β„‚ ↑m β„•))
189 simpr 484 . . . . . . . 8 (((πœ‘ ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ π‘Ž ∈ (0..^𝑆))
19029a1i 11 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)) β†’ (1...𝑁) βŠ† β„•)
191153adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)) β†’ 𝑁 ∈ β„€)
1929adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)) β†’ 𝑆 ∈ β„•0)
193 simpr 484 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)) β†’ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁))
194190, 191, 192, 193reprf 34153 . . . . . . . . . 10 ((πœ‘ ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)) β†’ 𝑐:(0..^𝑆)⟢(1...𝑁))
195194ffvelcdmda 7080 . . . . . . . . 9 (((πœ‘ ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ (π‘β€˜π‘Ž) ∈ (1...𝑁))
19629, 195sselid 3975 . . . . . . . 8 (((πœ‘ ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ (π‘β€˜π‘Ž) ∈ β„•)
197185, 186, 187, 188, 189, 196breprexplemb 34172 . . . . . . 7 (((πœ‘ ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)) ∧ π‘Ž ∈ (0..^𝑆)) β†’ ((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) ∈ β„‚)
198184, 197fprodcl 15902 . . . . . 6 ((πœ‘ ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)) β†’ βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) ∈ β„‚)
199183, 198fsumcl 15685 . . . . 5 (πœ‘ β†’ Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) ∈ β„‚)
200 oveq2 7413 . . . . . . 7 (π‘š = 𝑁 β†’ ((1...𝑁)(reprβ€˜π‘†)π‘š) = ((1...𝑁)(reprβ€˜π‘†)𝑁))
201200sumeq1d 15653 . . . . . 6 (π‘š = 𝑁 β†’ Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) = Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)))
202201sumsn 15698 . . . . 5 ((𝑁 ∈ β„•0 ∧ Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) ∈ β„‚) β†’ Ξ£π‘š ∈ {𝑁}Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) = Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)))
2031, 199, 202syl2anc 583 . . . 4 (πœ‘ β†’ Ξ£π‘š ∈ {𝑁}Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) = Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)))
204166, 180, 2033eqtr2d 2772 . . 3 (πœ‘ β†’ Ξ£π‘š ∈ (0...(𝑆 Β· 𝑁))Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· ∫(0(,)1)(expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯))) dπ‘₯) = Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)))
205139simprd 495 . . . . 5 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ ∫(0(,)1)Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))) dπ‘₯ = Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)∫(0(,)1)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))) dπ‘₯)
206110an32s 649 . . . . . . 7 ((((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) ∧ π‘₯ ∈ (0(,)1)) β†’ (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯))) ∈ β„‚)
207114, 206, 137itgmulc2 25718 . . . . . 6 (((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)) β†’ (βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· ∫(0(,)1)(expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯))) dπ‘₯) = ∫(0(,)1)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))) dπ‘₯)
208207sumeq2dv 15655 . . . . 5 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· ∫(0(,)1)(expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯))) dπ‘₯) = Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)∫(0(,)1)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))) dπ‘₯)
209205, 208eqtr4d 2769 . . . 4 ((πœ‘ ∧ π‘š ∈ (0...(𝑆 Β· 𝑁))) β†’ ∫(0(,)1)Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))) dπ‘₯ = Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· ∫(0(,)1)(expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯))) dπ‘₯))
210209sumeq2dv 15655 . . 3 (πœ‘ β†’ Ξ£π‘š ∈ (0...(𝑆 Β· 𝑁))∫(0(,)1)Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))) dπ‘₯ = Ξ£π‘š ∈ (0...(𝑆 Β· 𝑁))Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· ∫(0(,)1)(expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯))) dπ‘₯))
2111, 9reprfz1 34165 . . . 4 (πœ‘ β†’ (β„•(reprβ€˜π‘†)𝑁) = ((1...𝑁)(reprβ€˜π‘†)𝑁))
212211sumeq1d 15653 . . 3 (πœ‘ β†’ Σ𝑐 ∈ (β„•(reprβ€˜π‘†)𝑁)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) = Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)𝑁)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)))
213204, 210, 2123eqtr4d 2776 . 2 (πœ‘ β†’ Ξ£π‘š ∈ (0...(𝑆 Β· 𝑁))∫(0(,)1)Σ𝑐 ∈ ((1...𝑁)(reprβ€˜π‘†)π‘š)(βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· ((π‘š βˆ’ 𝑁) Β· π‘₯)))) dπ‘₯ = Σ𝑐 ∈ (β„•(reprβ€˜π‘†)𝑁)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)))
21491, 142, 2133eqtrrd 2771 1 (πœ‘ β†’ Σ𝑐 ∈ (β„•(reprβ€˜π‘†)𝑁)βˆπ‘Ž ∈ (0..^𝑆)((πΏβ€˜π‘Ž)β€˜(π‘β€˜π‘Ž)) = ∫(0(,)1)(βˆπ‘Ž ∈ (0..^𝑆)(((πΏβ€˜π‘Ž)vts𝑁)β€˜π‘₯) Β· (expβ€˜((i Β· (2 Β· Ο€)) Β· (-𝑁 Β· π‘₯)))) dπ‘₯)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 395   ∨ wo 844   = wceq 1533   ∈ wcel 2098  βˆ€wral 3055  Vcvv 3468   βŠ† wss 3943  ifcif 4523  {csn 4623   class class class wbr 5141   ↦ cmpt 5224  dom cdm 5669  βŸΆwf 6533  β€˜cfv 6537  (class class class)co 7405   ↑m cmap 8822  Fincfn 8941  β„‚cc 11110  β„cr 11111  0cc0 11112  1c1 11113  ici 11114   + caddc 11115   Β· cmul 11117   ≀ cle 11253   βˆ’ cmin 11448  -cneg 11449  β„•cn 12216  2c2 12271  β„•0cn0 12476  β„€cz 12562  β„€β‰₯cuz 12826  (,)cioo 13330  [,]cicc 13333  ...cfz 13490  ..^cfzo 13633  Ξ£csu 15638  βˆcprod 15855  expce 16011  Ο€cpi 16016  β€“cnβ†’ccncf 24751  volcvol 25347  πΏ1cibl 25501  βˆ«citg 25502  reprcrepr 34149  vtscvts 34176
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 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722  ax-inf2 9638  ax-cc 10432  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190  ax-addf 11191
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  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 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-symdif 4237  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-uni 4903  df-int 4944  df-iun 4992  df-iin 4993  df-disj 5107  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-se 5625  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6294  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-of 7667  df-ofr 7668  df-om 7853  df-1st 7974  df-2nd 7975  df-supp 8147  df-frecs 8267  df-wrecs 8298  df-recs 8372  df-rdg 8411  df-1o 8467  df-2o 8468  df-oadd 8471  df-omul 8472  df-er 8705  df-map 8824  df-pm 8825  df-ixp 8894  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fsupp 9364  df-fi 9408  df-sup 9439  df-inf 9440  df-oi 9507  df-dju 9898  df-card 9936  df-acn 9939  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-2 12279  df-3 12280  df-4 12281  df-5 12282  df-6 12283  df-7 12284  df-8 12285  df-9 12286  df-n0 12477  df-z 12563  df-dec 12682  df-uz 12827  df-q 12937  df-rp 12981  df-xneg 13098  df-xadd 13099  df-xmul 13100  df-ioo 13334  df-ioc 13335  df-ico 13336  df-icc 13337  df-fz 13491  df-fzo 13634  df-fl 13763  df-mod 13841  df-seq 13973  df-exp 14033  df-fac 14239  df-bc 14268  df-hash 14296  df-shft 15020  df-cj 15052  df-re 15053  df-im 15054  df-sqrt 15188  df-abs 15189  df-limsup 15421  df-clim 15438  df-rlim 15439  df-sum 15639  df-prod 15856  df-ef 16017  df-sin 16019  df-cos 16020  df-pi 16022  df-struct 17089  df-sets 17106  df-slot 17124  df-ndx 17136  df-base 17154  df-ress 17183  df-plusg 17219  df-mulr 17220  df-starv 17221  df-sca 17222  df-vsca 17223  df-ip 17224  df-tset 17225  df-ple 17226  df-ds 17228  df-unif 17229  df-hom 17230  df-cco 17231  df-rest 17377  df-topn 17378  df-0g 17396  df-gsum 17397  df-topgen 17398  df-pt 17399  df-prds 17402  df-xrs 17457  df-qtop 17462  df-imas 17463  df-xps 17465  df-mre 17539  df-mrc 17540  df-acs 17542  df-mgm 18573  df-sgrp 18652  df-mnd 18668  df-submnd 18714  df-mulg 18996  df-cntz 19233  df-cmn 19702  df-psmet 21232  df-xmet 21233  df-met 21234  df-bl 21235  df-mopn 21236  df-fbas 21237  df-fg 21238  df-cnfld 21241  df-top 22751  df-topon 22768  df-topsp 22790  df-bases 22804  df-cld 22878  df-ntr 22879  df-cls 22880  df-nei 22957  df-lp 22995  df-perf 22996  df-cn 23086  df-cnp 23087  df-haus 23174  df-cmp 23246  df-tx 23421  df-hmeo 23614  df-fil 23705  df-fm 23797  df-flim 23798  df-flf 23799  df-xms 24181  df-ms 24182  df-tms 24183  df-cncf 24753  df-ovol 25348  df-vol 25349  df-mbf 25503  df-itg1 25504  df-itg2 25505  df-ibl 25506  df-itg 25507  df-0p 25554  df-limc 25750  df-dv 25751  df-repr 34150  df-vts 34177
This theorem is referenced by:  circlemethnat  34182  circlevma  34183  circlemethhgt  34184
  Copyright terms: Public domain W3C validator