| Step | Hyp | Ref
| Expression |
| 1 | | flid 13848 |
. . . . 5
⊢ (𝐴 ∈ ℤ →
(⌊‘𝐴) = 𝐴) |
| 2 | 1 | oveq2d 7447 |
. . . 4
⊢ (𝐴 ∈ ℤ →
(1...(⌊‘𝐴)) =
(1...𝐴)) |
| 3 | 2 | sumeq1d 15736 |
. . 3
⊢ (𝐴 ∈ ℤ →
Σ𝑛 ∈
(1...(⌊‘𝐴))(((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) = Σ𝑛 ∈ (1...𝐴)(((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛)) |
| 4 | | fveq2 6906 |
. . . . . 6
⊢ (𝑛 = (𝑝↑𝑘) → (Λ‘𝑛) = (Λ‘(𝑝↑𝑘))) |
| 5 | | eleq1 2829 |
. . . . . . 7
⊢ (𝑛 = (𝑝↑𝑘) → (𝑛 ∈ ℙ ↔ (𝑝↑𝑘) ∈ ℙ)) |
| 6 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑛 = (𝑝↑𝑘) → (log‘𝑛) = (log‘(𝑝↑𝑘))) |
| 7 | 5, 6 | ifbieq1d 4550 |
. . . . . 6
⊢ (𝑛 = (𝑝↑𝑘) → if(𝑛 ∈ ℙ, (log‘𝑛), 0) = if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) |
| 8 | 4, 7 | oveq12d 7449 |
. . . . 5
⊢ (𝑛 = (𝑝↑𝑘) → ((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) = ((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0))) |
| 9 | | id 22 |
. . . . 5
⊢ (𝑛 = (𝑝↑𝑘) → 𝑛 = (𝑝↑𝑘)) |
| 10 | 8, 9 | oveq12d 7449 |
. . . 4
⊢ (𝑛 = (𝑝↑𝑘) → (((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) = (((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) / (𝑝↑𝑘))) |
| 11 | | zre 12617 |
. . . 4
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℝ) |
| 12 | | elfznn 13593 |
. . . . . . . . 9
⊢ (𝑛 ∈
(1...(⌊‘𝐴))
→ 𝑛 ∈
ℕ) |
| 13 | 12 | adantl 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ 𝑛 ∈
ℕ) |
| 14 | | vmacl 27161 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ →
(Λ‘𝑛) ∈
ℝ) |
| 15 | 13, 14 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ (Λ‘𝑛)
∈ ℝ) |
| 16 | 13 | nnrpd 13075 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ 𝑛 ∈
ℝ+) |
| 17 | 16 | relogcld 26665 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ (log‘𝑛) ∈
ℝ) |
| 18 | | 0re 11263 |
. . . . . . . 8
⊢ 0 ∈
ℝ |
| 19 | | ifcl 4571 |
. . . . . . . 8
⊢
(((log‘𝑛)
∈ ℝ ∧ 0 ∈ ℝ) → if(𝑛 ∈ ℙ, (log‘𝑛), 0) ∈
ℝ) |
| 20 | 17, 18, 19 | sylancl 586 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ if(𝑛 ∈ ℙ,
(log‘𝑛), 0) ∈
ℝ) |
| 21 | 15, 20 | resubcld 11691 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ ((Λ‘𝑛)
− if(𝑛 ∈
ℙ, (log‘𝑛), 0))
∈ ℝ) |
| 22 | 21, 13 | nndivred 12320 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ (((Λ‘𝑛)
− if(𝑛 ∈
ℙ, (log‘𝑛), 0))
/ 𝑛) ∈
ℝ) |
| 23 | 22 | recnd 11289 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ (((Λ‘𝑛)
− if(𝑛 ∈
ℙ, (log‘𝑛), 0))
/ 𝑛) ∈
ℂ) |
| 24 | | simprr 773 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ (𝑛 ∈
(1...(⌊‘𝐴))
∧ (Λ‘𝑛) =
0)) → (Λ‘𝑛) = 0) |
| 25 | | vmaprm 27160 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℙ →
(Λ‘𝑛) =
(log‘𝑛)) |
| 26 | | prmnn 16711 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℙ → 𝑛 ∈
ℕ) |
| 27 | 26 | nnred 12281 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℙ → 𝑛 ∈
ℝ) |
| 28 | | prmgt1 16734 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℙ → 1 <
𝑛) |
| 29 | 27, 28 | rplogcld 26671 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℙ →
(log‘𝑛) ∈
ℝ+) |
| 30 | 25, 29 | eqeltrd 2841 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℙ →
(Λ‘𝑛) ∈
ℝ+) |
| 31 | 30 | rpne0d 13082 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℙ →
(Λ‘𝑛) ≠
0) |
| 32 | 31 | necon2bi 2971 |
. . . . . . . . . 10
⊢
((Λ‘𝑛)
= 0 → ¬ 𝑛 ∈
ℙ) |
| 33 | 32 | ad2antll 729 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ (𝑛 ∈
(1...(⌊‘𝐴))
∧ (Λ‘𝑛) =
0)) → ¬ 𝑛 ∈
ℙ) |
| 34 | 33 | iffalsed 4536 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ (𝑛 ∈
(1...(⌊‘𝐴))
∧ (Λ‘𝑛) =
0)) → if(𝑛 ∈
ℙ, (log‘𝑛), 0)
= 0) |
| 35 | 24, 34 | oveq12d 7449 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ (𝑛 ∈
(1...(⌊‘𝐴))
∧ (Λ‘𝑛) =
0)) → ((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) = (0 −
0)) |
| 36 | | 0m0e0 12386 |
. . . . . . 7
⊢ (0
− 0) = 0 |
| 37 | 35, 36 | eqtrdi 2793 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ (𝑛 ∈
(1...(⌊‘𝐴))
∧ (Λ‘𝑛) =
0)) → ((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) = 0) |
| 38 | 37 | oveq1d 7446 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ (𝑛 ∈
(1...(⌊‘𝐴))
∧ (Λ‘𝑛) =
0)) → (((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) = (0 / 𝑛)) |
| 39 | 12 | ad2antrl 728 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ (𝑛 ∈
(1...(⌊‘𝐴))
∧ (Λ‘𝑛) =
0)) → 𝑛 ∈
ℕ) |
| 40 | 39 | nnrpd 13075 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ (𝑛 ∈
(1...(⌊‘𝐴))
∧ (Λ‘𝑛) =
0)) → 𝑛 ∈
ℝ+) |
| 41 | 40 | rpcnne0d 13086 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ (𝑛 ∈
(1...(⌊‘𝐴))
∧ (Λ‘𝑛) =
0)) → (𝑛 ∈
ℂ ∧ 𝑛 ≠
0)) |
| 42 | | div0 11955 |
. . . . . 6
⊢ ((𝑛 ∈ ℂ ∧ 𝑛 ≠ 0) → (0 / 𝑛) = 0) |
| 43 | 41, 42 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ (𝑛 ∈
(1...(⌊‘𝐴))
∧ (Λ‘𝑛) =
0)) → (0 / 𝑛) =
0) |
| 44 | 38, 43 | eqtrd 2777 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ (𝑛 ∈
(1...(⌊‘𝐴))
∧ (Λ‘𝑛) =
0)) → (((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) = 0) |
| 45 | 10, 11, 23, 44 | fsumvma2 27258 |
. . 3
⊢ (𝐴 ∈ ℤ →
Σ𝑛 ∈
(1...(⌊‘𝐴))(((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) / (𝑝↑𝑘))) |
| 46 | 3, 45 | eqtr3d 2779 |
. 2
⊢ (𝐴 ∈ ℤ →
Σ𝑛 ∈ (1...𝐴)(((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) / (𝑝↑𝑘))) |
| 47 | | fzfid 14014 |
. . . . 5
⊢ (𝐴 ∈ ℤ →
(2...((abs‘𝐴) + 1))
∈ Fin) |
| 48 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) |
| 49 | 48 | elin2d 4205 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℙ) |
| 50 | | prmnn 16711 |
. . . . . . . . . . 11
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) |
| 51 | 49, 50 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℕ) |
| 52 | 51 | nnred 12281 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℝ) |
| 53 | 11 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝐴 ∈ ℝ) |
| 54 | | zcn 12618 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
ℂ) |
| 55 | 54 | abscld 15475 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℤ →
(abs‘𝐴) ∈
ℝ) |
| 56 | | peano2re 11434 |
. . . . . . . . . . 11
⊢
((abs‘𝐴)
∈ ℝ → ((abs‘𝐴) + 1) ∈ ℝ) |
| 57 | 55, 56 | syl 17 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℤ →
((abs‘𝐴) + 1) ∈
ℝ) |
| 58 | 57 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((abs‘𝐴) + 1) ∈
ℝ) |
| 59 | | elinel1 4201 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) → 𝑝 ∈ (0[,]𝐴)) |
| 60 | | elicc2 13452 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (𝑝
∈ (0[,]𝐴) ↔
(𝑝 ∈ ℝ ∧ 0
≤ 𝑝 ∧ 𝑝 ≤ 𝐴))) |
| 61 | 18, 11, 60 | sylancr 587 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℤ → (𝑝 ∈ (0[,]𝐴) ↔ (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴))) |
| 62 | 59, 61 | imbitrid 244 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℤ → (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) → (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴))) |
| 63 | 62 | imp 406 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴)) |
| 64 | 63 | simp3d 1145 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ≤ 𝐴) |
| 65 | 54 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝐴 ∈ ℂ) |
| 66 | 65 | abscld 15475 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (abs‘𝐴) ∈
ℝ) |
| 67 | 53 | leabsd 15453 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝐴 ≤ (abs‘𝐴)) |
| 68 | 66 | lep1d 12199 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (abs‘𝐴) ≤ ((abs‘𝐴) + 1)) |
| 69 | 53, 66, 58, 67, 68 | letrd 11418 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝐴 ≤ ((abs‘𝐴) + 1)) |
| 70 | 52, 53, 58, 64, 69 | letrd 11418 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ≤ ((abs‘𝐴) + 1)) |
| 71 | | prmuz2 16733 |
. . . . . . . . . 10
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
(ℤ≥‘2)) |
| 72 | 49, 71 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈
(ℤ≥‘2)) |
| 73 | | nn0abscl 15351 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℤ →
(abs‘𝐴) ∈
ℕ0) |
| 74 | | nn0p1nn 12565 |
. . . . . . . . . . . 12
⊢
((abs‘𝐴)
∈ ℕ0 → ((abs‘𝐴) + 1) ∈ ℕ) |
| 75 | 73, 74 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℤ →
((abs‘𝐴) + 1) ∈
ℕ) |
| 76 | 75 | nnzd 12640 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℤ →
((abs‘𝐴) + 1) ∈
ℤ) |
| 77 | 76 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((abs‘𝐴) + 1) ∈
ℤ) |
| 78 | | elfz5 13556 |
. . . . . . . . 9
⊢ ((𝑝 ∈
(ℤ≥‘2) ∧ ((abs‘𝐴) + 1) ∈ ℤ) → (𝑝 ∈ (2...((abs‘𝐴) + 1)) ↔ 𝑝 ≤ ((abs‘𝐴) + 1))) |
| 79 | 72, 77, 78 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 ∈ (2...((abs‘𝐴) + 1)) ↔ 𝑝 ≤ ((abs‘𝐴) + 1))) |
| 80 | 70, 79 | mpbird 257 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ (2...((abs‘𝐴) + 1))) |
| 81 | 80 | ex 412 |
. . . . . 6
⊢ (𝐴 ∈ ℤ → (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) → 𝑝 ∈ (2...((abs‘𝐴) + 1)))) |
| 82 | 81 | ssrdv 3989 |
. . . . 5
⊢ (𝐴 ∈ ℤ →
((0[,]𝐴) ∩ ℙ)
⊆ (2...((abs‘𝐴)
+ 1))) |
| 83 | 47, 82 | ssfid 9301 |
. . . 4
⊢ (𝐴 ∈ ℤ →
((0[,]𝐴) ∩ ℙ)
∈ Fin) |
| 84 | | fzfid 14014 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(1...(⌊‘((log‘𝐴) / (log‘𝑝)))) ∈ Fin) |
| 85 | | simprl 771 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) |
| 86 | 85 | elin2d 4205 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → 𝑝 ∈ ℙ) |
| 87 | | elfznn 13593 |
. . . . . . . . . . 11
⊢ (𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝)))) → 𝑘 ∈ ℕ) |
| 88 | 87 | ad2antll 729 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → 𝑘 ∈ ℕ) |
| 89 | | vmappw 27159 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) →
(Λ‘(𝑝↑𝑘)) = (log‘𝑝)) |
| 90 | 86, 88, 89 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) →
(Λ‘(𝑝↑𝑘)) = (log‘𝑝)) |
| 91 | 51 | adantrr 717 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → 𝑝 ∈ ℕ) |
| 92 | 91 | nnrpd 13075 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → 𝑝 ∈ ℝ+) |
| 93 | 92 | relogcld 26665 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → (log‘𝑝) ∈
ℝ) |
| 94 | 90, 93 | eqeltrd 2841 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) →
(Λ‘(𝑝↑𝑘)) ∈ ℝ) |
| 95 | 88 | nnnn0d 12587 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → 𝑘 ∈ ℕ0) |
| 96 | | nnexpcl 14115 |
. . . . . . . . . . . 12
⊢ ((𝑝 ∈ ℕ ∧ 𝑘 ∈ ℕ0)
→ (𝑝↑𝑘) ∈
ℕ) |
| 97 | 91, 95, 96 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → (𝑝↑𝑘) ∈ ℕ) |
| 98 | 97 | nnrpd 13075 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → (𝑝↑𝑘) ∈
ℝ+) |
| 99 | 98 | relogcld 26665 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → (log‘(𝑝↑𝑘)) ∈ ℝ) |
| 100 | | ifcl 4571 |
. . . . . . . . 9
⊢
(((log‘(𝑝↑𝑘)) ∈ ℝ ∧ 0 ∈ ℝ)
→ if((𝑝↑𝑘) ∈ ℙ,
(log‘(𝑝↑𝑘)), 0) ∈
ℝ) |
| 101 | 99, 18, 100 | sylancl 586 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0) ∈ ℝ) |
| 102 | 94, 101 | resubcld 11691 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) →
((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) ∈ ℝ) |
| 103 | 102, 97 | nndivred 12320 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) →
(((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) / (𝑝↑𝑘)) ∈ ℝ) |
| 104 | 103 | anassrs 467 |
. . . . 5
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) →
(((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) / (𝑝↑𝑘)) ∈ ℝ) |
| 105 | 84, 104 | fsumrecl 15770 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) / (𝑝↑𝑘)) ∈ ℝ) |
| 106 | 83, 105 | fsumrecl 15770 |
. . 3
⊢ (𝐴 ∈ ℤ →
Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)Σ𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) / (𝑝↑𝑘)) ∈ ℝ) |
| 107 | 51 | nnrpd 13075 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℝ+) |
| 108 | 107 | relogcld 26665 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈
ℝ) |
| 109 | | uz2m1nn 12965 |
. . . . . . 7
⊢ (𝑝 ∈
(ℤ≥‘2) → (𝑝 − 1) ∈ ℕ) |
| 110 | 72, 109 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 − 1) ∈ ℕ) |
| 111 | 51, 110 | nnmulcld 12319 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 · (𝑝 − 1)) ∈ ℕ) |
| 112 | 108, 111 | nndivred 12320 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) / (𝑝 · (𝑝 − 1))) ∈
ℝ) |
| 113 | 83, 112 | fsumrecl 15770 |
. . 3
⊢ (𝐴 ∈ ℤ →
Σ𝑝 ∈ ((0[,]𝐴) ∩
ℙ)((log‘𝑝) /
(𝑝 · (𝑝 − 1))) ∈
ℝ) |
| 114 | | 2re 12340 |
. . . 4
⊢ 2 ∈
ℝ |
| 115 | 114 | a1i 11 |
. . 3
⊢ (𝐴 ∈ ℤ → 2 ∈
ℝ) |
| 116 | 18 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 0 ∈
ℝ) |
| 117 | 51 | nngt0d 12315 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 0 < 𝑝) |
| 118 | 116, 52, 53, 117, 64 | ltletrd 11421 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 0 < 𝐴) |
| 119 | 53, 118 | elrpd 13074 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝐴 ∈
ℝ+) |
| 120 | 119 | relogcld 26665 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝐴) ∈
ℝ) |
| 121 | | prmgt1 16734 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈ ℙ → 1 <
𝑝) |
| 122 | 49, 121 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 1 < 𝑝) |
| 123 | 52, 122 | rplogcld 26671 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈
ℝ+) |
| 124 | 120, 123 | rerpdivcld 13108 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝐴) / (log‘𝑝)) ∈
ℝ) |
| 125 | 123 | rpcnd 13079 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈
ℂ) |
| 126 | 125 | mullidd 11279 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 ·
(log‘𝑝)) =
(log‘𝑝)) |
| 127 | 107, 119 | logled 26669 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 ≤ 𝐴 ↔ (log‘𝑝) ≤ (log‘𝐴))) |
| 128 | 64, 127 | mpbid 232 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ≤ (log‘𝐴)) |
| 129 | 126, 128 | eqbrtrd 5165 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 ·
(log‘𝑝)) ≤
(log‘𝐴)) |
| 130 | | 1re 11261 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ |
| 131 | 130 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 1 ∈
ℝ) |
| 132 | 131, 120,
123 | lemuldivd 13126 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 ·
(log‘𝑝)) ≤
(log‘𝐴) ↔ 1 ≤
((log‘𝐴) /
(log‘𝑝)))) |
| 133 | 129, 132 | mpbid 232 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 1 ≤
((log‘𝐴) /
(log‘𝑝))) |
| 134 | | flge1nn 13861 |
. . . . . . . . 9
⊢
((((log‘𝐴) /
(log‘𝑝)) ∈
ℝ ∧ 1 ≤ ((log‘𝐴) / (log‘𝑝))) → (⌊‘((log‘𝐴) / (log‘𝑝))) ∈
ℕ) |
| 135 | 124, 133,
134 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℕ) |
| 136 | | nnuz 12921 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
| 137 | 135, 136 | eleqtrdi 2851 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(⌊‘((log‘𝐴) / (log‘𝑝))) ∈
(ℤ≥‘1)) |
| 138 | 103 | recnd 11289 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) →
(((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) / (𝑝↑𝑘)) ∈ ℂ) |
| 139 | 138 | anassrs 467 |
. . . . . . 7
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) →
(((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) / (𝑝↑𝑘)) ∈ ℂ) |
| 140 | | oveq2 7439 |
. . . . . . . . . 10
⊢ (𝑘 = 1 → (𝑝↑𝑘) = (𝑝↑1)) |
| 141 | 140 | fveq2d 6910 |
. . . . . . . . 9
⊢ (𝑘 = 1 →
(Λ‘(𝑝↑𝑘)) = (Λ‘(𝑝↑1))) |
| 142 | 140 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (𝑘 = 1 → ((𝑝↑𝑘) ∈ ℙ ↔ (𝑝↑1) ∈ ℙ)) |
| 143 | 140 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝑘 = 1 → (log‘(𝑝↑𝑘)) = (log‘(𝑝↑1))) |
| 144 | 142, 143 | ifbieq1d 4550 |
. . . . . . . . 9
⊢ (𝑘 = 1 → if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0) = if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0)) |
| 145 | 141, 144 | oveq12d 7449 |
. . . . . . . 8
⊢ (𝑘 = 1 →
((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) = ((Λ‘(𝑝↑1)) − if((𝑝↑1) ∈ ℙ,
(log‘(𝑝↑1)),
0))) |
| 146 | 145, 140 | oveq12d 7449 |
. . . . . . 7
⊢ (𝑘 = 1 →
(((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) / (𝑝↑𝑘)) = (((Λ‘(𝑝↑1)) − if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0)) / (𝑝↑1))) |
| 147 | 137, 139,
146 | fsum1p 15789 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) / (𝑝↑𝑘)) = ((((Λ‘(𝑝↑1)) − if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0)) / (𝑝↑1)) + Σ𝑘 ∈ ((1 +
1)...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) / (𝑝↑𝑘)))) |
| 148 | 51 | nncnd 12282 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℂ) |
| 149 | 148 | exp1d 14181 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝↑1) = 𝑝) |
| 150 | 149 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(Λ‘(𝑝↑1))
= (Λ‘𝑝)) |
| 151 | | vmaprm 27160 |
. . . . . . . . . . . . 13
⊢ (𝑝 ∈ ℙ →
(Λ‘𝑝) =
(log‘𝑝)) |
| 152 | 49, 151 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(Λ‘𝑝) =
(log‘𝑝)) |
| 153 | 150, 152 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(Λ‘(𝑝↑1))
= (log‘𝑝)) |
| 154 | 149, 49 | eqeltrd 2841 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝↑1) ∈ ℙ) |
| 155 | 154 | iftrued 4533 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → if((𝑝↑1) ∈ ℙ,
(log‘(𝑝↑1)), 0)
= (log‘(𝑝↑1))) |
| 156 | 149 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘(𝑝↑1)) = (log‘𝑝)) |
| 157 | 155, 156 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → if((𝑝↑1) ∈ ℙ,
(log‘(𝑝↑1)), 0)
= (log‘𝑝)) |
| 158 | 153, 157 | oveq12d 7449 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
((Λ‘(𝑝↑1)) − if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0)) =
((log‘𝑝) −
(log‘𝑝))) |
| 159 | 125 | subidd 11608 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) − (log‘𝑝)) = 0) |
| 160 | 158, 159 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
((Λ‘(𝑝↑1)) − if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0)) =
0) |
| 161 | 160, 149 | oveq12d 7449 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(((Λ‘(𝑝↑1)) − if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0)) / (𝑝↑1)) = (0 / 𝑝)) |
| 162 | 107 | rpcnne0d 13086 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 ∈ ℂ ∧ 𝑝 ≠ 0)) |
| 163 | | div0 11955 |
. . . . . . . . 9
⊢ ((𝑝 ∈ ℂ ∧ 𝑝 ≠ 0) → (0 / 𝑝) = 0) |
| 164 | 162, 163 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (0 / 𝑝) = 0) |
| 165 | 161, 164 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(((Λ‘(𝑝↑1)) − if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0)) / (𝑝↑1)) = 0) |
| 166 | | 1p1e2 12391 |
. . . . . . . . . 10
⊢ (1 + 1) =
2 |
| 167 | 166 | oveq1i 7441 |
. . . . . . . . 9
⊢ ((1 +
1)...(⌊‘((log‘𝐴) / (log‘𝑝)))) = (2...(⌊‘((log‘𝐴) / (log‘𝑝)))) |
| 168 | 167 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 +
1)...(⌊‘((log‘𝐴) / (log‘𝑝)))) = (2...(⌊‘((log‘𝐴) / (log‘𝑝))))) |
| 169 | | elfzuz 13560 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈
(2...(⌊‘((log‘𝐴) / (log‘𝑝)))) → 𝑘 ∈
(ℤ≥‘2)) |
| 170 | | eluz2nn 12924 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈
(ℤ≥‘2) → 𝑘 ∈ ℕ) |
| 171 | 169, 170 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈
(2...(⌊‘((log‘𝐴) / (log‘𝑝)))) → 𝑘 ∈ ℕ) |
| 172 | 171, 167 | eleq2s 2859 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ((1 +
1)...(⌊‘((log‘𝐴) / (log‘𝑝)))) → 𝑘 ∈ ℕ) |
| 173 | 49, 172, 89 | syl2an 596 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 +
1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → (Λ‘(𝑝↑𝑘)) = (log‘𝑝)) |
| 174 | 51 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 +
1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → 𝑝 ∈ ℕ) |
| 175 | | nnq 13004 |
. . . . . . . . . . . . . 14
⊢ (𝑝 ∈ ℕ → 𝑝 ∈
ℚ) |
| 176 | 174, 175 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 +
1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → 𝑝 ∈ ℚ) |
| 177 | 169, 167 | eleq2s 2859 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ((1 +
1)...(⌊‘((log‘𝐴) / (log‘𝑝)))) → 𝑘 ∈
(ℤ≥‘2)) |
| 178 | 177 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 +
1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → 𝑘 ∈
(ℤ≥‘2)) |
| 179 | | expnprm 16940 |
. . . . . . . . . . . . 13
⊢ ((𝑝 ∈ ℚ ∧ 𝑘 ∈
(ℤ≥‘2)) → ¬ (𝑝↑𝑘) ∈ ℙ) |
| 180 | 176, 178,
179 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 +
1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → ¬ (𝑝↑𝑘) ∈ ℙ) |
| 181 | 180 | iffalsed 4536 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 +
1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0) = 0) |
| 182 | 173, 181 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 +
1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → ((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) = ((log‘𝑝) − 0)) |
| 183 | 125 | subid1d 11609 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) − 0) = (log‘𝑝)) |
| 184 | 183 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 +
1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → ((log‘𝑝) − 0) = (log‘𝑝)) |
| 185 | 182, 184 | eqtrd 2777 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 +
1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → ((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) = (log‘𝑝)) |
| 186 | 185 | oveq1d 7446 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 +
1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → (((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) / (𝑝↑𝑘)) = ((log‘𝑝) / (𝑝↑𝑘))) |
| 187 | 168, 186 | sumeq12dv 15742 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈ ((1 +
1)...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) / (𝑝↑𝑘)) = Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝↑𝑘))) |
| 188 | 165, 187 | oveq12d 7449 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
((((Λ‘(𝑝↑1)) − if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0)) / (𝑝↑1)) + Σ𝑘 ∈ ((1 +
1)...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) / (𝑝↑𝑘))) = (0 + Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝↑𝑘)))) |
| 189 | | fzfid 14014 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(2...(⌊‘((log‘𝐴) / (log‘𝑝)))) ∈ Fin) |
| 190 | 108 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → (log‘𝑝) ∈
ℝ) |
| 191 | | nnnn0 12533 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) |
| 192 | 51, 191, 96 | syl2an 596 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → (𝑝↑𝑘) ∈ ℕ) |
| 193 | 190, 192 | nndivred 12320 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → ((log‘𝑝) / (𝑝↑𝑘)) ∈ ℝ) |
| 194 | 171, 193 | sylan2 593 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))) → ((log‘𝑝) / (𝑝↑𝑘)) ∈ ℝ) |
| 195 | 189, 194 | fsumrecl 15770 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈
(2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝↑𝑘)) ∈ ℝ) |
| 196 | 195 | recnd 11289 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈
(2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝↑𝑘)) ∈ ℂ) |
| 197 | 196 | addlidd 11462 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (0 + Σ𝑘 ∈
(2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝↑𝑘))) = Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝↑𝑘))) |
| 198 | 147, 188,
197 | 3eqtrd 2781 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) / (𝑝↑𝑘)) = Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝↑𝑘))) |
| 199 | 107 | rpreccld 13087 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 / 𝑝) ∈
ℝ+) |
| 200 | 124 | flcld 13838 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℤ) |
| 201 | 200 | peano2zd 12725 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
((⌊‘((log‘𝐴) / (log‘𝑝))) + 1) ∈ ℤ) |
| 202 | 199, 201 | rpexpcld 14286 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1)) ∈
ℝ+) |
| 203 | 202 | rpge0d 13081 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 0 ≤ ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) |
| 204 | 51 | nnrecred 12317 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 / 𝑝) ∈
ℝ) |
| 205 | 204 | resqcld 14165 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 / 𝑝)↑2) ∈
ℝ) |
| 206 | 135 | peano2nnd 12283 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
((⌊‘((log‘𝐴) / (log‘𝑝))) + 1) ∈ ℕ) |
| 207 | 206 | nnnn0d 12587 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
((⌊‘((log‘𝐴) / (log‘𝑝))) + 1) ∈
ℕ0) |
| 208 | 204, 207 | reexpcld 14203 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1)) ∈
ℝ) |
| 209 | 205, 208 | subge02d 11855 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (0 ≤ ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1)) ↔ (((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) ≤ ((1 / 𝑝)↑2))) |
| 210 | 203, 209 | mpbid 232 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) ≤ ((1 / 𝑝)↑2)) |
| 211 | 110 | nnrpd 13075 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 − 1) ∈
ℝ+) |
| 212 | 211 | rpcnne0d 13086 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((𝑝 − 1) ∈ ℂ ∧
(𝑝 − 1) ≠
0)) |
| 213 | 199 | rpcnd 13079 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 / 𝑝) ∈
ℂ) |
| 214 | | dmdcan 11977 |
. . . . . . . . . . 11
⊢ ((((𝑝 − 1) ∈ ℂ ∧
(𝑝 − 1) ≠ 0) ∧
(𝑝 ∈ ℂ ∧
𝑝 ≠ 0) ∧ (1 / 𝑝) ∈ ℂ) →
(((𝑝 − 1) / 𝑝) · ((1 / 𝑝) / (𝑝 − 1))) = ((1 / 𝑝) / 𝑝)) |
| 215 | 212, 162,
213, 214 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((𝑝 − 1) / 𝑝) · ((1 / 𝑝) / (𝑝 − 1))) = ((1 / 𝑝) / 𝑝)) |
| 216 | 131 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 1 ∈
ℂ) |
| 217 | | divsubdir 11961 |
. . . . . . . . . . . . 13
⊢ ((𝑝 ∈ ℂ ∧ 1 ∈
ℂ ∧ (𝑝 ∈
ℂ ∧ 𝑝 ≠ 0))
→ ((𝑝 − 1) /
𝑝) = ((𝑝 / 𝑝) − (1 / 𝑝))) |
| 218 | 148, 216,
162, 217 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((𝑝 − 1) / 𝑝) = ((𝑝 / 𝑝) − (1 / 𝑝))) |
| 219 | | divid 11953 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 ∈ ℂ ∧ 𝑝 ≠ 0) → (𝑝 / 𝑝) = 1) |
| 220 | 162, 219 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 / 𝑝) = 1) |
| 221 | 220 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((𝑝 / 𝑝) − (1 / 𝑝)) = (1 − (1 / 𝑝))) |
| 222 | 218, 221 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((𝑝 − 1) / 𝑝) = (1 − (1 / 𝑝))) |
| 223 | | divdiv1 11978 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℂ ∧ (𝑝
∈ ℂ ∧ 𝑝 ≠
0) ∧ ((𝑝 − 1)
∈ ℂ ∧ (𝑝
− 1) ≠ 0)) → ((1 / 𝑝) / (𝑝 − 1)) = (1 / (𝑝 · (𝑝 − 1)))) |
| 224 | 216, 162,
212, 223 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 / 𝑝) / (𝑝 − 1)) = (1 / (𝑝 · (𝑝 − 1)))) |
| 225 | 222, 224 | oveq12d 7449 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((𝑝 − 1) / 𝑝) · ((1 / 𝑝) / (𝑝 − 1))) = ((1 − (1 / 𝑝)) · (1 / (𝑝 · (𝑝 − 1))))) |
| 226 | 51 | nnne0d 12316 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ≠ 0) |
| 227 | 213, 148,
226 | divrecd 12046 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 / 𝑝) / 𝑝) = ((1 / 𝑝) · (1 / 𝑝))) |
| 228 | 213 | sqvald 14183 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 / 𝑝)↑2) = ((1 / 𝑝) · (1 / 𝑝))) |
| 229 | 227, 228 | eqtr4d 2780 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 / 𝑝) / 𝑝) = ((1 / 𝑝)↑2)) |
| 230 | 215, 225,
229 | 3eqtr3d 2785 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 − (1 /
𝑝)) · (1 / (𝑝 · (𝑝 − 1)))) = ((1 / 𝑝)↑2)) |
| 231 | 210, 230 | breqtrrd 5171 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) ≤ ((1 − (1 /
𝑝)) · (1 / (𝑝 · (𝑝 − 1))))) |
| 232 | 205, 208 | resubcld 11691 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) ∈
ℝ) |
| 233 | 111 | nnrecred 12317 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 / (𝑝 · (𝑝 − 1))) ∈
ℝ) |
| 234 | | resubcl 11573 |
. . . . . . . . . 10
⊢ ((1
∈ ℝ ∧ (1 / 𝑝) ∈ ℝ) → (1 − (1 /
𝑝)) ∈
ℝ) |
| 235 | 130, 204,
234 | sylancr 587 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 − (1 /
𝑝)) ∈
ℝ) |
| 236 | | recgt1 12164 |
. . . . . . . . . . . 12
⊢ ((𝑝 ∈ ℝ ∧ 0 <
𝑝) → (1 < 𝑝 ↔ (1 / 𝑝) < 1)) |
| 237 | 52, 117, 236 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 < 𝑝 ↔ (1 / 𝑝) < 1)) |
| 238 | 122, 237 | mpbid 232 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 / 𝑝) < 1) |
| 239 | | posdif 11756 |
. . . . . . . . . . 11
⊢ (((1 /
𝑝) ∈ ℝ ∧ 1
∈ ℝ) → ((1 / 𝑝) < 1 ↔ 0 < (1 − (1 / 𝑝)))) |
| 240 | 204, 130,
239 | sylancl 586 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 / 𝑝) < 1 ↔ 0 < (1
− (1 / 𝑝)))) |
| 241 | 238, 240 | mpbid 232 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 0 < (1 −
(1 / 𝑝))) |
| 242 | | ledivmul 12144 |
. . . . . . . . 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)))))) |
| 243 | 232, 233,
235, 241, 242 | syl112anc 1376 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 /
𝑝))) ≤ (1 / (𝑝 · (𝑝 − 1))) ↔ (((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) ≤ ((1 − (1 /
𝑝)) · (1 / (𝑝 · (𝑝 − 1)))))) |
| 244 | 231, 243 | mpbird 257 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 /
𝑝))) ≤ (1 / (𝑝 · (𝑝 − 1)))) |
| 245 | 235, 241 | elrpd 13074 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 − (1 /
𝑝)) ∈
ℝ+) |
| 246 | 232, 245 | rerpdivcld 13108 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 /
𝑝))) ∈
ℝ) |
| 247 | 246, 233,
123 | lemul2d 13121 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 /
𝑝))) ≤ (1 / (𝑝 · (𝑝 − 1))) ↔ ((log‘𝑝) · ((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 /
𝑝)))) ≤
((log‘𝑝) · (1
/ (𝑝 · (𝑝 −
1)))))) |
| 248 | 244, 247 | mpbid 232 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) · ((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 /
𝑝)))) ≤
((log‘𝑝) · (1
/ (𝑝 · (𝑝 − 1))))) |
| 249 | 125 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → (log‘𝑝) ∈
ℂ) |
| 250 | 192 | nncnd 12282 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → (𝑝↑𝑘) ∈ ℂ) |
| 251 | 192 | nnne0d 12316 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → (𝑝↑𝑘) ≠ 0) |
| 252 | 249, 250,
251 | divrecd 12046 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → ((log‘𝑝) / (𝑝↑𝑘)) = ((log‘𝑝) · (1 / (𝑝↑𝑘)))) |
| 253 | 148 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → 𝑝 ∈ ℂ) |
| 254 | 51 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → 𝑝 ∈ ℕ) |
| 255 | 254 | nnne0d 12316 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → 𝑝 ≠ 0) |
| 256 | | nnz 12634 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℤ) |
| 257 | 256 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℤ) |
| 258 | 253, 255,
257 | exprecd 14194 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → ((1 / 𝑝)↑𝑘) = (1 / (𝑝↑𝑘))) |
| 259 | 258 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → ((log‘𝑝) · ((1 / 𝑝)↑𝑘)) = ((log‘𝑝) · (1 / (𝑝↑𝑘)))) |
| 260 | 252, 259 | eqtr4d 2780 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → ((log‘𝑝) / (𝑝↑𝑘)) = ((log‘𝑝) · ((1 / 𝑝)↑𝑘))) |
| 261 | 171, 260 | sylan2 593 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))) → ((log‘𝑝) / (𝑝↑𝑘)) = ((log‘𝑝) · ((1 / 𝑝)↑𝑘))) |
| 262 | 261 | sumeq2dv 15738 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈
(2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝↑𝑘)) = Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) · ((1 / 𝑝)↑𝑘))) |
| 263 | 171 | nnnn0d 12587 |
. . . . . . . . 9
⊢ (𝑘 ∈
(2...(⌊‘((log‘𝐴) / (log‘𝑝)))) → 𝑘 ∈ ℕ0) |
| 264 | | expcl 14120 |
. . . . . . . . 9
⊢ (((1 /
𝑝) ∈ ℂ ∧
𝑘 ∈
ℕ0) → ((1 / 𝑝)↑𝑘) ∈ ℂ) |
| 265 | 213, 263,
264 | syl2an 596 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))) → ((1 / 𝑝)↑𝑘) ∈ ℂ) |
| 266 | 189, 125,
265 | fsummulc2 15820 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) · Σ𝑘 ∈
(2...(⌊‘((log‘𝐴) / (log‘𝑝))))((1 / 𝑝)↑𝑘)) = Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) · ((1 / 𝑝)↑𝑘))) |
| 267 | | fzval3 13773 |
. . . . . . . . . . 11
⊢
((⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℤ →
(2...(⌊‘((log‘𝐴) / (log‘𝑝)))) = (2..^((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) |
| 268 | 200, 267 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(2...(⌊‘((log‘𝐴) / (log‘𝑝)))) = (2..^((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) |
| 269 | 268 | sumeq1d 15736 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈
(2...(⌊‘((log‘𝐴) / (log‘𝑝))))((1 / 𝑝)↑𝑘) = Σ𝑘 ∈
(2..^((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))((1 / 𝑝)↑𝑘)) |
| 270 | 204, 238 | ltned 11397 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 / 𝑝) ≠ 1) |
| 271 | | 2nn0 12543 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ0 |
| 272 | 271 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 2 ∈
ℕ0) |
| 273 | | eluzp1p1 12906 |
. . . . . . . . . . . 12
⊢
((⌊‘((log‘𝐴) / (log‘𝑝))) ∈ (ℤ≥‘1)
→ ((⌊‘((log‘𝐴) / (log‘𝑝))) + 1) ∈
(ℤ≥‘(1 + 1))) |
| 274 | 137, 273 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
((⌊‘((log‘𝐴) / (log‘𝑝))) + 1) ∈
(ℤ≥‘(1 + 1))) |
| 275 | | df-2 12329 |
. . . . . . . . . . . 12
⊢ 2 = (1 +
1) |
| 276 | 275 | fveq2i 6909 |
. . . . . . . . . . 11
⊢
(ℤ≥‘2) = (ℤ≥‘(1 +
1)) |
| 277 | 274, 276 | eleqtrrdi 2852 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
((⌊‘((log‘𝐴) / (log‘𝑝))) + 1) ∈
(ℤ≥‘2)) |
| 278 | 213, 270,
272, 277 | geoserg 15902 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈
(2..^((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))((1 / 𝑝)↑𝑘) = ((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 /
𝑝)))) |
| 279 | 269, 278 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈
(2...(⌊‘((log‘𝐴) / (log‘𝑝))))((1 / 𝑝)↑𝑘) = ((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 /
𝑝)))) |
| 280 | 279 | oveq2d 7447 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) · Σ𝑘 ∈
(2...(⌊‘((log‘𝐴) / (log‘𝑝))))((1 / 𝑝)↑𝑘)) = ((log‘𝑝) · ((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 /
𝑝))))) |
| 281 | 262, 266,
280 | 3eqtr2d 2783 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈
(2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝↑𝑘)) = ((log‘𝑝) · ((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 /
𝑝))))) |
| 282 | 111 | nncnd 12282 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 · (𝑝 − 1)) ∈ ℂ) |
| 283 | 111 | nnne0d 12316 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 · (𝑝 − 1)) ≠ 0) |
| 284 | 125, 282,
283 | divrecd 12046 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) / (𝑝 · (𝑝 − 1))) = ((log‘𝑝) · (1 / (𝑝 · (𝑝 − 1))))) |
| 285 | 248, 281,
284 | 3brtr4d 5175 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈
(2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝↑𝑘)) ≤ ((log‘𝑝) / (𝑝 · (𝑝 − 1)))) |
| 286 | 198, 285 | eqbrtrd 5165 |
. . . 4
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) / (𝑝↑𝑘)) ≤ ((log‘𝑝) / (𝑝 · (𝑝 − 1)))) |
| 287 | 83, 105, 112, 286 | fsumle 15835 |
. . 3
⊢ (𝐴 ∈ ℤ →
Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)Σ𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) / (𝑝↑𝑘)) ≤ Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)((log‘𝑝) / (𝑝 · (𝑝 − 1)))) |
| 288 | | elfzuz 13560 |
. . . . . . . . . . 11
⊢ (𝑝 ∈ (2...((abs‘𝐴) + 1)) → 𝑝 ∈
(ℤ≥‘2)) |
| 289 | | eluz2nn 12924 |
. . . . . . . . . . 11
⊢ (𝑝 ∈
(ℤ≥‘2) → 𝑝 ∈ ℕ) |
| 290 | 288, 289 | syl 17 |
. . . . . . . . . 10
⊢ (𝑝 ∈ (2...((abs‘𝐴) + 1)) → 𝑝 ∈
ℕ) |
| 291 | 290 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → 𝑝 ∈
ℕ) |
| 292 | 291 | nnred 12281 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → 𝑝 ∈
ℝ) |
| 293 | 288 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → 𝑝 ∈
(ℤ≥‘2)) |
| 294 | | eluz2gt1 12962 |
. . . . . . . . 9
⊢ (𝑝 ∈
(ℤ≥‘2) → 1 < 𝑝) |
| 295 | 293, 294 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → 1 < 𝑝) |
| 296 | 292, 295 | rplogcld 26671 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → (log‘𝑝) ∈
ℝ+) |
| 297 | 293, 109 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → (𝑝 − 1) ∈
ℕ) |
| 298 | 291, 297 | nnmulcld 12319 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → (𝑝 · (𝑝 − 1)) ∈ ℕ) |
| 299 | 298 | nnrpd 13075 |
. . . . . . 7
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → (𝑝 · (𝑝 − 1)) ∈
ℝ+) |
| 300 | 296, 299 | rpdivcld 13094 |
. . . . . 6
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) →
((log‘𝑝) / (𝑝 · (𝑝 − 1))) ∈
ℝ+) |
| 301 | 300 | rpred 13077 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) →
((log‘𝑝) / (𝑝 · (𝑝 − 1))) ∈
ℝ) |
| 302 | 47, 301 | fsumrecl 15770 |
. . . 4
⊢ (𝐴 ∈ ℤ →
Σ𝑝 ∈
(2...((abs‘𝐴) +
1))((log‘𝑝) / (𝑝 · (𝑝 − 1))) ∈
ℝ) |
| 303 | 300 | rpge0d 13081 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → 0 ≤
((log‘𝑝) / (𝑝 · (𝑝 − 1)))) |
| 304 | 47, 301, 303, 82 | fsumless 15832 |
. . . 4
⊢ (𝐴 ∈ ℤ →
Σ𝑝 ∈ ((0[,]𝐴) ∩
ℙ)((log‘𝑝) /
(𝑝 · (𝑝 − 1))) ≤ Σ𝑝 ∈ (2...((abs‘𝐴) + 1))((log‘𝑝) / (𝑝 · (𝑝 − 1)))) |
| 305 | | rplogsumlem1 27528 |
. . . . 5
⊢
(((abs‘𝐴) + 1)
∈ ℕ → Σ𝑝 ∈ (2...((abs‘𝐴) + 1))((log‘𝑝) / (𝑝 · (𝑝 − 1))) ≤ 2) |
| 306 | 75, 305 | syl 17 |
. . . 4
⊢ (𝐴 ∈ ℤ →
Σ𝑝 ∈
(2...((abs‘𝐴) +
1))((log‘𝑝) / (𝑝 · (𝑝 − 1))) ≤ 2) |
| 307 | 113, 302,
115, 304, 306 | letrd 11418 |
. . 3
⊢ (𝐴 ∈ ℤ →
Σ𝑝 ∈ ((0[,]𝐴) ∩
ℙ)((log‘𝑝) /
(𝑝 · (𝑝 − 1))) ≤
2) |
| 308 | 106, 113,
115, 287, 307 | letrd 11418 |
. 2
⊢ (𝐴 ∈ ℤ →
Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)Σ𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝↑𝑘)) − if((𝑝↑𝑘) ∈ ℙ, (log‘(𝑝↑𝑘)), 0)) / (𝑝↑𝑘)) ≤ 2) |
| 309 | 46, 308 | eqbrtrd 5165 |
1
⊢ (𝐴 ∈ ℤ →
Σ𝑛 ∈ (1...𝐴)(((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) ≤ 2) |