| Step | Hyp | Ref
| Expression |
| 1 | | circlemeth.n |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
| 2 | 1 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → 𝑁 ∈
ℕ0) |
| 3 | | ioossre 13448 |
. . . . . . . . 9
⊢ (0(,)1)
⊆ ℝ |
| 4 | | ax-resscn 11212 |
. . . . . . . . 9
⊢ ℝ
⊆ ℂ |
| 5 | 3, 4 | sstri 3993 |
. . . . . . . 8
⊢ (0(,)1)
⊆ ℂ |
| 6 | 5 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (0(,)1) ⊆
ℂ) |
| 7 | 6 | sselda 3983 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → 𝑥 ∈ ℂ) |
| 8 | | circlemeth.s |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ ℕ) |
| 9 | 8 | nnnn0d 12587 |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈
ℕ0) |
| 10 | 9 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → 𝑆 ∈
ℕ0) |
| 11 | | circlemeth.l |
. . . . . . 7
⊢ (𝜑 → 𝐿:(0..^𝑆)⟶(ℂ ↑m
ℕ)) |
| 12 | 11 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m
ℕ)) |
| 13 | 2, 7, 10, 12 | vtsprod 34654 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → ∏𝑎 ∈ (0..^𝑆)(((𝐿‘𝑎)vts𝑁)‘𝑥) = Σ𝑚 ∈ (0...(𝑆 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · (𝑚
· 𝑥))))) |
| 14 | 13 | oveq1d 7446 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → (∏𝑎 ∈ (0..^𝑆)(((𝐿‘𝑎)vts𝑁)‘𝑥) · (exp‘((i · (2
· π)) · (-𝑁 · 𝑥)))) = (Σ𝑚 ∈ (0...(𝑆 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · (𝑚
· 𝑥)))) ·
(exp‘((i · (2 · π)) · (-𝑁 · 𝑥))))) |
| 15 | | fzfid 14014 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → (0...(𝑆 · 𝑁)) ∈ Fin) |
| 16 | | ax-icn 11214 |
. . . . . . . . 9
⊢ i ∈
ℂ |
| 17 | | 2cn 12341 |
. . . . . . . . . 10
⊢ 2 ∈
ℂ |
| 18 | | picn 26501 |
. . . . . . . . . 10
⊢ π
∈ ℂ |
| 19 | 17, 18 | mulcli 11268 |
. . . . . . . . 9
⊢ (2
· π) ∈ ℂ |
| 20 | 16, 19 | mulcli 11268 |
. . . . . . . 8
⊢ (i
· (2 · π)) ∈ ℂ |
| 21 | 20 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → (i · (2
· π)) ∈ ℂ) |
| 22 | 1 | nn0cnd 12589 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℂ) |
| 23 | 22 | negcld 11607 |
. . . . . . . . . 10
⊢ (𝜑 → -𝑁 ∈ ℂ) |
| 24 | 23 | ralrimivw 3150 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑥 ∈ (0(,)1)-𝑁 ∈ ℂ) |
| 25 | 24 | r19.21bi 3251 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → -𝑁 ∈ ℂ) |
| 26 | 25, 7 | mulcld 11281 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → (-𝑁 · 𝑥) ∈ ℂ) |
| 27 | 21, 26 | mulcld 11281 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → ((i · (2
· π)) · (-𝑁 · 𝑥)) ∈ ℂ) |
| 28 | 27 | efcld 16119 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → (exp‘((i
· (2 · π)) · (-𝑁 · 𝑥))) ∈ ℂ) |
| 29 | | fz1ssnn 13595 |
. . . . . . . 8
⊢
(1...𝑁) ⊆
ℕ |
| 30 | 29 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (1...𝑁) ⊆ ℕ) |
| 31 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → 𝑚 ∈ (0...(𝑆 · 𝑁))) |
| 32 | 31 | elfzelzd 13565 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → 𝑚 ∈ ℤ) |
| 33 | 32 | adantlr 715 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → 𝑚 ∈ ℤ) |
| 34 | 10 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → 𝑆 ∈
ℕ0) |
| 35 | | fzfid 14014 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (1...𝑁) ∈ Fin) |
| 36 | 30, 33, 34, 35 | reprfi 34631 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → ((1...𝑁)(repr‘𝑆)𝑚) ∈ Fin) |
| 37 | | fzofi 14015 |
. . . . . . . . 9
⊢
(0..^𝑆) ∈
Fin |
| 38 | 37 | a1i 11 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → (0..^𝑆) ∈ Fin) |
| 39 | 1 | ad3antrrr 730 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑁 ∈
ℕ0) |
| 40 | 9 | ad3antrrr 730 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑆 ∈
ℕ0) |
| 41 | 32 | zcnd 12723 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → 𝑚 ∈ ℂ) |
| 42 | 41 | ad2antrr 726 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑚 ∈ ℂ) |
| 43 | 11 | ad3antrrr 730 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) ∧ 𝑎 ∈ (0..^𝑆)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m
ℕ)) |
| 44 | | simpr 484 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆)) |
| 45 | 29 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → (1...𝑁) ⊆ ℕ) |
| 46 | 32 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → 𝑚 ∈ ℤ) |
| 47 | 9 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → 𝑆 ∈
ℕ0) |
| 48 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) |
| 49 | 45, 46, 47, 48 | reprf 34627 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → 𝑐:(0..^𝑆)⟶(1...𝑁)) |
| 50 | 49 | ffvelcdmda 7104 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑐‘𝑎) ∈ (1...𝑁)) |
| 51 | 29, 50 | sselid 3981 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑐‘𝑎) ∈ ℕ) |
| 52 | 39, 40, 42, 43, 44, 51 | breprexplemb 34646 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝐿‘𝑎)‘(𝑐‘𝑎)) ∈ ℂ) |
| 53 | 52 | adantl3r 750 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝐿‘𝑎)‘(𝑐‘𝑎)) ∈ ℂ) |
| 54 | 38, 53 | fprodcl 15988 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → ∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) ∈ ℂ) |
| 55 | 20 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (i · (2 · π))
∈ ℂ) |
| 56 | 33 | zcnd 12723 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → 𝑚 ∈ ℂ) |
| 57 | 7 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → 𝑥 ∈ ℂ) |
| 58 | 56, 57 | mulcld 11281 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (𝑚 · 𝑥) ∈ ℂ) |
| 59 | 55, 58 | mulcld 11281 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → ((i · (2 · π))
· (𝑚 · 𝑥)) ∈
ℂ) |
| 60 | 59 | efcld 16119 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (exp‘((i · (2
· π)) · (𝑚
· 𝑥))) ∈
ℂ) |
| 61 | 60 | adantr 480 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → (exp‘((i · (2 ·
π)) · (𝑚 ·
𝑥))) ∈
ℂ) |
| 62 | 54, 61 | mulcld 11281 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · (𝑚
· 𝑥)))) ∈
ℂ) |
| 63 | 36, 62 | fsumcl 15769 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · (𝑚
· 𝑥)))) ∈
ℂ) |
| 64 | 15, 28, 63 | fsummulc1 15821 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → (Σ𝑚 ∈ (0...(𝑆 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · (𝑚
· 𝑥)))) ·
(exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) = Σ𝑚 ∈ (0...(𝑆 · 𝑁))(Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · (𝑚
· 𝑥)))) ·
(exp‘((i · (2 · π)) · (-𝑁 · 𝑥))))) |
| 65 | 28 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (exp‘((i · (2
· π)) · (-𝑁 · 𝑥))) ∈ ℂ) |
| 66 | 36, 65, 62 | fsummulc1 15821 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · (𝑚
· 𝑥)))) ·
(exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)((∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · (𝑚
· 𝑥)))) ·
(exp‘((i · (2 · π)) · (-𝑁 · 𝑥))))) |
| 67 | 65 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → (exp‘((i · (2 ·
π)) · (-𝑁
· 𝑥))) ∈
ℂ) |
| 68 | 54, 61, 67 | mulassd 11284 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → ((∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · (𝑚
· 𝑥)))) ·
(exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) = (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · ((exp‘((i · (2
· π)) · (𝑚
· 𝑥))) ·
(exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))))) |
| 69 | 27 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → ((i · (2 · π))
· (-𝑁 · 𝑥)) ∈
ℂ) |
| 70 | | efadd 16130 |
. . . . . . . . . . . 12
⊢ ((((i
· (2 · π)) · (𝑚 · 𝑥)) ∈ ℂ ∧ ((i · (2
· π)) · (-𝑁 · 𝑥)) ∈ ℂ) → (exp‘(((i
· (2 · π)) · (𝑚 · 𝑥)) + ((i · (2 · π)) ·
(-𝑁 · 𝑥)))) = ((exp‘((i ·
(2 · π)) · (𝑚 · 𝑥))) · (exp‘((i · (2
· π)) · (-𝑁 · 𝑥))))) |
| 71 | 59, 69, 70 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (exp‘(((i · (2
· π)) · (𝑚
· 𝑥)) + ((i ·
(2 · π)) · (-𝑁 · 𝑥)))) = ((exp‘((i · (2 ·
π)) · (𝑚 ·
𝑥))) ·
(exp‘((i · (2 · π)) · (-𝑁 · 𝑥))))) |
| 72 | 26 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (-𝑁 · 𝑥) ∈ ℂ) |
| 73 | 55, 58, 72 | adddid 11285 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → ((i · (2 · π))
· ((𝑚 · 𝑥) + (-𝑁 · 𝑥))) = (((i · (2 · π))
· (𝑚 · 𝑥)) + ((i · (2 ·
π)) · (-𝑁
· 𝑥)))) |
| 74 | 25 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → -𝑁 ∈ ℂ) |
| 75 | 56, 74, 57 | adddird 11286 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → ((𝑚 + -𝑁) · 𝑥) = ((𝑚 · 𝑥) + (-𝑁 · 𝑥))) |
| 76 | 22 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → 𝑁 ∈ ℂ) |
| 77 | 56, 76 | negsubd 11626 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (𝑚 + -𝑁) = (𝑚 − 𝑁)) |
| 78 | 77 | oveq1d 7446 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → ((𝑚 + -𝑁) · 𝑥) = ((𝑚 − 𝑁) · 𝑥)) |
| 79 | 75, 78 | eqtr3d 2779 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → ((𝑚 · 𝑥) + (-𝑁 · 𝑥)) = ((𝑚 − 𝑁) · 𝑥)) |
| 80 | 79 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → ((i · (2 · π))
· ((𝑚 · 𝑥) + (-𝑁 · 𝑥))) = ((i · (2 · π))
· ((𝑚 − 𝑁) · 𝑥))) |
| 81 | 73, 80 | eqtr3d 2779 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (((i · (2 · π))
· (𝑚 · 𝑥)) + ((i · (2 ·
π)) · (-𝑁
· 𝑥))) = ((i
· (2 · π)) · ((𝑚 − 𝑁) · 𝑥))) |
| 82 | 81 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (exp‘(((i · (2
· π)) · (𝑚
· 𝑥)) + ((i ·
(2 · π)) · (-𝑁 · 𝑥)))) = (exp‘((i · (2 ·
π)) · ((𝑚 −
𝑁) · 𝑥)))) |
| 83 | 71, 82 | eqtr3d 2779 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → ((exp‘((i · (2
· π)) · (𝑚
· 𝑥))) ·
(exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) = (exp‘((i · (2 ·
π)) · ((𝑚 −
𝑁) · 𝑥)))) |
| 84 | 83 | oveq2d 7447 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · ((exp‘((i · (2
· π)) · (𝑚
· 𝑥))) ·
(exp‘((i · (2 · π)) · (-𝑁 · 𝑥))))) = (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥))))) |
| 85 | 84 | adantr 480 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · ((exp‘((i · (2
· π)) · (𝑚
· 𝑥))) ·
(exp‘((i · (2 · π)) · (-𝑁 · 𝑥))))) = (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥))))) |
| 86 | 68, 85 | eqtrd 2777 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → ((∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · (𝑚
· 𝑥)))) ·
(exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) = (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥))))) |
| 87 | 86 | sumeq2dv 15738 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)((∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · (𝑚
· 𝑥)))) ·
(exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥))))) |
| 88 | 66, 87 | eqtrd 2777 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · (𝑚
· 𝑥)))) ·
(exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥))))) |
| 89 | 88 | sumeq2dv 15738 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → Σ𝑚 ∈ (0...(𝑆 · 𝑁))(Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · (𝑚
· 𝑥)))) ·
(exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) = Σ𝑚 ∈ (0...(𝑆 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥))))) |
| 90 | 14, 64, 89 | 3eqtrd 2781 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → (∏𝑎 ∈ (0..^𝑆)(((𝐿‘𝑎)vts𝑁)‘𝑥) · (exp‘((i · (2
· π)) · (-𝑁 · 𝑥)))) = Σ𝑚 ∈ (0...(𝑆 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥))))) |
| 91 | 90 | itgeq2dv 25817 |
. 2
⊢ (𝜑 → ∫(0(,)1)(∏𝑎 ∈ (0..^𝑆)(((𝐿‘𝑎)vts𝑁)‘𝑥) · (exp‘((i · (2
· π)) · (-𝑁 · 𝑥)))) d𝑥 = ∫(0(,)1)Σ𝑚 ∈ (0...(𝑆 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥)))) d𝑥) |
| 92 | | ioombl 25600 |
. . . . 5
⊢ (0(,)1)
∈ dom vol |
| 93 | 92 | a1i 11 |
. . . 4
⊢ (𝜑 → (0(,)1) ∈ dom
vol) |
| 94 | | fzfid 14014 |
. . . 4
⊢ (𝜑 → (0...(𝑆 · 𝑁)) ∈ Fin) |
| 95 | | sumex 15724 |
. . . . 5
⊢
Σ𝑐 ∈
((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥)))) ∈ V |
| 96 | 95 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (0(,)1) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁)))) → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥)))) ∈ V) |
| 97 | 93 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (0(,)1) ∈ dom
vol) |
| 98 | 29 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (1...𝑁) ⊆ ℕ) |
| 99 | 9 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → 𝑆 ∈
ℕ0) |
| 100 | | fzfid 14014 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (1...𝑁) ∈ Fin) |
| 101 | 98, 32, 99, 100 | reprfi 34631 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → ((1...𝑁)(repr‘𝑆)𝑚) ∈ Fin) |
| 102 | 37 | a1i 11 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → (0..^𝑆) ∈ Fin) |
| 103 | 52 | adantllr 719 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝐿‘𝑎)‘(𝑐‘𝑎)) ∈ ℂ) |
| 104 | 102, 103 | fprodcl 15988 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → ∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) ∈ ℂ) |
| 105 | 56, 76 | subcld 11620 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (𝑚 − 𝑁) ∈ ℂ) |
| 106 | 105, 57 | mulcld 11281 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → ((𝑚 − 𝑁) · 𝑥) ∈ ℂ) |
| 107 | 55, 106 | mulcld 11281 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → ((i · (2 · π))
· ((𝑚 − 𝑁) · 𝑥)) ∈ ℂ) |
| 108 | 107 | an32s 652 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑥 ∈ (0(,)1)) → ((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥)) ∈ ℂ) |
| 109 | 108 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → ((i · (2 · π))
· ((𝑚 − 𝑁) · 𝑥)) ∈ ℂ) |
| 110 | 109 | efcld 16119 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → (exp‘((i · (2 ·
π)) · ((𝑚 −
𝑁) · 𝑥))) ∈
ℂ) |
| 111 | 104, 110 | mulcld 11281 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥)))) ∈ ℂ) |
| 112 | 111 | anasss 466 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ (𝑥 ∈ (0(,)1) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚))) → (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥)))) ∈ ℂ) |
| 113 | 37 | a1i 11 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → (0..^𝑆) ∈ Fin) |
| 114 | 113, 52 | fprodcl 15988 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → ∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) ∈ ℂ) |
| 115 | | fvex 6919 |
. . . . . . . 8
⊢
(exp‘((i · (2 · π)) · ((𝑚 − 𝑁) · 𝑥))) ∈ V |
| 116 | 115 | a1i 11 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) ∧ 𝑥 ∈ (0(,)1)) → (exp‘((i
· (2 · π)) · ((𝑚 − 𝑁) · 𝑥))) ∈ V) |
| 117 | | ioossicc 13473 |
. . . . . . . . . 10
⊢ (0(,)1)
⊆ (0[,]1) |
| 118 | 117 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (0(,)1) ⊆
(0[,]1)) |
| 119 | 92 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (0(,)1) ∈ dom
vol) |
| 120 | 115 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑥 ∈ (0[,]1)) → (exp‘((i
· (2 · π)) · ((𝑚 − 𝑁) · 𝑥))) ∈ V) |
| 121 | | 0red 11264 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → 0 ∈
ℝ) |
| 122 | | 1red 11262 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → 1 ∈
ℝ) |
| 123 | 22 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → 𝑁 ∈ ℂ) |
| 124 | 41, 123 | subcld 11620 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (𝑚 − 𝑁) ∈ ℂ) |
| 125 | | unitsscn 13540 |
. . . . . . . . . . . . . 14
⊢ (0[,]1)
⊆ ℂ |
| 126 | 125 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (0[,]1) ⊆
ℂ) |
| 127 | | ssidd 4007 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → ℂ ⊆
ℂ) |
| 128 | | cncfmptc 24938 |
. . . . . . . . . . . . 13
⊢ (((𝑚 − 𝑁) ∈ ℂ ∧ (0[,]1) ⊆
ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (0[,]1) ↦ (𝑚 − 𝑁)) ∈ ((0[,]1)–cn→ℂ)) |
| 129 | 124, 126,
127, 128 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (𝑥 ∈ (0[,]1) ↦ (𝑚 − 𝑁)) ∈ ((0[,]1)–cn→ℂ)) |
| 130 | | cncfmptid 24939 |
. . . . . . . . . . . . 13
⊢ (((0[,]1)
⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (0[,]1) ↦ 𝑥) ∈ ((0[,]1)–cn→ℂ)) |
| 131 | 126, 127,
130 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (𝑥 ∈ (0[,]1) ↦ 𝑥) ∈ ((0[,]1)–cn→ℂ)) |
| 132 | 129, 131 | mulcncf 25480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (𝑥 ∈ (0[,]1) ↦ ((𝑚 − 𝑁) · 𝑥)) ∈ ((0[,]1)–cn→ℂ)) |
| 133 | 132 | efmul2picn 34611 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (𝑥 ∈ (0[,]1) ↦ (exp‘((i
· (2 · π)) · ((𝑚 − 𝑁) · 𝑥)))) ∈ ((0[,]1)–cn→ℂ)) |
| 134 | | cniccibl 25876 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ ∧ 1 ∈ ℝ ∧ (𝑥 ∈ (0[,]1) ↦ (exp‘((i
· (2 · π)) · ((𝑚 − 𝑁) · 𝑥)))) ∈ ((0[,]1)–cn→ℂ)) → (𝑥 ∈ (0[,]1) ↦ (exp‘((i
· (2 · π)) · ((𝑚 − 𝑁) · 𝑥)))) ∈
𝐿1) |
| 135 | 121, 122,
133, 134 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (𝑥 ∈ (0[,]1) ↦ (exp‘((i
· (2 · π)) · ((𝑚 − 𝑁) · 𝑥)))) ∈
𝐿1) |
| 136 | 118, 119,
120, 135 | iblss 25840 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (𝑥 ∈ (0(,)1) ↦ (exp‘((i
· (2 · π)) · ((𝑚 − 𝑁) · 𝑥)))) ∈
𝐿1) |
| 137 | 136 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → (𝑥 ∈ (0(,)1) ↦ (exp‘((i
· (2 · π)) · ((𝑚 − 𝑁) · 𝑥)))) ∈
𝐿1) |
| 138 | 114, 116,
137 | iblmulc2 25866 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → (𝑥 ∈ (0(,)1) ↦ (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥))))) ∈
𝐿1) |
| 139 | 97, 101, 112, 138 | itgfsum 25862 |
. . . . 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𝑥)) |
| 140 | 139 | simpld 494 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (𝑥 ∈ (0(,)1) ↦ Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥))))) ∈
𝐿1) |
| 141 | 93, 94, 96, 140 | itgfsum 25862 |
. . 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𝑥)) |
| 142 | 141 | simprd 495 |
. 2
⊢ (𝜑 → ∫(0(,)1)Σ𝑚 ∈ (0...(𝑆 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥)))) d𝑥 = Σ𝑚 ∈ (0...(𝑆 · 𝑁))∫(0(,)1)Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥)))) d𝑥) |
| 143 | | oveq2 7439 |
. . . . . . 7
⊢
(if((𝑚 − 𝑁) = 0, 1, 0) = 1 →
(Σ𝑐 ∈
((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · if((𝑚 − 𝑁) = 0, 1, 0)) = (Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · 1)) |
| 144 | | oveq2 7439 |
. . . . . . 7
⊢
(if((𝑚 − 𝑁) = 0, 1, 0) = 0 →
(Σ𝑐 ∈
((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · if((𝑚 − 𝑁) = 0, 1, 0)) = (Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · 0)) |
| 145 | 101, 114 | fsumcl 15769 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) ∈ ℂ) |
| 146 | 145 | mulridd 11278 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · 1) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎))) |
| 147 | 145 | mul01d 11460 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · 0) = 0) |
| 148 | 143, 144,
146, 147 | ifeq3da 32559 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → if((𝑚 − 𝑁) = 0, Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)), 0) = (Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · if((𝑚 − 𝑁) = 0, 1, 0))) |
| 149 | | velsn 4642 |
. . . . . . . 8
⊢ (𝑚 ∈ {𝑁} ↔ 𝑚 = 𝑁) |
| 150 | 41, 123 | subeq0ad 11630 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → ((𝑚 − 𝑁) = 0 ↔ 𝑚 = 𝑁)) |
| 151 | 149, 150 | bitr4id 290 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (𝑚 ∈ {𝑁} ↔ (𝑚 − 𝑁) = 0)) |
| 152 | 151 | ifbid 4549 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → if(𝑚 ∈ {𝑁}, Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)), 0) = if((𝑚 − 𝑁) = 0, Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)), 0)) |
| 153 | 1 | nn0zd 12639 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 154 | 153 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → 𝑁 ∈ ℤ) |
| 155 | 46, 154 | zsubcld 12727 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → (𝑚 − 𝑁) ∈ ℤ) |
| 156 | | itgexpif 34621 |
. . . . . . . . . 10
⊢ ((𝑚 − 𝑁) ∈ ℤ →
∫(0(,)1)(exp‘((i · (2 · π)) · ((𝑚 − 𝑁) · 𝑥))) d𝑥 = if((𝑚 − 𝑁) = 0, 1, 0)) |
| 157 | 155, 156 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → ∫(0(,)1)(exp‘((i ·
(2 · π)) · ((𝑚 − 𝑁) · 𝑥))) d𝑥 = if((𝑚 − 𝑁) = 0, 1, 0)) |
| 158 | 157 | oveq2d 7447 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · ∫(0(,)1)(exp‘((i
· (2 · π)) · ((𝑚 − 𝑁) · 𝑥))) d𝑥) = (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · if((𝑚 − 𝑁) = 0, 1, 0))) |
| 159 | 158 | sumeq2dv 15738 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · ∫(0(,)1)(exp‘((i
· (2 · π)) · ((𝑚 − 𝑁) · 𝑥))) d𝑥) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · if((𝑚 − 𝑁) = 0, 1, 0))) |
| 160 | | 1cnd 11256 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → 1 ∈
ℂ) |
| 161 | | 0cnd 11254 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → 0 ∈
ℂ) |
| 162 | 160, 161 | ifcld 4572 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → if((𝑚 − 𝑁) = 0, 1, 0) ∈
ℂ) |
| 163 | 101, 162,
114 | fsummulc1 15821 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · if((𝑚 − 𝑁) = 0, 1, 0)) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · if((𝑚 − 𝑁) = 0, 1, 0))) |
| 164 | 159, 163 | eqtr4d 2780 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · ∫(0(,)1)(exp‘((i
· (2 · π)) · ((𝑚 − 𝑁) · 𝑥))) d𝑥) = (Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · if((𝑚 − 𝑁) = 0, 1, 0))) |
| 165 | 148, 152,
164 | 3eqtr4rd 2788 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · ∫(0(,)1)(exp‘((i
· (2 · π)) · ((𝑚 − 𝑁) · 𝑥))) d𝑥) = if(𝑚 ∈ {𝑁}, Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)), 0)) |
| 166 | 165 | sumeq2dv 15738 |
. . . 4
⊢ (𝜑 → Σ𝑚 ∈ (0...(𝑆 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · ∫(0(,)1)(exp‘((i
· (2 · π)) · ((𝑚 − 𝑁) · 𝑥))) d𝑥) = Σ𝑚 ∈ (0...(𝑆 · 𝑁))if(𝑚 ∈ {𝑁}, Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)), 0)) |
| 167 | | 0zd 12625 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℤ) |
| 168 | 9 | nn0zd 12639 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ ℤ) |
| 169 | 168, 153 | zmulcld 12728 |
. . . . . . 7
⊢ (𝜑 → (𝑆 · 𝑁) ∈ ℤ) |
| 170 | 1 | nn0ge0d 12590 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ 𝑁) |
| 171 | | nnmulge 32749 |
. . . . . . . 8
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ 𝑁 ≤ (𝑆 · 𝑁)) |
| 172 | 8, 1, 171 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ≤ (𝑆 · 𝑁)) |
| 173 | 167, 169,
153, 170, 172 | elfzd 13555 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ (0...(𝑆 · 𝑁))) |
| 174 | 173 | snssd 4809 |
. . . . 5
⊢ (𝜑 → {𝑁} ⊆ (0...(𝑆 · 𝑁))) |
| 175 | 174 | sselda 3983 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ {𝑁}) → 𝑚 ∈ (0...(𝑆 · 𝑁))) |
| 176 | 175, 145 | syldan 591 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ {𝑁}) → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) ∈ ℂ) |
| 177 | 176 | ralrimiva 3146 |
. . . . 5
⊢ (𝜑 → ∀𝑚 ∈ {𝑁}Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) ∈ ℂ) |
| 178 | 94 | olcd 875 |
. . . . 5
⊢ (𝜑 → ((0...(𝑆 · 𝑁)) ⊆ (ℤ≥‘0)
∨ (0...(𝑆 · 𝑁)) ∈ Fin)) |
| 179 | | sumss2 15762 |
. . . . 5
⊢ ((({𝑁} ⊆ (0...(𝑆 · 𝑁)) ∧ ∀𝑚 ∈ {𝑁}Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) ∈ ℂ) ∧ ((0...(𝑆 · 𝑁)) ⊆ (ℤ≥‘0)
∨ (0...(𝑆 · 𝑁)) ∈ Fin)) →
Σ𝑚 ∈ {𝑁}Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) = Σ𝑚 ∈ (0...(𝑆 · 𝑁))if(𝑚 ∈ {𝑁}, Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)), 0)) |
| 180 | 174, 177,
178, 179 | syl21anc 838 |
. . . 4
⊢ (𝜑 → Σ𝑚 ∈ {𝑁}Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) = Σ𝑚 ∈ (0...(𝑆 · 𝑁))if(𝑚 ∈ {𝑁}, Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)), 0)) |
| 181 | 29 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (1...𝑁) ⊆ ℕ) |
| 182 | | fzfid 14014 |
. . . . . . 7
⊢ (𝜑 → (1...𝑁) ∈ Fin) |
| 183 | 181, 153,
9, 182 | reprfi 34631 |
. . . . . 6
⊢ (𝜑 → ((1...𝑁)(repr‘𝑆)𝑁) ∈ Fin) |
| 184 | 37 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)) → (0..^𝑆) ∈ Fin) |
| 185 | 1 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑁 ∈
ℕ0) |
| 186 | 9 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑆 ∈
ℕ0) |
| 187 | 22 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑁 ∈ ℂ) |
| 188 | 11 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)) ∧ 𝑎 ∈ (0..^𝑆)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m
ℕ)) |
| 189 | | simpr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆)) |
| 190 | 29 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)) → (1...𝑁) ⊆ ℕ) |
| 191 | 153 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)) → 𝑁 ∈ ℤ) |
| 192 | 9 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)) → 𝑆 ∈
ℕ0) |
| 193 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)) → 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)) |
| 194 | 190, 191,
192, 193 | reprf 34627 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)) → 𝑐:(0..^𝑆)⟶(1...𝑁)) |
| 195 | 194 | ffvelcdmda 7104 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑐‘𝑎) ∈ (1...𝑁)) |
| 196 | 29, 195 | sselid 3981 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑐‘𝑎) ∈ ℕ) |
| 197 | 185, 186,
187, 188, 189, 196 | breprexplemb 34646 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝐿‘𝑎)‘(𝑐‘𝑎)) ∈ ℂ) |
| 198 | 184, 197 | fprodcl 15988 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)) → ∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) ∈ ℂ) |
| 199 | 183, 198 | fsumcl 15769 |
. . . . 5
⊢ (𝜑 → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) ∈ ℂ) |
| 200 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑚 = 𝑁 → ((1...𝑁)(repr‘𝑆)𝑚) = ((1...𝑁)(repr‘𝑆)𝑁)) |
| 201 | 200 | sumeq1d 15736 |
. . . . . 6
⊢ (𝑚 = 𝑁 → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎))) |
| 202 | 201 | sumsn 15782 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ Σ𝑐 ∈
((1...𝑁)(repr‘𝑆)𝑁)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) ∈ ℂ) → Σ𝑚 ∈ {𝑁}Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎))) |
| 203 | 1, 199, 202 | syl2anc 584 |
. . . 4
⊢ (𝜑 → Σ𝑚 ∈ {𝑁}Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎))) |
| 204 | 166, 180,
203 | 3eqtr2d 2783 |
. . 3
⊢ (𝜑 → Σ𝑚 ∈ (0...(𝑆 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · ∫(0(,)1)(exp‘((i
· (2 · π)) · ((𝑚 − 𝑁) · 𝑥))) d𝑥) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎))) |
| 205 | 139 | simprd 495 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → ∫(0(,)1)Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥)))) d𝑥 = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∫(0(,)1)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥)))) d𝑥) |
| 206 | 110 | an32s 652 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) ∧ 𝑥 ∈ (0(,)1)) → (exp‘((i
· (2 · π)) · ((𝑚 − 𝑁) · 𝑥))) ∈ ℂ) |
| 207 | 114, 206,
137 | itgmulc2 25869 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · ∫(0(,)1)(exp‘((i
· (2 · π)) · ((𝑚 − 𝑁) · 𝑥))) d𝑥) = ∫(0(,)1)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥)))) d𝑥) |
| 208 | 207 | sumeq2dv 15738 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · ∫(0(,)1)(exp‘((i
· (2 · π)) · ((𝑚 − 𝑁) · 𝑥))) d𝑥) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∫(0(,)1)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥)))) d𝑥) |
| 209 | 205, 208 | eqtr4d 2780 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → ∫(0(,)1)Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥)))) d𝑥 = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · ∫(0(,)1)(exp‘((i
· (2 · π)) · ((𝑚 − 𝑁) · 𝑥))) d𝑥)) |
| 210 | 209 | sumeq2dv 15738 |
. . 3
⊢ (𝜑 → Σ𝑚 ∈ (0...(𝑆 · 𝑁))∫(0(,)1)Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥)))) d𝑥 = Σ𝑚 ∈ (0...(𝑆 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · ∫(0(,)1)(exp‘((i
· (2 · π)) · ((𝑚 − 𝑁) · 𝑥))) d𝑥)) |
| 211 | 1, 9 | reprfz1 34639 |
. . . 4
⊢ (𝜑 → (ℕ(repr‘𝑆)𝑁) = ((1...𝑁)(repr‘𝑆)𝑁)) |
| 212 | 211 | sumeq1d 15736 |
. . 3
⊢ (𝜑 → Σ𝑐 ∈ (ℕ(repr‘𝑆)𝑁)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑁)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎))) |
| 213 | 204, 210,
212 | 3eqtr4d 2787 |
. 2
⊢ (𝜑 → Σ𝑚 ∈ (0...(𝑆 · 𝑁))∫(0(,)1)Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (exp‘((i · (2
· π)) · ((𝑚 − 𝑁) · 𝑥)))) d𝑥 = Σ𝑐 ∈ (ℕ(repr‘𝑆)𝑁)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎))) |
| 214 | 91, 142, 213 | 3eqtrrd 2782 |
1
⊢ (𝜑 → Σ𝑐 ∈ (ℕ(repr‘𝑆)𝑁)∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) = ∫(0(,)1)(∏𝑎 ∈ (0..^𝑆)(((𝐿‘𝑎)vts𝑁)‘𝑥) · (exp‘((i · (2
· π)) · (-𝑁 · 𝑥)))) d𝑥) |