Step | Hyp | Ref
| Expression |
1 | | circlemeth.n |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
2 | 1 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → 𝑁 ∈
ℕ0) |
3 | | ioossre 12551 |
. . . . . . . . 9
⊢ (0(,)1)
⊆ ℝ |
4 | | ax-resscn 10331 |
. . . . . . . . 9
⊢ ℝ
⊆ ℂ |
5 | 3, 4 | sstri 3830 |
. . . . . . . 8
⊢ (0(,)1)
⊆ ℂ |
6 | 5 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (0(,)1) ⊆
ℂ) |
7 | 6 | sselda 3821 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → 𝑥 ∈ ℂ) |
8 | | circlemeth.s |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ ℕ) |
9 | 8 | nnnn0d 11706 |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈
ℕ0) |
10 | 9 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → 𝑆 ∈
ℕ0) |
11 | | circlemeth.l |
. . . . . . 7
⊢ (𝜑 → 𝐿:(0..^𝑆)⟶(ℂ ↑𝑚
ℕ)) |
12 | 11 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → 𝐿:(0..^𝑆)⟶(ℂ ↑𝑚
ℕ)) |
13 | 2, 7, 10, 12 | vtsprod 31323 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → ∏𝑎 ∈ (0..^𝑆)(((𝐿‘𝑎)vts𝑁)‘𝑥) = Σ𝑚 ∈ (0...(𝑆 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · (𝑚
· 𝑥))))) |
14 | 13 | oveq1d 6939 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → (∏𝑎 ∈ (0..^𝑆)(((𝐿‘𝑎)vts𝑁)‘𝑥) · (exp‘((i · (2
· π)) · (-𝑁 · 𝑥)))) = (Σ𝑚 ∈ (0...(𝑆 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · (𝑚
· 𝑥)))) ·
(exp‘((i · (2 · π)) · (-𝑁 · 𝑥))))) |
15 | | fzfid 13095 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → (0...(𝑆 · 𝑁)) ∈ Fin) |
16 | | ax-icn 10333 |
. . . . . . . . 9
⊢ i ∈
ℂ |
17 | | 2cn 11454 |
. . . . . . . . . 10
⊢ 2 ∈
ℂ |
18 | | picn 24653 |
. . . . . . . . . 10
⊢ π
∈ ℂ |
19 | 17, 18 | mulcli 10386 |
. . . . . . . . 9
⊢ (2
· π) ∈ ℂ |
20 | 16, 19 | mulcli 10386 |
. . . . . . . 8
⊢ (i
· (2 · π)) ∈ ℂ |
21 | 20 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → (i · (2
· π)) ∈ ℂ) |
22 | 1 | nn0cnd 11708 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℂ) |
23 | 22 | negcld 10723 |
. . . . . . . . . 10
⊢ (𝜑 → -𝑁 ∈ ℂ) |
24 | 23 | ralrimivw 3149 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑥 ∈ (0(,)1)-𝑁 ∈ ℂ) |
25 | 24 | r19.21bi 3114 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → -𝑁 ∈ ℂ) |
26 | 25, 7 | mulcld 10399 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → (-𝑁 · 𝑥) ∈ ℂ) |
27 | 21, 26 | mulcld 10399 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → ((i · (2
· π)) · (-𝑁 · 𝑥)) ∈ ℂ) |
28 | 27 | efcld 31275 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → (exp‘((i
· (2 · π)) · (-𝑁 · 𝑥))) ∈ ℂ) |
29 | | fz1ssnn 12693 |
. . . . . . . 8
⊢
(1...𝑁) ⊆
ℕ |
30 | 29 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (1...𝑁) ⊆ ℕ) |
31 | | fzssz 12664 |
. . . . . . . . 9
⊢
(0...(𝑆 ·
𝑁)) ⊆
ℤ |
32 | | simpr 479 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → 𝑚 ∈ (0...(𝑆 · 𝑁))) |
33 | 31, 32 | sseldi 3819 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → 𝑚 ∈ ℤ) |
34 | 33 | adantlr 705 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → 𝑚 ∈ ℤ) |
35 | 10 | adantr 474 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → 𝑆 ∈
ℕ0) |
36 | | fzfid 13095 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (1...𝑁) ∈ Fin) |
37 | 30, 34, 35, 36 | reprfi 31300 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → ((1...𝑁)(repr‘𝑆)𝑚) ∈ Fin) |
38 | | fzofi 13096 |
. . . . . . . . 9
⊢
(0..^𝑆) ∈
Fin |
39 | 38 | a1i 11 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → (0..^𝑆) ∈ Fin) |
40 | 1 | ad3antrrr 720 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑁 ∈
ℕ0) |
41 | 9 | ad3antrrr 720 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑆 ∈
ℕ0) |
42 | 33 | zcnd 11839 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → 𝑚 ∈ ℂ) |
43 | 42 | ad2antrr 716 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑚 ∈ ℂ) |
44 | 11 | ad3antrrr 720 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) ∧ 𝑎 ∈ (0..^𝑆)) → 𝐿:(0..^𝑆)⟶(ℂ ↑𝑚
ℕ)) |
45 | | simpr 479 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆)) |
46 | 29 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → (1...𝑁) ⊆ ℕ) |
47 | 33 | adantr 474 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → 𝑚 ∈ ℤ) |
48 | 9 | ad2antrr 716 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → 𝑆 ∈
ℕ0) |
49 | | simpr 479 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) |
50 | 46, 47, 48, 49 | reprf 31296 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → 𝑐:(0..^𝑆)⟶(1...𝑁)) |
51 | 50 | ffvelrnda 6625 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑐‘𝑎) ∈ (1...𝑁)) |
52 | 29, 51 | sseldi 3819 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑐‘𝑎) ∈ ℕ) |
53 | 40, 41, 43, 44, 45, 52 | breprexplemb 31315 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝐿‘𝑎)‘(𝑐‘𝑎)) ∈ ℂ) |
54 | 53 | adantl3r 740 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝐿‘𝑎)‘(𝑐‘𝑎)) ∈ ℂ) |
55 | 39, 54 | fprodcl 15089 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → ∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) ∈ ℂ) |
56 | 20 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (i · (2 · π))
∈ ℂ) |
57 | 34 | zcnd 11839 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → 𝑚 ∈ ℂ) |
58 | 7 | adantr 474 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → 𝑥 ∈ ℂ) |
59 | 57, 58 | mulcld 10399 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (𝑚 · 𝑥) ∈ ℂ) |
60 | 56, 59 | mulcld 10399 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → ((i · (2 · π))
· (𝑚 · 𝑥)) ∈
ℂ) |
61 | 60 | efcld 31275 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (exp‘((i · (2
· π)) · (𝑚
· 𝑥))) ∈
ℂ) |
62 | 61 | adantr 474 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → (exp‘((i · (2 ·
π)) · (𝑚 ·
𝑥))) ∈
ℂ) |
63 | 55, 62 | mulcld 10399 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · (𝑚
· 𝑥)))) ∈
ℂ) |
64 | 37, 63 | fsumcl 14875 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · (𝑚
· 𝑥)))) ∈
ℂ) |
65 | 15, 28, 64 | fsummulc1 14925 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → (Σ𝑚 ∈ (0...(𝑆 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · (𝑚
· 𝑥)))) ·
(exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) = Σ𝑚 ∈ (0...(𝑆 · 𝑁))(Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · (𝑚
· 𝑥)))) ·
(exp‘((i · (2 · π)) · (-𝑁 · 𝑥))))) |
66 | 28 | adantr 474 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (exp‘((i · (2
· π)) · (-𝑁 · 𝑥))) ∈ ℂ) |
67 | 37, 66, 63 | fsummulc1 14925 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · (𝑚
· 𝑥)))) ·
(exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)((∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · (𝑚
· 𝑥)))) ·
(exp‘((i · (2 · π)) · (-𝑁 · 𝑥))))) |
68 | 66 | adantr 474 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → (exp‘((i · (2 ·
π)) · (-𝑁
· 𝑥))) ∈
ℂ) |
69 | 55, 62, 68 | mulassd 10402 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → ((∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · (𝑚
· 𝑥)))) ·
(exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) = (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · ((exp‘((i · (2
· π)) · (𝑚
· 𝑥))) ·
(exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))))) |
70 | 27 | adantr 474 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → ((i · (2 · π))
· (-𝑁 · 𝑥)) ∈
ℂ) |
71 | | efadd 15230 |
. . . . . . . . . . . 12
⊢ ((((i
· (2 · π)) · (𝑚 · 𝑥)) ∈ ℂ ∧ ((i · (2
· π)) · (-𝑁 · 𝑥)) ∈ ℂ) → (exp‘(((i
· (2 · π)) · (𝑚 · 𝑥)) + ((i · (2 · π)) ·
(-𝑁 · 𝑥)))) = ((exp‘((i ·
(2 · π)) · (𝑚 · 𝑥))) · (exp‘((i · (2
· π)) · (-𝑁 · 𝑥))))) |
72 | 60, 70, 71 | syl2anc 579 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (exp‘(((i · (2
· π)) · (𝑚
· 𝑥)) + ((i ·
(2 · π)) · (-𝑁 · 𝑥)))) = ((exp‘((i · (2 ·
π)) · (𝑚 ·
𝑥))) ·
(exp‘((i · (2 · π)) · (-𝑁 · 𝑥))))) |
73 | 26 | adantr 474 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (-𝑁 · 𝑥) ∈ ℂ) |
74 | 56, 59, 73 | adddid 10403 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → ((i · (2 · π))
· ((𝑚 · 𝑥) + (-𝑁 · 𝑥))) = (((i · (2 · π))
· (𝑚 · 𝑥)) + ((i · (2 ·
π)) · (-𝑁
· 𝑥)))) |
75 | 25 | adantr 474 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → -𝑁 ∈ ℂ) |
76 | 57, 75, 58 | adddird 10404 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → ((𝑚 + -𝑁) · 𝑥) = ((𝑚 · 𝑥) + (-𝑁 · 𝑥))) |
77 | 22 | ad2antrr 716 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → 𝑁 ∈ ℂ) |
78 | 57, 77 | negsubd 10742 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (𝑚 + -𝑁) = (𝑚 − 𝑁)) |
79 | 78 | oveq1d 6939 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → ((𝑚 + -𝑁) · 𝑥) = ((𝑚 − 𝑁) · 𝑥)) |
80 | 76, 79 | eqtr3d 2816 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → ((𝑚 · 𝑥) + (-𝑁 · 𝑥)) = ((𝑚 − 𝑁) · 𝑥)) |
81 | 80 | oveq2d 6940 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → ((i · (2 · π))
· ((𝑚 · 𝑥) + (-𝑁 · 𝑥))) = ((i · (2 · π))
· ((𝑚 − 𝑁) · 𝑥))) |
82 | 74, 81 | eqtr3d 2816 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (((i · (2 · π))
· (𝑚 · 𝑥)) + ((i · (2 ·
π)) · (-𝑁
· 𝑥))) = ((i
· (2 · π)) · ((𝑚 − 𝑁) · 𝑥))) |
83 | 82 | fveq2d 6452 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (exp‘(((i · (2
· π)) · (𝑚
· 𝑥)) + ((i ·
(2 · π)) · (-𝑁 · 𝑥)))) = (exp‘((i · (2 ·
π)) · ((𝑚 −
𝑁) · 𝑥)))) |
84 | 72, 83 | eqtr3d 2816 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → ((exp‘((i · (2
· π)) · (𝑚
· 𝑥))) ·
(exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) = (exp‘((i · (2 ·
π)) · ((𝑚 −
𝑁) · 𝑥)))) |
85 | 84 | oveq2d 6940 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · ((exp‘((i · (2
· π)) · (𝑚
· 𝑥))) ·
(exp‘((i · (2 · π)) · (-𝑁 · 𝑥))))) = (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥))))) |
86 | 85 | adantr 474 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · ((exp‘((i · (2
· π)) · (𝑚
· 𝑥))) ·
(exp‘((i · (2 · π)) · (-𝑁 · 𝑥))))) = (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥))))) |
87 | 69, 86 | eqtrd 2814 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → ((∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · (𝑚
· 𝑥)))) ·
(exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) = (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥))))) |
88 | 87 | sumeq2dv 14845 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)((∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · (𝑚
· 𝑥)))) ·
(exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥))))) |
89 | 67, 88 | eqtrd 2814 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · (𝑚
· 𝑥)))) ·
(exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥))))) |
90 | 89 | sumeq2dv 14845 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → Σ𝑚 ∈ (0...(𝑆 · 𝑁))(Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · (𝑚
· 𝑥)))) ·
(exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) = Σ𝑚 ∈ (0...(𝑆 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥))))) |
91 | 14, 65, 90 | 3eqtrd 2818 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → (∏𝑎 ∈ (0..^𝑆)(((𝐿‘𝑎)vts𝑁)‘𝑥) · (exp‘((i · (2
· π)) · (-𝑁 · 𝑥)))) = Σ𝑚 ∈ (0...(𝑆 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥))))) |
92 | 91 | itgeq2dv 23989 |
. 2
⊢ (𝜑 → ∫(0(,)1)(∏𝑎 ∈ (0..^𝑆)(((𝐿‘𝑎)vts𝑁)‘𝑥) · (exp‘((i · (2
· π)) · (-𝑁 · 𝑥)))) d𝑥 = ∫(0(,)1)Σ𝑚 ∈ (0...(𝑆 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥)))) d𝑥) |
93 | | ioombl 23773 |
. . . . 5
⊢ (0(,)1)
∈ dom vol |
94 | 93 | a1i 11 |
. . . 4
⊢ (𝜑 → (0(,)1) ∈ dom
vol) |
95 | | fzfid 13095 |
. . . 4
⊢ (𝜑 → (0...(𝑆 · 𝑁)) ∈ Fin) |
96 | | sumex 14830 |
. . . . 5
⊢
Σ𝑐 ∈
((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥)))) ∈ V |
97 | 96 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (0(,)1) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁)))) → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥)))) ∈ V) |
98 | 94 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (0(,)1) ∈ dom
vol) |
99 | 29 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (1...𝑁) ⊆ ℕ) |
100 | 9 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → 𝑆 ∈
ℕ0) |
101 | | fzfid 13095 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (1...𝑁) ∈ Fin) |
102 | 99, 33, 100, 101 | reprfi 31300 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → ((1...𝑁)(repr‘𝑆)𝑚) ∈ Fin) |
103 | 38 | a1i 11 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → (0..^𝑆) ∈ Fin) |
104 | 53 | adantllr 709 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝐿‘𝑎)‘(𝑐‘𝑎)) ∈ ℂ) |
105 | 103, 104 | fprodcl 15089 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → ∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) ∈ ℂ) |
106 | 57, 77 | subcld 10736 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (𝑚 − 𝑁) ∈ ℂ) |
107 | 106, 58 | mulcld 10399 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → ((𝑚 − 𝑁) · 𝑥) ∈ ℂ) |
108 | 56, 107 | mulcld 10399 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → ((i · (2 · π))
· ((𝑚 − 𝑁) · 𝑥)) ∈ ℂ) |
109 | 108 | an32s 642 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑥 ∈ (0(,)1)) → ((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥)) ∈ ℂ) |
110 | 109 | adantr 474 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → ((i · (2 · π))
· ((𝑚 − 𝑁) · 𝑥)) ∈ ℂ) |
111 | 110 | efcld 31275 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → (exp‘((i · (2 ·
π)) · ((𝑚 −
𝑁) · 𝑥))) ∈
ℂ) |
112 | 105, 111 | mulcld 10399 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥)))) ∈ ℂ) |
113 | 112 | anasss 460 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ (𝑥 ∈ (0(,)1) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚))) → (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥)))) ∈ ℂ) |
114 | 38 | a1i 11 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → (0..^𝑆) ∈ Fin) |
115 | 114, 53 | fprodcl 15089 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → ∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) ∈ ℂ) |
116 | | fvex 6461 |
. . . . . . . 8
⊢
(exp‘((i · (2 · π)) · ((𝑚 − 𝑁) · 𝑥))) ∈ V |
117 | 116 | a1i 11 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) ∧ 𝑥 ∈ (0(,)1)) → (exp‘((i
· (2 · π)) · ((𝑚 − 𝑁) · 𝑥))) ∈ V) |
118 | | ioossicc 12575 |
. . . . . . . . . 10
⊢ (0(,)1)
⊆ (0[,]1) |
119 | 118 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (0(,)1) ⊆
(0[,]1)) |
120 | 93 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (0(,)1) ∈ dom
vol) |
121 | 116 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑥 ∈ (0[,]1)) → (exp‘((i
· (2 · π)) · ((𝑚 − 𝑁) · 𝑥))) ∈ V) |
122 | | 0red 10382 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → 0 ∈
ℝ) |
123 | | 1red 10379 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → 1 ∈
ℝ) |
124 | 22 | adantr 474 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → 𝑁 ∈ ℂ) |
125 | 42, 124 | subcld 10736 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (𝑚 − 𝑁) ∈ ℂ) |
126 | | unitsscn 30544 |
. . . . . . . . . . . . . 14
⊢ (0[,]1)
⊆ ℂ |
127 | 126 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (0[,]1) ⊆
ℂ) |
128 | | ssidd 3843 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → ℂ ⊆
ℂ) |
129 | | cncfmptc 23126 |
. . . . . . . . . . . . 13
⊢ (((𝑚 − 𝑁) ∈ ℂ ∧ (0[,]1) ⊆
ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (0[,]1) ↦ (𝑚 − 𝑁)) ∈ ((0[,]1)–cn→ℂ)) |
130 | 125, 127,
128, 129 | syl3anc 1439 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (𝑥 ∈ (0[,]1) ↦ (𝑚 − 𝑁)) ∈ ((0[,]1)–cn→ℂ)) |
131 | | cncfmptid 23127 |
. . . . . . . . . . . . 13
⊢ (((0[,]1)
⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (0[,]1) ↦ 𝑥) ∈ ((0[,]1)–cn→ℂ)) |
132 | 127, 128,
131 | syl2anc 579 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (𝑥 ∈ (0[,]1) ↦ 𝑥) ∈ ((0[,]1)–cn→ℂ)) |
133 | 130, 132 | mulcncf 23654 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (𝑥 ∈ (0[,]1) ↦ ((𝑚 − 𝑁) · 𝑥)) ∈ ((0[,]1)–cn→ℂ)) |
134 | 133 | efmul2picn 31280 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (𝑥 ∈ (0[,]1) ↦ (exp‘((i
· (2 · π)) · ((𝑚 − 𝑁) · 𝑥)))) ∈ ((0[,]1)–cn→ℂ)) |
135 | | cniccibl 24048 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ ∧ 1 ∈ ℝ ∧ (𝑥 ∈ (0[,]1) ↦ (exp‘((i
· (2 · π)) · ((𝑚 − 𝑁) · 𝑥)))) ∈ ((0[,]1)–cn→ℂ)) → (𝑥 ∈ (0[,]1) ↦ (exp‘((i
· (2 · π)) · ((𝑚 − 𝑁) · 𝑥)))) ∈
𝐿1) |
136 | 122, 123,
134, 135 | syl3anc 1439 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (𝑥 ∈ (0[,]1) ↦ (exp‘((i
· (2 · π)) · ((𝑚 − 𝑁) · 𝑥)))) ∈
𝐿1) |
137 | 119, 120,
121, 136 | iblss 24012 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (𝑥 ∈ (0(,)1) ↦ (exp‘((i
· (2 · π)) · ((𝑚 − 𝑁) · 𝑥)))) ∈
𝐿1) |
138 | 137 | adantr 474 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → (𝑥 ∈ (0(,)1) ↦ (exp‘((i
· (2 · π)) · ((𝑚 − 𝑁) · 𝑥)))) ∈
𝐿1) |
139 | 115, 117,
138 | iblmulc2 24038 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → (𝑥 ∈ (0(,)1) ↦ (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥))))) ∈
𝐿1) |
140 | 98, 102, 113, 139 | itgfsum 24034 |
. . . . 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𝑥)) |
141 | 140 | simpld 490 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (𝑥 ∈ (0(,)1) ↦ Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥))))) ∈
𝐿1) |
142 | 94, 95, 97, 141 | itgfsum 24034 |
. . 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𝑥)) |
143 | 142 | simprd 491 |
. 2
⊢ (𝜑 → ∫(0(,)1)Σ𝑚 ∈ (0...(𝑆 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥)))) d𝑥 = Σ𝑚 ∈ (0...(𝑆 · 𝑁))∫(0(,)1)Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥)))) d𝑥) |
144 | | oveq2 6932 |
. . . . . . 7
⊢
(if((𝑚 − 𝑁) = 0, 1, 0) = 1 →
(Σ𝑐 ∈
((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · if((𝑚 − 𝑁) = 0, 1, 0)) = (Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · 1)) |
145 | | oveq2 6932 |
. . . . . . 7
⊢
(if((𝑚 − 𝑁) = 0, 1, 0) = 0 →
(Σ𝑐 ∈
((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · if((𝑚 − 𝑁) = 0, 1, 0)) = (Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · 0)) |
146 | 102, 115 | fsumcl 14875 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) ∈ ℂ) |
147 | 146 | mulid1d 10396 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · 1) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎))) |
148 | 146 | mul01d 10577 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · 0) = 0) |
149 | 144, 145,
147, 148 | ifeq3da 29932 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → if((𝑚 − 𝑁) = 0, Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)), 0) = (Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · if((𝑚 − 𝑁) = 0, 1, 0))) |
150 | 42, 124 | subeq0ad 10746 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → ((𝑚 − 𝑁) = 0 ↔ 𝑚 = 𝑁)) |
151 | | velsn 4414 |
. . . . . . . 8
⊢ (𝑚 ∈ {𝑁} ↔ 𝑚 = 𝑁) |
152 | 150, 151 | syl6rbbr 282 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (𝑚 ∈ {𝑁} ↔ (𝑚 − 𝑁) = 0)) |
153 | 152 | ifbid 4329 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → if(𝑚 ∈ {𝑁}, Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)), 0) = if((𝑚 − 𝑁) = 0, Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)), 0)) |
154 | 1 | nn0zd 11836 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℤ) |
155 | 154 | ad2antrr 716 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → 𝑁 ∈ ℤ) |
156 | 47, 155 | zsubcld 11843 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → (𝑚 − 𝑁) ∈ ℤ) |
157 | | itgexpif 31290 |
. . . . . . . . . 10
⊢ ((𝑚 − 𝑁) ∈ ℤ →
∫(0(,)1)(exp‘((i · (2 · π)) · ((𝑚 − 𝑁) · 𝑥))) d𝑥 = if((𝑚 − 𝑁) = 0, 1, 0)) |
158 | 156, 157 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → ∫(0(,)1)(exp‘((i ·
(2 · π)) · ((𝑚 − 𝑁) · 𝑥))) d𝑥 = if((𝑚 − 𝑁) = 0, 1, 0)) |
159 | 158 | oveq2d 6940 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · ∫(0(,)1)(exp‘((i
· (2 · π)) · ((𝑚 − 𝑁) · 𝑥))) d𝑥) = (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · if((𝑚 − 𝑁) = 0, 1, 0))) |
160 | 159 | sumeq2dv 14845 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · ∫(0(,)1)(exp‘((i
· (2 · π)) · ((𝑚 − 𝑁) · 𝑥))) d𝑥) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · if((𝑚 − 𝑁) = 0, 1, 0))) |
161 | | 1cnd 10373 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → 1 ∈
ℂ) |
162 | | 0cnd 10371 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → 0 ∈
ℂ) |
163 | 161, 162 | ifcld 4352 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → if((𝑚 − 𝑁) = 0, 1, 0) ∈
ℂ) |
164 | 102, 163,
115 | fsummulc1 14925 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · if((𝑚 − 𝑁) = 0, 1, 0)) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · if((𝑚 − 𝑁) = 0, 1, 0))) |
165 | 160, 164 | eqtr4d 2817 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · ∫(0(,)1)(exp‘((i
· (2 · π)) · ((𝑚 − 𝑁) · 𝑥))) d𝑥) = (Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · if((𝑚 − 𝑁) = 0, 1, 0))) |
166 | 149, 153,
165 | 3eqtr4rd 2825 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · ∫(0(,)1)(exp‘((i
· (2 · π)) · ((𝑚 − 𝑁) · 𝑥))) d𝑥) = if(𝑚 ∈ {𝑁}, Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)), 0)) |
167 | 166 | sumeq2dv 14845 |
. . . 4
⊢ (𝜑 → Σ𝑚 ∈ (0...(𝑆 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · ∫(0(,)1)(exp‘((i
· (2 · π)) · ((𝑚 − 𝑁) · 𝑥))) d𝑥) = Σ𝑚 ∈ (0...(𝑆 · 𝑁))if(𝑚 ∈ {𝑁}, Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)), 0)) |
168 | | 0zd 11744 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℤ) |
169 | 9 | nn0zd 11836 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ ℤ) |
170 | 169, 154 | zmulcld 11844 |
. . . . . . 7
⊢ (𝜑 → (𝑆 · 𝑁) ∈ ℤ) |
171 | 1 | nn0ge0d 11709 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ 𝑁) |
172 | | nnmulge 30084 |
. . . . . . . 8
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ 𝑁 ≤ (𝑆 · 𝑁)) |
173 | 8, 1, 172 | syl2anc 579 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ≤ (𝑆 · 𝑁)) |
174 | | elfz4 12656 |
. . . . . . 7
⊢ (((0
∈ ℤ ∧ (𝑆
· 𝑁) ∈ ℤ
∧ 𝑁 ∈ ℤ)
∧ (0 ≤ 𝑁 ∧ 𝑁 ≤ (𝑆 · 𝑁))) → 𝑁 ∈ (0...(𝑆 · 𝑁))) |
175 | 168, 170,
154, 171, 173, 174 | syl32anc 1446 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ (0...(𝑆 · 𝑁))) |
176 | 175 | snssd 4573 |
. . . . 5
⊢ (𝜑 → {𝑁} ⊆ (0...(𝑆 · 𝑁))) |
177 | 176 | sselda 3821 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ {𝑁}) → 𝑚 ∈ (0...(𝑆 · 𝑁))) |
178 | 177, 146 | syldan 585 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ {𝑁}) → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) ∈ ℂ) |
179 | 178 | ralrimiva 3148 |
. . . . 5
⊢ (𝜑 → ∀𝑚 ∈ {𝑁}Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) ∈ ℂ) |
180 | 95 | olcd 863 |
. . . . 5
⊢ (𝜑 → ((0...(𝑆 · 𝑁)) ⊆ (ℤ≥‘0)
∨ (0...(𝑆 · 𝑁)) ∈ Fin)) |
181 | | sumss2 14868 |
. . . . 5
⊢ ((({𝑁} ⊆ (0...(𝑆 · 𝑁)) ∧ ∀𝑚 ∈ {𝑁}Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) ∈ ℂ) ∧ ((0...(𝑆 · 𝑁)) ⊆ (ℤ≥‘0)
∨ (0...(𝑆 · 𝑁)) ∈ Fin)) →
Σ𝑚 ∈ {𝑁}Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) = Σ𝑚 ∈ (0...(𝑆 · 𝑁))if(𝑚 ∈ {𝑁}, Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)), 0)) |
182 | 176, 179,
180, 181 | syl21anc 828 |
. . . 4
⊢ (𝜑 → Σ𝑚 ∈ {𝑁}Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) = Σ𝑚 ∈ (0...(𝑆 · 𝑁))if(𝑚 ∈ {𝑁}, Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)), 0)) |
183 | 29 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (1...𝑁) ⊆ ℕ) |
184 | | fzfid 13095 |
. . . . . . 7
⊢ (𝜑 → (1...𝑁) ∈ Fin) |
185 | 183, 154,
9, 184 | reprfi 31300 |
. . . . . 6
⊢ (𝜑 → ((1...𝑁)(repr‘𝑆)𝑁) ∈ Fin) |
186 | 38 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)) → (0..^𝑆) ∈ Fin) |
187 | 1 | ad2antrr 716 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑁 ∈
ℕ0) |
188 | 9 | ad2antrr 716 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑆 ∈
ℕ0) |
189 | 22 | ad2antrr 716 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑁 ∈ ℂ) |
190 | 11 | ad2antrr 716 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)) ∧ 𝑎 ∈ (0..^𝑆)) → 𝐿:(0..^𝑆)⟶(ℂ ↑𝑚
ℕ)) |
191 | | simpr 479 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆)) |
192 | 29 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)) → (1...𝑁) ⊆ ℕ) |
193 | 154 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)) → 𝑁 ∈ ℤ) |
194 | 9 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)) → 𝑆 ∈
ℕ0) |
195 | | simpr 479 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)) → 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)) |
196 | 192, 193,
194, 195 | reprf 31296 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)) → 𝑐:(0..^𝑆)⟶(1...𝑁)) |
197 | 196 | ffvelrnda 6625 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑐‘𝑎) ∈ (1...𝑁)) |
198 | 29, 197 | sseldi 3819 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑐‘𝑎) ∈ ℕ) |
199 | 187, 188,
189, 190, 191, 198 | breprexplemb 31315 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝐿‘𝑎)‘(𝑐‘𝑎)) ∈ ℂ) |
200 | 186, 199 | fprodcl 15089 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)) → ∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) ∈ ℂ) |
201 | 185, 200 | fsumcl 14875 |
. . . . 5
⊢ (𝜑 → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) ∈ ℂ) |
202 | | oveq2 6932 |
. . . . . . 7
⊢ (𝑚 = 𝑁 → ((1...𝑁)(repr‘𝑆)𝑚) = ((1...𝑁)(repr‘𝑆)𝑁)) |
203 | 202 | sumeq1d 14843 |
. . . . . 6
⊢ (𝑚 = 𝑁 → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎))) |
204 | 203 | sumsn 14886 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ Σ𝑐 ∈
((1...𝑁)(repr‘𝑆)𝑁)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) ∈ ℂ) → Σ𝑚 ∈ {𝑁}Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎))) |
205 | 1, 201, 204 | syl2anc 579 |
. . . 4
⊢ (𝜑 → Σ𝑚 ∈ {𝑁}Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎))) |
206 | 167, 182,
205 | 3eqtr2d 2820 |
. . 3
⊢ (𝜑 → Σ𝑚 ∈ (0...(𝑆 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · ∫(0(,)1)(exp‘((i
· (2 · π)) · ((𝑚 − 𝑁) · 𝑥))) d𝑥) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎))) |
207 | 140 | simprd 491 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → ∫(0(,)1)Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥)))) d𝑥 = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∫(0(,)1)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥)))) d𝑥) |
208 | 111 | an32s 642 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) ∧ 𝑥 ∈ (0(,)1)) → (exp‘((i
· (2 · π)) · ((𝑚 − 𝑁) · 𝑥))) ∈ ℂ) |
209 | 115, 208,
138 | itgmulc2 24041 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · ∫(0(,)1)(exp‘((i
· (2 · π)) · ((𝑚 − 𝑁) · 𝑥))) d𝑥) = ∫(0(,)1)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥)))) d𝑥) |
210 | 209 | sumeq2dv 14845 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · ∫(0(,)1)(exp‘((i
· (2 · π)) · ((𝑚 − 𝑁) · 𝑥))) d𝑥) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∫(0(,)1)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥)))) d𝑥) |
211 | 207, 210 | eqtr4d 2817 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → ∫(0(,)1)Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥)))) d𝑥 = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · ∫(0(,)1)(exp‘((i
· (2 · π)) · ((𝑚 − 𝑁) · 𝑥))) d𝑥)) |
212 | 211 | sumeq2dv 14845 |
. . 3
⊢ (𝜑 → Σ𝑚 ∈ (0...(𝑆 · 𝑁))∫(0(,)1)Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥)))) d𝑥 = Σ𝑚 ∈ (0...(𝑆 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · ∫(0(,)1)(exp‘((i
· (2 · π)) · ((𝑚 − 𝑁) · 𝑥))) d𝑥)) |
213 | 1, 9 | reprfz1 31308 |
. . . 4
⊢ (𝜑 → (ℕ(repr‘𝑆)𝑁) = ((1...𝑁)(repr‘𝑆)𝑁)) |
214 | 213 | sumeq1d 14843 |
. . 3
⊢ (𝜑 → Σ𝑐 ∈ (ℕ(repr‘𝑆)𝑁)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎))) |
215 | 206, 212,
214 | 3eqtr4d 2824 |
. 2
⊢ (𝜑 → Σ𝑚 ∈ (0...(𝑆 · 𝑁))∫(0(,)1)Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥)))) d𝑥 = Σ𝑐 ∈ (ℕ(repr‘𝑆)𝑁)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎))) |
216 | 92, 143, 215 | 3eqtrrd 2819 |
1
⊢ (𝜑 → Σ𝑐 ∈ (ℕ(repr‘𝑆)𝑁)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) = ∫(0(,)1)(∏𝑎 ∈ (0..^𝑆)(((𝐿‘𝑎)vts𝑁)‘𝑥) · (exp‘((i · (2
· π)) · (-𝑁 · 𝑥)))) d𝑥) |