| Step | Hyp | Ref
| Expression |
| 1 | | circlevma.n |
. . 3
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
| 2 | | 3nn 12345 |
. . . 4
⊢ 3 ∈
ℕ |
| 3 | 2 | a1i 11 |
. . 3
⊢ (𝜑 → 3 ∈
ℕ) |
| 4 | | vmaf 27162 |
. . . . . . 7
⊢
Λ:ℕ⟶ℝ |
| 5 | | ax-resscn 11212 |
. . . . . . 7
⊢ ℝ
⊆ ℂ |
| 6 | | fss 6752 |
. . . . . . 7
⊢
((Λ:ℕ⟶ℝ ∧ ℝ ⊆ ℂ) →
Λ:ℕ⟶ℂ) |
| 7 | 4, 5, 6 | mp2an 692 |
. . . . . 6
⊢
Λ:ℕ⟶ℂ |
| 8 | | cnex 11236 |
. . . . . . 7
⊢ ℂ
∈ V |
| 9 | | nnex 12272 |
. . . . . . 7
⊢ ℕ
∈ V |
| 10 | | elmapg 8879 |
. . . . . . 7
⊢ ((ℂ
∈ V ∧ ℕ ∈ V) → (Λ ∈ (ℂ
↑m ℕ) ↔
Λ:ℕ⟶ℂ)) |
| 11 | 8, 9, 10 | mp2an 692 |
. . . . . 6
⊢ (Λ
∈ (ℂ ↑m ℕ) ↔
Λ:ℕ⟶ℂ) |
| 12 | 7, 11 | mpbir 231 |
. . . . 5
⊢ Λ
∈ (ℂ ↑m ℕ) |
| 13 | 12 | fconst6 6798 |
. . . 4
⊢ ((0..^3)
× {Λ}):(0..^3)⟶(ℂ ↑m
ℕ) |
| 14 | 13 | a1i 11 |
. . 3
⊢ (𝜑 → ((0..^3) ×
{Λ}):(0..^3)⟶(ℂ ↑m
ℕ)) |
| 15 | 1, 3, 14 | circlemeth 34655 |
. 2
⊢ (𝜑 → Σ𝑛 ∈ (ℕ(repr‘3)𝑁)∏𝑎 ∈ (0..^3)((((0..^3) ×
{Λ})‘𝑎)‘(𝑛‘𝑎)) = ∫(0(,)1)(∏𝑎 ∈ (0..^3)(((((0..^3) ×
{Λ})‘𝑎)vts𝑁)‘𝑥) · (exp‘((i · (2
· π)) · (-𝑁 · 𝑥)))) d𝑥) |
| 16 | | c0ex 11255 |
. . . . . . . . 9
⊢ 0 ∈
V |
| 17 | 16 | tpid1 4768 |
. . . . . . . 8
⊢ 0 ∈
{0, 1, 2} |
| 18 | | fzo0to3tp 13791 |
. . . . . . . 8
⊢ (0..^3) =
{0, 1, 2} |
| 19 | 17, 18 | eleqtrri 2840 |
. . . . . . 7
⊢ 0 ∈
(0..^3) |
| 20 | | eleq1 2829 |
. . . . . . 7
⊢ (𝑎 = 0 → (𝑎 ∈ (0..^3) ↔ 0 ∈
(0..^3))) |
| 21 | 19, 20 | mpbiri 258 |
. . . . . 6
⊢ (𝑎 = 0 → 𝑎 ∈ (0..^3)) |
| 22 | 12 | elexi 3503 |
. . . . . . 7
⊢ Λ
∈ V |
| 23 | 22 | fvconst2 7224 |
. . . . . 6
⊢ (𝑎 ∈ (0..^3) → (((0..^3)
× {Λ})‘𝑎) = Λ) |
| 24 | 21, 23 | syl 17 |
. . . . 5
⊢ (𝑎 = 0 → (((0..^3) ×
{Λ})‘𝑎) =
Λ) |
| 25 | | fveq2 6906 |
. . . . 5
⊢ (𝑎 = 0 → (𝑛‘𝑎) = (𝑛‘0)) |
| 26 | 24, 25 | fveq12d 6913 |
. . . 4
⊢ (𝑎 = 0 → ((((0..^3) ×
{Λ})‘𝑎)‘(𝑛‘𝑎)) = (Λ‘(𝑛‘0))) |
| 27 | | 1ex 11257 |
. . . . . . . . 9
⊢ 1 ∈
V |
| 28 | 27 | tpid2 4770 |
. . . . . . . 8
⊢ 1 ∈
{0, 1, 2} |
| 29 | 28, 18 | eleqtrri 2840 |
. . . . . . 7
⊢ 1 ∈
(0..^3) |
| 30 | | eleq1 2829 |
. . . . . . 7
⊢ (𝑎 = 1 → (𝑎 ∈ (0..^3) ↔ 1 ∈
(0..^3))) |
| 31 | 29, 30 | mpbiri 258 |
. . . . . 6
⊢ (𝑎 = 1 → 𝑎 ∈ (0..^3)) |
| 32 | 31, 23 | syl 17 |
. . . . 5
⊢ (𝑎 = 1 → (((0..^3) ×
{Λ})‘𝑎) =
Λ) |
| 33 | | fveq2 6906 |
. . . . 5
⊢ (𝑎 = 1 → (𝑛‘𝑎) = (𝑛‘1)) |
| 34 | 32, 33 | fveq12d 6913 |
. . . 4
⊢ (𝑎 = 1 → ((((0..^3) ×
{Λ})‘𝑎)‘(𝑛‘𝑎)) = (Λ‘(𝑛‘1))) |
| 35 | | 2ex 12343 |
. . . . . . . . 9
⊢ 2 ∈
V |
| 36 | 35 | tpid3 4773 |
. . . . . . . 8
⊢ 2 ∈
{0, 1, 2} |
| 37 | 36, 18 | eleqtrri 2840 |
. . . . . . 7
⊢ 2 ∈
(0..^3) |
| 38 | | eleq1 2829 |
. . . . . . 7
⊢ (𝑎 = 2 → (𝑎 ∈ (0..^3) ↔ 2 ∈
(0..^3))) |
| 39 | 37, 38 | mpbiri 258 |
. . . . . 6
⊢ (𝑎 = 2 → 𝑎 ∈ (0..^3)) |
| 40 | 39, 23 | syl 17 |
. . . . 5
⊢ (𝑎 = 2 → (((0..^3) ×
{Λ})‘𝑎) =
Λ) |
| 41 | | fveq2 6906 |
. . . . 5
⊢ (𝑎 = 2 → (𝑛‘𝑎) = (𝑛‘2)) |
| 42 | 40, 41 | fveq12d 6913 |
. . . 4
⊢ (𝑎 = 2 → ((((0..^3) ×
{Λ})‘𝑎)‘(𝑛‘𝑎)) = (Λ‘(𝑛‘2))) |
| 43 | 23 | fveq1d 6908 |
. . . . . 6
⊢ (𝑎 ∈ (0..^3) →
((((0..^3) × {Λ})‘𝑎)‘(𝑛‘𝑎)) = (Λ‘(𝑛‘𝑎))) |
| 44 | 43 | adantl 481 |
. . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) ∧ 𝑎 ∈ (0..^3)) → ((((0..^3) ×
{Λ})‘𝑎)‘(𝑛‘𝑎)) = (Λ‘(𝑛‘𝑎))) |
| 45 | 7 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) ∧ 𝑎 ∈ (0..^3)) →
Λ:ℕ⟶ℂ) |
| 46 | | ssidd 4007 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → ℕ ⊆
ℕ) |
| 47 | 1 | nn0zd 12639 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 48 | 47 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → 𝑁 ∈ ℤ) |
| 49 | 2 | nnnn0i 12534 |
. . . . . . . . 9
⊢ 3 ∈
ℕ0 |
| 50 | 49 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → 3 ∈
ℕ0) |
| 51 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → 𝑛 ∈ (ℕ(repr‘3)𝑁)) |
| 52 | 46, 48, 50, 51 | reprf 34627 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → 𝑛:(0..^3)⟶ℕ) |
| 53 | 52 | ffvelcdmda 7104 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) ∧ 𝑎 ∈ (0..^3)) → (𝑛‘𝑎) ∈ ℕ) |
| 54 | 45, 53 | ffvelcdmd 7105 |
. . . . 5
⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) ∧ 𝑎 ∈ (0..^3)) →
(Λ‘(𝑛‘𝑎)) ∈ ℂ) |
| 55 | 44, 54 | eqeltrd 2841 |
. . . 4
⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) ∧ 𝑎 ∈ (0..^3)) → ((((0..^3) ×
{Λ})‘𝑎)‘(𝑛‘𝑎)) ∈ ℂ) |
| 56 | 26, 34, 42, 55 | prodfzo03 34618 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → ∏𝑎 ∈ (0..^3)((((0..^3)
× {Λ})‘𝑎)‘(𝑛‘𝑎)) = ((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2))))) |
| 57 | 56 | sumeq2dv 15738 |
. 2
⊢ (𝜑 → Σ𝑛 ∈ (ℕ(repr‘3)𝑁)∏𝑎 ∈ (0..^3)((((0..^3) ×
{Λ})‘𝑎)‘(𝑛‘𝑎)) = Σ𝑛 ∈ (ℕ(repr‘3)𝑁)((Λ‘(𝑛‘0)) ·
((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))))) |
| 58 | 23 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑎 ∈ (0..^3)) → (((0..^3) ×
{Λ})‘𝑎) =
Λ) |
| 59 | 58 | oveq1d 7446 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑎 ∈ (0..^3)) → ((((0..^3) ×
{Λ})‘𝑎)vts𝑁) = (Λvts𝑁)) |
| 60 | 59 | fveq1d 6908 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑎 ∈ (0..^3)) → (((((0..^3) ×
{Λ})‘𝑎)vts𝑁)‘𝑥) = ((Λvts𝑁)‘𝑥)) |
| 61 | 60 | prodeq2dv 15958 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → ∏𝑎 ∈ (0..^3)(((((0..^3)
× {Λ})‘𝑎)vts𝑁)‘𝑥) = ∏𝑎 ∈ (0..^3)((Λvts𝑁)‘𝑥)) |
| 62 | | fzofi 14015 |
. . . . . . 7
⊢ (0..^3)
∈ Fin |
| 63 | 62 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → (0..^3) ∈
Fin) |
| 64 | 1 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → 𝑁 ∈
ℕ0) |
| 65 | | ioossre 13448 |
. . . . . . . . . 10
⊢ (0(,)1)
⊆ ℝ |
| 66 | 65, 5 | sstri 3993 |
. . . . . . . . 9
⊢ (0(,)1)
⊆ ℂ |
| 67 | 66 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (0(,)1) ⊆
ℂ) |
| 68 | 67 | sselda 3983 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → 𝑥 ∈ ℂ) |
| 69 | 7 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) →
Λ:ℕ⟶ℂ) |
| 70 | 64, 68, 69 | vtscl 34653 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → ((Λvts𝑁)‘𝑥) ∈ ℂ) |
| 71 | | fprodconst 16014 |
. . . . . 6
⊢ (((0..^3)
∈ Fin ∧ ((Λvts𝑁)‘𝑥) ∈ ℂ) → ∏𝑎 ∈
(0..^3)((Λvts𝑁)‘𝑥) = (((Λvts𝑁)‘𝑥)↑(♯‘(0..^3)))) |
| 72 | 63, 70, 71 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → ∏𝑎 ∈
(0..^3)((Λvts𝑁)‘𝑥) = (((Λvts𝑁)‘𝑥)↑(♯‘(0..^3)))) |
| 73 | | hashfzo0 14469 |
. . . . . . . 8
⊢ (3 ∈
ℕ0 → (♯‘(0..^3)) = 3) |
| 74 | 49, 73 | ax-mp 5 |
. . . . . . 7
⊢
(♯‘(0..^3)) = 3 |
| 75 | 74 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) →
(♯‘(0..^3)) = 3) |
| 76 | 75 | oveq2d 7447 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → (((Λvts𝑁)‘𝑥)↑(♯‘(0..^3))) =
(((Λvts𝑁)‘𝑥)↑3)) |
| 77 | 61, 72, 76 | 3eqtrd 2781 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → ∏𝑎 ∈ (0..^3)(((((0..^3)
× {Λ})‘𝑎)vts𝑁)‘𝑥) = (((Λvts𝑁)‘𝑥)↑3)) |
| 78 | 77 | oveq1d 7446 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (0(,)1)) → (∏𝑎 ∈ (0..^3)(((((0..^3)
× {Λ})‘𝑎)vts𝑁)‘𝑥) · (exp‘((i · (2
· π)) · (-𝑁 · 𝑥)))) = ((((Λvts𝑁)‘𝑥)↑3) · (exp‘((i · (2
· π)) · (-𝑁 · 𝑥))))) |
| 79 | 78 | itgeq2dv 25817 |
. 2
⊢ (𝜑 → ∫(0(,)1)(∏𝑎 ∈ (0..^3)(((((0..^3)
× {Λ})‘𝑎)vts𝑁)‘𝑥) · (exp‘((i · (2
· π)) · (-𝑁 · 𝑥)))) d𝑥 = ∫(0(,)1)((((Λvts𝑁)‘𝑥)↑3) · (exp‘((i · (2
· π)) · (-𝑁 · 𝑥)))) d𝑥) |
| 80 | 15, 57, 79 | 3eqtr3d 2785 |
1
⊢ (𝜑 → Σ𝑛 ∈ (ℕ(repr‘3)𝑁)((Λ‘(𝑛‘0)) ·
((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) =
∫(0(,)1)((((Λvts𝑁)‘𝑥)↑3) · (exp‘((i · (2
· π)) · (-𝑁 · 𝑥)))) d𝑥) |