Proof of Theorem tgoldbachgtde
Step | Hyp | Ref
| Expression |
1 | | tgoldbachgtda.o |
. . . . . . . . 9
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧} |
2 | | tgoldbachgtda.n |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ 𝑂) |
3 | | tgoldbachgtda.0 |
. . . . . . . . 9
⊢ (𝜑 → (;10↑;27) ≤ 𝑁) |
4 | 1, 2, 3 | tgoldbachgnn 30737 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℕ) |
5 | 4 | nnnn0d 11351 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
6 | | 3nn0 11310 |
. . . . . . . 8
⊢ 3 ∈
ℕ0 |
7 | 6 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 3 ∈
ℕ0) |
8 | | ssid 3624 |
. . . . . . . 8
⊢ ℕ
⊆ ℕ |
9 | 8 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℕ ⊆
ℕ) |
10 | 5, 7, 9 | reprfi2 30701 |
. . . . . 6
⊢ (𝜑 →
(ℕ(repr‘3)𝑁)
∈ Fin) |
11 | | diffi 8192 |
. . . . . 6
⊢
((ℕ(repr‘3)𝑁) ∈ Fin →
((ℕ(repr‘3)𝑁)
∖ ((𝑂 ∩
ℙ)(repr‘3)𝑁))
∈ Fin) |
12 | 10, 11 | syl 17 |
. . . . 5
⊢ (𝜑 →
((ℕ(repr‘3)𝑁)
∖ ((𝑂 ∩
ℙ)(repr‘3)𝑁))
∈ Fin) |
13 | | difssd 3738 |
. . . . . . 7
⊢ (𝜑 →
((ℕ(repr‘3)𝑁)
∖ ((𝑂 ∩
ℙ)(repr‘3)𝑁))
⊆ (ℕ(repr‘3)𝑁)) |
14 | 13 | sselda 3603 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝑛 ∈ (ℕ(repr‘3)𝑁)) |
15 | | vmaf 24845 |
. . . . . . . . . 10
⊢
Λ:ℕ⟶ℝ |
16 | 15 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) →
Λ:ℕ⟶ℝ) |
17 | 8 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → ℕ ⊆
ℕ) |
18 | 5 | nn0zd 11480 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℤ) |
19 | 18 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → 𝑁 ∈ ℤ) |
20 | 6 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → 3 ∈
ℕ0) |
21 | | simpr 477 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → 𝑛 ∈ (ℕ(repr‘3)𝑁)) |
22 | 17, 19, 20, 21 | reprf 30690 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → 𝑛:(0..^3)⟶ℕ) |
23 | | c0ex 10034 |
. . . . . . . . . . . . 13
⊢ 0 ∈
V |
24 | 23 | tpid1 4303 |
. . . . . . . . . . . 12
⊢ 0 ∈
{0, 1, 2} |
25 | | fzo0to3tp 12554 |
. . . . . . . . . . . 12
⊢ (0..^3) =
{0, 1, 2} |
26 | 24, 25 | eleqtrri 2700 |
. . . . . . . . . . 11
⊢ 0 ∈
(0..^3) |
27 | 26 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → 0 ∈
(0..^3)) |
28 | 22, 27 | ffvelrnd 6360 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → (𝑛‘0) ∈ ℕ) |
29 | 16, 28 | ffvelrnd 6360 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → (Λ‘(𝑛‘0)) ∈
ℝ) |
30 | | tgoldbachgtda.h |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐻:ℕ⟶(0[,)+∞)) |
31 | | rge0ssre 12280 |
. . . . . . . . . . 11
⊢
(0[,)+∞) ⊆ ℝ |
32 | | fss 6056 |
. . . . . . . . . . 11
⊢ ((𝐻:ℕ⟶(0[,)+∞)
∧ (0[,)+∞) ⊆ ℝ) → 𝐻:ℕ⟶ℝ) |
33 | 30, 31, 32 | sylancl 694 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐻:ℕ⟶ℝ) |
34 | 33 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → 𝐻:ℕ⟶ℝ) |
35 | 34, 28 | ffvelrnd 6360 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → (𝐻‘(𝑛‘0)) ∈ ℝ) |
36 | 29, 35 | remulcld 10070 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) →
((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) ∈ ℝ) |
37 | | 1ex 10035 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
V |
38 | 37 | tpid2 4304 |
. . . . . . . . . . . . 13
⊢ 1 ∈
{0, 1, 2} |
39 | 38, 25 | eleqtrri 2700 |
. . . . . . . . . . . 12
⊢ 1 ∈
(0..^3) |
40 | 39 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → 1 ∈
(0..^3)) |
41 | 22, 40 | ffvelrnd 6360 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → (𝑛‘1) ∈ ℕ) |
42 | 16, 41 | ffvelrnd 6360 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → (Λ‘(𝑛‘1)) ∈
ℝ) |
43 | | tgoldbachgtda.k |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾:ℕ⟶(0[,)+∞)) |
44 | | fss 6056 |
. . . . . . . . . . . 12
⊢ ((𝐾:ℕ⟶(0[,)+∞)
∧ (0[,)+∞) ⊆ ℝ) → 𝐾:ℕ⟶ℝ) |
45 | 43, 31, 44 | sylancl 694 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐾:ℕ⟶ℝ) |
46 | 45 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → 𝐾:ℕ⟶ℝ) |
47 | 46, 41 | ffvelrnd 6360 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → (𝐾‘(𝑛‘1)) ∈ ℝ) |
48 | 42, 47 | remulcld 10070 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) →
((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) ∈ ℝ) |
49 | | 2ex 11092 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
V |
50 | 49 | tpid3 4307 |
. . . . . . . . . . . . 13
⊢ 2 ∈
{0, 1, 2} |
51 | 50, 25 | eleqtrri 2700 |
. . . . . . . . . . . 12
⊢ 2 ∈
(0..^3) |
52 | 51 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → 2 ∈
(0..^3)) |
53 | 22, 52 | ffvelrnd 6360 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → (𝑛‘2) ∈ ℕ) |
54 | 16, 53 | ffvelrnd 6360 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → (Λ‘(𝑛‘2)) ∈
ℝ) |
55 | 46, 53 | ffvelrnd 6360 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) → (𝐾‘(𝑛‘2)) ∈ ℝ) |
56 | 54, 55 | remulcld 10070 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) →
((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))) ∈ ℝ) |
57 | 48, 56 | remulcld 10070 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) →
(((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2)))) ∈ ℝ) |
58 | 36, 57 | remulcld 10070 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) →
(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ∈
ℝ) |
59 | 14, 58 | syldan 487 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) →
(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ∈
ℝ) |
60 | 12, 59 | fsumrecl 14465 |
. . . 4
⊢ (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ∈
ℝ) |
61 | | 0nn0 11307 |
. . . . . . 7
⊢ 0 ∈
ℕ0 |
62 | | qssre 11798 |
. . . . . . . 8
⊢ ℚ
⊆ ℝ |
63 | | 4nn0 11311 |
. . . . . . . . . . . 12
⊢ 4 ∈
ℕ0 |
64 | | 2nn0 11309 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℕ0 |
65 | | nn0ssq 11796 |
. . . . . . . . . . . . . . . 16
⊢
ℕ0 ⊆ ℚ |
66 | | 8nn0 11315 |
. . . . . . . . . . . . . . . 16
⊢ 8 ∈
ℕ0 |
67 | 65, 66 | sselii 3600 |
. . . . . . . . . . . . . . 15
⊢ 8 ∈
ℚ |
68 | 63, 67 | dp2clq 29588 |
. . . . . . . . . . . . . 14
⊢ _48 ∈ ℚ |
69 | 64, 68 | dp2clq 29588 |
. . . . . . . . . . . . 13
⊢ _2_48 ∈ ℚ |
70 | 64, 69 | dp2clq 29588 |
. . . . . . . . . . . 12
⊢ _2_2_48
∈ ℚ |
71 | 63, 70 | dp2clq 29588 |
. . . . . . . . . . 11
⊢ _4_2_2_48
∈ ℚ |
72 | 61, 71 | dp2clq 29588 |
. . . . . . . . . 10
⊢ _0_4_2_2_48
∈ ℚ |
73 | 61, 72 | dp2clq 29588 |
. . . . . . . . 9
⊢ _0_0_4_2_2_48
∈ ℚ |
74 | 61, 73 | dp2clq 29588 |
. . . . . . . 8
⊢ _0_0_0_4_2_2_48
∈ ℚ |
75 | 62, 74 | sselii 3600 |
. . . . . . 7
⊢ _0_0_0_4_2_2_48
∈ ℝ |
76 | | dpcl 29598 |
. . . . . . 7
⊢ ((0
∈ ℕ0 ∧ _0_0_0_4_2_2_48
∈ ℝ) → (0._0_0_0_4_2_2_48)
∈ ℝ) |
77 | 61, 75, 76 | mp2an 708 |
. . . . . 6
⊢ (0._0_0_0_4_2_2_48)
∈ ℝ |
78 | 77 | a1i 11 |
. . . . 5
⊢ (𝜑 → (0._0_0_0_4_2_2_48)
∈ ℝ) |
79 | 4 | nnred 11035 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℝ) |
80 | 79 | resqcld 13035 |
. . . . 5
⊢ (𝜑 → (𝑁↑2) ∈ ℝ) |
81 | 78, 80 | remulcld 10070 |
. . . 4
⊢ (𝜑 → ((0._0_0_0_4_2_2_48)
· (𝑁↑2)) ∈
ℝ) |
82 | 10, 58 | fsumrecl 14465 |
. . . 4
⊢ (𝜑 → Σ𝑛 ∈ (ℕ(repr‘3)𝑁)(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ∈
ℝ) |
83 | | 7nn0 11314 |
. . . . . . . . 9
⊢ 7 ∈
ℕ0 |
84 | 6, 68 | dp2clq 29588 |
. . . . . . . . . 10
⊢ _3_48 ∈ ℚ |
85 | 62, 84 | sselii 3600 |
. . . . . . . . 9
⊢ _3_48 ∈ ℝ |
86 | | dpcl 29598 |
. . . . . . . . 9
⊢ ((7
∈ ℕ0 ∧ _3_48
∈ ℝ) → (7._3_48) ∈ ℝ) |
87 | 83, 85, 86 | mp2an 708 |
. . . . . . . 8
⊢ (7._3_48) ∈ ℝ |
88 | 87 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (7._3_48)
∈ ℝ) |
89 | 4 | nnrpd 11870 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈
ℝ+) |
90 | 89 | relogcld 24369 |
. . . . . . . 8
⊢ (𝜑 → (log‘𝑁) ∈
ℝ) |
91 | 5 | nn0ge0d 11354 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ 𝑁) |
92 | 79, 91 | resqrtcld 14156 |
. . . . . . . 8
⊢ (𝜑 → (√‘𝑁) ∈
ℝ) |
93 | 89 | sqrtgt0d 14151 |
. . . . . . . . 9
⊢ (𝜑 → 0 <
(√‘𝑁)) |
94 | 93 | gt0ne0d 10592 |
. . . . . . . 8
⊢ (𝜑 → (√‘𝑁) ≠ 0) |
95 | 90, 92, 94 | redivcld 10853 |
. . . . . . 7
⊢ (𝜑 → ((log‘𝑁) / (√‘𝑁)) ∈
ℝ) |
96 | 88, 95 | remulcld 10070 |
. . . . . 6
⊢ (𝜑 → ((7._3_48)
· ((log‘𝑁) /
(√‘𝑁))) ∈
ℝ) |
97 | 96, 80 | remulcld 10070 |
. . . . 5
⊢ (𝜑 → (((7._3_48)
· ((log‘𝑁) /
(√‘𝑁)))
· (𝑁↑2)) ∈
ℝ) |
98 | | tgoldbachgtda.1 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐾‘𝑚) ≤ (1._0_7_9_9_55)) |
99 | | tgoldbachgtda.2 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐻‘𝑚) ≤ (1._4_14)) |
100 | 1, 4, 3, 30, 43, 98, 99 | hgt750leme 30736 |
. . . . 5
⊢ (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ≤ (((7._3_48)
· ((log‘𝑁) /
(√‘𝑁)))
· (𝑁↑2))) |
101 | | 2z 11409 |
. . . . . . . 8
⊢ 2 ∈
ℤ |
102 | 101 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 2 ∈
ℤ) |
103 | 89, 102 | rpexpcld 13032 |
. . . . . 6
⊢ (𝜑 → (𝑁↑2) ∈
ℝ+) |
104 | | hgt750lem 30729 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ (;10↑;27) ≤ 𝑁) → ((7._3_48)
· ((log‘𝑁) /
(√‘𝑁))) <
(0._0_0_0_4_2_2_48)) |
105 | 5, 3, 104 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → ((7._3_48)
· ((log‘𝑁) /
(√‘𝑁))) <
(0._0_0_0_4_2_2_48)) |
106 | 96, 78, 103, 105 | ltmul1dd 11927 |
. . . . 5
⊢ (𝜑 → (((7._3_48)
· ((log‘𝑁) /
(√‘𝑁)))
· (𝑁↑2)) <
((0._0_0_0_4_2_2_48)
· (𝑁↑2))) |
107 | 60, 97, 81, 100, 106 | lelttrd 10195 |
. . . 4
⊢ (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) < ((0._0_0_0_4_2_2_48)
· (𝑁↑2))) |
108 | | tgoldbachgtda.3 |
. . . . 5
⊢ (𝜑 → ((0._0_0_0_4_2_2_48)
· (𝑁↑2)) ≤
∫(0(,)1)(((((Λ ∘𝑓 · 𝐻)vts𝑁)‘𝑥) · ((((Λ
∘𝑓 · 𝐾)vts𝑁)‘𝑥)↑2)) · (exp‘((i ·
(2 · π)) · (-𝑁 · 𝑥)))) d𝑥) |
109 | 33, 45, 5 | circlemethhgt 30721 |
. . . . 5
⊢ (𝜑 → Σ𝑛 ∈ (ℕ(repr‘3)𝑁)(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) = ∫(0(,)1)(((((Λ
∘𝑓 · 𝐻)vts𝑁)‘𝑥) · ((((Λ
∘𝑓 · 𝐾)vts𝑁)‘𝑥)↑2)) · (exp‘((i ·
(2 · π)) · (-𝑁 · 𝑥)))) d𝑥) |
110 | 108, 109 | breqtrrd 4681 |
. . . 4
⊢ (𝜑 → ((0._0_0_0_4_2_2_48)
· (𝑁↑2)) ≤
Σ𝑛 ∈
(ℕ(repr‘3)𝑁)(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2)))))) |
111 | 60, 81, 82, 107, 110 | ltletrd 10197 |
. . 3
⊢ (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) < Σ𝑛 ∈ (ℕ(repr‘3)𝑁)(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2)))))) |
112 | 60, 82 | posdifd 10614 |
. . 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)))))))) |
113 | 111, 112 | mpbid 222 |
. 2
⊢ (𝜑 → 0 < (Σ𝑛 ∈
(ℕ(repr‘3)𝑁)(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) − Σ𝑛 ∈
((ℕ(repr‘3)𝑁)
∖ ((𝑂 ∩
ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))))) |
114 | | inss2 3834 |
. . . . . . . 8
⊢ (𝑂 ∩ ℙ) ⊆
ℙ |
115 | | prmssnn 15390 |
. . . . . . . 8
⊢ ℙ
⊆ ℕ |
116 | 114, 115 | sstri 3612 |
. . . . . . 7
⊢ (𝑂 ∩ ℙ) ⊆
ℕ |
117 | 116 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝑂 ∩ ℙ) ⊆
ℕ) |
118 | 9, 18, 7, 117 | reprss 30695 |
. . . . 5
⊢ (𝜑 → ((𝑂 ∩ ℙ)(repr‘3)𝑁) ⊆
(ℕ(repr‘3)𝑁)) |
119 | 10, 118 | ssfid 8183 |
. . . 4
⊢ (𝜑 → ((𝑂 ∩ ℙ)(repr‘3)𝑁) ∈ Fin) |
120 | 118 | sselda 3603 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ((𝑂 ∩ ℙ)(repr‘3)𝑁)) → 𝑛 ∈ (ℕ(repr‘3)𝑁)) |
121 | 58 | recnd 10068 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ(repr‘3)𝑁)) →
(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ∈
ℂ) |
122 | 120, 121 | syldan 487 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ((𝑂 ∩ ℙ)(repr‘3)𝑁)) →
(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ∈
ℂ) |
123 | 119, 122 | fsumcl 14464 |
. . 3
⊢ (𝜑 → Σ𝑛 ∈ ((𝑂 ∩ ℙ)(repr‘3)𝑁)(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ∈
ℂ) |
124 | 60 | recnd 10068 |
. . 3
⊢ (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ∈
ℂ) |
125 | | disjdif 4040 |
. . . . 5
⊢ (((𝑂 ∩
ℙ)(repr‘3)𝑁)
∩ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) = ∅ |
126 | 125 | a1i 11 |
. . . 4
⊢ (𝜑 → (((𝑂 ∩ ℙ)(repr‘3)𝑁) ∩
((ℕ(repr‘3)𝑁)
∖ ((𝑂 ∩
ℙ)(repr‘3)𝑁)))
= ∅) |
127 | | undif 4049 |
. . . . . 6
⊢ (((𝑂 ∩
ℙ)(repr‘3)𝑁)
⊆ (ℕ(repr‘3)𝑁) ↔ (((𝑂 ∩ ℙ)(repr‘3)𝑁) ∪
((ℕ(repr‘3)𝑁)
∖ ((𝑂 ∩
ℙ)(repr‘3)𝑁)))
= (ℕ(repr‘3)𝑁)) |
128 | 118, 127 | sylib 208 |
. . . . 5
⊢ (𝜑 → (((𝑂 ∩ ℙ)(repr‘3)𝑁) ∪
((ℕ(repr‘3)𝑁)
∖ ((𝑂 ∩
ℙ)(repr‘3)𝑁)))
= (ℕ(repr‘3)𝑁)) |
129 | 128 | eqcomd 2628 |
. . . 4
⊢ (𝜑 →
(ℕ(repr‘3)𝑁) =
(((𝑂 ∩
ℙ)(repr‘3)𝑁)
∪ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁)))) |
130 | 126, 129,
10, 121 | fsumsplit 14471 |
. . 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))))))) |
131 | 123, 124,
130 | mvrraddd 10445 |
. 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)))))) |
132 | 113, 131 | breqtrd 4679 |
1
⊢ (𝜑 → 0 < Σ𝑛 ∈ ((𝑂 ∩ ℙ)(repr‘3)𝑁)(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2)))))) |