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

Theorem circlemethhgt 31043
Description: The circle method, where the Vinogradov sums are weighted using the Von Mangoldt function and smoothed using functions 𝐻 and 𝐾. Statement 7.49 of [Helfgott] p. 69. At this point there is no further constraint on the smoothing functions. (Contributed by Thierry Arnoux, 22-Dec-2021.)
Hypotheses
Ref Expression
circlemethhgt.h (𝜑𝐻:ℕ⟶ℝ)
circlemethhgt.k (𝜑𝐾:ℕ⟶ℝ)
circlemethhgt.n (𝜑𝑁 ∈ ℕ0)
Assertion
Ref Expression
circlemethhgt (𝜑 → Σ𝑛 ∈ (ℕ(repr‘3)𝑁)(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) = ∫(0(,)1)(((((Λ ∘𝑓 · 𝐻)vts𝑁)‘𝑥) · ((((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥)↑2)) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) d𝑥)
Distinct variable groups:   𝑛,𝐻,𝑥   𝑛,𝐾,𝑥   𝑛,𝑁,𝑥   𝜑,𝑛,𝑥

Proof of Theorem circlemethhgt
Dummy variables 𝑎 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 circlemethhgt.n . . 3 (𝜑𝑁 ∈ ℕ0)
2 3nn 11459 . . . 4 3 ∈ ℕ
32a1i 11 . . 3 (𝜑 → 3 ∈ ℕ)
4 s3len 13859 . . . . . 6 (♯‘⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩) = 3
54eqcomi 2814 . . . . 5 3 = (♯‘⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩)
65a1i 11 . . . 4 (𝜑 → 3 = (♯‘⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩))
7 simprl 778 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → 𝑥 ∈ ℝ)
8 simprr 780 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → 𝑦 ∈ ℝ)
97, 8remulcld 10352 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 · 𝑦) ∈ ℝ)
109recnd 10350 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 · 𝑦) ∈ ℂ)
11 vmaf 25055 . . . . . . . 8 Λ:ℕ⟶ℝ
1211a1i 11 . . . . . . 7 (𝜑 → Λ:ℕ⟶ℝ)
13 circlemethhgt.h . . . . . . 7 (𝜑𝐻:ℕ⟶ℝ)
14 nnex 11308 . . . . . . . 8 ℕ ∈ V
1514a1i 11 . . . . . . 7 (𝜑 → ℕ ∈ V)
16 inidm 4016 . . . . . . 7 (ℕ ∩ ℕ) = ℕ
1710, 12, 13, 15, 15, 16off 7139 . . . . . 6 (𝜑 → (Λ ∘𝑓 · 𝐻):ℕ⟶ℂ)
18 cnex 10299 . . . . . . 7 ℂ ∈ V
1918, 14elmap 8118 . . . . . 6 ((Λ ∘𝑓 · 𝐻) ∈ (ℂ ↑𝑚 ℕ) ↔ (Λ ∘𝑓 · 𝐻):ℕ⟶ℂ)
2017, 19sylibr 225 . . . . 5 (𝜑 → (Λ ∘𝑓 · 𝐻) ∈ (ℂ ↑𝑚 ℕ))
21 circlemethhgt.k . . . . . . 7 (𝜑𝐾:ℕ⟶ℝ)
2210, 12, 21, 15, 15, 16off 7139 . . . . . 6 (𝜑 → (Λ ∘𝑓 · 𝐾):ℕ⟶ℂ)
2318, 14elmap 8118 . . . . . 6 ((Λ ∘𝑓 · 𝐾) ∈ (ℂ ↑𝑚 ℕ) ↔ (Λ ∘𝑓 · 𝐾):ℕ⟶ℂ)
2422, 23sylibr 225 . . . . 5 (𝜑 → (Λ ∘𝑓 · 𝐾) ∈ (ℂ ↑𝑚 ℕ))
2520, 24, 24s3cld 13837 . . . 4 (𝜑 → ⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩ ∈ Word (ℂ ↑𝑚 ℕ))
266, 25wrdfd 30938 . . 3 (𝜑 → ⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩:(0..^3)⟶(ℂ ↑𝑚 ℕ))
271, 3, 26circlemeth 31040 . 2 (𝜑 → Σ𝑛 ∈ (ℕ(repr‘3)𝑁)∏𝑎 ∈ (0..^3)((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)‘(𝑛𝑎)) = ∫(0(,)1)(∏𝑎 ∈ (0..^3)(((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) d𝑥)
28 fveq2 6405 . . . . . 6 (𝑎 = 0 → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎) = (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘0))
29 fveq2 6405 . . . . . 6 (𝑎 = 0 → (𝑛𝑎) = (𝑛‘0))
3028, 29fveq12d 6412 . . . . 5 (𝑎 = 0 → ((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)‘(𝑛𝑎)) = ((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘0)‘(𝑛‘0)))
31 fveq2 6405 . . . . . 6 (𝑎 = 1 → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎) = (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘1))
32 fveq2 6405 . . . . . 6 (𝑎 = 1 → (𝑛𝑎) = (𝑛‘1))
3331, 32fveq12d 6412 . . . . 5 (𝑎 = 1 → ((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)‘(𝑛𝑎)) = ((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘1)‘(𝑛‘1)))
34 fveq2 6405 . . . . . 6 (𝑎 = 2 → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎) = (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘2))
35 fveq2 6405 . . . . . 6 (𝑎 = 2 → (𝑛𝑎) = (𝑛‘2))
3634, 35fveq12d 6412 . . . . 5 (𝑎 = 2 → ((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)‘(𝑛𝑎)) = ((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘2)‘(𝑛‘2)))
3726adantr 468 . . . . . . . 8 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → ⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩:(0..^3)⟶(ℂ ↑𝑚 ℕ))
3837ffvelrnda 6578 . . . . . . 7 (((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) ∧ 𝑎 ∈ (0..^3)) → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎) ∈ (ℂ ↑𝑚 ℕ))
39 elmapi 8111 . . . . . . 7 ((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎) ∈ (ℂ ↑𝑚 ℕ) → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎):ℕ⟶ℂ)
4038, 39syl 17 . . . . . 6 (((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) ∧ 𝑎 ∈ (0..^3)) → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎):ℕ⟶ℂ)
41 ssidd 3818 . . . . . . . 8 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → ℕ ⊆ ℕ)
421nn0zd 11742 . . . . . . . . 9 (𝜑𝑁 ∈ ℤ)
4342adantr 468 . . . . . . . 8 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → 𝑁 ∈ ℤ)
44 3nn0 11573 . . . . . . . . 9 3 ∈ ℕ0
4544a1i 11 . . . . . . . 8 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → 3 ∈ ℕ0)
46 simpr 473 . . . . . . . 8 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → 𝑛 ∈ (ℕ(repr‘3)𝑁))
4741, 43, 45, 46reprf 31012 . . . . . . 7 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → 𝑛:(0..^3)⟶ℕ)
4847ffvelrnda 6578 . . . . . 6 (((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) ∧ 𝑎 ∈ (0..^3)) → (𝑛𝑎) ∈ ℕ)
4940, 48ffvelrnd 6579 . . . . 5 (((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) ∧ 𝑎 ∈ (0..^3)) → ((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)‘(𝑛𝑎)) ∈ ℂ)
5030, 33, 36, 49prodfzo03 31003 . . . 4 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → ∏𝑎 ∈ (0..^3)((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)‘(𝑛𝑎)) = (((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘0)‘(𝑛‘0)) · (((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘1)‘(𝑛‘1)) · ((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘2)‘(𝑛‘2)))))
51 ovex 6903 . . . . . . . 8 (Λ ∘𝑓 · 𝐻) ∈ V
52 s3fv0 13856 . . . . . . . 8 ((Λ ∘𝑓 · 𝐻) ∈ V → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘0) = (Λ ∘𝑓 · 𝐻))
5351, 52mp1i 13 . . . . . . 7 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘0) = (Λ ∘𝑓 · 𝐻))
5453fveq1d 6407 . . . . . 6 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → ((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘0)‘(𝑛‘0)) = ((Λ ∘𝑓 · 𝐻)‘(𝑛‘0)))
55 simpl 470 . . . . . . 7 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → 𝜑)
56 c0ex 10316 . . . . . . . . . . 11 0 ∈ V
5756tpid1 4491 . . . . . . . . . 10 0 ∈ {0, 1, 2}
58 fzo0to3tp 12774 . . . . . . . . . 10 (0..^3) = {0, 1, 2}
5957, 58eleqtrri 2883 . . . . . . . . 9 0 ∈ (0..^3)
6059a1i 11 . . . . . . . 8 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → 0 ∈ (0..^3))
6147, 60ffvelrnd 6579 . . . . . . 7 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → (𝑛‘0) ∈ ℕ)
62 ffn 6253 . . . . . . . . . 10 (Λ:ℕ⟶ℝ → Λ Fn ℕ)
6311, 62ax-mp 5 . . . . . . . . 9 Λ Fn ℕ
6463a1i 11 . . . . . . . 8 (𝜑 → Λ Fn ℕ)
6513ffnd 6254 . . . . . . . 8 (𝜑𝐻 Fn ℕ)
66 eqidd 2806 . . . . . . . 8 ((𝜑 ∧ (𝑛‘0) ∈ ℕ) → (Λ‘(𝑛‘0)) = (Λ‘(𝑛‘0)))
67 eqidd 2806 . . . . . . . 8 ((𝜑 ∧ (𝑛‘0) ∈ ℕ) → (𝐻‘(𝑛‘0)) = (𝐻‘(𝑛‘0)))
6864, 65, 15, 15, 16, 66, 67ofval 7133 . . . . . . 7 ((𝜑 ∧ (𝑛‘0) ∈ ℕ) → ((Λ ∘𝑓 · 𝐻)‘(𝑛‘0)) = ((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))))
6955, 61, 68syl2anc 575 . . . . . 6 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → ((Λ ∘𝑓 · 𝐻)‘(𝑛‘0)) = ((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))))
7054, 69eqtrd 2839 . . . . 5 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → ((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘0)‘(𝑛‘0)) = ((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))))
71 ovex 6903 . . . . . . . . 9 (Λ ∘𝑓 · 𝐾) ∈ V
72 s3fv1 13857 . . . . . . . . 9 ((Λ ∘𝑓 · 𝐾) ∈ V → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘1) = (Λ ∘𝑓 · 𝐾))
7371, 72mp1i 13 . . . . . . . 8 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘1) = (Λ ∘𝑓 · 𝐾))
7473fveq1d 6407 . . . . . . 7 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → ((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘1)‘(𝑛‘1)) = ((Λ ∘𝑓 · 𝐾)‘(𝑛‘1)))
75 1ex 10318 . . . . . . . . . . . 12 1 ∈ V
7675tpid2 4492 . . . . . . . . . . 11 1 ∈ {0, 1, 2}
7776, 58eleqtrri 2883 . . . . . . . . . 10 1 ∈ (0..^3)
7877a1i 11 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → 1 ∈ (0..^3))
7947, 78ffvelrnd 6579 . . . . . . . 8 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → (𝑛‘1) ∈ ℕ)
8021ffnd 6254 . . . . . . . . 9 (𝜑𝐾 Fn ℕ)
81 eqidd 2806 . . . . . . . . 9 ((𝜑 ∧ (𝑛‘1) ∈ ℕ) → (Λ‘(𝑛‘1)) = (Λ‘(𝑛‘1)))
82 eqidd 2806 . . . . . . . . 9 ((𝜑 ∧ (𝑛‘1) ∈ ℕ) → (𝐾‘(𝑛‘1)) = (𝐾‘(𝑛‘1)))
8364, 80, 15, 15, 16, 81, 82ofval 7133 . . . . . . . 8 ((𝜑 ∧ (𝑛‘1) ∈ ℕ) → ((Λ ∘𝑓 · 𝐾)‘(𝑛‘1)) = ((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))))
8455, 79, 83syl2anc 575 . . . . . . 7 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → ((Λ ∘𝑓 · 𝐾)‘(𝑛‘1)) = ((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))))
8574, 84eqtrd 2839 . . . . . 6 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → ((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘1)‘(𝑛‘1)) = ((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))))
86 s3fv2 13858 . . . . . . . . 9 ((Λ ∘𝑓 · 𝐾) ∈ V → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘2) = (Λ ∘𝑓 · 𝐾))
8771, 86mp1i 13 . . . . . . . 8 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘2) = (Λ ∘𝑓 · 𝐾))
8887fveq1d 6407 . . . . . . 7 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → ((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘2)‘(𝑛‘2)) = ((Λ ∘𝑓 · 𝐾)‘(𝑛‘2)))
89 2ex 11372 . . . . . . . . . . . 12 2 ∈ V
9089tpid3 4494 . . . . . . . . . . 11 2 ∈ {0, 1, 2}
9190, 58eleqtrri 2883 . . . . . . . . . 10 2 ∈ (0..^3)
9291a1i 11 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → 2 ∈ (0..^3))
9347, 92ffvelrnd 6579 . . . . . . . 8 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → (𝑛‘2) ∈ ℕ)
94 eqidd 2806 . . . . . . . . 9 ((𝜑 ∧ (𝑛‘2) ∈ ℕ) → (Λ‘(𝑛‘2)) = (Λ‘(𝑛‘2)))
95 eqidd 2806 . . . . . . . . 9 ((𝜑 ∧ (𝑛‘2) ∈ ℕ) → (𝐾‘(𝑛‘2)) = (𝐾‘(𝑛‘2)))
9664, 80, 15, 15, 16, 94, 95ofval 7133 . . . . . . . 8 ((𝜑 ∧ (𝑛‘2) ∈ ℕ) → ((Λ ∘𝑓 · 𝐾)‘(𝑛‘2)) = ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))
9755, 93, 96syl2anc 575 . . . . . . 7 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → ((Λ ∘𝑓 · 𝐾)‘(𝑛‘2)) = ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))
9888, 97eqtrd 2839 . . . . . 6 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → ((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘2)‘(𝑛‘2)) = ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))
9985, 98oveq12d 6889 . . . . 5 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → (((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘1)‘(𝑛‘1)) · ((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘2)‘(𝑛‘2))) = (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2)))))
10070, 99oveq12d 6889 . . . 4 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → (((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘0)‘(𝑛‘0)) · (((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘1)‘(𝑛‘1)) · ((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘2)‘(𝑛‘2)))) = (((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))))
10150, 100eqtrd 2839 . . 3 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → ∏𝑎 ∈ (0..^3)((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)‘(𝑛𝑎)) = (((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))))
102101sumeq2dv 14652 . 2 (𝜑 → Σ𝑛 ∈ (ℕ(repr‘3)𝑁)∏𝑎 ∈ (0..^3)((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)‘(𝑛𝑎)) = Σ𝑛 ∈ (ℕ(repr‘3)𝑁)(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))))
103 nfv 2008 . . . . . 6 𝑎(𝜑𝑥 ∈ (0(,)1))
104 nfcv 2947 . . . . . 6 𝑎(((Λ ∘𝑓 · 𝐻)vts𝑁)‘𝑥)
105 fzofi 12993 . . . . . . 7 (1..^3) ∈ Fin
106105a1i 11 . . . . . 6 ((𝜑𝑥 ∈ (0(,)1)) → (1..^3) ∈ Fin)
10756a1i 11 . . . . . 6 ((𝜑𝑥 ∈ (0(,)1)) → 0 ∈ V)
108 eqid 2805 . . . . . . . . 9 0 = 0
109108orci 883 . . . . . . . 8 (0 = 0 ∨ 0 = 3)
110 0elfz 12656 . . . . . . . . 9 (3 ∈ ℕ0 → 0 ∈ (0...3))
111 elfznelfzob 12794 . . . . . . . . 9 (0 ∈ (0...3) → (¬ 0 ∈ (1..^3) ↔ (0 = 0 ∨ 0 = 3)))
11244, 110, 111mp2b 10 . . . . . . . 8 (¬ 0 ∈ (1..^3) ↔ (0 = 0 ∨ 0 = 3))
113109, 112mpbir 222 . . . . . . 7 ¬ 0 ∈ (1..^3)
114113a1i 11 . . . . . 6 ((𝜑𝑥 ∈ (0(,)1)) → ¬ 0 ∈ (1..^3))
1151ad2antrr 708 . . . . . . 7 (((𝜑𝑥 ∈ (0(,)1)) ∧ 𝑎 ∈ (1..^3)) → 𝑁 ∈ ℕ0)
116 ioossre 12449 . . . . . . . . . . 11 (0(,)1) ⊆ ℝ
117 ax-resscn 10275 . . . . . . . . . . 11 ℝ ⊆ ℂ
118116, 117sstri 3804 . . . . . . . . . 10 (0(,)1) ⊆ ℂ
119118a1i 11 . . . . . . . . 9 (𝜑 → (0(,)1) ⊆ ℂ)
120119sselda 3795 . . . . . . . 8 ((𝜑𝑥 ∈ (0(,)1)) → 𝑥 ∈ ℂ)
121120adantr 468 . . . . . . 7 (((𝜑𝑥 ∈ (0(,)1)) ∧ 𝑎 ∈ (1..^3)) → 𝑥 ∈ ℂ)
12226ad2antrr 708 . . . . . . . . 9 (((𝜑𝑥 ∈ (0(,)1)) ∧ 𝑎 ∈ (1..^3)) → ⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩:(0..^3)⟶(ℂ ↑𝑚 ℕ))
123 fzo0ss1 12718 . . . . . . . . . . 11 (1..^3) ⊆ (0..^3)
124123a1i 11 . . . . . . . . . 10 ((𝜑𝑥 ∈ (0(,)1)) → (1..^3) ⊆ (0..^3))
125124sselda 3795 . . . . . . . . 9 (((𝜑𝑥 ∈ (0(,)1)) ∧ 𝑎 ∈ (1..^3)) → 𝑎 ∈ (0..^3))
126122, 125ffvelrnd 6579 . . . . . . . 8 (((𝜑𝑥 ∈ (0(,)1)) ∧ 𝑎 ∈ (1..^3)) → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎) ∈ (ℂ ↑𝑚 ℕ))
127126, 39syl 17 . . . . . . 7 (((𝜑𝑥 ∈ (0(,)1)) ∧ 𝑎 ∈ (1..^3)) → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎):ℕ⟶ℂ)
128115, 121, 127vtscl 31038 . . . . . 6 (((𝜑𝑥 ∈ (0(,)1)) ∧ 𝑎 ∈ (1..^3)) → (((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥) ∈ ℂ)
12951, 52ax-mp 5 . . . . . . . . 9 (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘0) = (Λ ∘𝑓 · 𝐻)
13028, 129syl6eq 2855 . . . . . . . 8 (𝑎 = 0 → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎) = (Λ ∘𝑓 · 𝐻))
131130oveq1d 6886 . . . . . . 7 (𝑎 = 0 → ((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)vts𝑁) = ((Λ ∘𝑓 · 𝐻)vts𝑁))
132131fveq1d 6407 . . . . . 6 (𝑎 = 0 → (((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥) = (((Λ ∘𝑓 · 𝐻)vts𝑁)‘𝑥))
1331adantr 468 . . . . . . 7 ((𝜑𝑥 ∈ (0(,)1)) → 𝑁 ∈ ℕ0)
13417adantr 468 . . . . . . 7 ((𝜑𝑥 ∈ (0(,)1)) → (Λ ∘𝑓 · 𝐻):ℕ⟶ℂ)
135133, 120, 134vtscl 31038 . . . . . 6 ((𝜑𝑥 ∈ (0(,)1)) → (((Λ ∘𝑓 · 𝐻)vts𝑁)‘𝑥) ∈ ℂ)
136103, 104, 106, 107, 114, 128, 132, 135fprodsplitsn 14936 . . . . 5 ((𝜑𝑥 ∈ (0(,)1)) → ∏𝑎 ∈ ((1..^3) ∪ {0})(((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥) = (∏𝑎 ∈ (1..^3)(((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥) · (((Λ ∘𝑓 · 𝐻)vts𝑁)‘𝑥)))
137 uncom 3953 . . . . . . . 8 ((1..^3) ∪ {0}) = ({0} ∪ (1..^3))
138 fzo0sn0fzo1 12777 . . . . . . . . 9 (3 ∈ ℕ → (0..^3) = ({0} ∪ (1..^3)))
1392, 138ax-mp 5 . . . . . . . 8 (0..^3) = ({0} ∪ (1..^3))
140137, 139eqtr4i 2830 . . . . . . 7 ((1..^3) ∪ {0}) = (0..^3)
141140a1i 11 . . . . . 6 ((𝜑𝑥 ∈ (0(,)1)) → ((1..^3) ∪ {0}) = (0..^3))
142141prodeq1d 14868 . . . . 5 ((𝜑𝑥 ∈ (0(,)1)) → ∏𝑎 ∈ ((1..^3) ∪ {0})(((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥) = ∏𝑎 ∈ (0..^3)(((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥))
143 fzo13pr 12772 . . . . . . . . . . . . . . 15 (1..^3) = {1, 2}
144143eleq2i 2876 . . . . . . . . . . . . . 14 (𝑎 ∈ (1..^3) ↔ 𝑎 ∈ {1, 2})
145 vex 3393 . . . . . . . . . . . . . . 15 𝑎 ∈ V
146145elpr 4390 . . . . . . . . . . . . . 14 (𝑎 ∈ {1, 2} ↔ (𝑎 = 1 ∨ 𝑎 = 2))
147144, 146bitri 266 . . . . . . . . . . . . 13 (𝑎 ∈ (1..^3) ↔ (𝑎 = 1 ∨ 𝑎 = 2))
14831adantl 469 . . . . . . . . . . . . . . 15 ((𝜑𝑎 = 1) → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎) = (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘1))
14971, 72mp1i 13 . . . . . . . . . . . . . . 15 ((𝜑𝑎 = 1) → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘1) = (Λ ∘𝑓 · 𝐾))
150148, 149eqtrd 2839 . . . . . . . . . . . . . 14 ((𝜑𝑎 = 1) → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎) = (Λ ∘𝑓 · 𝐾))
15134adantl 469 . . . . . . . . . . . . . . 15 ((𝜑𝑎 = 2) → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎) = (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘2))
15271, 86mp1i 13 . . . . . . . . . . . . . . 15 ((𝜑𝑎 = 2) → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘2) = (Λ ∘𝑓 · 𝐾))
153151, 152eqtrd 2839 . . . . . . . . . . . . . 14 ((𝜑𝑎 = 2) → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎) = (Λ ∘𝑓 · 𝐾))
154150, 153jaodan 971 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑎 = 1 ∨ 𝑎 = 2)) → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎) = (Λ ∘𝑓 · 𝐾))
155147, 154sylan2b 583 . . . . . . . . . . . 12 ((𝜑𝑎 ∈ (1..^3)) → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎) = (Λ ∘𝑓 · 𝐾))
156155adantlr 697 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (0(,)1)) ∧ 𝑎 ∈ (1..^3)) → (⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎) = (Λ ∘𝑓 · 𝐾))
157156oveq1d 6886 . . . . . . . . . 10 (((𝜑𝑥 ∈ (0(,)1)) ∧ 𝑎 ∈ (1..^3)) → ((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)vts𝑁) = ((Λ ∘𝑓 · 𝐾)vts𝑁))
158157fveq1d 6407 . . . . . . . . 9 (((𝜑𝑥 ∈ (0(,)1)) ∧ 𝑎 ∈ (1..^3)) → (((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥) = (((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥))
159158prodeq2dv 14870 . . . . . . . 8 ((𝜑𝑥 ∈ (0(,)1)) → ∏𝑎 ∈ (1..^3)(((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥) = ∏𝑎 ∈ (1..^3)(((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥))
16022adantr 468 . . . . . . . . . 10 ((𝜑𝑥 ∈ (0(,)1)) → (Λ ∘𝑓 · 𝐾):ℕ⟶ℂ)
161133, 120, 160vtscl 31038 . . . . . . . . 9 ((𝜑𝑥 ∈ (0(,)1)) → (((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥) ∈ ℂ)
162 fprodconst 14925 . . . . . . . . 9 (((1..^3) ∈ Fin ∧ (((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥) ∈ ℂ) → ∏𝑎 ∈ (1..^3)(((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥) = ((((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥)↑(♯‘(1..^3))))
163106, 161, 162syl2anc 575 . . . . . . . 8 ((𝜑𝑥 ∈ (0(,)1)) → ∏𝑎 ∈ (1..^3)(((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥) = ((((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥)↑(♯‘(1..^3))))
164 nnuz 11937 . . . . . . . . . . . . 13 ℕ = (ℤ‘1)
1652, 164eleqtri 2882 . . . . . . . . . . . 12 3 ∈ (ℤ‘1)
166 hashfzo 13429 . . . . . . . . . . . 12 (3 ∈ (ℤ‘1) → (♯‘(1..^3)) = (3 − 1))
167165, 166ax-mp 5 . . . . . . . . . . 11 (♯‘(1..^3)) = (3 − 1)
168 3m1e2 11416 . . . . . . . . . . 11 (3 − 1) = 2
169167, 168eqtri 2827 . . . . . . . . . 10 (♯‘(1..^3)) = 2
170169a1i 11 . . . . . . . . 9 ((𝜑𝑥 ∈ (0(,)1)) → (♯‘(1..^3)) = 2)
171170oveq2d 6887 . . . . . . . 8 ((𝜑𝑥 ∈ (0(,)1)) → ((((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥)↑(♯‘(1..^3))) = ((((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥)↑2))
172159, 163, 1713eqtrd 2843 . . . . . . 7 ((𝜑𝑥 ∈ (0(,)1)) → ∏𝑎 ∈ (1..^3)(((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥) = ((((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥)↑2))
173172oveq1d 6886 . . . . . 6 ((𝜑𝑥 ∈ (0(,)1)) → (∏𝑎 ∈ (1..^3)(((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥) · (((Λ ∘𝑓 · 𝐻)vts𝑁)‘𝑥)) = (((((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥)↑2) · (((Λ ∘𝑓 · 𝐻)vts𝑁)‘𝑥)))
174161sqcld 13225 . . . . . . 7 ((𝜑𝑥 ∈ (0(,)1)) → ((((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥)↑2) ∈ ℂ)
175135, 174mulcomd 10343 . . . . . 6 ((𝜑𝑥 ∈ (0(,)1)) → ((((Λ ∘𝑓 · 𝐻)vts𝑁)‘𝑥) · ((((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥)↑2)) = (((((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥)↑2) · (((Λ ∘𝑓 · 𝐻)vts𝑁)‘𝑥)))
176173, 175eqtr4d 2842 . . . . 5 ((𝜑𝑥 ∈ (0(,)1)) → (∏𝑎 ∈ (1..^3)(((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥) · (((Λ ∘𝑓 · 𝐻)vts𝑁)‘𝑥)) = ((((Λ ∘𝑓 · 𝐻)vts𝑁)‘𝑥) · ((((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥)↑2)))
177136, 142, 1763eqtr3d 2847 . . . 4 ((𝜑𝑥 ∈ (0(,)1)) → ∏𝑎 ∈ (0..^3)(((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥) = ((((Λ ∘𝑓 · 𝐻)vts𝑁)‘𝑥) · ((((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥)↑2)))
178177oveq1d 6886 . . 3 ((𝜑𝑥 ∈ (0(,)1)) → (∏𝑎 ∈ (0..^3)(((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) = (((((Λ ∘𝑓 · 𝐻)vts𝑁)‘𝑥) · ((((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥)↑2)) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))))
179178itgeq2dv 23758 . 2 (𝜑 → ∫(0(,)1)(∏𝑎 ∈ (0..^3)(((⟨“(Λ ∘𝑓 · 𝐻)(Λ ∘𝑓 · 𝐾)(Λ ∘𝑓 · 𝐾)”⟩‘𝑎)vts𝑁)‘𝑥) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) d𝑥 = ∫(0(,)1)(((((Λ ∘𝑓 · 𝐻)vts𝑁)‘𝑥) · ((((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥)↑2)) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) d𝑥)
18027, 102, 1793eqtr3d 2847 1 (𝜑 → Σ𝑛 ∈ (ℕ(repr‘3)𝑁)(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) = ∫(0(,)1)(((((Λ ∘𝑓 · 𝐻)vts𝑁)‘𝑥) · ((((Λ ∘𝑓 · 𝐾)vts𝑁)‘𝑥)↑2)) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) d𝑥)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 865   = wceq 1637  wcel 2158  Vcvv 3390  cun 3764  wss 3766  {csn 4367  {cpr 4369  {ctp 4371   Fn wfn 6093  wf 6094  cfv 6098  (class class class)co 6871  𝑓 cof 7122  𝑚 cmap 8089  Fincfn 8189  cc 10216  cr 10217  0cc0 10218  1c1 10219  ici 10220   · cmul 10223  cmin 10548  -cneg 10549  cn 11302  2c2 11352  3c3 11353  0cn0 11555  cz 11639  cuz 11900  (,)cioo 12389  ...cfz 12545  ..^cfzo 12685  cexp 13079  chash 13333  ⟨“cs3 13807  Σcsu 14635  cprod 14852  expce 15008  πcpi 15013  citg 23595  Λcvma 25028  reprcrepr 31008  vtscvts 31035
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-8 2160  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784  ax-rep 4960  ax-sep 4971  ax-nul 4980  ax-pow 5032  ax-pr 5093  ax-un 7176  ax-inf2 8782  ax-cc 9539  ax-cnex 10274  ax-resscn 10275  ax-1cn 10276  ax-icn 10277  ax-addcl 10278  ax-addrcl 10279  ax-mulcl 10280  ax-mulrcl 10281  ax-mulcom 10282  ax-addass 10283  ax-mulass 10284  ax-distr 10285  ax-i2m1 10286  ax-1ne0 10287  ax-1rid 10288  ax-rnegex 10289  ax-rrecex 10290  ax-cnre 10291  ax-pre-lttri 10292  ax-pre-lttrn 10293  ax-pre-ltadd 10294  ax-pre-mulgt0 10295  ax-pre-sup 10296  ax-addf 10297  ax-mulf 10298
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1865  df-sb 2063  df-eu 2636  df-mo 2637  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-ne 2978  df-nel 3081  df-ral 3100  df-rex 3101  df-reu 3102  df-rmo 3103  df-rab 3104  df-v 3392  df-sbc 3631  df-csb 3726  df-dif 3769  df-un 3771  df-in 3773  df-ss 3780  df-pss 3782  df-symdif 4039  df-nul 4114  df-if 4277  df-pw 4350  df-sn 4368  df-pr 4370  df-tp 4372  df-op 4374  df-uni 4627  df-int 4666  df-iun 4710  df-iin 4711  df-disj 4809  df-br 4841  df-opab 4903  df-mpt 4920  df-tr 4943  df-id 5216  df-eprel 5221  df-po 5229  df-so 5230  df-fr 5267  df-se 5268  df-we 5269  df-xp 5314  df-rel 5315  df-cnv 5316  df-co 5317  df-dm 5318  df-rn 5319  df-res 5320  df-ima 5321  df-pred 5890  df-ord 5936  df-on 5937  df-lim 5938  df-suc 5939  df-iota 6061  df-fun 6100  df-fn 6101  df-f 6102  df-f1 6103  df-fo 6104  df-f1o 6105  df-fv 6106  df-isom 6107  df-riota 6832  df-ov 6874  df-oprab 6875  df-mpt2 6876  df-of 7124  df-ofr 7125  df-om 7293  df-1st 7395  df-2nd 7396  df-supp 7527  df-wrecs 7639  df-recs 7701  df-rdg 7739  df-1o 7793  df-2o 7794  df-oadd 7797  df-omul 7798  df-er 7976  df-map 8091  df-pm 8092  df-ixp 8143  df-en 8190  df-dom 8191  df-sdom 8192  df-fin 8193  df-fsupp 8512  df-fi 8553  df-sup 8584  df-inf 8585  df-oi 8651  df-card 9045  df-acn 9048  df-cda 9272  df-pnf 10358  df-mnf 10359  df-xr 10360  df-ltxr 10361  df-le 10362  df-sub 10550  df-neg 10551  df-div 10967  df-nn 11303  df-2 11360  df-3 11361  df-4 11362  df-5 11363  df-6 11364  df-7 11365  df-8 11366  df-9 11367  df-n0 11556  df-z 11640  df-dec 11756  df-uz 11901  df-q 12004  df-rp 12043  df-xneg 12158  df-xadd 12159  df-xmul 12160  df-ioo 12393  df-ioc 12394  df-ico 12395  df-icc 12396  df-fz 12546  df-fzo 12686  df-fl 12813  df-mod 12889  df-seq 13021  df-exp 13080  df-fac 13277  df-bc 13306  df-hash 13334  df-word 13506  df-concat 13508  df-s1 13509  df-s2 13813  df-s3 13814  df-shft 14026  df-cj 14058  df-re 14059  df-im 14060  df-sqrt 14194  df-abs 14195  df-limsup 14421  df-clim 14438  df-rlim 14439  df-sum 14636  df-prod 14853  df-ef 15014  df-sin 15016  df-cos 15017  df-pi 15019  df-dvds 15200  df-gcd 15432  df-prm 15600  df-pc 15755  df-struct 16066  df-ndx 16067  df-slot 16068  df-base 16070  df-sets 16071  df-ress 16072  df-plusg 16162  df-mulr 16163  df-starv 16164  df-sca 16165  df-vsca 16166  df-ip 16167  df-tset 16168  df-ple 16169  df-ds 16171  df-unif 16172  df-hom 16173  df-cco 16174  df-rest 16284  df-topn 16285  df-0g 16303  df-gsum 16304  df-topgen 16305  df-pt 16306  df-prds 16309  df-xrs 16363  df-qtop 16368  df-imas 16369  df-xps 16371  df-mre 16447  df-mrc 16448  df-acs 16450  df-mgm 17443  df-sgrp 17485  df-mnd 17496  df-submnd 17537  df-mulg 17742  df-cntz 17947  df-cmn 18392  df-psmet 19942  df-xmet 19943  df-met 19944  df-bl 19945  df-mopn 19946  df-fbas 19947  df-fg 19948  df-cnfld 19951  df-top 20908  df-topon 20925  df-topsp 20947  df-bases 20960  df-cld 21033  df-ntr 21034  df-cls 21035  df-nei 21112  df-lp 21150  df-perf 21151  df-cn 21241  df-cnp 21242  df-haus 21329  df-cmp 21400  df-tx 21575  df-hmeo 21768  df-fil 21859  df-fm 21951  df-flim 21952  df-flf 21953  df-xms 22334  df-ms 22335  df-tms 22336  df-cncf 22890  df-ovol 23441  df-vol 23442  df-mbf 23596  df-itg1 23597  df-itg2 23598  df-ibl 23599  df-itg 23600  df-0p 23647  df-limc 23840  df-dv 23841  df-log 24513  df-vma 25034  df-repr 31009  df-vts 31036
This theorem is referenced by:  tgoldbachgtde  31060
  Copyright terms: Public domain W3C validator