Step | Hyp | Ref
| Expression |
1 | | hgt750leme.n |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℕ) |
2 | 1 | nnnn0d 11351 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
3 | | 3nn0 11310 |
. . . . . 6
⊢ 3 ∈
ℕ0 |
4 | 3 | a1i 11 |
. . . . 5
⊢ (𝜑 → 3 ∈
ℕ0) |
5 | | ssid 3624 |
. . . . . 6
⊢ ℕ
⊆ ℕ |
6 | 5 | a1i 11 |
. . . . 5
⊢ (𝜑 → ℕ ⊆
ℕ) |
7 | 2, 4, 6 | reprfi2 30701 |
. . . 4
⊢ (𝜑 →
(ℕ(repr‘3)𝑁)
∈ Fin) |
8 | | diffi 8192 |
. . . 4
⊢
((ℕ(repr‘3)𝑁) ∈ Fin →
((ℕ(repr‘3)𝑁)
∖ ((𝑂 ∩
ℙ)(repr‘3)𝑁))
∈ Fin) |
9 | 7, 8 | syl 17 |
. . 3
⊢ (𝜑 →
((ℕ(repr‘3)𝑁)
∖ ((𝑂 ∩
ℙ)(repr‘3)𝑁))
∈ Fin) |
10 | | vmaf 24845 |
. . . . . . 7
⊢
Λ:ℕ⟶ℝ |
11 | 10 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) →
Λ:ℕ⟶ℝ) |
12 | 5 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → ℕ ⊆
ℕ) |
13 | 1 | nnzd 11481 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℤ) |
14 | 13 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝑁 ∈ ℤ) |
15 | 3 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 3 ∈
ℕ0) |
16 | | simpr 477 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) |
17 | 16 | eldifad 3586 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝑛 ∈ (ℕ(repr‘3)𝑁)) |
18 | 12, 14, 15, 17 | reprf 30690 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝑛:(0..^3)⟶ℕ) |
19 | | c0ex 10034 |
. . . . . . . . . 10
⊢ 0 ∈
V |
20 | 19 | tpid1 4303 |
. . . . . . . . 9
⊢ 0 ∈
{0, 1, 2} |
21 | | fzo0to3tp 12554 |
. . . . . . . . 9
⊢ (0..^3) =
{0, 1, 2} |
22 | 20, 21 | eleqtrri 2700 |
. . . . . . . 8
⊢ 0 ∈
(0..^3) |
23 | 22 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 0 ∈
(0..^3)) |
24 | 18, 23 | ffvelrnd 6360 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝑛‘0) ∈ ℕ) |
25 | 11, 24 | ffvelrnd 6360 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) →
(Λ‘(𝑛‘0)) ∈ ℝ) |
26 | | rge0ssre 12280 |
. . . . . 6
⊢
(0[,)+∞) ⊆ ℝ |
27 | | hgt750leme.h |
. . . . . . . 8
⊢ (𝜑 → 𝐻:ℕ⟶(0[,)+∞)) |
28 | 27 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝐻:ℕ⟶(0[,)+∞)) |
29 | 28, 24 | ffvelrnd 6360 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐻‘(𝑛‘0)) ∈
(0[,)+∞)) |
30 | 26, 29 | sseldi 3601 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐻‘(𝑛‘0)) ∈ ℝ) |
31 | 25, 30 | remulcld 10070 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) →
((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) ∈ ℝ) |
32 | | 1ex 10035 |
. . . . . . . . . . 11
⊢ 1 ∈
V |
33 | 32 | tpid2 4304 |
. . . . . . . . . 10
⊢ 1 ∈
{0, 1, 2} |
34 | 33, 21 | eleqtrri 2700 |
. . . . . . . . 9
⊢ 1 ∈
(0..^3) |
35 | 34 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 1 ∈
(0..^3)) |
36 | 18, 35 | ffvelrnd 6360 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝑛‘1) ∈ ℕ) |
37 | 11, 36 | ffvelrnd 6360 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) →
(Λ‘(𝑛‘1)) ∈ ℝ) |
38 | | hgt750leme.k |
. . . . . . . . 9
⊢ (𝜑 → 𝐾:ℕ⟶(0[,)+∞)) |
39 | 38 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 𝐾:ℕ⟶(0[,)+∞)) |
40 | 39, 36 | ffvelrnd 6360 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐾‘(𝑛‘1)) ∈
(0[,)+∞)) |
41 | 26, 40 | sseldi 3601 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐾‘(𝑛‘1)) ∈ ℝ) |
42 | 37, 41 | remulcld 10070 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) →
((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) ∈ ℝ) |
43 | | 2ex 11092 |
. . . . . . . . . . 11
⊢ 2 ∈
V |
44 | 43 | tpid3 4307 |
. . . . . . . . . 10
⊢ 2 ∈
{0, 1, 2} |
45 | 44, 21 | eleqtrri 2700 |
. . . . . . . . 9
⊢ 2 ∈
(0..^3) |
46 | 45 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → 2 ∈
(0..^3)) |
47 | 18, 46 | ffvelrnd 6360 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝑛‘2) ∈ ℕ) |
48 | 11, 47 | ffvelrnd 6360 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) →
(Λ‘(𝑛‘2)) ∈ ℝ) |
49 | 39, 47 | ffvelrnd 6360 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐾‘(𝑛‘2)) ∈
(0[,)+∞)) |
50 | 26, 49 | sseldi 3601 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) → (𝐾‘(𝑛‘2)) ∈ ℝ) |
51 | 48, 50 | remulcld 10070 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) →
((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))) ∈ ℝ) |
52 | 42, 51 | remulcld 10070 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) →
(((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2)))) ∈ ℝ) |
53 | 31, 52 | remulcld 10070 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) →
(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ∈
ℝ) |
54 | 9, 53 | fsumrecl 14465 |
. 2
⊢ (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ∈
ℝ) |
55 | | 3re 11094 |
. . . 4
⊢ 3 ∈
ℝ |
56 | 55 | a1i 11 |
. . 3
⊢ (𝜑 → 3 ∈
ℝ) |
57 | | 1nn0 11308 |
. . . . . . . . 9
⊢ 1 ∈
ℕ0 |
58 | | 0nn0 11307 |
. . . . . . . . . 10
⊢ 0 ∈
ℕ0 |
59 | | 7nn0 11314 |
. . . . . . . . . . 11
⊢ 7 ∈
ℕ0 |
60 | | 9nn0 11316 |
. . . . . . . . . . . 12
⊢ 9 ∈
ℕ0 |
61 | | 5nn0 11312 |
. . . . . . . . . . . . . 14
⊢ 5 ∈
ℕ0 |
62 | | 5nn 11188 |
. . . . . . . . . . . . . . 15
⊢ 5 ∈
ℕ |
63 | | nnrp 11842 |
. . . . . . . . . . . . . . 15
⊢ (5 ∈
ℕ → 5 ∈ ℝ+) |
64 | 62, 63 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ 5 ∈
ℝ+ |
65 | 61, 64 | rpdp2cl 29589 |
. . . . . . . . . . . . 13
⊢ _55 ∈
ℝ+ |
66 | 60, 65 | rpdp2cl 29589 |
. . . . . . . . . . . 12
⊢ _9_55 ∈ ℝ+ |
67 | 60, 66 | rpdp2cl 29589 |
. . . . . . . . . . 11
⊢ _9_9_55
∈ ℝ+ |
68 | 59, 67 | rpdp2cl 29589 |
. . . . . . . . . 10
⊢ _7_9_9_55
∈ ℝ+ |
69 | 58, 68 | rpdp2cl 29589 |
. . . . . . . . 9
⊢ _0_7_9_9_55
∈ ℝ+ |
70 | 57, 69 | rpdpcl 29611 |
. . . . . . . 8
⊢ (1._0_7_9_9_55)
∈ ℝ+ |
71 | 70 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (1._0_7_9_9_55)
∈ ℝ+) |
72 | 71 | rpred 11872 |
. . . . . 6
⊢ (𝜑 → (1._0_7_9_9_55)
∈ ℝ) |
73 | 72 | resqcld 13035 |
. . . . 5
⊢ (𝜑 → ((1._0_7_9_9_55)↑2) ∈ ℝ) |
74 | | 4nn0 11311 |
. . . . . . . . 9
⊢ 4 ∈
ℕ0 |
75 | | 4nn 11187 |
. . . . . . . . . . 11
⊢ 4 ∈
ℕ |
76 | | nnrp 11842 |
. . . . . . . . . . 11
⊢ (4 ∈
ℕ → 4 ∈ ℝ+) |
77 | 75, 76 | ax-mp 5 |
. . . . . . . . . 10
⊢ 4 ∈
ℝ+ |
78 | 57, 77 | rpdp2cl 29589 |
. . . . . . . . 9
⊢ _14 ∈
ℝ+ |
79 | 74, 78 | rpdp2cl 29589 |
. . . . . . . 8
⊢ _4_14 ∈ ℝ+ |
80 | 57, 79 | rpdpcl 29611 |
. . . . . . 7
⊢ (1._4_14) ∈ ℝ+ |
81 | 80 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (1._4_14)
∈ ℝ+) |
82 | 81 | rpred 11872 |
. . . . 5
⊢ (𝜑 → (1._4_14)
∈ ℝ) |
83 | 73, 82 | remulcld 10070 |
. . . 4
⊢ (𝜑 → (((1._0_7_9_9_55)↑2) · (1._4_14))
∈ ℝ) |
84 | | fveq1 6190 |
. . . . . . . . . 10
⊢ (𝑑 = 𝑐 → (𝑑‘0) = (𝑐‘0)) |
85 | 84 | eleq1d 2686 |
. . . . . . . . 9
⊢ (𝑑 = 𝑐 → ((𝑑‘0) ∈ (𝑂 ∩ ℙ) ↔ (𝑐‘0) ∈ (𝑂 ∩ ℙ))) |
86 | 85 | notbid 308 |
. . . . . . . 8
⊢ (𝑑 = 𝑐 → (¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ) ↔ ¬ (𝑐‘0) ∈ (𝑂 ∩
ℙ))) |
87 | 86 | cbvrabv 3199 |
. . . . . . 7
⊢ {𝑑 ∈
(ℕ(repr‘3)𝑁)
∣ ¬ (𝑑‘0)
∈ (𝑂 ∩ ℙ)} =
{𝑐 ∈
(ℕ(repr‘3)𝑁)
∣ ¬ (𝑐‘0)
∈ (𝑂 ∩
ℙ)} |
88 | 87 | ssrab3 3688 |
. . . . . 6
⊢ {𝑑 ∈
(ℕ(repr‘3)𝑁)
∣ ¬ (𝑑‘0)
∈ (𝑂 ∩ ℙ)}
⊆ (ℕ(repr‘3)𝑁) |
89 | | ssfi 8180 |
. . . . . 6
⊢
(((ℕ(repr‘3)𝑁) ∈ Fin ∧ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ⊆
(ℕ(repr‘3)𝑁))
→ {𝑑 ∈
(ℕ(repr‘3)𝑁)
∣ ¬ (𝑑‘0)
∈ (𝑂 ∩ ℙ)}
∈ Fin) |
90 | 7, 88, 89 | sylancl 694 |
. . . . 5
⊢ (𝜑 → {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ∈
Fin) |
91 | 10 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) →
Λ:ℕ⟶ℝ) |
92 | 5 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → ℕ
⊆ ℕ) |
93 | 13 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 𝑁 ∈
ℤ) |
94 | 3 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 3
∈ ℕ0) |
95 | 88 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)} ⊆
(ℕ(repr‘3)𝑁)) |
96 | 95 | sselda 3603 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 𝑛 ∈
(ℕ(repr‘3)𝑁)) |
97 | 92, 93, 94, 96 | reprf 30690 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 𝑛:(0..^3)⟶ℕ) |
98 | 22 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 0
∈ (0..^3)) |
99 | 97, 98 | ffvelrnd 6360 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (𝑛‘0) ∈
ℕ) |
100 | 91, 99 | ffvelrnd 6360 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) →
(Λ‘(𝑛‘0)) ∈ ℝ) |
101 | 34 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 1
∈ (0..^3)) |
102 | 97, 101 | ffvelrnd 6360 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (𝑛‘1) ∈
ℕ) |
103 | 91, 102 | ffvelrnd 6360 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) →
(Λ‘(𝑛‘1)) ∈ ℝ) |
104 | 45 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → 2
∈ (0..^3)) |
105 | 97, 104 | ffvelrnd 6360 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) → (𝑛‘2) ∈
ℕ) |
106 | 91, 105 | ffvelrnd 6360 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) →
(Λ‘(𝑛‘2)) ∈ ℝ) |
107 | 103, 106 | remulcld 10070 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) →
((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))) ∈
ℝ) |
108 | 100, 107 | remulcld 10070 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}) →
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2)))) ∈ ℝ) |
109 | 90, 108 | fsumrecl 14465 |
. . . 4
⊢ (𝜑 → Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2)))) ∈ ℝ) |
110 | 83, 109 | remulcld 10070 |
. . 3
⊢ (𝜑 → ((((1._0_7_9_9_55)↑2) · (1._4_14))
· Σ𝑛 ∈
{𝑑 ∈
(ℕ(repr‘3)𝑁)
∣ ¬ (𝑑‘0)
∈ (𝑂 ∩ ℙ)}
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2))))) ∈
ℝ) |
111 | 56, 110 | remulcld 10070 |
. 2
⊢ (𝜑 → (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14))
· Σ𝑛 ∈
{𝑑 ∈
(ℕ(repr‘3)𝑁)
∣ ¬ (𝑑‘0)
∈ (𝑂 ∩ ℙ)}
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2)))))) ∈
ℝ) |
112 | | 4re 11097 |
. . . . . . . . . 10
⊢ 4 ∈
ℝ |
113 | | 8re 11105 |
. . . . . . . . . 10
⊢ 8 ∈
ℝ |
114 | 112, 113 | pm3.2i 471 |
. . . . . . . . 9
⊢ (4 ∈
ℝ ∧ 8 ∈ ℝ) |
115 | | dp2cl 29587 |
. . . . . . . . 9
⊢ ((4
∈ ℝ ∧ 8 ∈ ℝ) → _48 ∈ ℝ) |
116 | 114, 115 | ax-mp 5 |
. . . . . . . 8
⊢ _48 ∈ ℝ |
117 | 55, 116 | pm3.2i 471 |
. . . . . . 7
⊢ (3 ∈
ℝ ∧ _48 ∈
ℝ) |
118 | | dp2cl 29587 |
. . . . . . 7
⊢ ((3
∈ ℝ ∧ _48 ∈
ℝ) → _3_48 ∈ ℝ) |
119 | 117, 118 | ax-mp 5 |
. . . . . 6
⊢ _3_48 ∈ ℝ |
120 | | dpcl 29598 |
. . . . . 6
⊢ ((7
∈ ℕ0 ∧ _3_48
∈ ℝ) → (7._3_48) ∈ ℝ) |
121 | 59, 119, 120 | mp2an 708 |
. . . . 5
⊢ (7._3_48) ∈ ℝ |
122 | 121 | a1i 11 |
. . . 4
⊢ (𝜑 → (7._3_48)
∈ ℝ) |
123 | 1 | nnrpd 11870 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈
ℝ+) |
124 | 123 | relogcld 24369 |
. . . . 5
⊢ (𝜑 → (log‘𝑁) ∈
ℝ) |
125 | 1 | nnred 11035 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℝ) |
126 | 123 | rpge0d 11876 |
. . . . . 6
⊢ (𝜑 → 0 ≤ 𝑁) |
127 | 125, 126 | resqrtcld 14156 |
. . . . 5
⊢ (𝜑 → (√‘𝑁) ∈
ℝ) |
128 | 123 | rpsqrtcld 14150 |
. . . . . 6
⊢ (𝜑 → (√‘𝑁) ∈
ℝ+) |
129 | 128 | rpne0d 11877 |
. . . . 5
⊢ (𝜑 → (√‘𝑁) ≠ 0) |
130 | 124, 127,
129 | redivcld 10853 |
. . . 4
⊢ (𝜑 → ((log‘𝑁) / (√‘𝑁)) ∈
ℝ) |
131 | 122, 130 | remulcld 10070 |
. . 3
⊢ (𝜑 → ((7._3_48)
· ((log‘𝑁) /
(√‘𝑁))) ∈
ℝ) |
132 | 125 | resqcld 13035 |
. . 3
⊢ (𝜑 → (𝑁↑2) ∈ ℝ) |
133 | 131, 132 | remulcld 10070 |
. 2
⊢ (𝜑 → (((7._3_48)
· ((log‘𝑁) /
(√‘𝑁)))
· (𝑁↑2)) ∈
ℝ) |
134 | | 0re 10040 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
135 | | 7re 11103 |
. . . . . . . . . . . . 13
⊢ 7 ∈
ℝ |
136 | | 9re 11107 |
. . . . . . . . . . . . . . 15
⊢ 9 ∈
ℝ |
137 | | 5re 11099 |
. . . . . . . . . . . . . . . . . . 19
⊢ 5 ∈
ℝ |
138 | 137, 137 | pm3.2i 471 |
. . . . . . . . . . . . . . . . . 18
⊢ (5 ∈
ℝ ∧ 5 ∈ ℝ) |
139 | | dp2cl 29587 |
. . . . . . . . . . . . . . . . . 18
⊢ ((5
∈ ℝ ∧ 5 ∈ ℝ) → _55 ∈ ℝ) |
140 | 138, 139 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ _55 ∈ ℝ |
141 | 136, 140 | pm3.2i 471 |
. . . . . . . . . . . . . . . 16
⊢ (9 ∈
ℝ ∧ _55 ∈
ℝ) |
142 | | dp2cl 29587 |
. . . . . . . . . . . . . . . 16
⊢ ((9
∈ ℝ ∧ _55 ∈
ℝ) → _9_55 ∈ ℝ) |
143 | 141, 142 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ _9_55 ∈ ℝ |
144 | 136, 143 | pm3.2i 471 |
. . . . . . . . . . . . . 14
⊢ (9 ∈
ℝ ∧ _9_55 ∈ ℝ) |
145 | | dp2cl 29587 |
. . . . . . . . . . . . . 14
⊢ ((9
∈ ℝ ∧ _9_55 ∈ ℝ) → _9_9_55
∈ ℝ) |
146 | 144, 145 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ _9_9_55
∈ ℝ |
147 | 135, 146 | pm3.2i 471 |
. . . . . . . . . . . 12
⊢ (7 ∈
ℝ ∧ _9_9_55
∈ ℝ) |
148 | | dp2cl 29587 |
. . . . . . . . . . . 12
⊢ ((7
∈ ℝ ∧ _9_9_55 ∈ ℝ) → _7_9_9_55
∈ ℝ) |
149 | 147, 148 | ax-mp 5 |
. . . . . . . . . . 11
⊢ _7_9_9_55
∈ ℝ |
150 | 134, 149 | pm3.2i 471 |
. . . . . . . . . 10
⊢ (0 ∈
ℝ ∧ _7_9_9_55
∈ ℝ) |
151 | | dp2cl 29587 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ ∧ _7_9_9_55
∈ ℝ) → _0_7_9_9_55
∈ ℝ) |
152 | 150, 151 | ax-mp 5 |
. . . . . . . . 9
⊢ _0_7_9_9_55
∈ ℝ |
153 | | dpcl 29598 |
. . . . . . . . 9
⊢ ((1
∈ ℕ0 ∧ _0_7_9_9_55
∈ ℝ) → (1._0_7_9_9_55)
∈ ℝ) |
154 | 57, 152, 153 | mp2an 708 |
. . . . . . . 8
⊢ (1._0_7_9_9_55)
∈ ℝ |
155 | 154 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (1._0_7_9_9_55)
∈ ℝ) |
156 | 155 | resqcld 13035 |
. . . . . 6
⊢ (𝜑 → ((1._0_7_9_9_55)↑2) ∈ ℝ) |
157 | | 1re 10039 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ |
158 | 157, 112 | pm3.2i 471 |
. . . . . . . . . . 11
⊢ (1 ∈
ℝ ∧ 4 ∈ ℝ) |
159 | | dp2cl 29587 |
. . . . . . . . . . 11
⊢ ((1
∈ ℝ ∧ 4 ∈ ℝ) → _14 ∈ ℝ) |
160 | 158, 159 | ax-mp 5 |
. . . . . . . . . 10
⊢ _14 ∈ ℝ |
161 | 112, 160 | pm3.2i 471 |
. . . . . . . . 9
⊢ (4 ∈
ℝ ∧ _14 ∈
ℝ) |
162 | | dp2cl 29587 |
. . . . . . . . 9
⊢ ((4
∈ ℝ ∧ _14 ∈
ℝ) → _4_14 ∈ ℝ) |
163 | 161, 162 | ax-mp 5 |
. . . . . . . 8
⊢ _4_14 ∈ ℝ |
164 | | dpcl 29598 |
. . . . . . . 8
⊢ ((1
∈ ℕ0 ∧ _4_14
∈ ℝ) → (1._4_14) ∈ ℝ) |
165 | 57, 163, 164 | mp2an 708 |
. . . . . . 7
⊢ (1._4_14) ∈ ℝ |
166 | 165 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (1._4_14)
∈ ℝ) |
167 | 156, 166 | remulcld 10070 |
. . . . 5
⊢ (𝜑 → (((1._0_7_9_9_55)↑2) · (1._4_14))
∈ ℝ) |
168 | 37, 48 | remulcld 10070 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) →
((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2))) ∈
ℝ) |
169 | 25, 168 | remulcld 10070 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))) →
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2)))) ∈ ℝ) |
170 | 9, 169 | fsumrecl 14465 |
. . . . 5
⊢ (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) ·
((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ∈
ℝ) |
171 | 167, 170 | remulcld 10070 |
. . . 4
⊢ (𝜑 → ((((1._0_7_9_9_55)↑2) · (1._4_14))
· Σ𝑛 ∈
((ℕ(repr‘3)𝑁)
∖ ((𝑂 ∩
ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2))))) ∈
ℝ) |
172 | 56, 109 | remulcld 10070 |
. . . . 5
⊢ (𝜑 → (3 · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2))))) ∈
ℝ) |
173 | 167, 172 | remulcld 10070 |
. . . 4
⊢ (𝜑 → ((((1._0_7_9_9_55)↑2) · (1._4_14))
· (3 · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2)))))) ∈
ℝ) |
174 | | hgt750leme.1 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐾‘𝑚) ≤ (1._0_7_9_9_55)) |
175 | | hgt750leme.2 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝐻‘𝑚) ≤ (1._4_14)) |
176 | 9, 155, 166, 27, 38, 24, 36, 47, 174, 175 | hgt750lemf 30731 |
. . . 4
⊢ (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ≤ ((((1._0_7_9_9_55)↑2) · (1._4_14))
· Σ𝑛 ∈
((ℕ(repr‘3)𝑁)
∖ ((𝑂 ∩
ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2)))))) |
177 | | hgt750leme.o |
. . . . . 6
⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧} |
178 | | 2re 11090 |
. . . . . . . 8
⊢ 2 ∈
ℝ |
179 | 178 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 2 ∈
ℝ) |
180 | | 10nn0 11516 |
. . . . . . . . . 10
⊢ ;10 ∈
ℕ0 |
181 | | 2nn0 11309 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ0 |
182 | 181, 59 | deccl 11512 |
. . . . . . . . . 10
⊢ ;27 ∈
ℕ0 |
183 | 180, 182 | nn0expcli 12886 |
. . . . . . . . 9
⊢ (;10↑;27) ∈ ℕ0 |
184 | 183 | nn0rei 11303 |
. . . . . . . 8
⊢ (;10↑;27) ∈ ℝ |
185 | 184 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (;10↑;27) ∈ ℝ) |
186 | 180 | numexp1 15781 |
. . . . . . . . . 10
⊢ (;10↑1) = ;10 |
187 | 180 | nn0rei 11303 |
. . . . . . . . . 10
⊢ ;10 ∈ ℝ |
188 | 186, 187 | eqeltri 2697 |
. . . . . . . . 9
⊢ (;10↑1) ∈
ℝ |
189 | 188 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (;10↑1) ∈ ℝ) |
190 | | 1nn 11031 |
. . . . . . . . . . 11
⊢ 1 ∈
ℕ |
191 | | 2lt9 11228 |
. . . . . . . . . . . 12
⊢ 2 <
9 |
192 | 178, 136,
191 | ltleii 10160 |
. . . . . . . . . . 11
⊢ 2 ≤
9 |
193 | 190, 58, 181, 192 | declei 11542 |
. . . . . . . . . 10
⊢ 2 ≤
;10 |
194 | 193, 186 | breqtrri 4680 |
. . . . . . . . 9
⊢ 2 ≤
(;10↑1) |
195 | 194 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 2 ≤ (;10↑1)) |
196 | | 1z 11407 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℤ |
197 | 182 | nn0zi 11402 |
. . . . . . . . . . . 12
⊢ ;27 ∈ ℤ |
198 | 187, 196,
197 | 3pm3.2i 1239 |
. . . . . . . . . . 11
⊢ (;10 ∈ ℝ ∧ 1 ∈
ℤ ∧ ;27 ∈
ℤ) |
199 | | 1lt10 11681 |
. . . . . . . . . . 11
⊢ 1 <
;10 |
200 | 198, 199 | pm3.2i 471 |
. . . . . . . . . 10
⊢ ((;10 ∈ ℝ ∧ 1 ∈
ℤ ∧ ;27 ∈ ℤ)
∧ 1 < ;10) |
201 | | 2nn 11185 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ |
202 | | 1lt9 11229 |
. . . . . . . . . . . 12
⊢ 1 <
9 |
203 | 157, 136,
202 | ltleii 10160 |
. . . . . . . . . . 11
⊢ 1 ≤
9 |
204 | 201, 59, 57, 203 | declei 11542 |
. . . . . . . . . 10
⊢ 1 ≤
;27 |
205 | | leexp2 12915 |
. . . . . . . . . . 11
⊢ (((;10 ∈ ℝ ∧ 1 ∈
ℤ ∧ ;27 ∈ ℤ)
∧ 1 < ;10) → (1 ≤
;27 ↔ (;10↑1) ≤ (;10↑;27))) |
206 | 205 | biimpa 501 |
. . . . . . . . . 10
⊢ ((((;10 ∈ ℝ ∧ 1 ∈
ℤ ∧ ;27 ∈ ℤ)
∧ 1 < ;10) ∧ 1 ≤
;27) → (;10↑1) ≤ (;10↑;27)) |
207 | 200, 204,
206 | mp2an 708 |
. . . . . . . . 9
⊢ (;10↑1) ≤ (;10↑;27) |
208 | 207 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (;10↑1) ≤ (;10↑;27)) |
209 | 179, 189,
185, 195, 208 | letrd 10194 |
. . . . . . 7
⊢ (𝜑 → 2 ≤ (;10↑;27)) |
210 | | hgt750leme.0 |
. . . . . . 7
⊢ (𝜑 → (;10↑;27) ≤ 𝑁) |
211 | 179, 185,
125, 209, 210 | letrd 10194 |
. . . . . 6
⊢ (𝜑 → 2 ≤ 𝑁) |
212 | | eqid 2622 |
. . . . . 6
⊢ (𝑒 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ↦ (𝑒 ∘ if(𝑎 = 0, ( I ↾ (0..^3)),
((pmTrsp‘(0..^3))‘{𝑎, 0})))) = (𝑒 ∈ {𝑐 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑐‘𝑎) ∈ (𝑂 ∩ ℙ)} ↦ (𝑒 ∘ if(𝑎 = 0, ( I ↾ (0..^3)),
((pmTrsp‘(0..^3))‘{𝑎, 0})))) |
213 | 177, 1, 211, 87, 212 | hgt750lema 30735 |
. . . . 5
⊢ (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) ·
((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ (3 ·
Σ𝑛 ∈ {𝑑 ∈
(ℕ(repr‘3)𝑁)
∣ ¬ (𝑑‘0)
∈ (𝑂 ∩ ℙ)}
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2)))))) |
214 | | 2z 11409 |
. . . . . . . . 9
⊢ 2 ∈
ℤ |
215 | 214 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 2 ∈
ℤ) |
216 | 71, 215 | rpexpcld 13032 |
. . . . . . 7
⊢ (𝜑 → ((1._0_7_9_9_55)↑2) ∈
ℝ+) |
217 | 216, 81 | rpmulcld 11888 |
. . . . . 6
⊢ (𝜑 → (((1._0_7_9_9_55)↑2) · (1._4_14))
∈ ℝ+) |
218 | 170, 172,
217 | lemul2d 11916 |
. . . . 5
⊢ (𝜑 → (Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) ·
((Λ‘(𝑛‘1)) · (Λ‘(𝑛‘2)))) ≤ (3 ·
Σ𝑛 ∈ {𝑑 ∈
(ℕ(repr‘3)𝑁)
∣ ¬ (𝑑‘0)
∈ (𝑂 ∩ ℙ)}
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2))))) ↔ ((((1._0_7_9_9_55)↑2) · (1._4_14))
· Σ𝑛 ∈
((ℕ(repr‘3)𝑁)
∖ ((𝑂 ∩
ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2))))) ≤ ((((1._0_7_9_9_55)↑2) · (1._4_14))
· (3 · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2)))))))) |
219 | 213, 218 | mpbid 222 |
. . . 4
⊢ (𝜑 → ((((1._0_7_9_9_55)↑2) · (1._4_14))
· Σ𝑛 ∈
((ℕ(repr‘3)𝑁)
∖ ((𝑂 ∩
ℙ)(repr‘3)𝑁))((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2))))) ≤ ((((1._0_7_9_9_55)↑2) · (1._4_14))
· (3 · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2))))))) |
220 | 54, 171, 173, 176, 219 | letrd 10194 |
. . 3
⊢ (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ≤ ((((1._0_7_9_9_55)↑2) · (1._4_14))
· (3 · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2))))))) |
221 | 155 | recnd 10068 |
. . . . . 6
⊢ (𝜑 → (1._0_7_9_9_55)
∈ ℂ) |
222 | 221 | sqcld 13006 |
. . . . 5
⊢ (𝜑 → ((1._0_7_9_9_55)↑2) ∈ ℂ) |
223 | 166 | recnd 10068 |
. . . . 5
⊢ (𝜑 → (1._4_14)
∈ ℂ) |
224 | 222, 223 | mulcld 10060 |
. . . 4
⊢ (𝜑 → (((1._0_7_9_9_55)↑2) · (1._4_14))
∈ ℂ) |
225 | | 3cn 11095 |
. . . . 5
⊢ 3 ∈
ℂ |
226 | 225 | a1i 11 |
. . . 4
⊢ (𝜑 → 3 ∈
ℂ) |
227 | 109 | recnd 10068 |
. . . 4
⊢ (𝜑 → Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2)))) ∈ ℂ) |
228 | 224, 226,
227 | mul12d 10245 |
. . 3
⊢ (𝜑 → ((((1._0_7_9_9_55)↑2) · (1._4_14))
· (3 · Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2)))))) = (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14))
· Σ𝑛 ∈
{𝑑 ∈
(ℕ(repr‘3)𝑁)
∣ ¬ (𝑑‘0)
∈ (𝑂 ∩ ℙ)}
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2))))))) |
229 | 220, 228 | breqtrd 4679 |
. 2
⊢ (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ≤ (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14))
· Σ𝑛 ∈
{𝑑 ∈
(ℕ(repr‘3)𝑁)
∣ ¬ (𝑑‘0)
∈ (𝑂 ∩ ℙ)}
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2))))))) |
230 | | fzfi 12771 |
. . . . . . . . . . 11
⊢
(1...𝑁) ∈
Fin |
231 | | diffi 8192 |
. . . . . . . . . . 11
⊢
((1...𝑁) ∈ Fin
→ ((1...𝑁) ∖
ℙ) ∈ Fin) |
232 | 230, 231 | ax-mp 5 |
. . . . . . . . . 10
⊢
((1...𝑁) ∖
ℙ) ∈ Fin |
233 | | snfi 8038 |
. . . . . . . . . 10
⊢ {2}
∈ Fin |
234 | | unfi 8227 |
. . . . . . . . . 10
⊢
((((1...𝑁) ∖
ℙ) ∈ Fin ∧ {2} ∈ Fin) → (((1...𝑁) ∖ ℙ) ∪ {2}) ∈
Fin) |
235 | 232, 233,
234 | mp2an 708 |
. . . . . . . . 9
⊢
(((1...𝑁) ∖
ℙ) ∪ {2}) ∈ Fin |
236 | 235 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (((1...𝑁) ∖ ℙ) ∪ {2}) ∈
Fin) |
237 | 10 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) →
Λ:ℕ⟶ℝ) |
238 | | fz1ssnn 12372 |
. . . . . . . . . . . . 13
⊢
(1...𝑁) ⊆
ℕ |
239 | 238 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1...𝑁) ⊆ ℕ) |
240 | 239 | ssdifssd 3748 |
. . . . . . . . . . 11
⊢ (𝜑 → ((1...𝑁) ∖ ℙ) ⊆
ℕ) |
241 | 201 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 2 ∈
ℕ) |
242 | 241 | snssd 4340 |
. . . . . . . . . . 11
⊢ (𝜑 → {2} ⊆
ℕ) |
243 | 240, 242 | unssd 3789 |
. . . . . . . . . 10
⊢ (𝜑 → (((1...𝑁) ∖ ℙ) ∪ {2}) ⊆
ℕ) |
244 | 243 | sselda 3603 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → 𝑖 ∈
ℕ) |
245 | 237, 244 | ffvelrnd 6360 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) →
(Λ‘𝑖) ∈
ℝ) |
246 | 236, 245 | fsumrecl 14465 |
. . . . . . 7
⊢ (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪
{2})(Λ‘𝑖)
∈ ℝ) |
247 | | chpvalz 30706 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℤ →
(ψ‘𝑁) =
Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) |
248 | 13, 247 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (ψ‘𝑁) = Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) |
249 | | chpf 24849 |
. . . . . . . . . 10
⊢
ψ:ℝ⟶ℝ |
250 | 249 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 →
ψ:ℝ⟶ℝ) |
251 | 250, 125 | ffvelrnd 6360 |
. . . . . . . 8
⊢ (𝜑 → (ψ‘𝑁) ∈
ℝ) |
252 | 248, 251 | eqeltrrd 2702 |
. . . . . . 7
⊢ (𝜑 → Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗) ∈ ℝ) |
253 | 246, 252 | remulcld 10070 |
. . . . . 6
⊢ (𝜑 → (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪
{2})(Λ‘𝑖)
· Σ𝑗 ∈
(1...𝑁)(Λ‘𝑗)) ∈ ℝ) |
254 | 124, 253 | remulcld 10070 |
. . . . 5
⊢ (𝜑 → ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪
{2})(Λ‘𝑖)
· Σ𝑗 ∈
(1...𝑁)(Λ‘𝑗))) ∈ ℝ) |
255 | 83, 254 | remulcld 10070 |
. . . 4
⊢ (𝜑 → ((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((log‘𝑁)
· (Σ𝑖 ∈
(((1...𝑁) ∖ ℙ)
∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))) ∈ ℝ) |
256 | 56, 255 | remulcld 10070 |
. . 3
⊢ (𝜑 → (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((log‘𝑁)
· (Σ𝑖 ∈
(((1...𝑁) ∖ ℙ)
∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))) ∈ ℝ) |
257 | 177, 1, 211, 87 | hgt750lemb 30734 |
. . . . 5
⊢ (𝜑 → Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2)))) ≤ ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪
{2})(Λ‘𝑖)
· Σ𝑗 ∈
(1...𝑁)(Λ‘𝑗)))) |
258 | 109, 254,
217 | lemul2d 11916 |
. . . . 5
⊢ (𝜑 → (Σ𝑛 ∈ {𝑑 ∈ (ℕ(repr‘3)𝑁) ∣ ¬ (𝑑‘0) ∈ (𝑂 ∩ ℙ)}
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2)))) ≤ ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪
{2})(Λ‘𝑖)
· Σ𝑗 ∈
(1...𝑁)(Λ‘𝑗))) ↔ ((((1._0_7_9_9_55)↑2) · (1._4_14))
· Σ𝑛 ∈
{𝑑 ∈
(ℕ(repr‘3)𝑁)
∣ ¬ (𝑑‘0)
∈ (𝑂 ∩ ℙ)}
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2))))) ≤ ((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((log‘𝑁)
· (Σ𝑖 ∈
(((1...𝑁) ∖ ℙ)
∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))))) |
259 | 257, 258 | mpbid 222 |
. . . 4
⊢ (𝜑 → ((((1._0_7_9_9_55)↑2) · (1._4_14))
· Σ𝑛 ∈
{𝑑 ∈
(ℕ(repr‘3)𝑁)
∣ ¬ (𝑑‘0)
∈ (𝑂 ∩ ℙ)}
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2))))) ≤ ((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((log‘𝑁)
· (Σ𝑖 ∈
(((1...𝑁) ∖ ℙ)
∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))) |
260 | | 3rp 11838 |
. . . . . 6
⊢ 3 ∈
ℝ+ |
261 | 260 | a1i 11 |
. . . . 5
⊢ (𝜑 → 3 ∈
ℝ+) |
262 | 110, 255,
261 | lemul2d 11916 |
. . . 4
⊢ (𝜑 → (((((1._0_7_9_9_55)↑2) · (1._4_14))
· Σ𝑛 ∈
{𝑑 ∈
(ℕ(repr‘3)𝑁)
∣ ¬ (𝑑‘0)
∈ (𝑂 ∩ ℙ)}
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2))))) ≤ ((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((log‘𝑁)
· (Σ𝑖 ∈
(((1...𝑁) ∖ ℙ)
∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))) ↔ (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14))
· Σ𝑛 ∈
{𝑑 ∈
(ℕ(repr‘3)𝑁)
∣ ¬ (𝑑‘0)
∈ (𝑂 ∩ ℙ)}
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2)))))) ≤ (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((log‘𝑁)
· (Σ𝑖 ∈
(((1...𝑁) ∖ ℙ)
∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))))) |
263 | 259, 262 | mpbid 222 |
. . 3
⊢ (𝜑 → (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14))
· Σ𝑛 ∈
{𝑑 ∈
(ℕ(repr‘3)𝑁)
∣ ¬ (𝑑‘0)
∈ (𝑂 ∩ ℙ)}
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2)))))) ≤ (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((log‘𝑁)
· (Σ𝑖 ∈
(((1...𝑁) ∖ ℙ)
∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))))) |
264 | | 6re 11101 |
. . . . . . . . . . . . . . . . 17
⊢ 6 ∈
ℝ |
265 | 264, 55 | pm3.2i 471 |
. . . . . . . . . . . . . . . 16
⊢ (6 ∈
ℝ ∧ 3 ∈ ℝ) |
266 | | dp2cl 29587 |
. . . . . . . . . . . . . . . 16
⊢ ((6
∈ ℝ ∧ 3 ∈ ℝ) → _63 ∈ ℝ) |
267 | 265, 266 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ _63 ∈ ℝ |
268 | 178, 267 | pm3.2i 471 |
. . . . . . . . . . . . . 14
⊢ (2 ∈
ℝ ∧ _63 ∈
ℝ) |
269 | | dp2cl 29587 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℝ ∧ _63 ∈
ℝ) → _2_63 ∈ ℝ) |
270 | 268, 269 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ _2_63 ∈ ℝ |
271 | 112, 270 | pm3.2i 471 |
. . . . . . . . . . . 12
⊢ (4 ∈
ℝ ∧ _2_63 ∈ ℝ) |
272 | | dp2cl 29587 |
. . . . . . . . . . . 12
⊢ ((4
∈ ℝ ∧ _2_63 ∈ ℝ) → _4_2_63
∈ ℝ) |
273 | 271, 272 | ax-mp 5 |
. . . . . . . . . . 11
⊢ _4_2_63
∈ ℝ |
274 | | dpcl 29598 |
. . . . . . . . . . 11
⊢ ((1
∈ ℕ0 ∧ _4_2_63
∈ ℝ) → (1._4_2_63) ∈ ℝ) |
275 | 57, 273, 274 | mp2an 708 |
. . . . . . . . . 10
⊢ (1._4_2_63)
∈ ℝ |
276 | 275 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (1._4_2_63)
∈ ℝ) |
277 | 276, 127 | remulcld 10070 |
. . . . . . . 8
⊢ (𝜑 → ((1._4_2_63)
· (√‘𝑁))
∈ ℝ) |
278 | 113, 55 | pm3.2i 471 |
. . . . . . . . . . . . . . . . . 18
⊢ (8 ∈
ℝ ∧ 3 ∈ ℝ) |
279 | | dp2cl 29587 |
. . . . . . . . . . . . . . . . . 18
⊢ ((8
∈ ℝ ∧ 3 ∈ ℝ) → _83 ∈ ℝ) |
280 | 278, 279 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ _83 ∈ ℝ |
281 | 113, 280 | pm3.2i 471 |
. . . . . . . . . . . . . . . 16
⊢ (8 ∈
ℝ ∧ _83 ∈
ℝ) |
282 | | dp2cl 29587 |
. . . . . . . . . . . . . . . 16
⊢ ((8
∈ ℝ ∧ _83 ∈
ℝ) → _8_83 ∈ ℝ) |
283 | 281, 282 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ _8_83 ∈ ℝ |
284 | 55, 283 | pm3.2i 471 |
. . . . . . . . . . . . . 14
⊢ (3 ∈
ℝ ∧ _8_83 ∈ ℝ) |
285 | | dp2cl 29587 |
. . . . . . . . . . . . . 14
⊢ ((3
∈ ℝ ∧ _8_83 ∈ ℝ) → _3_8_83
∈ ℝ) |
286 | 284, 285 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ _3_8_83
∈ ℝ |
287 | 134, 286 | pm3.2i 471 |
. . . . . . . . . . . 12
⊢ (0 ∈
ℝ ∧ _3_8_83
∈ ℝ) |
288 | | dp2cl 29587 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ ∧ _3_8_83 ∈ ℝ) → _0_3_8_83
∈ ℝ) |
289 | 287, 288 | ax-mp 5 |
. . . . . . . . . . 11
⊢ _0_3_8_83
∈ ℝ |
290 | | dpcl 29598 |
. . . . . . . . . . 11
⊢ ((1
∈ ℕ0 ∧ _0_3_8_83
∈ ℝ) → (1._0_3_8_83)
∈ ℝ) |
291 | 57, 289, 290 | mp2an 708 |
. . . . . . . . . 10
⊢ (1._0_3_8_83)
∈ ℝ |
292 | 291 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (1._0_3_8_83)
∈ ℝ) |
293 | 292, 125 | remulcld 10070 |
. . . . . . . 8
⊢ (𝜑 → ((1._0_3_8_83)
· 𝑁) ∈
ℝ) |
294 | 277, 293 | remulcld 10070 |
. . . . . . 7
⊢ (𝜑 → (((1._4_2_63)
· (√‘𝑁))
· ((1._0_3_8_83)
· 𝑁)) ∈
ℝ) |
295 | 124, 294 | remulcld 10070 |
. . . . . 6
⊢ (𝜑 → ((log‘𝑁) · (((1._4_2_63)
· (√‘𝑁))
· ((1._0_3_8_83)
· 𝑁))) ∈
ℝ) |
296 | 83, 295 | remulcld 10070 |
. . . . 5
⊢ (𝜑 → ((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((log‘𝑁)
· (((1._4_2_63)
· (√‘𝑁))
· ((1._0_3_8_83)
· 𝑁)))) ∈
ℝ) |
297 | 56, 296 | remulcld 10070 |
. . . 4
⊢ (𝜑 → (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((log‘𝑁)
· (((1._4_2_63)
· (√‘𝑁))
· ((1._0_3_8_83)
· 𝑁))))) ∈
ℝ) |
298 | | vmage0 24847 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ ℕ → 0 ≤
(Λ‘𝑖)) |
299 | 244, 298 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪ {2})) → 0 ≤
(Λ‘𝑖)) |
300 | 236, 245,
299 | fsumge0 14527 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪
{2})(Λ‘𝑖)) |
301 | 1, 210 | hgt750lemd 30726 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪
{2})(Λ‘𝑖) <
((1._4_2_63)
· (√‘𝑁))) |
302 | | fzfid 12772 |
. . . . . . . . . 10
⊢ (𝜑 → (1...𝑁) ∈ Fin) |
303 | 10 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) →
Λ:ℕ⟶ℝ) |
304 | 239 | sselda 3603 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → 𝑗 ∈ ℕ) |
305 | 303, 304 | ffvelrnd 6360 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → (Λ‘𝑗) ∈ ℝ) |
306 | | vmage0 24847 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → 0 ≤
(Λ‘𝑗)) |
307 | 304, 306 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (1...𝑁)) → 0 ≤ (Λ‘𝑗)) |
308 | 302, 305,
307 | fsumge0 14527 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)) |
309 | 1 | hgt750lemc 30725 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗) < ((1._0_3_8_83)
· 𝑁)) |
310 | 246, 277,
252, 293, 300, 301, 308, 309 | ltmul12ad 10965 |
. . . . . . . 8
⊢ (𝜑 → (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪
{2})(Λ‘𝑖)
· Σ𝑗 ∈
(1...𝑁)(Λ‘𝑗)) < (((1._4_2_63)
· (√‘𝑁))
· ((1._0_3_8_83)
· 𝑁))) |
311 | 253, 294,
310 | ltled 10185 |
. . . . . . 7
⊢ (𝜑 → (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪
{2})(Λ‘𝑖)
· Σ𝑗 ∈
(1...𝑁)(Λ‘𝑗)) ≤ (((1._4_2_63)
· (√‘𝑁))
· ((1._0_3_8_83)
· 𝑁))) |
312 | 157 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℝ) |
313 | | 1lt2 11194 |
. . . . . . . . . . 11
⊢ 1 <
2 |
314 | 313 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 1 < 2) |
315 | 312, 179,
125, 314, 211 | ltletrd 10197 |
. . . . . . . . 9
⊢ (𝜑 → 1 < 𝑁) |
316 | 125, 315 | rplogcld 24375 |
. . . . . . . 8
⊢ (𝜑 → (log‘𝑁) ∈
ℝ+) |
317 | 253, 294,
316 | lemul2d 11916 |
. . . . . . 7
⊢ (𝜑 → ((Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪
{2})(Λ‘𝑖)
· Σ𝑗 ∈
(1...𝑁)(Λ‘𝑗)) ≤ (((1._4_2_63)
· (√‘𝑁))
· ((1._0_3_8_83)
· 𝑁)) ↔
((log‘𝑁) ·
(Σ𝑖 ∈
(((1...𝑁) ∖ ℙ)
∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))) ≤ ((log‘𝑁) · (((1._4_2_63)
· (√‘𝑁))
· ((1._0_3_8_83)
· 𝑁))))) |
318 | 311, 317 | mpbid 222 |
. . . . . 6
⊢ (𝜑 → ((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪
{2})(Λ‘𝑖)
· Σ𝑗 ∈
(1...𝑁)(Λ‘𝑗))) ≤ ((log‘𝑁) · (((1._4_2_63)
· (√‘𝑁))
· ((1._0_3_8_83)
· 𝑁)))) |
319 | 254, 295,
217 | lemul2d 11916 |
. . . . . 6
⊢ (𝜑 → (((log‘𝑁) · (Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪
{2})(Λ‘𝑖)
· Σ𝑗 ∈
(1...𝑁)(Λ‘𝑗))) ≤ ((log‘𝑁) · (((1._4_2_63)
· (√‘𝑁))
· ((1._0_3_8_83)
· 𝑁))) ↔
((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((log‘𝑁)
· (Σ𝑖 ∈
(((1...𝑁) ∖ ℙ)
∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))) ≤ ((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((log‘𝑁)
· (((1._4_2_63)
· (√‘𝑁))
· ((1._0_3_8_83)
· 𝑁)))))) |
320 | 318, 319 | mpbid 222 |
. . . . 5
⊢ (𝜑 → ((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((log‘𝑁)
· (Σ𝑖 ∈
(((1...𝑁) ∖ ℙ)
∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))) ≤ ((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((log‘𝑁)
· (((1._4_2_63)
· (√‘𝑁))
· ((1._0_3_8_83)
· 𝑁))))) |
321 | 255, 296,
261 | lemul2d 11916 |
. . . . 5
⊢ (𝜑 → (((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((log‘𝑁)
· (Σ𝑖 ∈
(((1...𝑁) ∖ ℙ)
∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗)))) ≤ ((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((log‘𝑁)
· (((1._4_2_63)
· (√‘𝑁))
· ((1._0_3_8_83)
· 𝑁)))) ↔ (3
· ((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((log‘𝑁)
· (Σ𝑖 ∈
(((1...𝑁) ∖ ℙ)
∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))) ≤ (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((log‘𝑁)
· (((1._4_2_63)
· (√‘𝑁))
· ((1._0_3_8_83)
· 𝑁))))))) |
322 | 320, 321 | mpbid 222 |
. . . 4
⊢ (𝜑 → (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((log‘𝑁)
· (Σ𝑖 ∈
(((1...𝑁) ∖ ℙ)
∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))) ≤ (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((log‘𝑁)
· (((1._4_2_63)
· (√‘𝑁))
· ((1._0_3_8_83)
· 𝑁)))))) |
323 | 154 | resqcli 12949 |
. . . . . . . . . 10
⊢ ((1._0_7_9_9_55)↑2) ∈ ℝ |
324 | 323, 165 | remulcli 10054 |
. . . . . . . . 9
⊢
(((1._0_7_9_9_55)↑2) · (1._4_14))
∈ ℝ |
325 | 275, 291 | remulcli 10054 |
. . . . . . . . 9
⊢ ((1._4_2_63)
· (1._0_3_8_83))
∈ ℝ |
326 | 324, 325 | remulcli 10054 |
. . . . . . . 8
⊢
((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((1._4_2_63)
· (1._0_3_8_83)))
∈ ℝ |
327 | 55, 326 | remulcli 10054 |
. . . . . . 7
⊢ (3
· ((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((1._4_2_63)
· (1._0_3_8_83)))) ∈ ℝ |
328 | | hgt750lem2 30730 |
. . . . . . 7
⊢ (3
· ((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((1._4_2_63)
· (1._0_3_8_83)))) < (7._3_48) |
329 | 327, 121,
328 | ltleii 10160 |
. . . . . 6
⊢ (3
· ((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((1._4_2_63)
· (1._0_3_8_83)))) ≤ (7._3_48) |
330 | 327 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((1._4_2_63)
· (1._0_3_8_83)))) ∈ ℝ) |
331 | 316, 128 | rpdivcld 11889 |
. . . . . . . 8
⊢ (𝜑 → ((log‘𝑁) / (√‘𝑁)) ∈
ℝ+) |
332 | 123, 215 | rpexpcld 13032 |
. . . . . . . 8
⊢ (𝜑 → (𝑁↑2) ∈
ℝ+) |
333 | 331, 332 | rpmulcld 11888 |
. . . . . . 7
⊢ (𝜑 → (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2)) ∈
ℝ+) |
334 | 330, 122,
333 | lemul1d 11915 |
. . . . . 6
⊢ (𝜑 → ((3 · ((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((1._4_2_63)
· (1._0_3_8_83)))) ≤ (7._3_48)
↔ ((3 · ((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((1._4_2_63)
· (1._0_3_8_83)))) · (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2))) ≤ ((7._3_48)
· (((log‘𝑁) /
(√‘𝑁)) ·
(𝑁↑2))))) |
335 | 329, 334 | mpbii 223 |
. . . . 5
⊢ (𝜑 → ((3 · ((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((1._4_2_63)
· (1._0_3_8_83)))) · (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2))) ≤ ((7._3_48)
· (((log‘𝑁) /
(√‘𝑁)) ·
(𝑁↑2)))) |
336 | 276 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1._4_2_63)
∈ ℂ) |
337 | 127 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (√‘𝑁) ∈
ℂ) |
338 | 292 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1._0_3_8_83)
∈ ℂ) |
339 | 125 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℂ) |
340 | 336, 337,
338, 339 | mul4d 10248 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((1._4_2_63)
· (√‘𝑁))
· ((1._0_3_8_83)
· 𝑁)) = (((1._4_2_63)
· (1._0_3_8_83))
· ((√‘𝑁)
· 𝑁))) |
341 | 340 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((log‘𝑁) · (((1._4_2_63)
· (√‘𝑁))
· ((1._0_3_8_83)
· 𝑁))) =
((log‘𝑁) ·
(((1._4_2_63)
· (1._0_3_8_83))
· ((√‘𝑁)
· 𝑁)))) |
342 | 124 | recnd 10068 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (log‘𝑁) ∈
ℂ) |
343 | 336, 338 | mulcld 10060 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((1._4_2_63)
· (1._0_3_8_83))
∈ ℂ) |
344 | 337, 339 | mulcld 10060 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((√‘𝑁) · 𝑁) ∈ ℂ) |
345 | 343, 344 | mulcld 10060 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((1._4_2_63)
· (1._0_3_8_83))
· ((√‘𝑁)
· 𝑁)) ∈
ℂ) |
346 | 342, 345 | mulcomd 10061 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((log‘𝑁) · (((1._4_2_63)
· (1._0_3_8_83))
· ((√‘𝑁)
· 𝑁))) = ((((1._4_2_63)
· (1._0_3_8_83))
· ((√‘𝑁)
· 𝑁)) ·
(log‘𝑁))) |
347 | 341, 346 | eqtrd 2656 |
. . . . . . . . . . 11
⊢ (𝜑 → ((log‘𝑁) · (((1._4_2_63)
· (√‘𝑁))
· ((1._0_3_8_83)
· 𝑁))) = ((((1._4_2_63)
· (1._0_3_8_83))
· ((√‘𝑁)
· 𝑁)) ·
(log‘𝑁))) |
348 | 343, 344,
342 | mulassd 10063 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((1._4_2_63)
· (1._0_3_8_83))
· ((√‘𝑁)
· 𝑁)) ·
(log‘𝑁)) = (((1._4_2_63)
· (1._0_3_8_83))
· (((√‘𝑁) · 𝑁) · (log‘𝑁)))) |
349 | 347, 348 | eqtrd 2656 |
. . . . . . . . . 10
⊢ (𝜑 → ((log‘𝑁) · (((1._4_2_63)
· (√‘𝑁))
· ((1._0_3_8_83)
· 𝑁))) = (((1._4_2_63)
· (1._0_3_8_83))
· (((√‘𝑁) · 𝑁) · (log‘𝑁)))) |
350 | 349 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝜑 → ((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((log‘𝑁)
· (((1._4_2_63)
· (√‘𝑁))
· ((1._0_3_8_83)
· 𝑁)))) =
((((1._0_7_9_9_55)↑2) · (1._4_14))
· (((1._4_2_63)
· (1._0_3_8_83))
· (((√‘𝑁) · 𝑁) · (log‘𝑁))))) |
351 | 83 | recnd 10068 |
. . . . . . . . . 10
⊢ (𝜑 → (((1._0_7_9_9_55)↑2) · (1._4_14))
∈ ℂ) |
352 | 344, 342 | mulcld 10060 |
. . . . . . . . . 10
⊢ (𝜑 → (((√‘𝑁) · 𝑁) · (log‘𝑁)) ∈ ℂ) |
353 | 351, 343,
352 | mulassd 10063 |
. . . . . . . . 9
⊢ (𝜑 → (((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((1._4_2_63)
· (1._0_3_8_83)))
· (((√‘𝑁) · 𝑁) · (log‘𝑁))) = ((((1._0_7_9_9_55)↑2) · (1._4_14))
· (((1._4_2_63)
· (1._0_3_8_83))
· (((√‘𝑁) · 𝑁) · (log‘𝑁))))) |
354 | 350, 353 | eqtr4d 2659 |
. . . . . . . 8
⊢ (𝜑 → ((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((log‘𝑁)
· (((1._4_2_63)
· (√‘𝑁))
· ((1._0_3_8_83)
· 𝑁)))) =
(((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((1._4_2_63)
· (1._0_3_8_83)))
· (((√‘𝑁) · 𝑁) · (log‘𝑁)))) |
355 | 354 | oveq2d 6666 |
. . . . . . 7
⊢ (𝜑 → (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((log‘𝑁)
· (((1._4_2_63)
· (√‘𝑁))
· ((1._0_3_8_83)
· 𝑁))))) = (3
· (((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((1._4_2_63)
· (1._0_3_8_83)))
· (((√‘𝑁) · 𝑁) · (log‘𝑁))))) |
356 | 56 | recnd 10068 |
. . . . . . . 8
⊢ (𝜑 → 3 ∈
ℂ) |
357 | 351, 343 | mulcld 10060 |
. . . . . . . 8
⊢ (𝜑 → ((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((1._4_2_63)
· (1._0_3_8_83)))
∈ ℂ) |
358 | 356, 357,
352 | mulassd 10063 |
. . . . . . 7
⊢ (𝜑 → ((3 · ((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((1._4_2_63)
· (1._0_3_8_83)))) · (((√‘𝑁) · 𝑁) · (log‘𝑁))) = (3 · (((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((1._4_2_63)
· (1._0_3_8_83)))
· (((√‘𝑁) · 𝑁) · (log‘𝑁))))) |
359 | 355, 358 | eqtr4d 2659 |
. . . . . 6
⊢ (𝜑 → (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((log‘𝑁)
· (((1._4_2_63)
· (√‘𝑁))
· ((1._0_3_8_83)
· 𝑁))))) = ((3
· ((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((1._4_2_63)
· (1._0_3_8_83)))) · (((√‘𝑁) · 𝑁) · (log‘𝑁)))) |
360 | 132 | recnd 10068 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁↑2) ∈ ℂ) |
361 | 342, 337,
360, 129 | div32d 10824 |
. . . . . . . 8
⊢ (𝜑 → (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2)) = ((log‘𝑁) · ((𝑁↑2) / (√‘𝑁)))) |
362 | 360, 337,
129 | divcld 10801 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁↑2) / (√‘𝑁)) ∈ ℂ) |
363 | 342, 362 | mulcomd 10061 |
. . . . . . . 8
⊢ (𝜑 → ((log‘𝑁) · ((𝑁↑2) / (√‘𝑁))) = (((𝑁↑2) / (√‘𝑁)) · (log‘𝑁))) |
364 | 339 | sqvald 13005 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁↑2) = (𝑁 · 𝑁)) |
365 | 364 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑁↑2) / (√‘𝑁)) = ((𝑁 · 𝑁) / (√‘𝑁))) |
366 | 339, 339,
337, 129 | divassd 10836 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑁 · 𝑁) / (√‘𝑁)) = (𝑁 · (𝑁 / (√‘𝑁)))) |
367 | | divsqrtid 30672 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℝ+
→ (𝑁 /
(√‘𝑁)) =
(√‘𝑁)) |
368 | 123, 367 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 / (√‘𝑁)) = (√‘𝑁)) |
369 | 368 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 · (𝑁 / (√‘𝑁))) = (𝑁 · (√‘𝑁))) |
370 | 365, 366,
369 | 3eqtrd 2660 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑁↑2) / (√‘𝑁)) = (𝑁 · (√‘𝑁))) |
371 | 339, 337 | mulcomd 10061 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 · (√‘𝑁)) = ((√‘𝑁) · 𝑁)) |
372 | 370, 371 | eqtrd 2656 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁↑2) / (√‘𝑁)) = ((√‘𝑁) · 𝑁)) |
373 | 372 | oveq1d 6665 |
. . . . . . . 8
⊢ (𝜑 → (((𝑁↑2) / (√‘𝑁)) · (log‘𝑁)) = (((√‘𝑁) · 𝑁) · (log‘𝑁))) |
374 | 361, 363,
373 | 3eqtrrd 2661 |
. . . . . . 7
⊢ (𝜑 → (((√‘𝑁) · 𝑁) · (log‘𝑁)) = (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2))) |
375 | 374 | oveq2d 6666 |
. . . . . 6
⊢ (𝜑 → ((3 · ((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((1._4_2_63)
· (1._0_3_8_83)))) · (((√‘𝑁) · 𝑁) · (log‘𝑁))) = ((3 · ((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((1._4_2_63)
· (1._0_3_8_83)))) · (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2)))) |
376 | 359, 375 | eqtrd 2656 |
. . . . 5
⊢ (𝜑 → (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((log‘𝑁)
· (((1._4_2_63)
· (√‘𝑁))
· ((1._0_3_8_83)
· 𝑁))))) = ((3
· ((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((1._4_2_63)
· (1._0_3_8_83)))) · (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2)))) |
377 | 122 | recnd 10068 |
. . . . . 6
⊢ (𝜑 → (7._3_48)
∈ ℂ) |
378 | 130 | recnd 10068 |
. . . . . 6
⊢ (𝜑 → ((log‘𝑁) / (√‘𝑁)) ∈
ℂ) |
379 | 377, 378,
360 | mulassd 10063 |
. . . . 5
⊢ (𝜑 → (((7._3_48)
· ((log‘𝑁) /
(√‘𝑁)))
· (𝑁↑2)) =
((7._3_48) · (((log‘𝑁) / (√‘𝑁)) · (𝑁↑2)))) |
380 | 335, 376,
379 | 3brtr4d 4685 |
. . . 4
⊢ (𝜑 → (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((log‘𝑁)
· (((1._4_2_63)
· (√‘𝑁))
· ((1._0_3_8_83)
· 𝑁))))) ≤
(((7._3_48) · ((log‘𝑁) / (√‘𝑁))) · (𝑁↑2))) |
381 | 256, 297,
133, 322, 380 | letrd 10194 |
. . 3
⊢ (𝜑 → (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14))
· ((log‘𝑁)
· (Σ𝑖 ∈
(((1...𝑁) ∖ ℙ)
∪ {2})(Λ‘𝑖) · Σ𝑗 ∈ (1...𝑁)(Λ‘𝑗))))) ≤ (((7._3_48)
· ((log‘𝑁) /
(√‘𝑁)))
· (𝑁↑2))) |
382 | 111, 256,
133, 263, 381 | letrd 10194 |
. 2
⊢ (𝜑 → (3 · ((((1._0_7_9_9_55)↑2) · (1._4_14))
· Σ𝑛 ∈
{𝑑 ∈
(ℕ(repr‘3)𝑁)
∣ ¬ (𝑑‘0)
∈ (𝑂 ∩ ℙ)}
((Λ‘(𝑛‘0)) · ((Λ‘(𝑛‘1)) ·
(Λ‘(𝑛‘2)))))) ≤ (((7._3_48)
· ((log‘𝑁) /
(√‘𝑁)))
· (𝑁↑2))) |
383 | 54, 111, 133, 229, 382 | letrd 10194 |
1
⊢ (𝜑 → Σ𝑛 ∈ ((ℕ(repr‘3)𝑁) ∖ ((𝑂 ∩ ℙ)(repr‘3)𝑁))(((Λ‘(𝑛‘0)) · (𝐻‘(𝑛‘0))) · (((Λ‘(𝑛‘1)) · (𝐾‘(𝑛‘1))) · ((Λ‘(𝑛‘2)) · (𝐾‘(𝑛‘2))))) ≤ (((7._3_48)
· ((log‘𝑁) /
(√‘𝑁)))
· (𝑁↑2))) |