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

Theorem tgoldbachgtde 32746
Description: Lemma for tgoldbachgtd 32748. (Contributed by Thierry Arnoux, 15-Dec-2021.)
Hypotheses
Ref Expression
tgoldbachgtda.o 𝑂 = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧}
tgoldbachgtda.n (𝜑𝑁𝑂)
tgoldbachgtda.0 (𝜑 → (10↑27) ≤ 𝑁)
tgoldbachgtda.h (𝜑𝐻:ℕ⟶(0[,)+∞))
tgoldbachgtda.k (𝜑𝐾:ℕ⟶(0[,)+∞))
tgoldbachgtda.1 ((𝜑𝑚 ∈ ℕ) → (𝐾𝑚) ≤ (1.079955))
tgoldbachgtda.2 ((𝜑𝑚 ∈ ℕ) → (𝐻𝑚) ≤ (1.414))
tgoldbachgtda.3 (𝜑 → ((0.00042248) · (𝑁↑2)) ≤ ∫(0(,)1)(((((Λ ∘f · 𝐻)vts𝑁)‘𝑥) · ((((Λ ∘f · 𝐾)vts𝑁)‘𝑥)↑2)) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) d𝑥)
Assertion
Ref Expression
tgoldbachgtde (𝜑 → 0 < Σ𝑛 ∈ ((𝑂 ∩ ℙ)(repr‘3)𝑁)(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))))
Distinct variable groups:   𝑚,𝐻,𝑛,𝑥   𝑚,𝐾,𝑛,𝑥   𝑚,𝑁,𝑛,𝑥,𝑧   𝑚,𝑂,𝑛,𝑧   𝜑,𝑚,𝑛,𝑥
Allowed substitution hints:   𝜑(𝑧)   𝐻(𝑧)   𝐾(𝑧)   𝑂(𝑥)

