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

Theorem tgoldbachgtde 32107
 Description: Lemma for tgoldbachgtd 32109. (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 32106 . . . . . . . 8 (𝜑𝑁 ∈ ℕ)
54nnnn0d 11963 . . . . . . 7 (𝜑𝑁 ∈ ℕ0)
6 3nn0 11921 . . . . . . . 8 3 ∈ ℕ0
76a1i 11 . . . . . . 7 (𝜑 → 3 ∈ ℕ0)
8 ssidd 3940 . . . . . . 7 (𝜑 → ℕ ⊆ ℕ)
95, 7, 8reprfi2 32070 . . . . . 6 (𝜑 → (ℕ(repr‘3)𝑁) ∈ Fin)
10 diffi 8752 . . . . . 6 ((ℕ(repr‘3)𝑁) ∈ Fin → ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁)) ∈ Fin)
119, 10syl 17 . . . . 5 (𝜑 → ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁)) ∈ Fin)
12 difssd 4063 . . . . . . 7 (𝜑 → ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁)) ⊆ (ℕ(repr‘3)𝑁))
1312sselda 3917 . . . . . 6 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝑛 ∈ (ℕ(repr‘3)𝑁))
14 vmaf 25748 . . . . . . . . . 10 Λ:ℕ⟶ℝ
1514a1i 11 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → Λ:ℕ⟶ℝ)
16 ssidd 3940 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → ℕ ⊆ ℕ)
175nn0zd 12093 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℤ)
1817adantr 484 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → 𝑁 ∈ ℤ)
196a1i 11 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → 3 ∈ ℕ0)
20 simpr 488 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → 𝑛 ∈ (ℕ(repr‘3)𝑁))
2116, 18, 19, 20reprf 32059 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → 𝑛:(0..^3)⟶ℕ)
22 c0ex 10642 . . . . . . . . . . . . 13 0 ∈ V
2322tpid1 4667 . . . . . . . . . . . 12 0 ∈ {0, 1, 2}
24 fzo0to3tp 13138 . . . . . . . . . . . 12 (0..^3) = {0, 1, 2}
2523, 24eleqtrri 2889 . . . . . . . . . . 11 0 ∈ (0..^3)
2625a1i 11 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → 0 ∈ (0..^3))
2721, 26ffvelrnd 6839 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → (𝑛‘0) ∈ ℕ)
2815, 27ffvelrnd 6839 . . . . . . . 8 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → (Λ‘(𝑛‘0)) ∈ ℝ)
29 tgoldbachgtda.h . . . . . . . . . . 11 (𝜑𝐻:ℕ⟶(0[,)+∞))
30 rge0ssre 12854 . . . . . . . . . . 11 (0[,)+∞) ⊆ ℝ
31 fss 6509 . . . . . . . . . . 11 ((𝐻:ℕ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝐻:ℕ⟶ℝ)
3229, 30, 31sylancl 589 . . . . . . . . . 10 (𝜑𝐻:ℕ⟶ℝ)
3332adantr 484 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → 𝐻:ℕ⟶ℝ)
3433, 27ffvelrnd 6839 . . . . . . . 8 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → (𝐻‘(𝑛‘0)) ∈ ℝ)
3528, 34remulcld 10678 . . . . . . 7 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → ((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) ∈ ℝ)
36 1ex 10644 . . . . . . . . . . . . . 14 1 ∈ V
3736tpid2 4669 . . . . . . . . . . . . 13 1 ∈ {0, 1, 2}
3837, 24eleqtrri 2889 . . . . . . . . . . . 12 1 ∈ (0..^3)
3938a1i 11 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → 1 ∈ (0..^3))
4021, 39ffvelrnd 6839 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → (𝑛‘1) ∈ ℕ)
4115, 40ffvelrnd 6839 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → (Λ‘(𝑛‘1)) ∈ ℝ)
42 tgoldbachgtda.k . . . . . . . . . . . 12 (𝜑𝐾:ℕ⟶(0[,)+∞))
43 fss 6509 . . . . . . . . . . . 12 ((𝐾:ℕ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝐾:ℕ⟶ℝ)
4442, 30, 43sylancl 589 . . . . . . . . . . 11 (𝜑𝐾:ℕ⟶ℝ)
4544adantr 484 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → 𝐾:ℕ⟶ℝ)
4645, 40ffvelrnd 6839 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → (𝐾‘(𝑛‘1)) ∈ ℝ)
4741, 46remulcld 10678 . . . . . . . 8 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → ((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) ∈ ℝ)
48 2ex 11720 . . . . . . . . . . . . . 14 2 ∈ V
4948tpid3 4672 . . . . . . . . . . . . 13 2 ∈ {0, 1, 2}
5049, 24eleqtrri 2889 . . . . . . . . . . . 12 2 ∈ (0..^3)
5150a1i 11 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → 2 ∈ (0..^3))
5221, 51ffvelrnd 6839 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → (𝑛‘2) ∈ ℕ)
5315, 52ffvelrnd 6839 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → (Λ‘(𝑛‘2)) ∈ ℝ)
5445, 52ffvelrnd 6839 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → (𝐾‘(𝑛‘2)) ∈ ℝ)
5553, 54remulcld 10678 . . . . . . . 8 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))) ∈ ℝ)
5647, 55remulcld 10678 . . . . . . 7 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2)))) ∈ ℝ)
5735, 56remulcld 10678 . . . . . 6 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → (((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ∈ ℝ)
5813, 57syldan 594 . . . . 5 ((𝜑𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ∈ ℝ)
5911, 58fsumrecl 15103 . . . 4 (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ∈ ℝ)
60 0nn0 11918 . . . . . . 7 0 ∈ ℕ0
61 qssre 12366 . . . . . . . 8 ℚ ⊆ ℝ
62 4nn0 11922 . . . . . . . . . . . 12 4 ∈ ℕ0
63 2nn0 11920 . . . . . . . . . . . . 13 2 ∈ ℕ0
64 nn0ssq 12364 . . . . . . . . . . . . . . . 16 0 ⊆ ℚ
65 8nn0 11926 . . . . . . . . . . . . . . . 16 8 ∈ ℕ0
6664, 65sselii 3914 . . . . . . . . . . . . . . 15 8 ∈ ℚ
6762, 66dp2clq 30627 . . . . . . . . . . . . . 14 48 ∈ ℚ
6863, 67dp2clq 30627 . . . . . . . . . . . . 13 248 ∈ ℚ
6963, 68dp2clq 30627 . . . . . . . . . . . 12 2248 ∈ ℚ
7062, 69dp2clq 30627 . . . . . . . . . . 11 42248 ∈ ℚ
7160, 70dp2clq 30627 . . . . . . . . . 10 042248 ∈ ℚ
7260, 71dp2clq 30627 . . . . . . . . 9 0042248 ∈ ℚ
7360, 72dp2clq 30627 . . . . . . . 8 00042248 ∈ ℚ
7461, 73sselii 3914 . . . . . . 7 00042248 ∈ ℝ
75 dpcl 30637 . . . . . . 7 ((0 ∈ ℕ000042248 ∈ ℝ) → (0.00042248) ∈ ℝ)
7660, 74, 75mp2an 691 . . . . . 6 (0.00042248) ∈ ℝ
7776a1i 11 . . . . 5 (𝜑 → (0.00042248) ∈ ℝ)
784nnred 11658 . . . . . 6 (𝜑𝑁 ∈ ℝ)
7978resqcld 13627 . . . . 5 (𝜑 → (𝑁↑2) ∈ ℝ)
8077, 79remulcld 10678 . . . 4 (𝜑 → ((0.00042248) · (𝑁↑2)) ∈ ℝ)
819, 57fsumrecl 15103 . . . 4 (𝜑 → Σ𝑛 ∈ (ℕ(repr‘3)𝑁)(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ∈ ℝ)
82 7nn0 11925 . . . . . . . . 9 7 ∈ ℕ0
836, 67dp2clq 30627 . . . . . . . . . 10 348 ∈ ℚ
8461, 83sselii 3914 . . . . . . . . 9 348 ∈ ℝ
85 dpcl 30637 . . . . . . . . 9 ((7 ∈ ℕ0348 ∈ ℝ) → (7.348) ∈ ℝ)
8682, 84, 85mp2an 691 . . . . . . . 8 (7.348) ∈ ℝ
8786a1i 11 . . . . . . 7 (𝜑 → (7.348) ∈ ℝ)
884nnrpd 12437 . . . . . . . . 9 (𝜑𝑁 ∈ ℝ+)
8988relogcld 25258 . . . . . . . 8 (𝜑 → (log‘𝑁) ∈ ℝ)
905nn0ge0d 11966 . . . . . . . . 9 (𝜑 → 0 ≤ 𝑁)
9178, 90resqrtcld 14789 . . . . . . . 8 (𝜑 → (√‘𝑁) ∈ ℝ)
9288sqrtgt0d 14784 . . . . . . . . 9 (𝜑 → 0 < (√‘𝑁))
9392gt0ne0d 11211 . . . . . . . 8 (𝜑 → (√‘𝑁) ≠ 0)
9489, 91, 93redivcld 11475 . . . . . . 7 (𝜑 → ((log‘𝑁) / (√‘𝑁)) ∈ ℝ)
9587, 94remulcld 10678 . . . . . 6 (𝜑 → ((7.348) · ((log‘𝑁) / (√‘𝑁))) ∈ ℝ)
9695, 79remulcld 10678 . . . . 5 (𝜑 → (((7.348) · ((log‘𝑁) / (√‘𝑁))) · (𝑁↑2)) ∈ ℝ)
97 tgoldbachgtda.1 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → (𝐾𝑚) ≤ (1.079955))
98 tgoldbachgtda.2 . . . . . 6 ((𝜑𝑚 ∈ ℕ) → (𝐻𝑚) ≤ (1.414))
991, 4, 3, 29, 42, 97, 98hgt750leme 32105 . . . . 5 (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ≤ (((7.348) · ((log‘𝑁) / (√‘𝑁))) · (𝑁↑2)))
100 2z 12022 . . . . . . . 8 2 ∈ ℤ
101100a1i 11 . . . . . . 7 (𝜑 → 2 ∈ ℤ)
10288, 101rpexpcld 13624 . . . . . 6 (𝜑 → (𝑁↑2) ∈ ℝ+)
103 hgt750lem 32098 . . . . . . 7 ((𝑁 ∈ ℕ0 ∧ (10↑27) ≤ 𝑁) → ((7.348) · ((log‘𝑁) / (√‘𝑁))) < (0.00042248))
1045, 3, 103syl2anc 587 . . . . . 6 (𝜑 → ((7.348) · ((log‘𝑁) / (√‘𝑁))) < (0.00042248))
10595, 77, 102, 104ltmul1dd 12494 . . . . 5 (𝜑 → (((7.348) · ((log‘𝑁) / (√‘𝑁))) · (𝑁↑2)) < ((0.00042248) · (𝑁↑2)))
10659, 96, 80, 99, 105lelttrd 10805 . . . 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 32090 . . . . 5 (𝜑 → Σ𝑛 ∈ (ℕ(repr‘3)𝑁)(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) = ∫(0(,)1)(((((Λ ∘f · 𝐻)vts𝑁)‘𝑥) · ((((Λ ∘f · 𝐾)vts𝑁)‘𝑥)↑2)) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) d𝑥)
109107, 108breqtrrd 5062 . . . 4 (𝜑 → ((0.00042248) · (𝑁↑2)) ≤ Σ𝑛 ∈ (ℕ(repr‘3)𝑁)(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))))
11059, 80, 81, 106, 109ltletrd 10807 . . 3 (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) < Σ𝑛 ∈ (ℕ(repr‘3)𝑁)(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))))
11159, 81posdifd 11234 . . 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 235 . 2 (𝜑 → 0 < (Σ𝑛 ∈ (ℕ(repr‘3)𝑁)(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) − Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2)))))))
113 inss2 4159 . . . . . . . 8 (𝑂 ∩ ℙ) ⊆ ℙ
114 prmssnn 16030 . . . . . . . 8 ℙ ⊆ ℕ
115113, 114sstri 3926 . . . . . . 7 (𝑂 ∩ ℙ) ⊆ ℕ
116115a1i 11 . . . . . 6 (𝜑 → (𝑂 ∩ ℙ) ⊆ ℕ)
1178, 17, 7, 116reprss 32064 . . . . 5 (𝜑 → ((𝑂 ∩ ℙ)(repr‘3)𝑁) ⊆ (ℕ(repr‘3)𝑁))
1189, 117ssfid 8743 . . . 4 (𝜑 → ((𝑂 ∩ ℙ)(repr‘3)𝑁) ∈ Fin)
119117sselda 3917 . . . . 5 ((𝜑𝑛 ∈ ((𝑂 ∩ ℙ)(repr‘3)𝑁)) → 𝑛 ∈ (ℕ(repr‘3)𝑁))
12057recnd 10676 . . . . 5 ((𝜑𝑛 ∈ (ℕ(repr‘3)𝑁)) → (((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ∈ ℂ)
121119, 120syldan 594 . . . 4 ((𝜑𝑛 ∈ ((𝑂 ∩ ℙ)(repr‘3)𝑁)) → (((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ∈ ℂ)
122118, 121fsumcl 15102 . . 3 (𝜑 → Σ𝑛 ∈ ((𝑂 ∩ ℙ)(repr‘3)𝑁)(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ∈ ℂ)
12359recnd 10676 . . 3 (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ∈ ℂ)
124 disjdif 4382 . . . . 5 (((𝑂 ∩ ℙ)(repr‘3)𝑁) ∩ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) = ∅
125124a1i 11 . . . 4 (𝜑 → (((𝑂 ∩ ℙ)(repr‘3)𝑁) ∩ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) = ∅)
126 undif 4391 . . . . . 6 (((𝑂 ∩ ℙ)(repr‘3)𝑁) ⊆ (ℕ(repr‘3)𝑁) ↔ (((𝑂 ∩ ℙ)(repr‘3)𝑁) ∪ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) = (ℕ(repr‘3)𝑁))
127117, 126sylib 221 . . . . 5 (𝜑 → (((𝑂 ∩ ℙ)(repr‘3)𝑁) ∪ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) = (ℕ(repr‘3)𝑁))
128127eqcomd 2804 . . . 4 (𝜑 → (ℕ(repr‘3)𝑁) = (((𝑂 ∩ ℙ)(repr‘3)𝑁) ∪ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))))
129125, 128, 9, 120fsumsplit 15109 . . 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 11059 . 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 5060 1 (𝜑 → 0 < Σ𝑛 ∈ ((𝑂 ∩ ℙ)(repr‘3)𝑁)(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111  {crab 3110   ∖ cdif 3880   ∪ cun 3881   ∩ cin 3882   ⊆ wss 3883  ∅c0 4246  {ctp 4532   class class class wbr 5034  ⟶wf 6328  ‘cfv 6332  (class class class)co 7145   ∘f cof 7398  Fincfn 8510  ℂcc 10542  ℝcr 10543  0cc0 10544  1c1 10545  ici 10546   · cmul 10549  +∞cpnf 10679   < clt 10682   ≤ cle 10683   − cmin 10877  -cneg 10878   / cdiv 11304  ℕcn 11643  2c2 11698  3c3 11699  4c4 11700  5c5 11701  7c7 11703  8c8 11704  9c9 11705  ℕ0cn0 11903  ℤcz 11989  ;cdc 12106  ℚcq 12356  (,)cioo 12746  [,)cico 12748  ..^cfzo 13048  ↑cexp 13445  √csqrt 14604  Σcsu 15054  expce 15427  πcpi 15432   ∥ cdvds 15619  ℙcprime 16025  ∫citg 24263  logclog 25190  Λcvma 25721  _cdp2 30617  .cdp 30634  reprcrepr 32055  vtscvts 32082 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5158  ax-sep 5171  ax-nul 5178  ax-pow 5235  ax-pr 5299  ax-un 7454  ax-reg 9058  ax-inf2 9106  ax-cc 9864  ax-ac2 9892  ax-cnex 10600  ax-resscn 10601  ax-1cn 10602  ax-icn 10603  ax-addcl 10604  ax-addrcl 10605  ax-mulcl 10606  ax-mulrcl 10607  ax-mulcom 10608  ax-addass 10609  ax-mulass 10610  ax-distr 10611  ax-i2m1 10612  ax-1ne0 10613  ax-1rid 10614  ax-rnegex 10615  ax-rrecex 10616  ax-cnre 10617  ax-pre-lttri 10618  ax-pre-lttrn 10619  ax-pre-ltadd 10620  ax-pre-mulgt0 10621  ax-pre-sup 10622  ax-addf 10623  ax-mulf 10624  ax-ros335 32092  ax-ros336 32093 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3444  df-sbc 3723  df-csb 3831  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-symdif 4172  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4805  df-int 4843  df-iun 4887  df-iin 4888  df-disj 5000  df-br 5035  df-opab 5097  df-mpt 5115  df-tr 5141  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5482  df-se 5483  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6123  df-ord 6169  df-on 6170  df-lim 6171  df-suc 6172  df-iota 6291  df-fun 6334  df-fn 6335  df-f 6336  df-f1 6337  df-fo 6338  df-f1o 6339  df-fv 6340  df-isom 6341  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-of 7400  df-ofr 7401  df-om 7574  df-1st 7684  df-2nd 7685  df-supp 7827  df-wrecs 7948  df-recs 8009  df-rdg 8047  df-1o 8103  df-2o 8104  df-oadd 8107  df-omul 8108  df-er 8290  df-map 8409  df-pm 8410  df-ixp 8463  df-en 8511  df-dom 8512  df-sdom 8513  df-fin 8514  df-fsupp 8836  df-fi 8877  df-sup 8908  df-inf 8909  df-oi 8976  df-r1 9195  df-rank 9196  df-dju 9332  df-card 9370  df-acn 9373  df-ac 9545  df-pnf 10684  df-mnf 10685  df-xr 10686  df-ltxr 10687  df-le 10688  df-sub 10879  df-neg 10880  df-div 11305  df-nn 11644  df-2 11706  df-3 11707  df-4 11708  df-5 11709  df-6 11710  df-7 11711  df-8 11712  df-9 11713  df-n0 11904  df-xnn0 11976  df-z 11990  df-dec 12107  df-uz 12252  df-q 12357  df-rp 12398  df-xneg 12515  df-xadd 12516  df-xmul 12517  df-ioo 12750  df-ioc 12751  df-ico 12752  df-icc 12753  df-fz 12906  df-fzo 13049  df-fl 13177  df-mod 13253  df-seq 13385  df-exp 13446  df-fac 13650  df-bc 13679  df-hash 13707  df-word 13878  df-concat 13934  df-s1 13961  df-s2 14221  df-s3 14222  df-shft 14438  df-cj 14470  df-re 14471  df-im 14472  df-sqrt 14606  df-abs 14607  df-limsup 14840  df-clim 14857  df-rlim 14858  df-sum 15055  df-prod 15272  df-ef 15433  df-e 15434  df-sin 15435  df-cos 15436  df-tan 15437  df-pi 15438  df-dvds 15620  df-gcd 15854  df-prm 16026  df-pc 16184  df-struct 16497  df-ndx 16498  df-slot 16499  df-base 16501  df-sets 16502  df-ress 16503  df-plusg 16590  df-mulr 16591  df-starv 16592  df-sca 16593  df-vsca 16594  df-ip 16595  df-tset 16596  df-ple 16597  df-ds 16599  df-unif 16600  df-hom 16601  df-cco 16602  df-rest 16708  df-topn 16709  df-0g 16727  df-gsum 16728  df-topgen 16729  df-pt 16730  df-prds 16733  df-xrs 16787  df-qtop 16792  df-imas 16793  df-xps 16795  df-mre 16869  df-mrc 16870  df-acs 16872  df-mgm 17864  df-sgrp 17913  df-mnd 17924  df-submnd 17969  df-mulg 18238  df-cntz 18460  df-pmtr 18583  df-cmn 18921  df-psmet 20104  df-xmet 20105  df-met 20106  df-bl 20107  df-mopn 20108  df-fbas 20109  df-fg 20110  df-cnfld 20113  df-top 21540  df-topon 21557  df-topsp 21579  df-bases 21592  df-cld 21665  df-ntr 21666  df-cls 21667  df-nei 21744  df-lp 21782  df-perf 21783  df-cn 21873  df-cnp 21874  df-haus 21961  df-cmp 22033  df-tx 22208  df-hmeo 22401  df-fil 22492  df-fm 22584  df-flim 22585  df-flf 22586  df-xms 22968  df-ms 22969  df-tms 22970  df-cncf 23524  df-ovol 24109  df-vol 24110  df-mbf 24264  df-itg1 24265  df-itg2 24266  df-ibl 24267  df-itg 24268  df-0p 24315  df-limc 24510  df-dv 24511  df-ulm 25016  df-log 25192  df-cxp 25193  df-atan 25497  df-cht 25726  df-vma 25727  df-chp 25728  df-dp2 30618  df-dp 30635  df-repr 32056  df-vts 32083 This theorem is referenced by:  tgoldbachgtda  32108
 Copyright terms: Public domain W3C validator