Step | Hyp | Ref
| Expression |
1 | | flid 12609 |
. . . . 5
⊢ (𝐴 ∈ ℤ →
(⌊‘𝐴) = 𝐴) |
2 | 1 | oveq2d 6666 |
. . . 4
⊢ (𝐴 ∈ ℤ →
(1...(⌊‘𝐴)) =
(1...𝐴)) |
3 | 2 | sumeq1d 14431 |
. . 3
⊢ (𝐴 ∈ ℤ →
Σ𝑛 ∈
(1...(⌊‘𝐴))(((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) = Σ𝑛 ∈ (1...𝐴)(((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛)) |
4 | | fveq2 6191 |
. . . . . 6
⊢ (𝑛 = (𝑝↑𝑘) → (Λ‘𝑛) = (Λ‘(𝑝↑𝑘))) |
5 | | eleq1 2689 |
. . . . . . 7
⊢ (𝑛 = (𝑝↑𝑘) → (𝑛 ∈ ℙ ↔ (𝑝↑𝑘) ∈ ℙ)) |
6 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑛 = (𝑝↑𝑘) → (log‘𝑛) = (log‘(𝑝↑𝑘))) |
7 | 5, 6 | ifbieq1d 4109 |
. . . . . 6
⊢ (𝑛 = (𝑝↑𝑘) → if(𝑛 ∈ ℙ, (log‘𝑛), 0) = if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) |
8 | 4, 7 | oveq12d 6668 |
. . . . 5
⊢ (𝑛 = (𝑝↑𝑘) → ((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) = ((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0))) |
9 | | id 22 |
. . . . 5
⊢ (𝑛 = (𝑝↑𝑘) → 𝑛 = (𝑝↑𝑘)) |
10 | 8, 9 | oveq12d 6668 |
. . . 4
⊢ (𝑛 = (𝑝↑𝑘) → (((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) = (((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) / (𝑝↑𝑘))) |
11 | | zre 11381 |
. . . 4
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℝ) |
12 | | elfznn 12370 |
. . . . . . . . 9
⊢ (𝑛 ∈
(1...(⌊‘𝐴))
→ 𝑛 ∈
ℕ) |
13 | 12 | adantl 482 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ 𝑛 ∈
ℕ) |
14 | | vmacl 24844 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ →
(Λ‘𝑛) ∈
ℝ) |
15 | 13, 14 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ (Λ‘𝑛)
∈ ℝ) |
16 | 13 | nnrpd 11870 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ 𝑛 ∈
ℝ+) |
17 | 16 | relogcld 24369 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ (log‘𝑛) ∈
ℝ) |
18 | | 0re 10040 |
. . . . . . . 8
⊢ 0 ∈
ℝ |
19 | | ifcl 4130 |
. . . . . . . 8
⊢
(((log‘𝑛)
∈ ℝ ∧ 0 ∈ ℝ) → if(𝑛 ∈ ℙ, (log‘𝑛), 0) ∈
ℝ) |
20 | 17, 18, 19 | sylancl 694 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ if(𝑛 ∈ ℙ,
(log‘𝑛), 0) ∈
ℝ) |
21 | 15, 20 | resubcld 10458 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ ((Λ‘𝑛)
− if(𝑛 ∈
ℙ, (log‘𝑛), 0))
∈ ℝ) |
22 | 21, 13 | nndivred 11069 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ (((Λ‘𝑛)
− if(𝑛 ∈
ℙ, (log‘𝑛), 0))
/ 𝑛) ∈
ℝ) |
23 | 22 | recnd 10068 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ (((Λ‘𝑛)
− if(𝑛 ∈
ℙ, (log‘𝑛), 0))
/ 𝑛) ∈
ℂ) |
24 | | simprr 796 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ (𝑛 ∈
(1...(⌊‘𝐴))
∧ (Λ‘𝑛) =
0)) → (Λ‘𝑛) = 0) |
25 | | vmaprm 24843 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℙ →
(Λ‘𝑛) =
(log‘𝑛)) |
26 | | prmnn 15388 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℙ → 𝑛 ∈
ℕ) |
27 | 26 | nnred 11035 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℙ → 𝑛 ∈
ℝ) |
28 | | prmgt1 15409 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℙ → 1 <
𝑛) |
29 | 27, 28 | rplogcld 24375 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℙ →
(log‘𝑛) ∈
ℝ+) |
30 | 25, 29 | eqeltrd 2701 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℙ →
(Λ‘𝑛) ∈
ℝ+) |
31 | 30 | rpne0d 11877 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℙ →
(Λ‘𝑛) ≠
0) |
32 | 31 | necon2bi 2824 |
. . . . . . . . . 10
⊢
((Λ‘𝑛)
= 0 → ¬ 𝑛 ∈
ℙ) |
33 | 32 | ad2antll 765 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ (𝑛 ∈
(1...(⌊‘𝐴))
∧ (Λ‘𝑛) =
0)) → ¬ 𝑛 ∈
ℙ) |
34 | 33 | iffalsed 4097 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ (𝑛 ∈
(1...(⌊‘𝐴))
∧ (Λ‘𝑛) =
0)) → if(𝑛 ∈
ℙ, (log‘𝑛), 0)
= 0) |
35 | 24, 34 | oveq12d 6668 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ (𝑛 ∈
(1...(⌊‘𝐴))
∧ (Λ‘𝑛) =
0)) → ((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) = (0 −
0)) |
36 | | 0m0e0 11130 |
. . . . . . 7
⊢ (0
− 0) = 0 |
37 | 35, 36 | syl6eq 2672 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ (𝑛 ∈
(1...(⌊‘𝐴))
∧ (Λ‘𝑛) =
0)) → ((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) = 0) |
38 | 37 | oveq1d 6665 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ (𝑛 ∈
(1...(⌊‘𝐴))
∧ (Λ‘𝑛) =
0)) → (((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) = (0 / 𝑛)) |
39 | 12 | ad2antrl 764 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ (𝑛 ∈
(1...(⌊‘𝐴))
∧ (Λ‘𝑛) =
0)) → 𝑛 ∈
ℕ) |
40 | 39 | nnrpd 11870 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ (𝑛 ∈
(1...(⌊‘𝐴))
∧ (Λ‘𝑛) =
0)) → 𝑛 ∈
ℝ+) |
41 | 40 | rpcnne0d 11881 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ (𝑛 ∈
(1...(⌊‘𝐴))
∧ (Λ‘𝑛) =
0)) → (𝑛 ∈
ℂ ∧ 𝑛 ≠
0)) |
42 | | div0 10715 |
. . . . . 6
⊢ ((𝑛 ∈ ℂ ∧ 𝑛 ≠ 0) → (0 / 𝑛) = 0) |
43 | 41, 42 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ (𝑛 ∈
(1...(⌊‘𝐴))
∧ (Λ‘𝑛) =
0)) → (0 / 𝑛) =
0) |
44 | 38, 43 | eqtrd 2656 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ (𝑛 ∈
(1...(⌊‘𝐴))
∧ (Λ‘𝑛) =
0)) → (((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) = 0) |
45 | 10, 11, 23, 44 | fsumvma2 24939 |
. . 3
⊢ (𝐴 ∈ ℤ →
Σ𝑛 ∈
(1...(⌊‘𝐴))(((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) / (𝑝↑𝑘))) |
46 | 3, 45 | eqtr3d 2658 |
. 2
⊢ (𝐴 ∈ ℤ →
Σ𝑛 ∈ (1...𝐴)(((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) / (𝑝↑𝑘))) |
47 | | fzfid 12772 |
. . . . 5
⊢ (𝐴 ∈ ℤ →
(2...((abs‘𝐴) + 1))
∈ Fin) |
48 | | inss2 3834 |
. . . . . . . . . . . 12
⊢
((0[,]𝐴) ∩
ℙ) ⊆ ℙ |
49 | | simpr 477 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) |
50 | 48, 49 | sseldi 3601 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℙ) |
51 | | prmnn 15388 |
. . . . . . . . . . 11
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) |
52 | 50, 51 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℕ) |
53 | 52 | nnred 11035 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℝ) |
54 | 11 | adantr 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝐴 ∈ ℝ) |
55 | | zcn 11382 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℂ) |
56 | 55 | abscld 14175 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℤ →
(abs‘𝐴) ∈
ℝ) |
57 | | peano2re 10209 |
. . . . . . . . . . 11
⊢
((abs‘𝐴)
∈ ℝ → ((abs‘𝐴) + 1) ∈ ℝ) |
58 | 56, 57 | syl 17 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℤ →
((abs‘𝐴) + 1) ∈
ℝ) |
59 | 58 | adantr 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((abs‘𝐴) + 1) ∈
ℝ) |
60 | | inss1 3833 |
. . . . . . . . . . . . 13
⊢
((0[,]𝐴) ∩
ℙ) ⊆ (0[,]𝐴) |
61 | 60 | sseli 3599 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) → 𝑝 ∈ (0[,]𝐴)) |
62 | | elicc2 12238 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (𝑝
∈ (0[,]𝐴) ↔
(𝑝 ∈ ℝ ∧ 0
≤ 𝑝 ∧ 𝑝 ≤ 𝐴))) |
63 | 18, 11, 62 | sylancr 695 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℤ → (𝑝 ∈ (0[,]𝐴) ↔ (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴))) |
64 | 61, 63 | syl5ib 234 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℤ → (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) → (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴))) |
65 | 64 | imp 445 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴)) |
66 | 65 | simp3d 1075 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ≤ 𝐴) |
67 | 55 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝐴 ∈ ℂ) |
68 | 67 | abscld 14175 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (abs‘𝐴) ∈
ℝ) |
69 | 54 | leabsd 14153 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝐴 ≤ (abs‘𝐴)) |
70 | 68 | lep1d 10955 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (abs‘𝐴) ≤ ((abs‘𝐴) + 1)) |
71 | 54, 68, 59, 69, 70 | letrd 10194 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝐴 ≤ ((abs‘𝐴) + 1)) |
72 | 53, 54, 59, 66, 71 | letrd 10194 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ≤ ((abs‘𝐴) + 1)) |
73 | | prmuz2 15408 |
. . . . . . . . . 10
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
(ℤ≥‘2)) |
74 | 50, 73 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈
(ℤ≥‘2)) |
75 | | nn0abscl 14052 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℤ →
(abs‘𝐴) ∈
ℕ0) |
76 | | nn0p1nn 11332 |
. . . . . . . . . . . 12
⊢
((abs‘𝐴)
∈ ℕ0 → ((abs‘𝐴) + 1) ∈ ℕ) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℤ →
((abs‘𝐴) + 1) ∈
ℕ) |
78 | 77 | nnzd 11481 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℤ →
((abs‘𝐴) + 1) ∈
ℤ) |
79 | 78 | adantr 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((abs‘𝐴) + 1) ∈
ℤ) |
80 | | elfz5 12334 |
. . . . . . . . 9
⊢ ((𝑝 ∈
(ℤ≥‘2) ∧ ((abs‘𝐴) + 1) ∈ ℤ) → (𝑝 ∈ (2...((abs‘𝐴) + 1)) ↔ 𝑝 ≤ ((abs‘𝐴) + 1))) |
81 | 74, 79, 80 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 ∈ (2...((abs‘𝐴) + 1)) ↔ 𝑝 ≤ ((abs‘𝐴) + 1))) |
82 | 72, 81 | mpbird 247 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ (2...((abs‘𝐴) + 1))) |
83 | 82 | ex 450 |
. . . . . 6
⊢ (𝐴 ∈ ℤ → (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) → 𝑝 ∈ (2...((abs‘𝐴) + 1)))) |
84 | 83 | ssrdv 3609 |
. . . . 5
⊢ (𝐴 ∈ ℤ →
((0[,]𝐴) ∩ ℙ)
⊆ (2...((abs‘𝐴)
+ 1))) |
85 | | ssfi 8180 |
. . . . 5
⊢
(((2...((abs‘𝐴) + 1)) ∈ Fin ∧ ((0[,]𝐴) ∩ ℙ) ⊆
(2...((abs‘𝐴) + 1)))
→ ((0[,]𝐴) ∩
ℙ) ∈ Fin) |
86 | 47, 84, 85 | syl2anc 693 |
. . . 4
⊢ (𝐴 ∈ ℤ →
((0[,]𝐴) ∩ ℙ)
∈ Fin) |
87 | | fzfid 12772 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(1...(⌊‘((log‘𝐴) / (log‘𝑝)))) ∈ Fin) |
88 | | simprl 794 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) |
89 | 48, 88 | sseldi 3601 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → 𝑝 ∈ ℙ) |
90 | | elfznn 12370 |
. . . . . . . . . . 11
⊢ (𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝)))) → 𝑘 ∈ ℕ) |
91 | 90 | ad2antll 765 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → 𝑘 ∈ ℕ) |
92 | | vmappw 24842 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) →
(Λ‘(𝑝↑𝑘)) = (log‘𝑝)) |
93 | 89, 91, 92 | syl2anc 693 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) →
(Λ‘(𝑝↑𝑘)) = (log‘𝑝)) |
94 | 52 | adantrr 753 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → 𝑝 ∈ ℕ) |
95 | 94 | nnrpd 11870 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → 𝑝 ∈ ℝ+) |
96 | 95 | relogcld 24369 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → (log‘𝑝) ∈
ℝ) |
97 | 93, 96 | eqeltrd 2701 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) →
(Λ‘(𝑝↑𝑘)) ∈ ℝ) |
98 | 91 | nnnn0d 11351 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → 𝑘 ∈ ℕ0) |
99 | | nnexpcl 12873 |
. . . . . . . . . . . 12
⊢ ((𝑝 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (𝑝↑𝑘) ∈
ℕ) |
100 | 94, 98, 99 | syl2anc 693 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → (𝑝↑𝑘) ∈ ℕ) |
101 | 100 | nnrpd 11870 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → (𝑝↑𝑘) ∈
ℝ+) |
102 | 101 | relogcld 24369 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → (log‘(𝑝↑𝑘)) ∈ ℝ) |
103 | | ifcl 4130 |
. . . . . . . . 9
⊢
(((log‘(𝑝↑𝑘)) ∈ ℝ ∧ 0 ∈ ℝ)
→ if((𝑝↑𝑘) ∈ ℙ,
(log‘(𝑝↑𝑘)), 0) ∈
ℝ) |
104 | 102, 18, 103 | sylancl 694 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0) ∈ ℝ) |
105 | 97, 104 | resubcld 10458 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) →
((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) ∈ ℝ) |
106 | 105, 100 | nndivred 11069 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) →
(((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) / (𝑝↑𝑘)) ∈ ℝ) |
107 | 106 | anassrs 680 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) →
(((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) / (𝑝↑𝑘)) ∈ ℝ) |
108 | 87, 107 | fsumrecl 14465 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) / (𝑝↑𝑘)) ∈ ℝ) |
109 | 86, 108 | fsumrecl 14465 |
. . 3
⊢ (𝐴 ∈ ℤ →
Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)Σ𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) / (𝑝↑𝑘)) ∈ ℝ) |
110 | 52 | nnrpd 11870 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℝ+) |
111 | 110 | relogcld 24369 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈
ℝ) |
112 | | uz2m1nn 11763 |
. . . . . . 7
⊢ (𝑝 ∈
(ℤ≥‘2) → (𝑝 − 1) ∈ ℕ) |
113 | 74, 112 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 − 1) ∈ ℕ) |
114 | 52, 113 | nnmulcld 11068 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 · (𝑝 − 1)) ∈ ℕ) |
115 | 111, 114 | nndivred 11069 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) / (𝑝 · (𝑝 − 1))) ∈
ℝ) |
116 | 86, 115 | fsumrecl 14465 |
. . 3
⊢ (𝐴 ∈ ℤ →
Σ𝑝 ∈ ((0[,]𝐴) ∩
ℙ)((log‘𝑝) /
(𝑝 · (𝑝 − 1))) ∈
ℝ) |
117 | | 2re 11090 |
. . . 4
⊢ 2 ∈
ℝ |
118 | 117 | a1i 11 |
. . 3
⊢ (𝐴 ∈ ℤ → 2 ∈
ℝ) |
119 | 18 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 0 ∈
ℝ) |
120 | 52 | nngt0d 11064 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 0 < 𝑝) |
121 | 119, 53, 54, 120, 66 | ltletrd 10197 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 0 < 𝐴) |
122 | 54, 121 | elrpd 11869 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝐴 ∈
ℝ+) |
123 | 122 | relogcld 24369 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝐴) ∈
ℝ) |
124 | | prmgt1 15409 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈ ℙ → 1 <
𝑝) |
125 | 50, 124 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 1 < 𝑝) |
126 | 53, 125 | rplogcld 24375 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈
ℝ+) |
127 | 123, 126 | rerpdivcld 11903 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝐴) / (log‘𝑝)) ∈
ℝ) |
128 | 126 | rpcnd 11874 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈
ℂ) |
129 | 128 | mulid2d 10058 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 ·
(log‘𝑝)) =
(log‘𝑝)) |
130 | 110, 122 | logled 24373 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 ≤ 𝐴 ↔ (log‘𝑝) ≤ (log‘𝐴))) |
131 | 66, 130 | mpbid 222 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ≤ (log‘𝐴)) |
132 | 129, 131 | eqbrtrd 4675 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 ·
(log‘𝑝)) ≤
(log‘𝐴)) |
133 | | 1re 10039 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ |
134 | 133 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 1 ∈
ℝ) |
135 | 134, 123,
126 | lemuldivd 11921 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 ·
(log‘𝑝)) ≤
(log‘𝐴) ↔ 1 ≤
((log‘𝐴) /
(log‘𝑝)))) |
136 | 132, 135 | mpbid 222 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 1 ≤
((log‘𝐴) /
(log‘𝑝))) |
137 | | flge1nn 12622 |
. . . . . . . . 9
⊢
((((log‘𝐴) /
(log‘𝑝)) ∈
ℝ ∧ 1 ≤ ((log‘𝐴) / (log‘𝑝))) → (⌊‘((log‘𝐴) / (log‘𝑝))) ∈
ℕ) |
138 | 127, 136,
137 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℕ) |
139 | | nnuz 11723 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
140 | 138, 139 | syl6eleq 2711 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(⌊‘((log‘𝐴) / (log‘𝑝))) ∈
(ℤ≥‘1)) |
141 | 106 | recnd 10068 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) →
(((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) / (𝑝↑𝑘)) ∈ ℂ) |
142 | 141 | anassrs 680 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) →
(((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) / (𝑝↑𝑘)) ∈ ℂ) |
143 | | oveq2 6658 |
. . . . . . . . . 10
⊢ (𝑘 = 1 → (𝑝↑𝑘) = (𝑝↑1)) |
144 | 143 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑘 = 1 →
(Λ‘(𝑝↑𝑘)) = (Λ‘(𝑝↑1))) |
145 | 143 | eleq1d 2686 |
. . . . . . . . . 10
⊢ (𝑘 = 1 → ((𝑝↑𝑘) ∈ ℙ ↔ (𝑝↑1) ∈ ℙ)) |
146 | 143 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑘 = 1 → (log‘(𝑝↑𝑘)) = (log‘(𝑝↑1))) |
147 | 145, 146 | ifbieq1d 4109 |
. . . . . . . . 9
⊢ (𝑘 = 1 → if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0) = if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0)) |
148 | 144, 147 | oveq12d 6668 |
. . . . . . . 8
⊢ (𝑘 = 1 →
((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) = ((Λ‘(𝑝↑1)) − if((𝑝↑1) ∈ ℙ,
(log‘(𝑝↑1)),
0))) |
149 | 148, 143 | oveq12d 6668 |
. . . . . . 7
⊢ (𝑘 = 1 →
(((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) / (𝑝↑𝑘)) = (((Λ‘(𝑝↑1)) − if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0)) / (𝑝↑1))) |
150 | 140, 142,
149 | fsum1p 14482 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) / (𝑝↑𝑘)) = ((((Λ‘(𝑝↑1)) − if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0)) / (𝑝↑1)) + Σ𝑘 ∈ ((1 +
1)...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) / (𝑝↑𝑘)))) |
151 | 52 | nncnd 11036 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℂ) |
152 | 151 | exp1d 13003 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝↑1) = 𝑝) |
153 | 152 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(Λ‘(𝑝↑1))
= (Λ‘𝑝)) |
154 | | vmaprm 24843 |
. . . . . . . . . . . . 13
⊢ (𝑝 ∈ ℙ →
(Λ‘𝑝) =
(log‘𝑝)) |
155 | 50, 154 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(Λ‘𝑝) =
(log‘𝑝)) |
156 | 153, 155 | eqtrd 2656 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(Λ‘(𝑝↑1))
= (log‘𝑝)) |
157 | 152, 50 | eqeltrd 2701 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝↑1) ∈ ℙ) |
158 | 157 | iftrued 4094 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → if((𝑝↑1) ∈ ℙ,
(log‘(𝑝↑1)), 0)
= (log‘(𝑝↑1))) |
159 | 152 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘(𝑝↑1)) = (log‘𝑝)) |
160 | 158, 159 | eqtrd 2656 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → if((𝑝↑1) ∈ ℙ,
(log‘(𝑝↑1)), 0)
= (log‘𝑝)) |
161 | 156, 160 | oveq12d 6668 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
((Λ‘(𝑝↑1)) − if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0)) =
((log‘𝑝) −
(log‘𝑝))) |
162 | 128 | subidd 10380 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) − (log‘𝑝)) = 0) |
163 | 161, 162 | eqtrd 2656 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
((Λ‘(𝑝↑1)) − if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0)) =
0) |
164 | 163, 152 | oveq12d 6668 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(((Λ‘(𝑝↑1)) − if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0)) / (𝑝↑1)) = (0 / 𝑝)) |
165 | 110 | rpcnne0d 11881 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 ∈ ℂ ∧ 𝑝 ≠ 0)) |
166 | | div0 10715 |
. . . . . . . . 9
⊢ ((𝑝 ∈ ℂ ∧ 𝑝 ≠ 0) → (0 / 𝑝) = 0) |
167 | 165, 166 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (0 / 𝑝) = 0) |
168 | 164, 167 | eqtrd 2656 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(((Λ‘(𝑝↑1)) − if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0)) / (𝑝↑1)) = 0) |
169 | | 1p1e2 11134 |
. . . . . . . . . 10
⊢ (1 + 1) =
2 |
170 | 169 | oveq1i 6660 |
. . . . . . . . 9
⊢ ((1 +
1)...(⌊‘((log‘𝐴) / (log‘𝑝)))) = (2...(⌊‘((log‘𝐴) / (log‘𝑝)))) |
171 | 170 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 +
1)...(⌊‘((log‘𝐴) / (log‘𝑝)))) = (2...(⌊‘((log‘𝐴) / (log‘𝑝))))) |
172 | | elfzuz 12338 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈
(2...(⌊‘((log‘𝐴) / (log‘𝑝)))) → 𝑘 ∈
(ℤ≥‘2)) |
173 | | eluz2nn 11726 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈
(ℤ≥‘2) → 𝑘 ∈ ℕ) |
174 | 172, 173 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈
(2...(⌊‘((log‘𝐴) / (log‘𝑝)))) → 𝑘 ∈ ℕ) |
175 | 174, 170 | eleq2s 2719 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ((1 +
1)...(⌊‘((log‘𝐴) / (log‘𝑝)))) → 𝑘 ∈ ℕ) |
176 | 50, 175, 92 | syl2an 494 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 +
1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → (Λ‘(𝑝↑𝑘)) = (log‘𝑝)) |
177 | 52 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 +
1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → 𝑝 ∈ ℕ) |
178 | | nnq 11801 |
. . . . . . . . . . . . . 14
⊢ (𝑝 ∈ ℕ → 𝑝 ∈
ℚ) |
179 | 177, 178 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 +
1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → 𝑝 ∈ ℚ) |
180 | 172, 170 | eleq2s 2719 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ((1 +
1)...(⌊‘((log‘𝐴) / (log‘𝑝)))) → 𝑘 ∈
(ℤ≥‘2)) |
181 | 180 | adantl 482 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 +
1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → 𝑘 ∈
(ℤ≥‘2)) |
182 | | expnprm 15606 |
. . . . . . . . . . . . 13
⊢ ((𝑝 ∈ ℚ ∧ 𝑘 ∈
(ℤ≥‘2)) → ¬ (𝑝↑𝑘) ∈ ℙ) |
183 | 179, 181,
182 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 +
1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → ¬ (𝑝↑𝑘) ∈ ℙ) |
184 | 183 | iffalsed 4097 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 +
1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0) = 0) |
185 | 176, 184 | oveq12d 6668 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 +
1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → ((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) = ((log‘𝑝) − 0)) |
186 | 128 | subid1d 10381 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) − 0) = (log‘𝑝)) |
187 | 186 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 +
1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → ((log‘𝑝) − 0) = (log‘𝑝)) |
188 | 185, 187 | eqtrd 2656 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 +
1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → ((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) = (log‘𝑝)) |
189 | 188 | oveq1d 6665 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 +
1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → (((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) / (𝑝↑𝑘)) = ((log‘𝑝) / (𝑝↑𝑘))) |
190 | 171, 189 | sumeq12dv 14437 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈ ((1 +
1)...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) / (𝑝↑𝑘)) = Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝↑𝑘))) |
191 | 168, 190 | oveq12d 6668 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
((((Λ‘(𝑝↑1)) − if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0)) / (𝑝↑1)) + Σ𝑘 ∈ ((1 +
1)...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) / (𝑝↑𝑘))) = (0 + Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝↑𝑘)))) |
192 | | fzfid 12772 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(2...(⌊‘((log‘𝐴) / (log‘𝑝)))) ∈ Fin) |
193 | 111 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → (log‘𝑝) ∈
ℝ) |
194 | | nnnn0 11299 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) |
195 | 52, 194, 99 | syl2an 494 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → (𝑝↑𝑘) ∈ ℕ) |
196 | 193, 195 | nndivred 11069 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → ((log‘𝑝) / (𝑝↑𝑘)) ∈ ℝ) |
197 | 174, 196 | sylan2 491 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))) → ((log‘𝑝) / (𝑝↑𝑘)) ∈ ℝ) |
198 | 192, 197 | fsumrecl 14465 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈
(2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝↑𝑘)) ∈ ℝ) |
199 | 198 | recnd 10068 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈
(2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝↑𝑘)) ∈ ℂ) |
200 | 199 | addid2d 10237 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (0 + Σ𝑘 ∈
(2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝↑𝑘))) = Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝↑𝑘))) |
201 | 150, 191,
200 | 3eqtrd 2660 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) / (𝑝↑𝑘)) = Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝↑𝑘))) |
202 | 110 | rpreccld 11882 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 / 𝑝) ∈
ℝ+) |
203 | 127 | flcld 12599 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℤ) |
204 | 203 | peano2zd 11485 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
((⌊‘((log‘𝐴) / (log‘𝑝))) + 1) ∈ ℤ) |
205 | 202, 204 | rpexpcld 13032 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1)) ∈
ℝ+) |
206 | 205 | rpge0d 11876 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 0 ≤ ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) |
207 | 52 | nnrecred 11066 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 / 𝑝) ∈
ℝ) |
208 | 207 | resqcld 13035 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 / 𝑝)↑2) ∈
ℝ) |
209 | 138 | peano2nnd 11037 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
((⌊‘((log‘𝐴) / (log‘𝑝))) + 1) ∈ ℕ) |
210 | 209 | nnnn0d 11351 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
((⌊‘((log‘𝐴) / (log‘𝑝))) + 1) ∈
ℕ0) |
211 | 207, 210 | reexpcld 13025 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1)) ∈
ℝ) |
212 | 208, 211 | subge02d 10619 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (0 ≤ ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1)) ↔ (((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) ≤ ((1 / 𝑝)↑2))) |
213 | 206, 212 | mpbid 222 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) ≤ ((1 / 𝑝)↑2)) |
214 | 113 | nnrpd 11870 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 − 1) ∈
ℝ+) |
215 | 214 | rpcnne0d 11881 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((𝑝 − 1) ∈ ℂ ∧
(𝑝 − 1) ≠
0)) |
216 | 202 | rpcnd 11874 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 / 𝑝) ∈
ℂ) |
217 | | dmdcan 10735 |
. . . . . . . . . . 11
⊢ ((((𝑝 − 1) ∈ ℂ ∧
(𝑝 − 1) ≠ 0) ∧
(𝑝 ∈ ℂ ∧
𝑝 ≠ 0) ∧ (1 / 𝑝) ∈ ℂ) →
(((𝑝 − 1) / 𝑝) · ((1 / 𝑝) / (𝑝 − 1))) = ((1 / 𝑝) / 𝑝)) |
218 | 215, 165,
216, 217 | syl3anc 1326 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((𝑝 − 1) / 𝑝) · ((1 / 𝑝) / (𝑝 − 1))) = ((1 / 𝑝) / 𝑝)) |
219 | 134 | recnd 10068 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 1 ∈
ℂ) |
220 | | divsubdir 10721 |
. . . . . . . . . . . . 13
⊢ ((𝑝 ∈ ℂ ∧ 1 ∈
ℂ ∧ (𝑝 ∈
ℂ ∧ 𝑝 ≠ 0))
→ ((𝑝 − 1) /
𝑝) = ((𝑝 / 𝑝) − (1 / 𝑝))) |
221 | 151, 219,
165, 220 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((𝑝 − 1) / 𝑝) = ((𝑝 / 𝑝) − (1 / 𝑝))) |
222 | | divid 10714 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 ∈ ℂ ∧ 𝑝 ≠ 0) → (𝑝 / 𝑝) = 1) |
223 | 165, 222 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 / 𝑝) = 1) |
224 | 223 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((𝑝 / 𝑝) − (1 / 𝑝)) = (1 − (1 / 𝑝))) |
225 | 221, 224 | eqtrd 2656 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((𝑝 − 1) / 𝑝) = (1 − (1 / 𝑝))) |
226 | | divdiv1 10736 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℂ ∧ (𝑝
∈ ℂ ∧ 𝑝 ≠
0) ∧ ((𝑝 − 1)
∈ ℂ ∧ (𝑝
− 1) ≠ 0)) → ((1 / 𝑝) / (𝑝 − 1)) = (1 / (𝑝 · (𝑝 − 1)))) |
227 | 219, 165,
215, 226 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 / 𝑝) / (𝑝 − 1)) = (1 / (𝑝 · (𝑝 − 1)))) |
228 | 225, 227 | oveq12d 6668 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((𝑝 − 1) / 𝑝) · ((1 / 𝑝) / (𝑝 − 1))) = ((1 − (1 / 𝑝)) · (1 / (𝑝 · (𝑝 − 1))))) |
229 | 52 | nnne0d 11065 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ≠ 0) |
230 | 216, 151,
229 | divrecd 10804 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 / 𝑝) / 𝑝) = ((1 / 𝑝) · (1 / 𝑝))) |
231 | 216 | sqvald 13005 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 / 𝑝)↑2) = ((1 / 𝑝) · (1 / 𝑝))) |
232 | 230, 231 | eqtr4d 2659 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 / 𝑝) / 𝑝) = ((1 / 𝑝)↑2)) |
233 | 218, 228,
232 | 3eqtr3d 2664 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 − (1 /
𝑝)) · (1 / (𝑝 · (𝑝 − 1)))) = ((1 / 𝑝)↑2)) |
234 | 213, 233 | breqtrrd 4681 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) ≤ ((1 − (1 /
𝑝)) · (1 / (𝑝 · (𝑝 − 1))))) |
235 | 208, 211 | resubcld 10458 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) ∈
ℝ) |
236 | 114 | nnrecred 11066 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 / (𝑝 · (𝑝 − 1))) ∈
ℝ) |
237 | | resubcl 10345 |
. . . . . . . . . 10
⊢ ((1
∈ ℝ ∧ (1 / 𝑝) ∈ ℝ) → (1 − (1 /
𝑝)) ∈
ℝ) |
238 | 133, 207,
237 | sylancr 695 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 − (1 /
𝑝)) ∈
ℝ) |
239 | | recgt1 10919 |
. . . . . . . . . . . 12
⊢ ((𝑝 ∈ ℝ ∧ 0 <
𝑝) → (1 < 𝑝 ↔ (1 / 𝑝) < 1)) |
240 | 53, 120, 239 | syl2anc 693 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 < 𝑝 ↔ (1 / 𝑝) < 1)) |
241 | 125, 240 | mpbid 222 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 / 𝑝) < 1) |
242 | | posdif 10521 |
. . . . . . . . . . 11
⊢ (((1 /
𝑝) ∈ ℝ ∧ 1
∈ ℝ) → ((1 / 𝑝) < 1 ↔ 0 < (1 − (1 / 𝑝)))) |
243 | 207, 133,
242 | sylancl 694 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 / 𝑝) < 1 ↔ 0 < (1
− (1 / 𝑝)))) |
244 | 241, 243 | mpbid 222 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 0 < (1 −
(1 / 𝑝))) |
245 | | ledivmul 10899 |
. . . . . . . . 9
⊢ (((((1 /
𝑝)↑2) − ((1 /
𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) ∈ ℝ ∧
(1 / (𝑝 · (𝑝 − 1))) ∈ ℝ
∧ ((1 − (1 / 𝑝))
∈ ℝ ∧ 0 < (1 − (1 / 𝑝)))) → (((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 /
𝑝))) ≤ (1 / (𝑝 · (𝑝 − 1))) ↔ (((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) ≤ ((1 − (1 /
𝑝)) · (1 / (𝑝 · (𝑝 − 1)))))) |
246 | 235, 236,
238, 244, 245 | syl112anc 1330 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 /
𝑝))) ≤ (1 / (𝑝 · (𝑝 − 1))) ↔ (((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) ≤ ((1 − (1 /
𝑝)) · (1 / (𝑝 · (𝑝 − 1)))))) |
247 | 234, 246 | mpbird 247 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 /
𝑝))) ≤ (1 / (𝑝 · (𝑝 − 1)))) |
248 | 238, 244 | elrpd 11869 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 − (1 /
𝑝)) ∈
ℝ+) |
249 | 235, 248 | rerpdivcld 11903 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 /
𝑝))) ∈
ℝ) |
250 | 249, 236,
126 | lemul2d 11916 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 /
𝑝))) ≤ (1 / (𝑝 · (𝑝 − 1))) ↔ ((log‘𝑝) · ((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 /
𝑝)))) ≤
((log‘𝑝) · (1
/ (𝑝 · (𝑝 −
1)))))) |
251 | 247, 250 | mpbid 222 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) · ((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 /
𝑝)))) ≤
((log‘𝑝) · (1
/ (𝑝 · (𝑝 − 1))))) |
252 | 128 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → (log‘𝑝) ∈
ℂ) |
253 | 195 | nncnd 11036 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → (𝑝↑𝑘) ∈ ℂ) |
254 | 195 | nnne0d 11065 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → (𝑝↑𝑘) ≠ 0) |
255 | 252, 253,
254 | divrecd 10804 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → ((log‘𝑝) / (𝑝↑𝑘)) = ((log‘𝑝) · (1 / (𝑝↑𝑘)))) |
256 | 151 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → 𝑝 ∈ ℂ) |
257 | 52 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → 𝑝 ∈ ℕ) |
258 | 257 | nnne0d 11065 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → 𝑝 ≠ 0) |
259 | | nnz 11399 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℤ) |
260 | 259 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℤ) |
261 | 256, 258,
260 | exprecd 13016 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → ((1 / 𝑝)↑𝑘) = (1 / (𝑝↑𝑘))) |
262 | 261 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → ((log‘𝑝) · ((1 / 𝑝)↑𝑘)) = ((log‘𝑝) · (1 / (𝑝↑𝑘)))) |
263 | 255, 262 | eqtr4d 2659 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → ((log‘𝑝) / (𝑝↑𝑘)) = ((log‘𝑝) · ((1 / 𝑝)↑𝑘))) |
264 | 174, 263 | sylan2 491 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))) → ((log‘𝑝) / (𝑝↑𝑘)) = ((log‘𝑝) · ((1 / 𝑝)↑𝑘))) |
265 | 264 | sumeq2dv 14433 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈
(2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝↑𝑘)) = Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) · ((1 / 𝑝)↑𝑘))) |
266 | 174 | nnnn0d 11351 |
. . . . . . . . 9
⊢ (𝑘 ∈
(2...(⌊‘((log‘𝐴) / (log‘𝑝)))) → 𝑘 ∈ ℕ0) |
267 | | expcl 12878 |
. . . . . . . . 9
⊢ (((1 /
𝑝) ∈ ℂ ∧
𝑘 ∈
ℕ0) → ((1 / 𝑝)↑𝑘) ∈ ℂ) |
268 | 216, 266,
267 | syl2an 494 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))) → ((1 / 𝑝)↑𝑘) ∈ ℂ) |
269 | 192, 128,
268 | fsummulc2 14516 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) · Σ𝑘 ∈
(2...(⌊‘((log‘𝐴) / (log‘𝑝))))((1 / 𝑝)↑𝑘)) = Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) · ((1 / 𝑝)↑𝑘))) |
270 | | fzval3 12536 |
. . . . . . . . . . 11
⊢
((⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℤ →
(2...(⌊‘((log‘𝐴) / (log‘𝑝)))) = (2..^((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) |
271 | 203, 270 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(2...(⌊‘((log‘𝐴) / (log‘𝑝)))) = (2..^((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) |
272 | 271 | sumeq1d 14431 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈
(2...(⌊‘((log‘𝐴) / (log‘𝑝))))((1 / 𝑝)↑𝑘) = Σ𝑘 ∈
(2..^((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))((1 / 𝑝)↑𝑘)) |
273 | 207, 241 | ltned 10173 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 / 𝑝) ≠ 1) |
274 | | 2nn0 11309 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ0 |
275 | 274 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 2 ∈
ℕ0) |
276 | | eluzp1p1 11713 |
. . . . . . . . . . . 12
⊢
((⌊‘((log‘𝐴) / (log‘𝑝))) ∈ (ℤ≥‘1)
→ ((⌊‘((log‘𝐴) / (log‘𝑝))) + 1) ∈
(ℤ≥‘(1 + 1))) |
277 | 140, 276 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
((⌊‘((log‘𝐴) / (log‘𝑝))) + 1) ∈
(ℤ≥‘(1 + 1))) |
278 | | df-2 11079 |
. . . . . . . . . . . 12
⊢ 2 = (1 +
1) |
279 | 278 | fveq2i 6194 |
. . . . . . . . . . 11
⊢
(ℤ≥‘2) = (ℤ≥‘(1 +
1)) |
280 | 277, 279 | syl6eleqr 2712 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
((⌊‘((log‘𝐴) / (log‘𝑝))) + 1) ∈
(ℤ≥‘2)) |
281 | 216, 273,
275, 280 | geoserg 14598 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈
(2..^((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))((1 / 𝑝)↑𝑘) = ((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 /
𝑝)))) |
282 | 272, 281 | eqtrd 2656 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈
(2...(⌊‘((log‘𝐴) / (log‘𝑝))))((1 / 𝑝)↑𝑘) = ((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 /
𝑝)))) |
283 | 282 | oveq2d 6666 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) · Σ𝑘 ∈
(2...(⌊‘((log‘𝐴) / (log‘𝑝))))((1 / 𝑝)↑𝑘)) = ((log‘𝑝) · ((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 /
𝑝))))) |
284 | 265, 269,
283 | 3eqtr2d 2662 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈
(2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝↑𝑘)) = ((log‘𝑝) · ((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 /
𝑝))))) |
285 | 114 | nncnd 11036 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 · (𝑝 − 1)) ∈ ℂ) |
286 | 114 | nnne0d 11065 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 · (𝑝 − 1)) ≠ 0) |
287 | 128, 285,
286 | divrecd 10804 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) / (𝑝 · (𝑝 − 1))) = ((log‘𝑝) · (1 / (𝑝 · (𝑝 − 1))))) |
288 | 251, 284,
287 | 3brtr4d 4685 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈
(2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝↑𝑘)) ≤ ((log‘𝑝) / (𝑝 · (𝑝 − 1)))) |
289 | 201, 288 | eqbrtrd 4675 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) / (𝑝↑𝑘)) ≤ ((log‘𝑝) / (𝑝 · (𝑝 − 1)))) |
290 | 86, 108, 115, 289 | fsumle 14531 |
. . 3
⊢ (𝐴 ∈ ℤ →
Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)Σ𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) / (𝑝↑𝑘)) ≤ Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)((log‘𝑝) / (𝑝 · (𝑝 − 1)))) |
291 | | elfzuz 12338 |
. . . . . . . . . . 11
⊢ (𝑝 ∈ (2...((abs‘𝐴) + 1)) → 𝑝 ∈
(ℤ≥‘2)) |
292 | | eluz2nn 11726 |
. . . . . . . . . . 11
⊢ (𝑝 ∈
(ℤ≥‘2) → 𝑝 ∈ ℕ) |
293 | 291, 292 | syl 17 |
. . . . . . . . . 10
⊢ (𝑝 ∈ (2...((abs‘𝐴) + 1)) → 𝑝 ∈
ℕ) |
294 | 293 | adantl 482 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → 𝑝 ∈
ℕ) |
295 | 294 | nnred 11035 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → 𝑝 ∈
ℝ) |
296 | 291 | adantl 482 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → 𝑝 ∈
(ℤ≥‘2)) |
297 | | eluz2b2 11761 |
. . . . . . . . . 10
⊢ (𝑝 ∈
(ℤ≥‘2) ↔ (𝑝 ∈ ℕ ∧ 1 < 𝑝)) |
298 | 297 | simprbi 480 |
. . . . . . . . 9
⊢ (𝑝 ∈
(ℤ≥‘2) → 1 < 𝑝) |
299 | 296, 298 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → 1 < 𝑝) |
300 | 295, 299 | rplogcld 24375 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → (log‘𝑝) ∈
ℝ+) |
301 | 296, 112 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → (𝑝 − 1) ∈
ℕ) |
302 | 294, 301 | nnmulcld 11068 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → (𝑝 · (𝑝 − 1)) ∈ ℕ) |
303 | 302 | nnrpd 11870 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → (𝑝 · (𝑝 − 1)) ∈
ℝ+) |
304 | 300, 303 | rpdivcld 11889 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) →
((log‘𝑝) / (𝑝 · (𝑝 − 1))) ∈
ℝ+) |
305 | 304 | rpred 11872 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) →
((log‘𝑝) / (𝑝 · (𝑝 − 1))) ∈
ℝ) |
306 | 47, 305 | fsumrecl 14465 |
. . . 4
⊢ (𝐴 ∈ ℤ →
Σ𝑝 ∈
(2...((abs‘𝐴) +
1))((log‘𝑝) / (𝑝 · (𝑝 − 1))) ∈
ℝ) |
307 | 304 | rpge0d 11876 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → 0 ≤
((log‘𝑝) / (𝑝 · (𝑝 − 1)))) |
308 | 47, 305, 307, 84 | fsumless 14528 |
. . . 4
⊢ (𝐴 ∈ ℤ →
Σ𝑝 ∈ ((0[,]𝐴) ∩
ℙ)((log‘𝑝) /
(𝑝 · (𝑝 − 1))) ≤ Σ𝑝 ∈ (2...((abs‘𝐴) + 1))((log‘𝑝) / (𝑝 · (𝑝 − 1)))) |
309 | | rplogsumlem1 25173 |
. . . . 5
⊢
(((abs‘𝐴) + 1)
∈ ℕ → Σ𝑝 ∈ (2...((abs‘𝐴) + 1))((log‘𝑝) / (𝑝 · (𝑝 − 1))) ≤ 2) |
310 | 77, 309 | syl 17 |
. . . 4
⊢ (𝐴 ∈ ℤ →
Σ𝑝 ∈
(2...((abs‘𝐴) +
1))((log‘𝑝) / (𝑝 · (𝑝 − 1))) ≤ 2) |
311 | 116, 306,
118, 308, 310 | letrd 10194 |
. . 3
⊢ (𝐴 ∈ ℤ →
Σ𝑝 ∈ ((0[,]𝐴) ∩
ℙ)((log‘𝑝) /
(𝑝 · (𝑝 − 1))) ≤
2) |
312 | 109, 116,
118, 290, 311 | letrd 10194 |
. 2
⊢ (𝐴 ∈ ℤ →
Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)Σ𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) / (𝑝↑𝑘)) ≤ 2) |
313 | 46, 312 | eqbrtrd 4675 |
1
⊢ (𝐴 ∈ ℤ →
Σ𝑛 ∈ (1...𝐴)(((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) ≤ 2) |