Proof of Theorem tgoldbachgtde
StepHypRef Expression
1 tgoldbachgtda.o . . . . . . . . 9 𝑂 = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧}
2 tgoldbachgtda.n . . . . . . . . 9 (𝜑𝑁𝑂)
3 tgoldbachgtda.0 . . . . . . . . 9 (𝜑 → (10↑27) ≤ 𝑁)
41, 2, 3tgoldbachgnn 32745 . . . . . . . 8 (𝜑𝑁 ∈ ℕ)
54nnnn0d 12366 . . . . . . 7 (𝜑𝑁 ∈ ℕ0)
6 3nn0 12324 . . . . . . . 8 3 ∈ ℕ0
76a1i 11 . . . . . . 7 (𝜑 → 3 ∈ ℕ0)
8 ssidd 3954 . . . . . . 7 (𝜑 → ℕ ⊆ ℕ)
95, 7, 8reprfi2 32709 . . . . . 6 (𝜑 → (ℕ(repr‘3)𝑁) ∈ Fin)
10 diffi 9021 . . . . . 6 ((ℕ(repr‘3)𝑁) ∈ Fin → ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁)) ∈ Fin)
119, 10syl 17 . . . . 5 (𝜑 → ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁)) ∈ Fin)
12 difssd 4078 . . . . . . 7 (𝜑 → ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁)) ⊆ (ℕ(repr‘3)𝑁))
1312sselda 3931 . . . . . 6 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝑛 ∈ (ℕ(repr‘3)𝑁))
14 vmaf 26340 . . . . . . . . . 10 Λ:ℕ⟶ℝ
1514a1i 11 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → Λ:ℕ⟶ℝ)
16 ssidd 3954 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → ℕ ⊆ ℕ)
175nn0zd 12497 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℤ)
1817adantr 481 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → 𝑁 ∈ ℤ)
196a1i 11 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → 3 ∈ ℕ0)
20 simpr 485 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → 𝑛 ∈ (ℕ(repr‘3)𝑁))
2116, 18, 19, 20reprf 32698 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → 𝑛:(0..^3)⟶ℕ)
22 c0ex 11042 . . . . . . . . . . . . 13 0 ∈ V
2322tpid1 4714 . . . . . . . . . . . 12 0 ∈ {0, 1, 2}
24 fzo0to3tp 13546 . . . . . . . . . . . 12 (0..^3) = {0, 1, 2}
2523, 24eleqtrri 2837 . . . . . . . . . . 11 0 ∈ (0..^3)
2625a1i 11 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → 0 ∈ (0..^3))
2721, 26ffvelcdmd 7001 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → (𝑛‘0) ∈ ℕ)
2815, 27ffvelcdmd 7001 . . . . . . . 8 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → (Λ‘(𝑛‘0)) ∈ ℝ)
29 tgoldbachgtda.h . . . . . . . . . . 11 (𝜑𝐻:ℕ⟶(0[,)+∞))
30 rge0ssre 13261 . . . . . . . . . . 11 (0[,)+∞) ⊆ ℝ
31 fss 6654 . . . . . . . . . . 11 ((𝐻:ℕ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝐻:ℕ⟶ℝ)
3229, 30, 31sylancl 586 . . . . . . . . . 10 (𝜑𝐻:ℕ⟶ℝ)
3332adantr 481 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → 𝐻:ℕ⟶ℝ)
3433, 27ffvelcdmd 7001 . . . . . . . 8 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → (𝐻‘(𝑛‘0)) ∈ ℝ)
3528, 34remulcld 11078 . . . . . . 7 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → ((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) ∈ ℝ)
36 1ex 11044 . . . . . . . . . . . . . 14 1 ∈ V
3736tpid2 4716 . . . . . . . . . . . . 13 1 ∈ {0, 1, 2}
3837, 24eleqtrri 2837 . . . . . . . . . . . 12 1 ∈ (0..^3)
3938a1i 11 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → 1 ∈ (0..^3))
4021, 39ffvelcdmd 7001 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → (𝑛‘1) ∈ ℕ)
4115, 40ffvelcdmd 7001 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → (Λ‘(𝑛‘1)) ∈ ℝ)
42 tgoldbachgtda.k . . . . . . . . . . . 12 (𝜑𝐾:ℕ⟶(0[,)+∞))
43 fss 6654 . . . . . . . . . . . 12 ((𝐾:ℕ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝐾:ℕ⟶ℝ)
4442, 30, 43sylancl 586 . . . . . . . . . . 11 (𝜑𝐾:ℕ⟶ℝ)
4544adantr 481 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → 𝐾:ℕ⟶ℝ)
4645, 40ffvelcdmd 7001 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → (𝐾‘(𝑛‘1)) ∈ ℝ)
4741, 46remulcld 11078 . . . . . . . 8 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → ((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) ∈ ℝ)
48 2ex 12123 . . . . . . . . . . . . . 14 2 ∈ V
4948tpid3 4719 . . . . . . . . . . . . 13 2 ∈ {0, 1, 2}
5049, 24eleqtrri 2837 . . . . . . . . . . . 12 2 ∈ (0..^3)
5150a1i 11 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → 2 ∈ (0..^3))
5221, 51ffvelcdmd 7001 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → (𝑛‘2) ∈ ℕ)
5315, 52ffvelcdmd 7001 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → (Λ‘(𝑛‘2)) ∈ ℝ)
5445, 52ffvelcdmd 7001 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → (𝐾‘(𝑛‘2)) ∈ ℝ)
5553, 54remulcld 11078 . . . . . . . 8 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))) ∈ ℝ)
5647, 55remulcld 11078 . . . . . . 7 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2)))) ∈ ℝ)
5735, 56remulcld 11078 . . . . . 6 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → (((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ∈ ℝ)
5813, 57syldan 591 . . . . 5 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ∈ ℝ)
5911, 58fsumrecl 15518 . . . 4 (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ∈ ℝ)
60 0nn0 12321 . . . . . . 7 0 ∈ ℕ0
61 qssre 12772 . . . . . . . 8 ℚ ⊆ ℝ
62 4nn0 12325 . . . . . . . . . . . 12 4 ∈ ℕ0
63 2nn0 12323 . . . . . . . . . . . . 13 2 ∈ ℕ0
64 nn0ssq 12770 . . . . . . . . . . . . . . . 16 0 ⊆ ℚ
65 8nn0 12329 . . . . . . . . . . . . . . . 16 8 ∈ ℕ0
6664, 65sselii 3928 . . . . . . . . . . . . . . 15 8 ∈ ℚ
6762, 66dp2clq 31263 . . . . . . . . . . . . . 14 48 ∈ ℚ
6863, 67dp2clq 31263 . . . . . . . . . . . . 13 248 ∈ ℚ
6963, 68dp2clq 31263 . . . . . . . . . . . 12 2248 ∈ ℚ
7062, 69dp2clq 31263 . . . . . . . . . . 11 42248 ∈ ℚ
7160, 70dp2clq 31263 . . . . . . . . . 10 042248 ∈ ℚ
7260, 71dp2clq 31263 . . . . . . . . 9 0042248 ∈ ℚ
7360, 72dp2clq 31263 . . . . . . . 8 00042248 ∈ ℚ
7461, 73sselii 3928 . . . . . . 7 00042248 ∈ ℝ
75 dpcl 31273 . . . . . . 7 ((0 ∈ ℕ000042248 ∈ ℝ) → (0.00042248) ∈ ℝ)
7660, 74, 75mp2an 689 . . . . . 6 (0.00042248) ∈ ℝ
7776a1i 11 . . . . 5 (𝜑 → (0.00042248) ∈ ℝ)
784nnred 12061 . . . . . 6 (𝜑𝑁 ∈ ℝ)
7978resqcld 14038 . . . . 5 (𝜑 → (𝑁↑2) ∈ ℝ)
8077, 79remulcld 11078 . . . 4 (𝜑 → ((0.00042248) · (𝑁↑2)) ∈ ℝ)
819, 57fsumrecl 15518 . . . 4 (𝜑 → Σ𝑛 ∈ (ℕ(repr‘3)𝑁)(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ∈ ℝ)
82 7nn0 12328 . . . . . . . . 9 7 ∈ ℕ0
836, 67dp2clq 31263 . . . . . . . . . 10 348 ∈ ℚ
8461, 83sselii 3928 . . . . . . . . 9 348 ∈ ℝ
85 dpcl 31273 . . . . . . . . 9 ((7 ∈ ℕ0348 ∈ ℝ) → (7.348) ∈ ℝ)
8682, 84, 85mp2an 689 . . . . . . . 8 (7.348) ∈ ℝ
8786a1i 11 . . . . . . 7 (𝜑 → (7.348) ∈ ℝ)
884nnrpd 12843 . . . . . . . . 9 (𝜑𝑁 ∈ ℝ+)
8988relogcld 25850 . . . . . . . 8 (𝜑 → (log‘𝑁) ∈ ℝ)
905nn0ge0d 12369 . . . . . . . . 9 (𝜑 → 0 ≤ 𝑁)
9178, 90resqrtcld 15201 . . . . . . . 8 (𝜑 → (√‘𝑁) ∈ ℝ)
9288sqrtgt0d 15196 . . . . . . . . 9 (𝜑 → 0 < (√‘𝑁))
9392gt0ne0d 11612 . . . . . . . 8 (𝜑 → (√‘𝑁) ≠ 0)
9489, 91, 93redivcld 11876 . . . . . . 7 (𝜑 → ((log‘𝑁) / (√‘𝑁)) ∈ ℝ)
9587, 94remulcld 11078 . . . . . 6 (𝜑 → ((7.348) · ((log‘𝑁) / (√‘𝑁))) ∈ ℝ)
9695, 79remulcld 11078 . . . . 5 (𝜑 → (((7.348) · ((log‘𝑁) / (√‘𝑁))) · (𝑁↑2)) ∈ ℝ)
97 tgoldbachgtda.1 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → (𝐾𝑚) ≤ (1.079955))
98 tgoldbachgtda.2 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → (𝐻𝑚) ≤ (1.414))
991, 4, 3, 29, 42, 97, 98hgt750leme 32744 . . . . 5 (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ≤ (((7.348) · ((log‘𝑁) / (√‘𝑁))) · (𝑁↑2)))
100 2z 12425 . . . . . . . 8 2 ∈ ℤ
101100a1i 11 . . . . . . 7 (𝜑 → 2 ∈ ℤ)
10288, 101rpexpcld 14035 . . . . . 6 (𝜑 → (𝑁↑2) ∈ ℝ+)
103 hgt750lem 32737 . . . . . . 7 ((𝑁 ∈ ℕ0 ∧ (10↑27) ≤ 𝑁) → ((7.348) · ((log‘𝑁) / (√‘𝑁))) < (0.00042248))
1045, 3, 103syl2anc 584 . . . . . 6 (𝜑 → ((7.348) · ((log‘𝑁) / (√‘𝑁))) < (0.00042248))
10595, 77, 102, 104ltmul1dd 12900 . . . . 5 (𝜑 → (((7.348) · ((log‘𝑁) / (√‘𝑁))) · (𝑁↑2)) < ((0.00042248) · (𝑁↑2)))
10659, 96, 80, 99, 105lelttrd 11206 . . . 4 (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) < ((0.00042248) · (𝑁↑2)))
107 tgoldbachgtda.3 . . . . 5 (𝜑 → ((0.00042248) · (𝑁↑2)) ≤ ∫(0(,)1)(((((Λ ∘f · 𝐻)vts𝑁)‘𝑥) · ((((Λ ∘f · 𝐾)vts𝑁)‘𝑥)↑2)) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) d𝑥)
10832, 44, 5circlemethhgt 32729 . . . . 5 (𝜑 → Σ𝑛 ∈ (ℕ(repr‘3)𝑁)(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) = ∫(0(,)1)(((((Λ ∘f · 𝐻)vts𝑁)‘𝑥) · ((((Λ ∘f · 𝐾)vts𝑁)‘𝑥)↑2)) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) d𝑥)
109107, 108breqtrrd 5115 . . . 4 (𝜑 → ((0.00042248) · (𝑁↑2)) ≤ Σ𝑛 ∈ (ℕ(repr‘3)𝑁)(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))))
11059, 80, 81, 106, 109ltletrd 11208 . . 3 (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) < Σ𝑛 ∈ (ℕ(repr‘3)𝑁)(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))))
11159, 81posdifd 11635 . . 3 (𝜑 → (Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) < Σ𝑛 ∈ (ℕ(repr‘3)𝑁)(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ↔ 0 < (Σ𝑛 ∈ (ℕ(repr‘3)𝑁)(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) − Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))))))
112110, 111mpbid 231 . 2 (𝜑 → 0 < (Σ𝑛 ∈ (ℕ(repr‘3)𝑁)(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) − Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2)))))))
113 inss2 4174 . . . . . . . 8 (𝑂 ∩ ℙ) ⊆ ℙ
114 prmssnn 16451 . . . . . . . 8 ℙ ⊆ ℕ
115113, 114sstri 3940 . . . . . . 7 (𝑂 ∩ ℙ) ⊆ ℕ
116115a1i 11 . . . . . 6 (𝜑 → (𝑂 ∩ ℙ) ⊆ ℕ)
1178, 17, 7, 116reprss 32703 . . . . 5 (𝜑 → ((𝑂 ∩ ℙ)(repr‘3)𝑁) ⊆ (ℕ(repr‘3)𝑁))
1189, 117ssfid 9109 . . . 4 (𝜑 → ((𝑂 ∩ ℙ)(repr‘3)𝑁) ∈ Fin)
119117sselda 3931 . . . . 5 ((𝜑𝑛 ∈ ((𝑂 ∩ ℙ)(repr‘3)𝑁)) → 𝑛 ∈ (ℕ(repr‘3)𝑁))
12057recnd 11076 . . . . 5 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → (((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ∈ ℂ)
121119, 120syldan 591 . . . 4 ((𝜑𝑛 ∈ ((𝑂 ∩ ℙ)(repr‘3)𝑁)) → (((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ∈ ℂ)
122118, 121fsumcl 15517 . . 3 (𝜑 → Σ𝑛 ∈ ((𝑂 ∩ ℙ)(repr‘3)𝑁)(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ∈ ℂ)
12359recnd 11076 . . 3 (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ∈ ℂ)
124 disjdif 4416 . . . . 5 (((𝑂 ∩ ℙ)(repr‘3)𝑁) ∩ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) = ∅
125124a1i 11 . . . 4 (𝜑 → (((𝑂 ∩ ℙ)(repr‘3)𝑁) ∩ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) = ∅)
126 undif 4426 . . . . . 6 (((𝑂 ∩ ℙ)(repr‘3)𝑁) ⊆ (ℕ(repr‘3)𝑁) ↔ (((𝑂 ∩ ℙ)(repr‘3)𝑁) ∪ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) = (ℕ(repr‘3)𝑁))
127117, 126sylib 217 . . . . 5 (𝜑 → (((𝑂 ∩ ℙ)(repr‘3)𝑁) ∪ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) = (ℕ(repr‘3)𝑁))
128127eqcomd 2743 . . . 4 (𝜑 → (ℕ(repr‘3)𝑁) = (((𝑂 ∩ ℙ)(repr‘3)𝑁) ∪ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))))
129125, 128, 9, 120fsumsplit 15525 . . 3 (𝜑 → Σ𝑛 ∈ (ℕ(repr‘3)𝑁)(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) = (Σ𝑛 ∈ ((𝑂 ∩ ℙ)(repr‘3)𝑁)(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) + Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2)))))))
130122, 123, 129mvrraddd 11460 . 2 (𝜑 → (Σ𝑛 ∈ (ℕ(repr‘3)𝑁)(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) − Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2)))))) = Σ𝑛 ∈ ((𝑂 ∩ ℙ)(repr‘3)𝑁)(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))))
131112, 130breqtrd 5113 1 (𝜑 → 0 < Σ𝑛 ∈ ((𝑂 ∩ ℙ)(repr‘3)𝑁)(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396   = wceq 1540  wcel 2105  {crab 3404  cdif 3894  cun 3895  cin 3896  wss 3897  c0 4267  {ctp 4575   class class class wbr 5087  wf 6461  cfv 6465  (class class class)co 7315  f cof 7571  Fincfn 8781  cc 10942  cr 10943  0cc0 10944  1c1 10945  ici 10946   · cmul 10949  +∞cpnf 11079   < clt 11082  cle 11083  cmin 11278  -cneg 11279   / cdiv 11705  cn 12046  2c2 12101  3c3 12102  4c4 12103  5c5 12104  7c7 12106  8c8 12107  9c9 12108  0cn0 12306  cz 12392  cdc 12510  cq 12761  (,)cioo 13152  [,)cico 13154  ..^cfzo 13455  cexp 13855  csqrt 15016  Σcsu 15469  expce 15843  πcpi 15848  cdvds 16035  cprime 16446  citg 24854  logclog 25782  Λcvma 26313  cdp2 31253  .cdp 31270  reprcrepr 32694  vtscvts 32721
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-rep 5224  ax-sep 5238  ax-nul 5245  ax-pow 5303  ax-pr 5367  ax-un 7628  ax-reg 9421  ax-inf2 9470  ax-cc 10264  ax-ac2 10292  ax-cnex 11000  ax-resscn 11001  ax-1cn 11002  ax-icn 11003  ax-addcl 11004  ax-addrcl 11005  ax-mulcl 11006  ax-mulrcl 11007  ax-mulcom 11008  ax-addass 11009  ax-mulass 11010  ax-distr 11011  ax-i2m1 11012  ax-1ne0 11013  ax-1rid 11014  ax-rnegex 11015  ax-rrecex 11016  ax-cnre 11017  ax-pre-lttri 11018  ax-pre-lttrn 11019  ax-pre-ltadd 11020  ax-pre-mulgt0 11021  ax-pre-sup 11022  ax-addf 11023  ax-mulf 11024  ax-ros335 32731  ax-ros336 32732
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-symdif 4187  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-tp 4576  df-op 4578  df-uni 4851  df-int 4893  df-iun 4939  df-iin 4940  df-disj 5053  df-br 5088  df-opab 5150  df-mpt 5171  df-tr 5205  df-id 5507  df-eprel 5513  df-po 5521  df-so 5522  df-fr 5562  df-se 5563  df-we 5564  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-pred 6224  df-ord 6291  df-on 6292  df-lim 6293  df-suc 6294  df-iota 6417  df-fun 6467  df-fn 6468  df-f 6469  df-f1 6470  df-fo 6471  df-f1o 6472  df-fv 6473  df-isom 6474  df-riota 7272  df-ov 7318  df-oprab 7319  df-mpo 7320  df-of 7573  df-ofr 7574  df-om 7758  df-1st 7876  df-2nd 7877  df-supp 8025  df-frecs 8144  df-wrecs 8175  df-recs 8249  df-rdg 8288  df-1o 8344  df-2o 8345  df-oadd 8348  df-omul 8349  df-er 8546  df-map 8665  df-pm 8666  df-ixp 8734  df-en 8782  df-dom 8783  df-sdom 8784  df-fin 8785  df-fsupp 9199  df-fi 9240  df-sup 9271  df-inf 9272  df-oi 9339  df-r1 9593  df-rank 9594  df-dju 9730  df-card 9768  df-acn 9771  df-ac 9945  df-pnf 11084  df-mnf 11085  df-xr 11086  df-ltxr 11087  df-le 11088  df-sub 11280  df-neg 11281  df-div 11706  df-nn 12047  df-2 12109  df-3 12110  df-4 12111  df-5 12112  df-6 12113  df-7 12114  df-8 12115  df-9 12116  df-n0 12307  df-xnn0 12379  df-z 12393  df-dec 12511  df-uz 12656  df-q 12762  df-rp 12804  df-xneg 12921  df-xadd 12922  df-xmul 12923  df-ioo 13156  df-ioc 13157  df-ico 13158  df-icc 13159  df-fz 13313  df-fzo 13456  df-fl 13585  df-mod 13663  df-seq 13795  df-exp 13856  df-fac 14061  df-bc 14090  df-hash 14118  df-word 14290  df-concat 14346  df-s1 14373  df-s2 14633  df-s3 14634  df-shft 14850  df-cj 14882  df-re 14883  df-im 14884  df-sqrt 15018  df-abs 15019  df-limsup 15252  df-clim 15269  df-rlim 15270  df-sum 15470  df-prod 15688  df-ef 15849  df-e 15850  df-sin 15851  df-cos 15852  df-tan 15853  df-pi 15854  df-dvds 16036  df-gcd 16274  df-prm 16447  df-pc 16608  df-struct 16918  df-sets 16935  df-slot 16953  df-ndx 16965  df-base 16983  df-ress 17012  df-plusg 17045  df-mulr 17046  df-starv 17047  df-sca 17048  df-vsca 17049  df-ip 17050  df-tset 17051  df-ple 17052  df-ds 17054  df-unif 17055  df-hom 17056  df-cco 17057  df-rest 17203  df-topn 17204  df-0g 17222  df-gsum 17223  df-topgen 17224  df-pt 17225  df-prds 17228  df-xrs 17283  df-qtop 17288  df-imas 17289  df-xps 17291  df-mre 17365  df-mrc 17366  df-acs 17368  df-mgm 18396  df-sgrp 18445  df-mnd 18456  df-submnd 18501  df-mulg 18770  df-cntz 18992  df-pmtr 19119  df-cmn 19456  df-psmet 20661  df-xmet 20662  df-met 20663  df-bl 20664  df-mopn 20665  df-fbas 20666  df-fg 20667  df-cnfld 20670  df-top 22115  df-topon 22132  df-topsp 22154  df-bases 22168  df-cld 22242  df-ntr 22243  df-cls 22244  df-nei 22321  df-lp 22359  df-perf 22360  df-cn 22450  df-cnp 22451  df-haus 22538  df-cmp 22610  df-tx 22785  df-hmeo 22978  df-fil 23069  df-fm 23161  df-flim 23162  df-flf 23163  df-xms 23545  df-ms 23546  df-tms 23547  df-cncf 24113  df-ovol 24700  df-vol 24701  df-mbf 24855  df-itg1 24856  df-itg2 24857  df-ibl 24858  df-itg 24859  df-0p 24906  df-limc 25102  df-dv 25103  df-ulm 25608  df-log 25784  df-cxp 25785  df-atan 26089  df-cht 26318  df-vma 26319  df-chp 26320  df-dp2 31254  df-dp 31271  df-repr 32695  df-vts 32722
This theorem is referenced by:  tgoldbachgtda  32747
  Copyright terms: Public domain W3C validator