Step | Hyp | Ref
| Expression |
1 | | reex 10363 |
. . . . . 6
⊢ ℝ
∈ V |
2 | | rpssre 12144 |
. . . . . 6
⊢
ℝ+ ⊆ ℝ |
3 | 1, 2 | ssexi 5040 |
. . . . 5
⊢
ℝ+ ∈ V |
4 | 3 | a1i 11 |
. . . 4
⊢ (𝜑 → ℝ+ ∈
V) |
5 | | fzfid 13091 |
. . . . . . 7
⊢ (𝜑 → (1...(⌊‘𝑥)) ∈ Fin) |
6 | | elfznn 12687 |
. . . . . . . . . . 11
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) |
7 | 6 | adantl 475 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ) |
8 | | vmacl 25296 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ →
(Λ‘𝑛) ∈
ℝ) |
9 | 7, 8 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈
ℝ) |
10 | 9, 7 | nndivred 11429 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((Λ‘𝑛) / 𝑛) ∈
ℝ) |
11 | 10 | recnd 10405 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((Λ‘𝑛) / 𝑛) ∈
ℂ) |
12 | 5, 11 | fsumcl 14871 |
. . . . . 6
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℂ) |
13 | 12 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℂ) |
14 | | relogcl 24759 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℝ) |
15 | 14 | adantl 475 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(log‘𝑥) ∈
ℝ) |
16 | 15 | recnd 10405 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(log‘𝑥) ∈
ℂ) |
17 | 13, 16 | subcld 10734 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) ∈ ℂ) |
18 | | 1re 10376 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
19 | | rpvmasum.g |
. . . . . . . . . . . 12
⊢ 𝐺 = (DChr‘𝑁) |
20 | | rpvmasum.z |
. . . . . . . . . . . 12
⊢ 𝑍 =
(ℤ/nℤ‘𝑁) |
21 | | rpvmasum.1 |
. . . . . . . . . . . 12
⊢ 1 =
(0g‘𝐺) |
22 | | eqid 2778 |
. . . . . . . . . . . 12
⊢
(Base‘𝑍) =
(Base‘𝑍) |
23 | | rpvmasum.a |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℕ) |
24 | 19, 20, 21, 22, 23 | dchr1re 25440 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 :(Base‘𝑍)⟶ℝ) |
25 | 24 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 :(Base‘𝑍)⟶ℝ) |
26 | 23 | nnnn0d 11702 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
27 | | rpvmasum.l |
. . . . . . . . . . . . 13
⊢ 𝐿 = (ℤRHom‘𝑍) |
28 | 20, 22, 27 | znzrhfo 20291 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ 𝐿:ℤ–onto→(Base‘𝑍)) |
29 | | fof 6366 |
. . . . . . . . . . . 12
⊢ (𝐿:ℤ–onto→(Base‘𝑍) → 𝐿:ℤ⟶(Base‘𝑍)) |
30 | 26, 28, 29 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐿:ℤ⟶(Base‘𝑍)) |
31 | | elfzelz 12659 |
. . . . . . . . . . 11
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℤ) |
32 | | ffvelrn 6621 |
. . . . . . . . . . 11
⊢ ((𝐿:ℤ⟶(Base‘𝑍) ∧ 𝑛 ∈ ℤ) → (𝐿‘𝑛) ∈ (Base‘𝑍)) |
33 | 30, 31, 32 | syl2an 589 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝐿‘𝑛) ∈ (Base‘𝑍)) |
34 | 25, 33 | ffvelrnd 6624 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ( 1 ‘(𝐿‘𝑛)) ∈ ℝ) |
35 | | resubcl 10687 |
. . . . . . . . 9
⊢ ((1
∈ ℝ ∧ ( 1 ‘(𝐿‘𝑛)) ∈ ℝ) → (1 − ( 1 ‘(𝐿‘𝑛))) ∈ ℝ) |
36 | 18, 34, 35 | sylancr 581 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 − ( 1 ‘(𝐿‘𝑛))) ∈ ℝ) |
37 | 36, 10 | remulcld 10407 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℝ) |
38 | 37 | recnd 10405 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ) |
39 | 5, 38 | fsumcl 14871 |
. . . . 5
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ) |
40 | 39 | adantr 474 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ) |
41 | | eqidd 2779 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)))) |
42 | | eqidd 2779 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) = (𝑥 ∈ ℝ+ ↦
Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))) |
43 | 4, 17, 40, 41, 42 | offval2 7191 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘𝑓 −
(𝑥 ∈
ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))) = (𝑥 ∈ ℝ+ ↦
((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))))) |
44 | 13, 16, 40 | sub32d 10766 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) − (log‘𝑥))) |
45 | 5, 11, 38 | fsumsub 14924 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) − ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))) |
46 | | 1cnd 10371 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈
ℂ) |
47 | 36 | recnd 10405 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 − ( 1 ‘(𝐿‘𝑛))) ∈ ℂ) |
48 | 46, 47, 11 | subdird 10832 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 − (1
− ( 1 ‘(𝐿‘𝑛)))) · ((Λ‘𝑛) / 𝑛)) = ((1 · ((Λ‘𝑛) / 𝑛)) − ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))) |
49 | | ax-1cn 10330 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℂ |
50 | 34 | recnd 10405 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ( 1 ‘(𝐿‘𝑛)) ∈ ℂ) |
51 | | nncan 10652 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℂ ∧ ( 1 ‘(𝐿‘𝑛)) ∈ ℂ) → (1 − (1
− ( 1 ‘(𝐿‘𝑛)))) = ( 1 ‘(𝐿‘𝑛))) |
52 | 49, 50, 51 | sylancr 581 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 − (1 −
( 1
‘(𝐿‘𝑛)))) = ( 1 ‘(𝐿‘𝑛))) |
53 | 52 | oveq1d 6937 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 − (1
− ( 1 ‘(𝐿‘𝑛)))) · ((Λ‘𝑛) / 𝑛)) = (( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) |
54 | 11 | mulid2d 10395 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 ·
((Λ‘𝑛) / 𝑛)) = ((Λ‘𝑛) / 𝑛)) |
55 | 54 | oveq1d 6937 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 ·
((Λ‘𝑛) / 𝑛)) − ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) = (((Λ‘𝑛) / 𝑛) − ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))) |
56 | 48, 53, 55 | 3eqtr3rd 2823 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(((Λ‘𝑛) /
𝑛) − ((1 − (
1
‘(𝐿‘𝑛))) ·
((Λ‘𝑛) / 𝑛))) = (( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) |
57 | 56 | sumeq2dv 14841 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) − ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) |
58 | 45, 57 | eqtr3d 2816 |
. . . . . . 7
⊢ (𝜑 → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) |
59 | 58 | oveq1d 6937 |
. . . . . 6
⊢ (𝜑 → ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) − (log‘𝑥)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) |
60 | 59 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) − (log‘𝑥)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) |
61 | 44, 60 | eqtrd 2814 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) |
62 | 61 | mpteq2dva 4979 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) − Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((
1
‘(𝐿‘𝑛)) ·
((Λ‘𝑛) / 𝑛)) − (log‘𝑥)))) |
63 | 43, 62 | eqtrd 2814 |
. 2
⊢ (𝜑 → ((𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘𝑓 −
(𝑥 ∈
ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((
1
‘(𝐿‘𝑛)) ·
((Λ‘𝑛) / 𝑛)) − (log‘𝑥)))) |
64 | | vmadivsum 25623 |
. . 3
⊢ (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1) |
65 | 2 | a1i 11 |
. . . 4
⊢ (𝜑 → ℝ+
⊆ ℝ) |
66 | | 1red 10377 |
. . . 4
⊢ (𝜑 → 1 ∈
ℝ) |
67 | | prmdvdsfi 25285 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} ∈ Fin) |
68 | 23, 67 | syl 17 |
. . . . 5
⊢ (𝜑 → {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} ∈ Fin) |
69 | | elrabi 3567 |
. . . . . 6
⊢ (𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} → 𝑝 ∈ ℙ) |
70 | | prmnn 15793 |
. . . . . . . . . 10
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) |
71 | 70 | adantl 475 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℕ) |
72 | 71 | nnrpd 12179 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℝ+) |
73 | 72 | relogcld 24806 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (log‘𝑝) ∈
ℝ) |
74 | | prmuz2 15813 |
. . . . . . . . 9
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
(ℤ≥‘2)) |
75 | 74 | adantl 475 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝑝 ∈
(ℤ≥‘2)) |
76 | | uz2m1nn 12070 |
. . . . . . . 8
⊢ (𝑝 ∈
(ℤ≥‘2) → (𝑝 − 1) ∈ ℕ) |
77 | 75, 76 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 − 1) ∈ ℕ) |
78 | 73, 77 | nndivred 11429 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ) |
79 | 69, 78 | sylan2 586 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁}) → ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ) |
80 | 68, 79 | fsumrecl 14872 |
. . . 4
⊢ (𝜑 → Σ𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ) |
81 | | fzfid 13091 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(1...(⌊‘𝑥))
∈ Fin) |
82 | | simpr 479 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ ( 1
‘(𝐿‘𝑛)) = 0) → ( 1 ‘(𝐿‘𝑛)) = 0) |
83 | | 0re 10378 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
84 | 82, 83 | syl6eqel 2867 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ ( 1
‘(𝐿‘𝑛)) = 0) → ( 1 ‘(𝐿‘𝑛)) ∈ ℝ) |
85 | | eqid 2778 |
. . . . . . . . . . . 12
⊢
(Unit‘𝑍) =
(Unit‘𝑍) |
86 | 23 | ad3antrrr 720 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ ( 1
‘(𝐿‘𝑛)) ≠ 0) → 𝑁 ∈
ℕ) |
87 | | rpvmasum.d |
. . . . . . . . . . . . . 14
⊢ 𝐷 = (Base‘𝐺) |
88 | 19 | dchrabl 25431 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → 𝐺 ∈ Abel) |
89 | | ablgrp 18584 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) |
90 | 87, 21 | grpidcl 17837 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ Grp → 1 ∈ 𝐷) |
91 | 23, 88, 89, 90 | 4syl 19 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ∈ 𝐷) |
92 | 91 | ad2antrr 716 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 1
∈ 𝐷) |
93 | 33 | adantlr 705 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝐿‘𝑛) ∈ (Base‘𝑍)) |
94 | 19, 20, 87, 22, 85, 92, 93 | dchrn0 25427 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (( 1 ‘(𝐿‘𝑛)) ≠ 0 ↔ (𝐿‘𝑛) ∈ (Unit‘𝑍))) |
95 | 94 | biimpa 470 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ ( 1
‘(𝐿‘𝑛)) ≠ 0) → (𝐿‘𝑛) ∈ (Unit‘𝑍)) |
96 | 19, 20, 21, 85, 86, 95 | dchr1 25434 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ ( 1
‘(𝐿‘𝑛)) ≠ 0) → ( 1 ‘(𝐿‘𝑛)) = 1) |
97 | 96, 18 | syl6eqel 2867 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ ( 1
‘(𝐿‘𝑛)) ≠ 0) → ( 1 ‘(𝐿‘𝑛)) ∈ ℝ) |
98 | 84, 97 | pm2.61dane 3057 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ( 1 ‘(𝐿‘𝑛)) ∈ ℝ) |
99 | 18, 98, 35 | sylancr 581 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (1 − ( 1 ‘(𝐿‘𝑛))) ∈ ℝ) |
100 | 10 | adantlr 705 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
/ 𝑛) ∈
ℝ) |
101 | 99, 100 | remulcld 10407 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℝ) |
102 | 81, 101 | fsumrecl 14872 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℝ) |
103 | | 0le1 10898 |
. . . . . . . . . . 11
⊢ 0 ≤
1 |
104 | 82, 103 | syl6eqbr 4925 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ ( 1
‘(𝐿‘𝑛)) = 0) → ( 1 ‘(𝐿‘𝑛)) ≤ 1) |
105 | 18 | leidi 10909 |
. . . . . . . . . . 11
⊢ 1 ≤
1 |
106 | 96, 105 | syl6eqbr 4925 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ ( 1
‘(𝐿‘𝑛)) ≠ 0) → ( 1 ‘(𝐿‘𝑛)) ≤ 1) |
107 | 104, 106 | pm2.61dane 3057 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ( 1 ‘(𝐿‘𝑛)) ≤ 1) |
108 | | subge0 10888 |
. . . . . . . . . 10
⊢ ((1
∈ ℝ ∧ ( 1 ‘(𝐿‘𝑛)) ∈ ℝ) → (0 ≤ (1 −
( 1
‘(𝐿‘𝑛))) ↔ ( 1 ‘(𝐿‘𝑛)) ≤ 1)) |
109 | 18, 98, 108 | sylancr 581 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (0 ≤ (1 − ( 1 ‘(𝐿‘𝑛))) ↔ ( 1 ‘(𝐿‘𝑛)) ≤ 1)) |
110 | 107, 109 | mpbird 249 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (1 − ( 1 ‘(𝐿‘𝑛)))) |
111 | 9 | adantlr 705 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Λ‘𝑛)
∈ ℝ) |
112 | 6 | adantl 475 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℕ) |
113 | | vmage0 25299 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → 0 ≤
(Λ‘𝑛)) |
114 | 112, 113 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (Λ‘𝑛)) |
115 | 112 | nnred 11391 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℝ) |
116 | 112 | nngt0d 11424 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 < 𝑛) |
117 | | divge0 11246 |
. . . . . . . . 9
⊢
((((Λ‘𝑛) ∈ ℝ ∧ 0 ≤
(Λ‘𝑛)) ∧
(𝑛 ∈ ℝ ∧ 0
< 𝑛)) → 0 ≤
((Λ‘𝑛) / 𝑛)) |
118 | 111, 114,
115, 116, 117 | syl22anc 829 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ ((Λ‘𝑛) / 𝑛)) |
119 | 99, 100, 110, 118 | mulge0d 10952 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) |
120 | 81, 101, 119 | fsumge0 14931 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 0 ≤
Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) |
121 | 102, 120 | absidd 14569 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) |
122 | 68 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} ∈ Fin) |
123 | | inss2 4054 |
. . . . . . . . 9
⊢
((0[,]𝑥) ∩
ℙ) ⊆ ℙ |
124 | | rabss2 3906 |
. . . . . . . . 9
⊢
(((0[,]𝑥) ∩
ℙ) ⊆ ℙ → {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ⊆ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁}) |
125 | 123, 124 | mp1i 13 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ⊆ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁}) |
126 | | ssfi 8468 |
. . . . . . . 8
⊢ (({𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} ∈ Fin ∧ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ⊆ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁}) → {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ∈ Fin) |
127 | 122, 125,
126 | syl2anc 579 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ∈ Fin) |
128 | | ssrab2 3908 |
. . . . . . . . . 10
⊢ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ⊆ ((0[,]𝑥) ∩ ℙ) |
129 | 128, 123 | sstri 3830 |
. . . . . . . . 9
⊢ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ⊆ ℙ |
130 | 129 | sseli 3817 |
. . . . . . . 8
⊢ (𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} → 𝑝 ∈ ℙ) |
131 | 78 | adantlr 705 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
((log‘𝑝) / (𝑝 − 1)) ∈
ℝ) |
132 | 130, 131 | sylan2 586 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁}) → ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ) |
133 | 127, 132 | fsumrecl 14872 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ) |
134 | 80 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ) |
135 | | 2fveq3 6451 |
. . . . . . . . . . 11
⊢ (𝑛 = (𝑝↑𝑘) → ( 1 ‘(𝐿‘𝑛)) = ( 1 ‘(𝐿‘(𝑝↑𝑘)))) |
136 | 135 | oveq2d 6938 |
. . . . . . . . . 10
⊢ (𝑛 = (𝑝↑𝑘) → (1 − ( 1 ‘(𝐿‘𝑛))) = (1 − ( 1 ‘(𝐿‘(𝑝↑𝑘))))) |
137 | | fveq2 6446 |
. . . . . . . . . . 11
⊢ (𝑛 = (𝑝↑𝑘) → (Λ‘𝑛) = (Λ‘(𝑝↑𝑘))) |
138 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑛 = (𝑝↑𝑘) → 𝑛 = (𝑝↑𝑘)) |
139 | 137, 138 | oveq12d 6940 |
. . . . . . . . . 10
⊢ (𝑛 = (𝑝↑𝑘) → ((Λ‘𝑛) / 𝑛) = ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) |
140 | 136, 139 | oveq12d 6940 |
. . . . . . . . 9
⊢ (𝑛 = (𝑝↑𝑘) → ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) = ((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)))) |
141 | | rpre 12145 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
142 | 141 | ad2antrl 718 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 𝑥 ∈
ℝ) |
143 | 38 | adantlr 705 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ) |
144 | | simprr 763 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ (Λ‘𝑛) =
0)) → (Λ‘𝑛) = 0) |
145 | 144 | oveq1d 6937 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ (Λ‘𝑛) =
0)) → ((Λ‘𝑛) / 𝑛) = (0 / 𝑛)) |
146 | 6 | ad2antrl 718 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ (Λ‘𝑛) =
0)) → 𝑛 ∈
ℕ) |
147 | 146 | nncnd 11392 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ (Λ‘𝑛) =
0)) → 𝑛 ∈
ℂ) |
148 | 146 | nnne0d 11425 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ (Λ‘𝑛) =
0)) → 𝑛 ≠
0) |
149 | 147, 148 | div0d 11150 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ (Λ‘𝑛) =
0)) → (0 / 𝑛) =
0) |
150 | 145, 149 | eqtrd 2814 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ (Λ‘𝑛) =
0)) → ((Λ‘𝑛) / 𝑛) = 0) |
151 | 150 | oveq2d 6938 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ (Λ‘𝑛) =
0)) → ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) = ((1 − ( 1 ‘(𝐿‘𝑛))) · 0)) |
152 | 47 | ad2ant2r 737 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ (Λ‘𝑛) =
0)) → (1 − ( 1 ‘(𝐿‘𝑛))) ∈ ℂ) |
153 | 152 | mul01d 10575 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ (Λ‘𝑛) =
0)) → ((1 − ( 1 ‘(𝐿‘𝑛))) · 0) = 0) |
154 | 151, 153 | eqtrd 2814 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ (Λ‘𝑛) =
0)) → ((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) = 0) |
155 | 140, 142,
143, 154 | fsumvma2 25391 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) = Σ𝑝 ∈ ((0[,]𝑥) ∩ ℙ)Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)))) |
156 | 128 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ⊆ ((0[,]𝑥) ∩ ℙ)) |
157 | | fzfid 13091 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))) ∈ Fin) |
158 | 24 | ad2antrr 716 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 1 :(Base‘𝑍)⟶ℝ) |
159 | 30 | ad2antrr 716 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝐿:ℤ⟶(Base‘𝑍)) |
160 | 70 | ad2antrl 718 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑝 ∈ ℕ) |
161 | | elfznn 12687 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))) → 𝑘 ∈ ℕ) |
162 | 161 | ad2antll 719 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑘 ∈ ℕ) |
163 | 162 | nnnn0d 11702 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑘 ∈ ℕ0) |
164 | 160, 163 | nnexpcld 13351 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝑝↑𝑘) ∈ ℕ) |
165 | 164 | nnzd 11833 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝑝↑𝑘) ∈ ℤ) |
166 | 159, 165 | ffvelrnd 6624 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝐿‘(𝑝↑𝑘)) ∈ (Base‘𝑍)) |
167 | 158, 166 | ffvelrnd 6624 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ( 1 ‘(𝐿‘(𝑝↑𝑘))) ∈ ℝ) |
168 | | resubcl 10687 |
. . . . . . . . . . . . . . 15
⊢ ((1
∈ ℝ ∧ ( 1 ‘(𝐿‘(𝑝↑𝑘))) ∈ ℝ) → (1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) ∈ ℝ) |
169 | 18, 167, 168 | sylancr 581 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) ∈ ℝ) |
170 | | vmacl 25296 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑝↑𝑘) ∈ ℕ →
(Λ‘(𝑝↑𝑘)) ∈ ℝ) |
171 | 164, 170 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (Λ‘(𝑝↑𝑘)) ∈ ℝ) |
172 | 171, 164 | nndivred 11429 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)) ∈ ℝ) |
173 | 169, 172 | remulcld 10407 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ∈ ℝ) |
174 | 173 | anassrs 461 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ∈ ℝ) |
175 | 174 | recnd 10405 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ∈ ℂ) |
176 | 157, 175 | fsumcl 14871 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
Σ𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ∈ ℂ) |
177 | 130, 176 | sylan2 586 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁}) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ∈ ℂ) |
178 | | breq1 4889 |
. . . . . . . . . . . 12
⊢ (𝑞 = 𝑝 → (𝑞 ∥ 𝑁 ↔ 𝑝 ∥ 𝑁)) |
179 | 178 | notbid 310 |
. . . . . . . . . . 11
⊢ (𝑞 = 𝑝 → (¬ 𝑞 ∥ 𝑁 ↔ ¬ 𝑝 ∥ 𝑁)) |
180 | | notrab 4130 |
. . . . . . . . . . 11
⊢
(((0[,]𝑥) ∩
ℙ) ∖ {𝑞 ∈
((0[,]𝑥) ∩ ℙ)
∣ 𝑞 ∥ 𝑁}) = {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ ¬ 𝑞 ∥ 𝑁} |
181 | 179, 180 | elrab2 3576 |
. . . . . . . . . 10
⊢ (𝑝 ∈ (((0[,]𝑥) ∩ ℙ) ∖ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁}) ↔ (𝑝 ∈ ((0[,]𝑥) ∩ ℙ) ∧ ¬ 𝑝 ∥ 𝑁)) |
182 | 123 | sseli 3817 |
. . . . . . . . . . 11
⊢ (𝑝 ∈ ((0[,]𝑥) ∩ ℙ) → 𝑝 ∈ ℙ) |
183 | 23 | ad3antrrr 720 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑁 ∈ ℕ) |
184 | | simplrr 768 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ¬ 𝑝 ∥ 𝑁) |
185 | | simplrl 767 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑝 ∈ ℙ) |
186 | 183 | nnzd 11833 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑁 ∈ ℤ) |
187 | | coprm 15827 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑝 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (¬
𝑝 ∥ 𝑁 ↔ (𝑝 gcd 𝑁) = 1)) |
188 | 185, 186,
187 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (¬ 𝑝 ∥ 𝑁 ↔ (𝑝 gcd 𝑁) = 1)) |
189 | 184, 188 | mpbid 224 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (𝑝 gcd 𝑁) = 1) |
190 | | prmz 15794 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℤ) |
191 | 185, 190 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑝 ∈ ℤ) |
192 | 161 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑘 ∈ ℕ) |
193 | 192 | nnnn0d 11702 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑘 ∈ ℕ0) |
194 | | rpexp1i 15837 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑝 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑘 ∈ ℕ0)
→ ((𝑝 gcd 𝑁) = 1 → ((𝑝↑𝑘) gcd 𝑁) = 1)) |
195 | 191, 186,
193, 194 | syl3anc 1439 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((𝑝 gcd 𝑁) = 1 → ((𝑝↑𝑘) gcd 𝑁) = 1)) |
196 | 189, 195 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((𝑝↑𝑘) gcd 𝑁) = 1) |
197 | 183 | nnnn0d 11702 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → 𝑁 ∈
ℕ0) |
198 | 165 | anassrs 461 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (𝑝↑𝑘) ∈ ℤ) |
199 | 198 | adantlrr 711 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (𝑝↑𝑘) ∈ ℤ) |
200 | 20, 85, 27 | znunit 20307 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℕ0
∧ (𝑝↑𝑘) ∈ ℤ) → ((𝐿‘(𝑝↑𝑘)) ∈ (Unit‘𝑍) ↔ ((𝑝↑𝑘) gcd 𝑁) = 1)) |
201 | 197, 199,
200 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((𝐿‘(𝑝↑𝑘)) ∈ (Unit‘𝑍) ↔ ((𝑝↑𝑘) gcd 𝑁) = 1)) |
202 | 196, 201 | mpbird 249 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (𝐿‘(𝑝↑𝑘)) ∈ (Unit‘𝑍)) |
203 | 19, 20, 21, 85, 183, 202 | dchr1 25434 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ( 1 ‘(𝐿‘(𝑝↑𝑘))) = 1) |
204 | 203 | oveq2d 6938 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) = (1 − 1)) |
205 | | 1m1e0 11447 |
. . . . . . . . . . . . . . . 16
⊢ (1
− 1) = 0 |
206 | 204, 205 | syl6eq 2830 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) = 0) |
207 | 206 | oveq1d 6937 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = (0 · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)))) |
208 | 172 | recnd 10405 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)) ∈ ℂ) |
209 | 208 | anassrs 461 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)) ∈ ℂ) |
210 | 209 | adantlrr 711 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) →
((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)) ∈ ℂ) |
211 | 210 | mul02d 10574 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → (0 ·
((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = 0) |
212 | 207, 211 | eqtrd 2814 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = 0) |
213 | 212 | sumeq2dv 14841 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))0) |
214 | | fzfid 13091 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) →
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))) ∈ Fin) |
215 | 214 | olcd 863 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) →
((1...(⌊‘((log‘𝑥) / (log‘𝑝)))) ⊆ (ℤ≥‘1)
∨ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))) ∈ Fin)) |
216 | | sumz 14860 |
. . . . . . . . . . . . 13
⊢
(((1...(⌊‘((log‘𝑥) / (log‘𝑝)))) ⊆ (ℤ≥‘1)
∨ (1...(⌊‘((log‘𝑥) / (log‘𝑝)))) ∈ Fin) → Σ𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))0 = 0) |
217 | 215, 216 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))0 = 0) |
218 | 213, 217 | eqtrd 2814 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ ¬
𝑝 ∥ 𝑁)) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = 0) |
219 | 182, 218 | sylanr1 672 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ((0[,]𝑥) ∩ ℙ) ∧ ¬ 𝑝 ∥ 𝑁)) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = 0) |
220 | 181, 219 | sylan2b 587 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ (((0[,]𝑥) ∩ ℙ) ∖ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁})) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = 0) |
221 | | ppifi 25284 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ →
((0[,]𝑥) ∩ ℙ)
∈ Fin) |
222 | 142, 221 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → ((0[,]𝑥) ∩ ℙ) ∈
Fin) |
223 | 156, 177,
220, 222 | fsumss 14863 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁}Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = Σ𝑝 ∈ ((0[,]𝑥) ∩ ℙ)Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)))) |
224 | 155, 223 | eqtr4d 2817 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) = Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁}Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)))) |
225 | 157, 174 | fsumrecl 14872 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
Σ𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ∈ ℝ) |
226 | 130, 225 | sylan2 586 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁}) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ∈ ℝ) |
227 | 73 | adantlr 705 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
(log‘𝑝) ∈
ℝ) |
228 | 70 | adantl 475 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈
ℕ) |
229 | 228 | nnrecred 11426 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (1 /
𝑝) ∈
ℝ) |
230 | 228 | nnrpd 12179 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈
ℝ+) |
231 | 230 | rpreccld 12191 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (1 /
𝑝) ∈
ℝ+) |
232 | | simplrl 767 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 𝑥 ∈
ℝ+) |
233 | 232 | relogcld 24806 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
(log‘𝑥) ∈
ℝ) |
234 | 228 | nnred 11391 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈
ℝ) |
235 | 74 | adantl 475 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈
(ℤ≥‘2)) |
236 | | eluz2b2 12068 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑝 ∈
(ℤ≥‘2) ↔ (𝑝 ∈ ℕ ∧ 1 < 𝑝)) |
237 | 236 | simprbi 492 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑝 ∈
(ℤ≥‘2) → 1 < 𝑝) |
238 | 235, 237 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 1 <
𝑝) |
239 | 234, 238 | rplogcld 24812 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
(log‘𝑝) ∈
ℝ+) |
240 | 233, 239 | rerpdivcld 12212 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
((log‘𝑥) /
(log‘𝑝)) ∈
ℝ) |
241 | 240 | flcld 12918 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
(⌊‘((log‘𝑥) / (log‘𝑝))) ∈ ℤ) |
242 | 241 | peano2zd 11837 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
((⌊‘((log‘𝑥) / (log‘𝑝))) + 1) ∈ ℤ) |
243 | 231, 242 | rpexpcld 13353 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → ((1 /
𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1)) ∈
ℝ+) |
244 | 243 | rpred 12181 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → ((1 /
𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1)) ∈
ℝ) |
245 | 229, 244 | resubcld 10803 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → ((1 /
𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) ∈
ℝ) |
246 | 235, 76 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 − 1) ∈
ℕ) |
247 | 246 | nnrpd 12179 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 − 1) ∈
ℝ+) |
248 | 247, 230 | rpdivcld 12198 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → ((𝑝 − 1) / 𝑝) ∈
ℝ+) |
249 | 245, 248 | rerpdivcld 12212 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (((1 /
𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝)) ∈ ℝ) |
250 | 227, 249 | remulcld 10407 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
((log‘𝑝) ·
(((1 / 𝑝) − ((1 /
𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))) ∈ ℝ) |
251 | 171 | recnd 10405 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (Λ‘(𝑝↑𝑘)) ∈ ℂ) |
252 | 164 | nncnd 11392 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝑝↑𝑘) ∈ ℂ) |
253 | 164 | nnne0d 11425 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝑝↑𝑘) ≠ 0) |
254 | 251, 252,
253 | divrecd 11154 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)) = ((Λ‘(𝑝↑𝑘)) · (1 / (𝑝↑𝑘)))) |
255 | | simprl 761 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑝 ∈ ℙ) |
256 | | vmappw 25294 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) →
(Λ‘(𝑝↑𝑘)) = (log‘𝑝)) |
257 | 255, 162,
256 | syl2anc 579 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (Λ‘(𝑝↑𝑘)) = (log‘𝑝)) |
258 | 160 | nncnd 11392 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑝 ∈ ℂ) |
259 | 160 | nnne0d 11425 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑝 ≠ 0) |
260 | | elfzelz 12659 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))) → 𝑘 ∈ ℤ) |
261 | 260 | ad2antll 719 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 𝑘 ∈ ℤ) |
262 | 258, 259,
261 | exprecd 13335 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((1 / 𝑝)↑𝑘) = (1 / (𝑝↑𝑘))) |
263 | 262 | eqcomd 2784 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (1 / (𝑝↑𝑘)) = ((1 / 𝑝)↑𝑘)) |
264 | 257, 263 | oveq12d 6940 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((Λ‘(𝑝↑𝑘)) · (1 / (𝑝↑𝑘))) = ((log‘𝑝) · ((1 / 𝑝)↑𝑘))) |
265 | 254, 264 | eqtrd 2814 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)) = ((log‘𝑝) · ((1 / 𝑝)↑𝑘))) |
266 | 265, 172 | eqeltrrd 2860 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((log‘𝑝) · ((1 / 𝑝)↑𝑘)) ∈ ℝ) |
267 | 266 | anassrs 461 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((log‘𝑝) · ((1 / 𝑝)↑𝑘)) ∈ ℝ) |
268 | | 1red 10377 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 1 ∈
ℝ) |
269 | | vmage0 25299 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑝↑𝑘) ∈ ℕ → 0 ≤
(Λ‘(𝑝↑𝑘))) |
270 | 164, 269 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 0 ≤ (Λ‘(𝑝↑𝑘))) |
271 | 164 | nnred 11391 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (𝑝↑𝑘) ∈ ℝ) |
272 | 164 | nngt0d 11424 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 0 < (𝑝↑𝑘)) |
273 | | divge0 11246 |
. . . . . . . . . . . . . . . 16
⊢
((((Λ‘(𝑝↑𝑘)) ∈ ℝ ∧ 0 ≤
(Λ‘(𝑝↑𝑘))) ∧ ((𝑝↑𝑘) ∈ ℝ ∧ 0 < (𝑝↑𝑘))) → 0 ≤ ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) |
274 | 171, 270,
271, 272, 273 | syl22anc 829 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 0 ≤ ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) |
275 | 83 | leidi 10909 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ≤
0 |
276 | | simpr 479 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) ∧ ( 1 ‘(𝐿‘(𝑝↑𝑘))) = 0) → ( 1 ‘(𝐿‘(𝑝↑𝑘))) = 0) |
277 | 275, 276 | syl5breqr 4924 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) ∧ ( 1 ‘(𝐿‘(𝑝↑𝑘))) = 0) → 0 ≤ ( 1 ‘(𝐿‘(𝑝↑𝑘)))) |
278 | 23 | ad3antrrr 720 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) ∧ ( 1 ‘(𝐿‘(𝑝↑𝑘))) ≠ 0) → 𝑁 ∈ ℕ) |
279 | 91 | ad2antrr 716 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 1 ∈ 𝐷) |
280 | 19, 20, 87, 22, 85, 279, 166 | dchrn0 25427 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (( 1 ‘(𝐿‘(𝑝↑𝑘))) ≠ 0 ↔ (𝐿‘(𝑝↑𝑘)) ∈ (Unit‘𝑍))) |
281 | 280 | biimpa 470 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) ∧ ( 1 ‘(𝐿‘(𝑝↑𝑘))) ≠ 0) → (𝐿‘(𝑝↑𝑘)) ∈ (Unit‘𝑍)) |
282 | 19, 20, 21, 85, 278, 281 | dchr1 25434 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) ∧ ( 1 ‘(𝐿‘(𝑝↑𝑘))) ≠ 0) → ( 1 ‘(𝐿‘(𝑝↑𝑘))) = 1) |
283 | 103, 282 | syl5breqr 4924 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) ∧ ( 1 ‘(𝐿‘(𝑝↑𝑘))) ≠ 0) → 0 ≤ ( 1 ‘(𝐿‘(𝑝↑𝑘)))) |
284 | 277, 283 | pm2.61dane 3057 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → 0 ≤ ( 1 ‘(𝐿‘(𝑝↑𝑘)))) |
285 | | subge02 10891 |
. . . . . . . . . . . . . . . . 17
⊢ ((1
∈ ℝ ∧ ( 1 ‘(𝐿‘(𝑝↑𝑘))) ∈ ℝ) → (0 ≤ ( 1 ‘(𝐿‘(𝑝↑𝑘))) ↔ (1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) ≤ 1)) |
286 | 18, 167, 285 | sylancr 581 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (0 ≤ ( 1 ‘(𝐿‘(𝑝↑𝑘))) ↔ (1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) ≤ 1)) |
287 | 284, 286 | mpbid 224 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) ≤ 1) |
288 | 169, 268,
172, 274, 287 | lemul1ad 11317 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ≤ (1 · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘)))) |
289 | 208 | mulid2d 10395 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (1 ·
((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) |
290 | 289, 265 | eqtrd 2814 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (1 ·
((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) = ((log‘𝑝) · ((1 / 𝑝)↑𝑘))) |
291 | 288, 290 | breqtrd 4912 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ≤ ((log‘𝑝) · ((1 / 𝑝)↑𝑘))) |
292 | 291 | anassrs 461 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ≤ ((log‘𝑝) · ((1 / 𝑝)↑𝑘))) |
293 | 157, 174,
267, 292 | fsumle 14935 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
Σ𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ≤ Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((log‘𝑝) · ((1 / 𝑝)↑𝑘))) |
294 | 227 | recnd 10405 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
(log‘𝑝) ∈
ℂ) |
295 | 160 | nnrecred 11426 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → (1 / 𝑝) ∈ ℝ) |
296 | 295, 163 | reexpcld 13344 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((1 / 𝑝)↑𝑘) ∈ ℝ) |
297 | 296 | recnd 10405 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))))) → ((1 / 𝑝)↑𝑘) ∈ ℂ) |
298 | 297 | anassrs 461 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) ∧ 𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))) → ((1 / 𝑝)↑𝑘) ∈ ℂ) |
299 | 157, 294,
298 | fsummulc2 14920 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
((log‘𝑝) ·
Σ𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 / 𝑝)↑𝑘)) = Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((log‘𝑝) · ((1 / 𝑝)↑𝑘))) |
300 | | fzval3 12856 |
. . . . . . . . . . . . . . . 16
⊢
((⌊‘((log‘𝑥) / (log‘𝑝))) ∈ ℤ →
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))) = (1..^((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) |
301 | 241, 300 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
(1...(⌊‘((log‘𝑥) / (log‘𝑝)))) = (1..^((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) |
302 | 301 | sumeq1d 14839 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
Σ𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 / 𝑝)↑𝑘) = Σ𝑘 ∈
(1..^((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))((1 / 𝑝)↑𝑘)) |
303 | 229 | recnd 10405 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (1 /
𝑝) ∈
ℂ) |
304 | 228 | nngt0d 11424 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 0 <
𝑝) |
305 | | recgt1 11273 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑝 ∈ ℝ ∧ 0 <
𝑝) → (1 < 𝑝 ↔ (1 / 𝑝) < 1)) |
306 | 234, 304,
305 | syl2anc 579 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (1 <
𝑝 ↔ (1 / 𝑝) < 1)) |
307 | 238, 306 | mpbid 224 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (1 /
𝑝) < 1) |
308 | 229, 307 | ltned 10512 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (1 /
𝑝) ≠ 1) |
309 | | 1nn0 11660 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℕ0 |
310 | 309 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 1 ∈
ℕ0) |
311 | | log1 24769 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(log‘1) = 0 |
312 | | simprr 763 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 1 ≤ 𝑥) |
313 | | 1rp 12141 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 1 ∈
ℝ+ |
314 | | simprl 761 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 𝑥 ∈
ℝ+) |
315 | | logleb 24786 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((1
∈ ℝ+ ∧ 𝑥 ∈ ℝ+) → (1 ≤
𝑥 ↔ (log‘1) ≤
(log‘𝑥))) |
316 | 313, 314,
315 | sylancr 581 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (1 ≤ 𝑥 ↔ (log‘1) ≤
(log‘𝑥))) |
317 | 312, 316 | mpbid 224 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (log‘1)
≤ (log‘𝑥)) |
318 | 311, 317 | syl5eqbrr 4922 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 0 ≤
(log‘𝑥)) |
319 | 318 | adantr 474 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 0 ≤
(log‘𝑥)) |
320 | 233, 239,
319 | divge0d 12221 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 0 ≤
((log‘𝑥) /
(log‘𝑝))) |
321 | | flge0nn0 12940 |
. . . . . . . . . . . . . . . . . 18
⊢
((((log‘𝑥) /
(log‘𝑝)) ∈
ℝ ∧ 0 ≤ ((log‘𝑥) / (log‘𝑝))) → (⌊‘((log‘𝑥) / (log‘𝑝))) ∈
ℕ0) |
322 | 240, 320,
321 | syl2anc 579 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
(⌊‘((log‘𝑥) / (log‘𝑝))) ∈
ℕ0) |
323 | | nn0p1nn 11683 |
. . . . . . . . . . . . . . . . 17
⊢
((⌊‘((log‘𝑥) / (log‘𝑝))) ∈ ℕ0 →
((⌊‘((log‘𝑥) / (log‘𝑝))) + 1) ∈ ℕ) |
324 | 322, 323 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
((⌊‘((log‘𝑥) / (log‘𝑝))) + 1) ∈ ℕ) |
325 | | nnuz 12029 |
. . . . . . . . . . . . . . . 16
⊢ ℕ =
(ℤ≥‘1) |
326 | 324, 325 | syl6eleq 2869 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
((⌊‘((log‘𝑥) / (log‘𝑝))) + 1) ∈
(ℤ≥‘1)) |
327 | 303, 308,
310, 326 | geoserg 15002 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
Σ𝑘 ∈
(1..^((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))((1 / 𝑝)↑𝑘) = ((((1 / 𝑝)↑1) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / (1 − (1 /
𝑝)))) |
328 | 303 | exp1d 13322 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → ((1 /
𝑝)↑1) = (1 / 𝑝)) |
329 | 328 | oveq1d 6937 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (((1 /
𝑝)↑1) − ((1 /
𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) = ((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1)))) |
330 | 228 | nncnd 11392 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈
ℂ) |
331 | | 1cnd 10371 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 1 ∈
ℂ) |
332 | 230 | rpcnne0d 12190 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 ∈ ℂ ∧ 𝑝 ≠ 0)) |
333 | | divsubdir 11069 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑝 ∈ ℂ ∧ 1 ∈
ℂ ∧ (𝑝 ∈
ℂ ∧ 𝑝 ≠ 0))
→ ((𝑝 − 1) /
𝑝) = ((𝑝 / 𝑝) − (1 / 𝑝))) |
334 | 330, 331,
332, 333 | syl3anc 1439 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → ((𝑝 − 1) / 𝑝) = ((𝑝 / 𝑝) − (1 / 𝑝))) |
335 | | divid 11062 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑝 ∈ ℂ ∧ 𝑝 ≠ 0) → (𝑝 / 𝑝) = 1) |
336 | 332, 335 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 / 𝑝) = 1) |
337 | 336 | oveq1d 6937 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → ((𝑝 / 𝑝) − (1 / 𝑝)) = (1 − (1 / 𝑝))) |
338 | 334, 337 | eqtr2d 2815 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (1
− (1 / 𝑝)) = ((𝑝 − 1) / 𝑝)) |
339 | 329, 338 | oveq12d 6940 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → ((((1 /
𝑝)↑1) − ((1 /
𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / (1 − (1 /
𝑝))) = (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))) |
340 | 302, 327,
339 | 3eqtrd 2818 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
Σ𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 / 𝑝)↑𝑘) = (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))) |
341 | 340 | oveq2d 6938 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
((log‘𝑝) ·
Σ𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 / 𝑝)↑𝑘)) = ((log‘𝑝) · (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝)))) |
342 | 299, 341 | eqtr3d 2816 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
Σ𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))((log‘𝑝) · ((1 / 𝑝)↑𝑘)) = ((log‘𝑝) · (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝)))) |
343 | 293, 342 | breqtrd 4912 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
Σ𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ≤ ((log‘𝑝) · (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝)))) |
344 | 243 | rpge0d 12185 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 0 ≤
((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) |
345 | 229, 244 | subge02d 10967 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (0 ≤
((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1)) ↔ ((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) ≤ (1 / 𝑝))) |
346 | 344, 345 | mpbid 224 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → ((1 /
𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) ≤ (1 / 𝑝)) |
347 | 247 | rpcnne0d 12190 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → ((𝑝 − 1) ∈ ℂ ∧
(𝑝 − 1) ≠
0)) |
348 | | dmdcan 11085 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑝 − 1) ∈ ℂ ∧
(𝑝 − 1) ≠ 0) ∧
(𝑝 ∈ ℂ ∧
𝑝 ≠ 0) ∧ 1 ∈
ℂ) → (((𝑝
− 1) / 𝑝) · (1
/ (𝑝 − 1))) = (1 /
𝑝)) |
349 | 347, 332,
331, 348 | syl3anc 1439 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (((𝑝 − 1) / 𝑝) · (1 / (𝑝 − 1))) = (1 / 𝑝)) |
350 | 346, 349 | breqtrrd 4914 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → ((1 /
𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) ≤ (((𝑝 − 1) / 𝑝) · (1 / (𝑝 − 1)))) |
351 | 246 | nnrecred 11426 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (1 /
(𝑝 − 1)) ∈
ℝ) |
352 | 245, 351,
248 | ledivmuld 12234 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → ((((1 /
𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝)) ≤ (1 / (𝑝 − 1)) ↔ ((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) ≤ (((𝑝 − 1) / 𝑝) · (1 / (𝑝 − 1))))) |
353 | 350, 352 | mpbird 249 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (((1 /
𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝)) ≤ (1 / (𝑝 − 1))) |
354 | 249, 351,
239 | lemul2d 12225 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → ((((1 /
𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝)) ≤ (1 / (𝑝 − 1)) ↔ ((log‘𝑝) · (((1 / 𝑝) − ((1 / 𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))) ≤ ((log‘𝑝) · (1 / (𝑝 − 1))))) |
355 | 353, 354 | mpbid 224 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
((log‘𝑝) ·
(((1 / 𝑝) − ((1 /
𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))) ≤ ((log‘𝑝) · (1 / (𝑝 − 1)))) |
356 | 246 | nncnd 11392 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 − 1) ∈
ℂ) |
357 | 246 | nnne0d 11425 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → (𝑝 − 1) ≠
0) |
358 | 294, 356,
357 | divrecd 11154 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
((log‘𝑝) / (𝑝 − 1)) = ((log‘𝑝) · (1 / (𝑝 − 1)))) |
359 | 355, 358 | breqtrrd 4914 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
((log‘𝑝) ·
(((1 / 𝑝) − ((1 /
𝑝)↑((⌊‘((log‘𝑥) / (log‘𝑝))) + 1))) / ((𝑝 − 1) / 𝑝))) ≤ ((log‘𝑝) / (𝑝 − 1))) |
360 | 225, 250,
131, 343, 359 | letrd 10533 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
Σ𝑘 ∈
(1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ≤ ((log‘𝑝) / (𝑝 − 1))) |
361 | 130, 360 | sylan2 586 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁}) → Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ≤ ((log‘𝑝) / (𝑝 − 1))) |
362 | 127, 226,
132, 361 | fsumle 14935 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁}Σ𝑘 ∈ (1...(⌊‘((log‘𝑥) / (log‘𝑝))))((1 − ( 1 ‘(𝐿‘(𝑝↑𝑘)))) · ((Λ‘(𝑝↑𝑘)) / (𝑝↑𝑘))) ≤ Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1))) |
363 | 224, 362 | eqbrtrd 4908 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ≤ Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1))) |
364 | 79 | adantlr 705 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁}) → ((log‘𝑝) / (𝑝 − 1)) ∈ ℝ) |
365 | 239, 247 | rpdivcld 12198 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) →
((log‘𝑝) / (𝑝 − 1)) ∈
ℝ+) |
366 | 365 | rpge0d 12185 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ ℙ) → 0 ≤
((log‘𝑝) / (𝑝 − 1))) |
367 | 69, 366 | sylan2 586 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁}) → 0 ≤ ((log‘𝑝) / (𝑝 − 1))) |
368 | 122, 364,
367, 125 | fsumless 14932 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑝 ∈ {𝑞 ∈ ((0[,]𝑥) ∩ ℙ) ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1)) ≤ Σ𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1))) |
369 | 102, 133,
134, 363, 368 | letrd 10533 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)) ≤ Σ𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1))) |
370 | 121, 369 | eqbrtrd 4908 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) ≤ Σ𝑝 ∈ {𝑞 ∈ ℙ ∣ 𝑞 ∥ 𝑁} ((log‘𝑝) / (𝑝 − 1))) |
371 | 65, 40, 66, 80, 370 | elo1d 14675 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) ∈ 𝑂(1)) |
372 | | o1sub 14754 |
. . 3
⊢ (((𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1) ∧ (𝑥 ∈ ℝ+
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((1
− ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛))) ∈ 𝑂(1)) → ((𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘𝑓 −
(𝑥 ∈
ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))) ∈ 𝑂(1)) |
373 | 64, 371, 372 | sylancr 581 |
. 2
⊢ (𝜑 → ((𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∘𝑓 −
(𝑥 ∈
ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((1 − ( 1 ‘(𝐿‘𝑛))) · ((Λ‘𝑛) / 𝑛)))) ∈ 𝑂(1)) |
374 | 63, 373 | eqeltrrd 2860 |
1
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((
1
‘(𝐿‘𝑛)) ·
((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) ∈
𝑂(1)) |