MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rplogsumlem2 Structured version   Visualization version   GIF version

Theorem rplogsumlem2 25411
Description: Lemma for rplogsum 25453. Equation 9.2.14 of [Shapiro], p. 331. (Contributed by Mario Carneiro, 2-May-2016.)
Assertion
Ref Expression
rplogsumlem2 (𝐴 ∈ ℤ → Σ𝑛 ∈ (1...𝐴)(((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) ≤ 2)
Distinct variable group:   𝐴,𝑛

Proof of Theorem rplogsumlem2
Dummy variables 𝑘 𝑝 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 flid 12853 . . . . 5 (𝐴 ∈ ℤ → (⌊‘𝐴) = 𝐴)
21oveq2d 6900 . . . 4 (𝐴 ∈ ℤ → (1...(⌊‘𝐴)) = (1...𝐴))
32sumeq1d 14674 . . 3 (𝐴 ∈ ℤ → Σ𝑛 ∈ (1...(⌊‘𝐴))(((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) = Σ𝑛 ∈ (1...𝐴)(((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛))
4 fveq2 6418 . . . . . 6 (𝑛 = (𝑝𝑘) → (Λ‘𝑛) = (Λ‘(𝑝𝑘)))
5 eleq1 2884 . . . . . . 7 (𝑛 = (𝑝𝑘) → (𝑛 ∈ ℙ ↔ (𝑝𝑘) ∈ ℙ))
6 fveq2 6418 . . . . . . 7 (𝑛 = (𝑝𝑘) → (log‘𝑛) = (log‘(𝑝𝑘)))
75, 6ifbieq1d 4313 . . . . . 6 (𝑛 = (𝑝𝑘) → if(𝑛 ∈ ℙ, (log‘𝑛), 0) = if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0))
84, 7oveq12d 6902 . . . . 5 (𝑛 = (𝑝𝑘) → ((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) = ((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)))
9 id 22 . . . . 5 (𝑛 = (𝑝𝑘) → 𝑛 = (𝑝𝑘))
108, 9oveq12d 6902 . . . 4 (𝑛 = (𝑝𝑘) → (((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) = (((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)))
11 zre 11667 . . . 4 (𝐴 ∈ ℤ → 𝐴 ∈ ℝ)
12 elfznn 12613 . . . . . . . . 9 (𝑛 ∈ (1...(⌊‘𝐴)) → 𝑛 ∈ ℕ)
1312adantl 469 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝑛 ∈ ℕ)
14 vmacl 25081 . . . . . . . 8 (𝑛 ∈ ℕ → (Λ‘𝑛) ∈ ℝ)
1513, 14syl 17 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (Λ‘𝑛) ∈ ℝ)
1613nnrpd 12104 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝑛 ∈ ℝ+)
1716relogcld 24606 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (log‘𝑛) ∈ ℝ)
18 0re 10337 . . . . . . . 8 0 ∈ ℝ
19 ifcl 4334 . . . . . . . 8 (((log‘𝑛) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑛 ∈ ℙ, (log‘𝑛), 0) ∈ ℝ)
2017, 18, 19sylancl 576 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → if(𝑛 ∈ ℙ, (log‘𝑛), 0) ∈ ℝ)
2115, 20resubcld 10753 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → ((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) ∈ ℝ)
2221, 13nndivred 11367 . . . . 5 ((𝐴 ∈ ℤ ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) ∈ ℝ)
2322recnd 10363 . . . 4 ((𝐴 ∈ ℤ ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) ∈ ℂ)
24 simprr 780 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (Λ‘𝑛) = 0)) → (Λ‘𝑛) = 0)
25 vmaprm 25080 . . . . . . . . . . . . 13 (𝑛 ∈ ℙ → (Λ‘𝑛) = (log‘𝑛))
26 prmnn 15626 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℙ → 𝑛 ∈ ℕ)
2726nnred 11332 . . . . . . . . . . . . . 14 (𝑛 ∈ ℙ → 𝑛 ∈ ℝ)
28 prmgt1 15647 . . . . . . . . . . . . . 14 (𝑛 ∈ ℙ → 1 < 𝑛)
2927, 28rplogcld 24612 . . . . . . . . . . . . 13 (𝑛 ∈ ℙ → (log‘𝑛) ∈ ℝ+)
3025, 29eqeltrd 2896 . . . . . . . . . . . 12 (𝑛 ∈ ℙ → (Λ‘𝑛) ∈ ℝ+)
3130rpne0d 12111 . . . . . . . . . . 11 (𝑛 ∈ ℙ → (Λ‘𝑛) ≠ 0)
3231necon2bi 3019 . . . . . . . . . 10 ((Λ‘𝑛) = 0 → ¬ 𝑛 ∈ ℙ)
3332ad2antll 711 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (Λ‘𝑛) = 0)) → ¬ 𝑛 ∈ ℙ)
3433iffalsed 4301 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (Λ‘𝑛) = 0)) → if(𝑛 ∈ ℙ, (log‘𝑛), 0) = 0)
3524, 34oveq12d 6902 . . . . . . 7 ((𝐴 ∈ ℤ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (Λ‘𝑛) = 0)) → ((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) = (0 − 0))
36 0m0e0 11440 . . . . . . 7 (0 − 0) = 0
3735, 36syl6eq 2867 . . . . . 6 ((𝐴 ∈ ℤ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (Λ‘𝑛) = 0)) → ((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) = 0)
3837oveq1d 6899 . . . . 5 ((𝐴 ∈ ℤ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (Λ‘𝑛) = 0)) → (((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) = (0 / 𝑛))
3912ad2antrl 710 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (Λ‘𝑛) = 0)) → 𝑛 ∈ ℕ)
4039nnrpd 12104 . . . . . . 7 ((𝐴 ∈ ℤ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (Λ‘𝑛) = 0)) → 𝑛 ∈ ℝ+)
4140rpcnne0d 12115 . . . . . 6 ((𝐴 ∈ ℤ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (Λ‘𝑛) = 0)) → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0))
42 div0 11010 . . . . . 6 ((𝑛 ∈ ℂ ∧ 𝑛 ≠ 0) → (0 / 𝑛) = 0)
4341, 42syl 17 . . . . 5 ((𝐴 ∈ ℤ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (Λ‘𝑛) = 0)) → (0 / 𝑛) = 0)
4438, 43eqtrd 2851 . . . 4 ((𝐴 ∈ ℤ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (Λ‘𝑛) = 0)) → (((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) = 0)
4510, 11, 23, 44fsumvma2 25176 . . 3 (𝐴 ∈ ℤ → Σ𝑛 ∈ (1...(⌊‘𝐴))(((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)))
463, 45eqtr3d 2853 . 2 (𝐴 ∈ ℤ → Σ𝑛 ∈ (1...𝐴)(((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)))
47 fzfid 13016 . . . . 5 (𝐴 ∈ ℤ → (2...((abs‘𝐴) + 1)) ∈ Fin)
48 inss2 4041 . . . . . . . . . . . 12 ((0[,]𝐴) ∩ ℙ) ⊆ ℙ
49 simpr 473 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ((0[,]𝐴) ∩ ℙ))
5048, 49sseldi 3807 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℙ)
51 prmnn 15626 . . . . . . . . . . 11 (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
5250, 51syl 17 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℕ)
5352nnred 11332 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℝ)
5411adantr 468 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝐴 ∈ ℝ)
55 zcn 11668 . . . . . . . . . . . 12 (𝐴 ∈ ℤ → 𝐴 ∈ ℂ)
5655abscld 14418 . . . . . . . . . . 11 (𝐴 ∈ ℤ → (abs‘𝐴) ∈ ℝ)
57 peano2re 10504 . . . . . . . . . . 11 ((abs‘𝐴) ∈ ℝ → ((abs‘𝐴) + 1) ∈ ℝ)
5856, 57syl 17 . . . . . . . . . 10 (𝐴 ∈ ℤ → ((abs‘𝐴) + 1) ∈ ℝ)
5958adantr 468 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((abs‘𝐴) + 1) ∈ ℝ)
60 inss1 4040 . . . . . . . . . . . . 13 ((0[,]𝐴) ∩ ℙ) ⊆ (0[,]𝐴)
6160sseli 3805 . . . . . . . . . . . 12 (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) → 𝑝 ∈ (0[,]𝐴))
62 elicc2 12476 . . . . . . . . . . . . 13 ((0 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝑝 ∈ (0[,]𝐴) ↔ (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝𝑝𝐴)))
6318, 11, 62sylancr 577 . . . . . . . . . . . 12 (𝐴 ∈ ℤ → (𝑝 ∈ (0[,]𝐴) ↔ (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝𝑝𝐴)))
6461, 63syl5ib 235 . . . . . . . . . . 11 (𝐴 ∈ ℤ → (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) → (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝𝑝𝐴)))
6564imp 395 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝𝑝𝐴))
6665simp3d 1167 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝𝐴)
6755adantr 468 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝐴 ∈ ℂ)
6867abscld 14418 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (abs‘𝐴) ∈ ℝ)
6954leabsd 14396 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝐴 ≤ (abs‘𝐴))
7068lep1d 11250 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (abs‘𝐴) ≤ ((abs‘𝐴) + 1))
7154, 68, 59, 69, 70letrd 10489 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝐴 ≤ ((abs‘𝐴) + 1))
7253, 54, 59, 66, 71letrd 10489 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ≤ ((abs‘𝐴) + 1))
73 prmuz2 15646 . . . . . . . . . 10 (𝑝 ∈ ℙ → 𝑝 ∈ (ℤ‘2))
7450, 73syl 17 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ (ℤ‘2))
75 nn0abscl 14295 . . . . . . . . . . . 12 (𝐴 ∈ ℤ → (abs‘𝐴) ∈ ℕ0)
76 nn0p1nn 11618 . . . . . . . . . . . 12 ((abs‘𝐴) ∈ ℕ0 → ((abs‘𝐴) + 1) ∈ ℕ)
7775, 76syl 17 . . . . . . . . . . 11 (𝐴 ∈ ℤ → ((abs‘𝐴) + 1) ∈ ℕ)
7877nnzd 11767 . . . . . . . . . 10 (𝐴 ∈ ℤ → ((abs‘𝐴) + 1) ∈ ℤ)
7978adantr 468 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((abs‘𝐴) + 1) ∈ ℤ)
80 elfz5 12577 . . . . . . . . 9 ((𝑝 ∈ (ℤ‘2) ∧ ((abs‘𝐴) + 1) ∈ ℤ) → (𝑝 ∈ (2...((abs‘𝐴) + 1)) ↔ 𝑝 ≤ ((abs‘𝐴) + 1)))
8174, 79, 80syl2anc 575 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 ∈ (2...((abs‘𝐴) + 1)) ↔ 𝑝 ≤ ((abs‘𝐴) + 1)))
8272, 81mpbird 248 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ (2...((abs‘𝐴) + 1)))
8382ex 399 . . . . . 6 (𝐴 ∈ ℤ → (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) → 𝑝 ∈ (2...((abs‘𝐴) + 1))))
8483ssrdv 3815 . . . . 5 (𝐴 ∈ ℤ → ((0[,]𝐴) ∩ ℙ) ⊆ (2...((abs‘𝐴) + 1)))
85 ssfi 8429 . . . . 5 (((2...((abs‘𝐴) + 1)) ∈ Fin ∧ ((0[,]𝐴) ∩ ℙ) ⊆ (2...((abs‘𝐴) + 1))) → ((0[,]𝐴) ∩ ℙ) ∈ Fin)
8647, 84, 85syl2anc 575 . . . 4 (𝐴 ∈ ℤ → ((0[,]𝐴) ∩ ℙ) ∈ Fin)
87 fzfid 13016 . . . . 5 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1...(⌊‘((log‘𝐴) / (log‘𝑝)))) ∈ Fin)
88 simprl 778 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → 𝑝 ∈ ((0[,]𝐴) ∩ ℙ))
8948, 88sseldi 3807 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → 𝑝 ∈ ℙ)
90 elfznn 12613 . . . . . . . . . . 11 (𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))) → 𝑘 ∈ ℕ)
9190ad2antll 711 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → 𝑘 ∈ ℕ)
92 vmappw 25079 . . . . . . . . . 10 ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) → (Λ‘(𝑝𝑘)) = (log‘𝑝))
9389, 91, 92syl2anc 575 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → (Λ‘(𝑝𝑘)) = (log‘𝑝))
9452adantrr 699 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → 𝑝 ∈ ℕ)
9594nnrpd 12104 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → 𝑝 ∈ ℝ+)
9695relogcld 24606 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → (log‘𝑝) ∈ ℝ)
9793, 96eqeltrd 2896 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → (Λ‘(𝑝𝑘)) ∈ ℝ)
9891nnnn0d 11637 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → 𝑘 ∈ ℕ0)
99 nnexpcl 13116 . . . . . . . . . . . 12 ((𝑝 ∈ ℕ ∧ 𝑘 ∈ ℕ0) → (𝑝𝑘) ∈ ℕ)
10094, 98, 99syl2anc 575 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → (𝑝𝑘) ∈ ℕ)
101100nnrpd 12104 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → (𝑝𝑘) ∈ ℝ+)
102101relogcld 24606 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → (log‘(𝑝𝑘)) ∈ ℝ)
103 ifcl 4334 . . . . . . . . 9 (((log‘(𝑝𝑘)) ∈ ℝ ∧ 0 ∈ ℝ) → if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0) ∈ ℝ)
104102, 18, 103sylancl 576 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0) ∈ ℝ)
10597, 104resubcld 10753 . . . . . . 7 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → ((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) ∈ ℝ)
106105, 100nndivred 11367 . . . . . 6 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → (((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)) ∈ ℝ)
107106anassrs 455 . . . . 5 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) → (((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)) ∈ ℝ)
10887, 107fsumrecl 14708 . . . 4 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)) ∈ ℝ)
10986, 108fsumrecl 14708 . . 3 (𝐴 ∈ ℤ → Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)) ∈ ℝ)
11052nnrpd 12104 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℝ+)
111110relogcld 24606 . . . . 5 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈ ℝ)
112 uz2m1nn 12002 . . . . . . 7 (𝑝 ∈ (ℤ‘2) → (𝑝 − 1) ∈ ℕ)
11374, 112syl 17 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 − 1) ∈ ℕ)
11452, 113nnmulcld 11366 . . . . 5 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 · (𝑝 − 1)) ∈ ℕ)
115111, 114nndivred 11367 . . . 4 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) / (𝑝 · (𝑝 − 1))) ∈ ℝ)
11686, 115fsumrecl 14708 . . 3 (𝐴 ∈ ℤ → Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)((log‘𝑝) / (𝑝 · (𝑝 − 1))) ∈ ℝ)
117 2re 11387 . . . 4 2 ∈ ℝ
118117a1i 11 . . 3 (𝐴 ∈ ℤ → 2 ∈ ℝ)
11918a1i 11 . . . . . . . . . . . . 13 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 0 ∈ ℝ)
12052nngt0d 11362 . . . . . . . . . . . . 13 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 0 < 𝑝)
121119, 53, 54, 120, 66ltletrd 10492 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 0 < 𝐴)
12254, 121elrpd 12103 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝐴 ∈ ℝ+)
123122relogcld 24606 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝐴) ∈ ℝ)
124 prmgt1 15647 . . . . . . . . . . . 12 (𝑝 ∈ ℙ → 1 < 𝑝)
12550, 124syl 17 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 1 < 𝑝)
12653, 125rplogcld 24612 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈ ℝ+)
127123, 126rerpdivcld 12137 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝐴) / (log‘𝑝)) ∈ ℝ)
128126rpcnd 12108 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈ ℂ)
129128mulid2d 10353 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 · (log‘𝑝)) = (log‘𝑝))
130110, 122logled 24610 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝𝐴 ↔ (log‘𝑝) ≤ (log‘𝐴)))
13166, 130mpbid 223 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ≤ (log‘𝐴))
132129, 131eqbrtrd 4877 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 · (log‘𝑝)) ≤ (log‘𝐴))
133 1re 10335 . . . . . . . . . . . 12 1 ∈ ℝ
134133a1i 11 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 1 ∈ ℝ)
135134, 123, 126lemuldivd 12155 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 · (log‘𝑝)) ≤ (log‘𝐴) ↔ 1 ≤ ((log‘𝐴) / (log‘𝑝))))
136132, 135mpbid 223 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 1 ≤ ((log‘𝐴) / (log‘𝑝)))
137 flge1nn 12866 . . . . . . . . 9 ((((log‘𝐴) / (log‘𝑝)) ∈ ℝ ∧ 1 ≤ ((log‘𝐴) / (log‘𝑝))) → (⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℕ)
138127, 136, 137syl2anc 575 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℕ)
139 nnuz 11961 . . . . . . . 8 ℕ = (ℤ‘1)
140138, 139syl6eleq 2906 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (⌊‘((log‘𝐴) / (log‘𝑝))) ∈ (ℤ‘1))
141106recnd 10363 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → (((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)) ∈ ℂ)
142141anassrs 455 . . . . . . 7 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) → (((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)) ∈ ℂ)
143 oveq2 6892 . . . . . . . . . 10 (𝑘 = 1 → (𝑝𝑘) = (𝑝↑1))
144143fveq2d 6422 . . . . . . . . 9 (𝑘 = 1 → (Λ‘(𝑝𝑘)) = (Λ‘(𝑝↑1)))
145143eleq1d 2881 . . . . . . . . . 10 (𝑘 = 1 → ((𝑝𝑘) ∈ ℙ ↔ (𝑝↑1) ∈ ℙ))
146143fveq2d 6422 . . . . . . . . . 10 (𝑘 = 1 → (log‘(𝑝𝑘)) = (log‘(𝑝↑1)))
147145, 146ifbieq1d 4313 . . . . . . . . 9 (𝑘 = 1 → if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0) = if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0))
148144, 147oveq12d 6902 . . . . . . . 8 (𝑘 = 1 → ((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) = ((Λ‘(𝑝↑1)) − if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0)))
149148, 143oveq12d 6902 . . . . . . 7 (𝑘 = 1 → (((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)) = (((Λ‘(𝑝↑1)) − if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0)) / (𝑝↑1)))
150140, 142, 149fsum1p 14725 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)) = ((((Λ‘(𝑝↑1)) − if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0)) / (𝑝↑1)) + Σ𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘))))
15152nncnd 11333 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℂ)
152151exp1d 13246 . . . . . . . . . . . . 13 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝↑1) = 𝑝)
153152fveq2d 6422 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (Λ‘(𝑝↑1)) = (Λ‘𝑝))
154 vmaprm 25080 . . . . . . . . . . . . 13 (𝑝 ∈ ℙ → (Λ‘𝑝) = (log‘𝑝))
15550, 154syl 17 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (Λ‘𝑝) = (log‘𝑝))
156153, 155eqtrd 2851 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (Λ‘(𝑝↑1)) = (log‘𝑝))
157152, 50eqeltrd 2896 . . . . . . . . . . . . 13 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝↑1) ∈ ℙ)
158157iftrued 4298 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0) = (log‘(𝑝↑1)))
159152fveq2d 6422 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘(𝑝↑1)) = (log‘𝑝))
160158, 159eqtrd 2851 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0) = (log‘𝑝))
161156, 160oveq12d 6902 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((Λ‘(𝑝↑1)) − if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0)) = ((log‘𝑝) − (log‘𝑝)))
162128subidd 10675 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) − (log‘𝑝)) = 0)
163161, 162eqtrd 2851 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((Λ‘(𝑝↑1)) − if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0)) = 0)
164163, 152oveq12d 6902 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((Λ‘(𝑝↑1)) − if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0)) / (𝑝↑1)) = (0 / 𝑝))
165110rpcnne0d 12115 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 ∈ ℂ ∧ 𝑝 ≠ 0))
166 div0 11010 . . . . . . . . 9 ((𝑝 ∈ ℂ ∧ 𝑝 ≠ 0) → (0 / 𝑝) = 0)
167165, 166syl 17 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (0 / 𝑝) = 0)
168164, 167eqtrd 2851 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((Λ‘(𝑝↑1)) − if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0)) / (𝑝↑1)) = 0)
169 1p1e2 11445 . . . . . . . . . 10 (1 + 1) = 2
170169oveq1i 6894 . . . . . . . . 9 ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝)))) = (2...(⌊‘((log‘𝐴) / (log‘𝑝))))
171170a1i 11 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝)))) = (2...(⌊‘((log‘𝐴) / (log‘𝑝)))))
172 elfzuz 12581 . . . . . . . . . . . . . 14 (𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝)))) → 𝑘 ∈ (ℤ‘2))
173 eluz2nn 11964 . . . . . . . . . . . . . 14 (𝑘 ∈ (ℤ‘2) → 𝑘 ∈ ℕ)
174172, 173syl 17 . . . . . . . . . . . . 13 (𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝)))) → 𝑘 ∈ ℕ)
175174, 170eleq2s 2914 . . . . . . . . . . . 12 (𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝)))) → 𝑘 ∈ ℕ)
17650, 175, 92syl2an 585 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → (Λ‘(𝑝𝑘)) = (log‘𝑝))
17752adantr 468 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → 𝑝 ∈ ℕ)
178 nnq 12040 . . . . . . . . . . . . . 14 (𝑝 ∈ ℕ → 𝑝 ∈ ℚ)
179177, 178syl 17 . . . . . . . . . . . . 13 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → 𝑝 ∈ ℚ)
180172, 170eleq2s 2914 . . . . . . . . . . . . . 14 (𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝)))) → 𝑘 ∈ (ℤ‘2))
181180adantl 469 . . . . . . . . . . . . 13 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → 𝑘 ∈ (ℤ‘2))
182 expnprm 15843 . . . . . . . . . . . . 13 ((𝑝 ∈ ℚ ∧ 𝑘 ∈ (ℤ‘2)) → ¬ (𝑝𝑘) ∈ ℙ)
183179, 181, 182syl2anc 575 . . . . . . . . . . . 12 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → ¬ (𝑝𝑘) ∈ ℙ)
184183iffalsed 4301 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0) = 0)
185176, 184oveq12d 6902 . . . . . . . . . 10 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → ((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) = ((log‘𝑝) − 0))
186128subid1d 10676 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) − 0) = (log‘𝑝))
187186adantr 468 . . . . . . . . . 10 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → ((log‘𝑝) − 0) = (log‘𝑝))
188185, 187eqtrd 2851 . . . . . . . . 9 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → ((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) = (log‘𝑝))
189188oveq1d 6899 . . . . . . . 8 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → (((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)) = ((log‘𝑝) / (𝑝𝑘)))
190171, 189sumeq12dv 14680 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)) = Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝𝑘)))
191168, 190oveq12d 6902 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((((Λ‘(𝑝↑1)) − if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0)) / (𝑝↑1)) + Σ𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘))) = (0 + Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝𝑘))))
192 fzfid 13016 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (2...(⌊‘((log‘𝐴) / (log‘𝑝)))) ∈ Fin)
193111adantr 468 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → (log‘𝑝) ∈ ℝ)
194 nnnn0 11586 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
19552, 194, 99syl2an 585 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → (𝑝𝑘) ∈ ℕ)
196193, 195nndivred 11367 . . . . . . . . . 10 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → ((log‘𝑝) / (𝑝𝑘)) ∈ ℝ)
197174, 196sylan2 582 . . . . . . . . 9 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))) → ((log‘𝑝) / (𝑝𝑘)) ∈ ℝ)
198192, 197fsumrecl 14708 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝𝑘)) ∈ ℝ)
199198recnd 10363 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝𝑘)) ∈ ℂ)
200199addid2d 10532 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (0 + Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝𝑘))) = Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝𝑘)))
201150, 191, 2003eqtrd 2855 . . . . 5 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)) = Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝𝑘)))
202110rpreccld 12116 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 / 𝑝) ∈ ℝ+)
203127flcld 12843 . . . . . . . . . . . . 13 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℤ)
204203peano2zd 11771 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((⌊‘((log‘𝐴) / (log‘𝑝))) + 1) ∈ ℤ)
205202, 204rpexpcld 13275 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1)) ∈ ℝ+)
206205rpge0d 12110 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 0 ≤ ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1)))
20752nnrecred 11364 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 / 𝑝) ∈ ℝ)
208207resqcld 13278 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 / 𝑝)↑2) ∈ ℝ)
209138peano2nnd 11334 . . . . . . . . . . . . 13 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((⌊‘((log‘𝐴) / (log‘𝑝))) + 1) ∈ ℕ)
210209nnnn0d 11637 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((⌊‘((log‘𝐴) / (log‘𝑝))) + 1) ∈ ℕ0)
211207, 210reexpcld 13268 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1)) ∈ ℝ)
212208, 211subge02d 10914 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (0 ≤ ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1)) ↔ (((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) ≤ ((1 / 𝑝)↑2)))
213206, 212mpbid 223 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) ≤ ((1 / 𝑝)↑2))
214113nnrpd 12104 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 − 1) ∈ ℝ+)
215214rpcnne0d 12115 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((𝑝 − 1) ∈ ℂ ∧ (𝑝 − 1) ≠ 0))
216202rpcnd 12108 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 / 𝑝) ∈ ℂ)
217 dmdcan 11030 . . . . . . . . . . 11 ((((𝑝 − 1) ∈ ℂ ∧ (𝑝 − 1) ≠ 0) ∧ (𝑝 ∈ ℂ ∧ 𝑝 ≠ 0) ∧ (1 / 𝑝) ∈ ℂ) → (((𝑝 − 1) / 𝑝) · ((1 / 𝑝) / (𝑝 − 1))) = ((1 / 𝑝) / 𝑝))
218215, 165, 216, 217syl3anc 1483 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((𝑝 − 1) / 𝑝) · ((1 / 𝑝) / (𝑝 − 1))) = ((1 / 𝑝) / 𝑝))
219134recnd 10363 . . . . . . . . . . . . 13 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 1 ∈ ℂ)
220 divsubdir 11016 . . . . . . . . . . . . 13 ((𝑝 ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝑝 ∈ ℂ ∧ 𝑝 ≠ 0)) → ((𝑝 − 1) / 𝑝) = ((𝑝 / 𝑝) − (1 / 𝑝)))
221151, 219, 165, 220syl3anc 1483 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((𝑝 − 1) / 𝑝) = ((𝑝 / 𝑝) − (1 / 𝑝)))
222 divid 11009 . . . . . . . . . . . . . 14 ((𝑝 ∈ ℂ ∧ 𝑝 ≠ 0) → (𝑝 / 𝑝) = 1)
223165, 222syl 17 . . . . . . . . . . . . 13 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 / 𝑝) = 1)
224223oveq1d 6899 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((𝑝 / 𝑝) − (1 / 𝑝)) = (1 − (1 / 𝑝)))
225221, 224eqtrd 2851 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((𝑝 − 1) / 𝑝) = (1 − (1 / 𝑝)))
226 divdiv1 11031 . . . . . . . . . . . 12 ((1 ∈ ℂ ∧ (𝑝 ∈ ℂ ∧ 𝑝 ≠ 0) ∧ ((𝑝 − 1) ∈ ℂ ∧ (𝑝 − 1) ≠ 0)) → ((1 / 𝑝) / (𝑝 − 1)) = (1 / (𝑝 · (𝑝 − 1))))
227219, 165, 215, 226syl3anc 1483 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 / 𝑝) / (𝑝 − 1)) = (1 / (𝑝 · (𝑝 − 1))))
228225, 227oveq12d 6902 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((𝑝 − 1) / 𝑝) · ((1 / 𝑝) / (𝑝 − 1))) = ((1 − (1 / 𝑝)) · (1 / (𝑝 · (𝑝 − 1)))))
22952nnne0d 11363 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ≠ 0)
230216, 151, 229divrecd 11099 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 / 𝑝) / 𝑝) = ((1 / 𝑝) · (1 / 𝑝)))
231216sqvald 13248 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 / 𝑝)↑2) = ((1 / 𝑝) · (1 / 𝑝)))
232230, 231eqtr4d 2854 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 / 𝑝) / 𝑝) = ((1 / 𝑝)↑2))
233218, 228, 2323eqtr3d 2859 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 − (1 / 𝑝)) · (1 / (𝑝 · (𝑝 − 1)))) = ((1 / 𝑝)↑2))
234213, 233breqtrrd 4883 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) ≤ ((1 − (1 / 𝑝)) · (1 / (𝑝 · (𝑝 − 1)))))
235208, 211resubcld 10753 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) ∈ ℝ)
236114nnrecred 11364 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 / (𝑝 · (𝑝 − 1))) ∈ ℝ)
237 resubcl 10640 . . . . . . . . . 10 ((1 ∈ ℝ ∧ (1 / 𝑝) ∈ ℝ) → (1 − (1 / 𝑝)) ∈ ℝ)
238133, 207, 237sylancr 577 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 − (1 / 𝑝)) ∈ ℝ)
239 recgt1 11214 . . . . . . . . . . . 12 ((𝑝 ∈ ℝ ∧ 0 < 𝑝) → (1 < 𝑝 ↔ (1 / 𝑝) < 1))
24053, 120, 239syl2anc 575 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 < 𝑝 ↔ (1 / 𝑝) < 1))
241125, 240mpbid 223 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 / 𝑝) < 1)
242 posdif 10816 . . . . . . . . . . 11 (((1 / 𝑝) ∈ ℝ ∧ 1 ∈ ℝ) → ((1 / 𝑝) < 1 ↔ 0 < (1 − (1 / 𝑝))))
243207, 133, 242sylancl 576 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 / 𝑝) < 1 ↔ 0 < (1 − (1 / 𝑝))))
244241, 243mpbid 223 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 0 < (1 − (1 / 𝑝)))
245 ledivmul 11194 . . . . . . . . 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))))))
246235, 236, 238, 244, 245syl112anc 1486 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 / 𝑝))) ≤ (1 / (𝑝 · (𝑝 − 1))) ↔ (((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) ≤ ((1 − (1 / 𝑝)) · (1 / (𝑝 · (𝑝 − 1))))))
247234, 246mpbird 248 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 / 𝑝))) ≤ (1 / (𝑝 · (𝑝 − 1))))
248238, 244elrpd 12103 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 − (1 / 𝑝)) ∈ ℝ+)
249235, 248rerpdivcld 12137 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 / 𝑝))) ∈ ℝ)
250249, 236, 126lemul2d 12150 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 / 𝑝))) ≤ (1 / (𝑝 · (𝑝 − 1))) ↔ ((log‘𝑝) · ((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 / 𝑝)))) ≤ ((log‘𝑝) · (1 / (𝑝 · (𝑝 − 1))))))
251247, 250mpbid 223 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) · ((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 / 𝑝)))) ≤ ((log‘𝑝) · (1 / (𝑝 · (𝑝 − 1)))))
252128adantr 468 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → (log‘𝑝) ∈ ℂ)
253195nncnd 11333 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → (𝑝𝑘) ∈ ℂ)
254195nnne0d 11363 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → (𝑝𝑘) ≠ 0)
255252, 253, 254divrecd 11099 . . . . . . . . . 10 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → ((log‘𝑝) / (𝑝𝑘)) = ((log‘𝑝) · (1 / (𝑝𝑘))))
256151adantr 468 . . . . . . . . . . . 12 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → 𝑝 ∈ ℂ)
25752adantr 468 . . . . . . . . . . . . 13 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → 𝑝 ∈ ℕ)
258257nnne0d 11363 . . . . . . . . . . . 12 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → 𝑝 ≠ 0)
259 nnz 11685 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
260259adantl 469 . . . . . . . . . . . 12 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℤ)
261256, 258, 260exprecd 13259 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → ((1 / 𝑝)↑𝑘) = (1 / (𝑝𝑘)))
262261oveq2d 6900 . . . . . . . . . 10 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → ((log‘𝑝) · ((1 / 𝑝)↑𝑘)) = ((log‘𝑝) · (1 / (𝑝𝑘))))
263255, 262eqtr4d 2854 . . . . . . . . 9 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → ((log‘𝑝) / (𝑝𝑘)) = ((log‘𝑝) · ((1 / 𝑝)↑𝑘)))
264174, 263sylan2 582 . . . . . . . 8 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))) → ((log‘𝑝) / (𝑝𝑘)) = ((log‘𝑝) · ((1 / 𝑝)↑𝑘)))
265264sumeq2dv 14676 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝𝑘)) = Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) · ((1 / 𝑝)↑𝑘)))
266174nnnn0d 11637 . . . . . . . . 9 (𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝)))) → 𝑘 ∈ ℕ0)
267 expcl 13121 . . . . . . . . 9 (((1 / 𝑝) ∈ ℂ ∧ 𝑘 ∈ ℕ0) → ((1 / 𝑝)↑𝑘) ∈ ℂ)
268216, 266, 267syl2an 585 . . . . . . . 8 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))) → ((1 / 𝑝)↑𝑘) ∈ ℂ)
269192, 128, 268fsummulc2 14758 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) · Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((1 / 𝑝)↑𝑘)) = Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) · ((1 / 𝑝)↑𝑘)))
270 fzval3 12781 . . . . . . . . . . 11 ((⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℤ → (2...(⌊‘((log‘𝐴) / (log‘𝑝)))) = (2..^((⌊‘((log‘𝐴) / (log‘𝑝))) + 1)))
271203, 270syl 17 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (2...(⌊‘((log‘𝐴) / (log‘𝑝)))) = (2..^((⌊‘((log‘𝐴) / (log‘𝑝))) + 1)))
272271sumeq1d 14674 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((1 / 𝑝)↑𝑘) = Σ𝑘 ∈ (2..^((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))((1 / 𝑝)↑𝑘))
273207, 241ltned 10468 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 / 𝑝) ≠ 1)
274 2nn0 11596 . . . . . . . . . . 11 2 ∈ ℕ0
275274a1i 11 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 2 ∈ ℕ0)
276 eluzp1p1 11950 . . . . . . . . . . . 12 ((⌊‘((log‘𝐴) / (log‘𝑝))) ∈ (ℤ‘1) → ((⌊‘((log‘𝐴) / (log‘𝑝))) + 1) ∈ (ℤ‘(1 + 1)))
277140, 276syl 17 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((⌊‘((log‘𝐴) / (log‘𝑝))) + 1) ∈ (ℤ‘(1 + 1)))
278 df-2 11376 . . . . . . . . . . . 12 2 = (1 + 1)
279278fveq2i 6421 . . . . . . . . . . 11 (ℤ‘2) = (ℤ‘(1 + 1))
280277, 279syl6eleqr 2907 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((⌊‘((log‘𝐴) / (log‘𝑝))) + 1) ∈ (ℤ‘2))
281216, 273, 275, 280geoserg 14840 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈ (2..^((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))((1 / 𝑝)↑𝑘) = ((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 / 𝑝))))
282272, 281eqtrd 2851 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((1 / 𝑝)↑𝑘) = ((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 / 𝑝))))
283282oveq2d 6900 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) · Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((1 / 𝑝)↑𝑘)) = ((log‘𝑝) · ((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 / 𝑝)))))
284265, 269, 2833eqtr2d 2857 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝𝑘)) = ((log‘𝑝) · ((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 / 𝑝)))))
285114nncnd 11333 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 · (𝑝 − 1)) ∈ ℂ)
286114nnne0d 11363 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 · (𝑝 − 1)) ≠ 0)
287128, 285, 286divrecd 11099 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) / (𝑝 · (𝑝 − 1))) = ((log‘𝑝) · (1 / (𝑝 · (𝑝 − 1)))))
288251, 284, 2873brtr4d 4887 . . . . 5 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝𝑘)) ≤ ((log‘𝑝) / (𝑝 · (𝑝 − 1))))
289201, 288eqbrtrd 4877 . . . 4 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)) ≤ ((log‘𝑝) / (𝑝 · (𝑝 − 1))))
29086, 108, 115, 289fsumle 14773 . . 3 (𝐴 ∈ ℤ → Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)) ≤ Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)((log‘𝑝) / (𝑝 · (𝑝 − 1))))
291 elfzuz 12581 . . . . . . . . . . 11 (𝑝 ∈ (2...((abs‘𝐴) + 1)) → 𝑝 ∈ (ℤ‘2))
292 eluz2nn 11964 . . . . . . . . . . 11 (𝑝 ∈ (ℤ‘2) → 𝑝 ∈ ℕ)
293291, 292syl 17 . . . . . . . . . 10 (𝑝 ∈ (2...((abs‘𝐴) + 1)) → 𝑝 ∈ ℕ)
294293adantl 469 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → 𝑝 ∈ ℕ)
295294nnred 11332 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → 𝑝 ∈ ℝ)
296291adantl 469 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → 𝑝 ∈ (ℤ‘2))
297 eluz2b2 12000 . . . . . . . . . 10 (𝑝 ∈ (ℤ‘2) ↔ (𝑝 ∈ ℕ ∧ 1 < 𝑝))
298297simprbi 486 . . . . . . . . 9 (𝑝 ∈ (ℤ‘2) → 1 < 𝑝)
299296, 298syl 17 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → 1 < 𝑝)
300295, 299rplogcld 24612 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → (log‘𝑝) ∈ ℝ+)
301296, 112syl 17 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → (𝑝 − 1) ∈ ℕ)
302294, 301nnmulcld 11366 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → (𝑝 · (𝑝 − 1)) ∈ ℕ)
303302nnrpd 12104 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → (𝑝 · (𝑝 − 1)) ∈ ℝ+)
304300, 303rpdivcld 12123 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → ((log‘𝑝) / (𝑝 · (𝑝 − 1))) ∈ ℝ+)
305304rpred 12106 . . . . 5 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → ((log‘𝑝) / (𝑝 · (𝑝 − 1))) ∈ ℝ)
30647, 305fsumrecl 14708 . . . 4 (𝐴 ∈ ℤ → Σ𝑝 ∈ (2...((abs‘𝐴) + 1))((log‘𝑝) / (𝑝 · (𝑝 − 1))) ∈ ℝ)
307304rpge0d 12110 . . . . 5 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → 0 ≤ ((log‘𝑝) / (𝑝 · (𝑝 − 1))))
30847, 305, 307, 84fsumless 14770 . . . 4 (𝐴 ∈ ℤ → Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)((log‘𝑝) / (𝑝 · (𝑝 − 1))) ≤ Σ𝑝 ∈ (2...((abs‘𝐴) + 1))((log‘𝑝) / (𝑝 · (𝑝 − 1))))
309 rplogsumlem1 25410 . . . . 5 (((abs‘𝐴) + 1) ∈ ℕ → Σ𝑝 ∈ (2...((abs‘𝐴) + 1))((log‘𝑝) / (𝑝 · (𝑝 − 1))) ≤ 2)
31077, 309syl 17 . . . 4 (𝐴 ∈ ℤ → Σ𝑝 ∈ (2...((abs‘𝐴) + 1))((log‘𝑝) / (𝑝 · (𝑝 − 1))) ≤ 2)
311116, 306, 118, 308, 310letrd 10489 . . 3 (𝐴 ∈ ℤ → Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)((log‘𝑝) / (𝑝 · (𝑝 − 1))) ≤ 2)
312109, 116, 118, 290, 311letrd 10489 . 2 (𝐴 ∈ ℤ → Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)) ≤ 2)
31346, 312eqbrtrd 4877 1 (𝐴 ∈ ℤ → Σ𝑛 ∈ (1...𝐴)(((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) ≤ 2)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1100   = wceq 1637  wcel 2157  wne 2989  cin 3779  wss 3780  ifcif 4290   class class class wbr 4855  cfv 6111  (class class class)co 6884  Fincfn 8202  cc 10229  cr 10230  0cc0 10231  1c1 10232   + caddc 10234   · cmul 10236   < clt 10369  cle 10370  cmin 10561   / cdiv 10979  cn 11315  2c2 11368  0cn0 11579  cz 11663  cuz 11924  cq 12027  +crp 12066  [,]cicc 12416  ...cfz 12569  ..^cfzo 12709  cfl 12835  cexp 13103  abscabs 14217  Σcsu 14659  cprime 15623  logclog 24538  Λcvma 25055
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-rep 4977  ax-sep 4988  ax-nul 4996  ax-pow 5048  ax-pr 5109  ax-un 7189  ax-inf2 8795  ax-cnex 10287  ax-resscn 10288  ax-1cn 10289  ax-icn 10290  ax-addcl 10291  ax-addrcl 10292  ax-mulcl 10293  ax-mulrcl 10294  ax-mulcom 10295  ax-addass 10296  ax-mulass 10297  ax-distr 10298  ax-i2m1 10299  ax-1ne0 10300  ax-1rid 10301  ax-rnegex 10302  ax-rrecex 10303  ax-cnre 10304  ax-pre-lttri 10305  ax-pre-lttrn 10306  ax-pre-ltadd 10307  ax-pre-mulgt0 10308  ax-pre-sup 10309  ax-addf 10310  ax-mulf 10311
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-pss 3796  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-tp 4386  df-op 4388  df-uni 4642  df-int 4681  df-iun 4725  df-iin 4726  df-br 4856  df-opab 4918  df-mpt 4935  df-tr 4958  df-id 5232  df-eprel 5237  df-po 5245  df-so 5246  df-fr 5283  df-se 5284  df-we 5285  df-xp 5330  df-rel 5331  df-cnv 5332  df-co 5333  df-dm 5334  df-rn 5335  df-res 5336  df-ima 5337  df-pred 5907  df-ord 5953  df-on 5954  df-lim 5955  df-suc 5956  df-iota 6074  df-fun 6113  df-fn 6114  df-f 6115  df-f1 6116  df-fo 6117  df-f1o 6118  df-fv 6119  df-isom 6120  df-riota 6845  df-ov 6887  df-oprab 6888  df-mpt2 6889  df-of 7137  df-om 7306  df-1st 7408  df-2nd 7409  df-supp 7540  df-wrecs 7652  df-recs 7714  df-rdg 7752  df-1o 7806  df-2o 7807  df-oadd 7810  df-er 7989  df-map 8104  df-pm 8105  df-ixp 8156  df-en 8203  df-dom 8204  df-sdom 8205  df-fin 8206  df-fsupp 8525  df-fi 8566  df-sup 8597  df-inf 8598  df-oi 8664  df-card 9058  df-cda 9285  df-pnf 10371  df-mnf 10372  df-xr 10373  df-ltxr 10374  df-le 10375  df-sub 10563  df-neg 10564  df-div 10980  df-nn 11316  df-2 11376  df-3 11377  df-4 11378  df-5 11379  df-6 11380  df-7 11381  df-8 11382  df-9 11383  df-n0 11580  df-z 11664  df-dec 11780  df-uz 11925  df-q 12028  df-rp 12067  df-xneg 12182  df-xadd 12183  df-xmul 12184  df-ioo 12417  df-ioc 12418  df-ico 12419  df-icc 12420  df-fz 12570  df-fzo 12710  df-fl 12837  df-mod 12913  df-seq 13045  df-exp 13104  df-fac 13301  df-bc 13330  df-hash 13358  df-shft 14050  df-cj 14082  df-re 14083  df-im 14084  df-sqrt 14218  df-abs 14219  df-limsup 14445  df-clim 14462  df-rlim 14463  df-sum 14660  df-ef 15038  df-sin 15040  df-cos 15041  df-tan 15042  df-pi 15043  df-dvds 15224  df-gcd 15456  df-prm 15624  df-pc 15779  df-struct 16090  df-ndx 16091  df-slot 16092  df-base 16094  df-sets 16095  df-ress 16096  df-plusg 16186  df-mulr 16187  df-starv 16188  df-sca 16189  df-vsca 16190  df-ip 16191  df-tset 16192  df-ple 16193  df-ds 16195  df-unif 16196  df-hom 16197  df-cco 16198  df-rest 16308  df-topn 16309  df-0g 16327  df-gsum 16328  df-topgen 16329  df-pt 16330  df-prds 16333  df-xrs 16387  df-qtop 16392  df-imas 16393  df-xps 16395  df-mre 16471  df-mrc 16472  df-acs 16474  df-mgm 17467  df-sgrp 17509  df-mnd 17520  df-submnd 17561  df-mulg 17766  df-cntz 17971  df-cmn 18416  df-psmet 19966  df-xmet 19967  df-met 19968  df-bl 19969  df-mopn 19970  df-fbas 19971  df-fg 19972  df-cnfld 19975  df-top 20933  df-topon 20950  df-topsp 20972  df-bases 20985  df-cld 21058  df-ntr 21059  df-cls 21060  df-nei 21137  df-lp 21175  df-perf 21176  df-cn 21266  df-cnp 21267  df-haus 21354  df-cmp 21425  df-tx 21600  df-hmeo 21793  df-fil 21884  df-fm 21976  df-flim 21977  df-flf 21978  df-xms 22359  df-ms 22360  df-tms 22361  df-cncf 22915  df-limc 23867  df-dv 23868  df-log 24540  df-cxp 24541  df-vma 25061
This theorem is referenced by:  rplogsum  25453
  Copyright terms: Public domain W3C validator