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

Theorem rplogsumlem2 27529
Description: Lemma for rplogsum 27571. 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 13848 . . . . 5 (𝐴 ∈ ℤ → (⌊‘𝐴) = 𝐴)
21oveq2d 7447 . . . 4 (𝐴 ∈ ℤ → (1...(⌊‘𝐴)) = (1...𝐴))
32sumeq1d 15736 . . 3 (𝐴 ∈ ℤ → Σ𝑛 ∈ (1...(⌊‘𝐴))(((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) = Σ𝑛 ∈ (1...𝐴)(((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛))
4 fveq2 6906 . . . . . 6 (𝑛 = (𝑝𝑘) → (Λ‘𝑛) = (Λ‘(𝑝𝑘)))
5 eleq1 2829 . . . . . . 7 (𝑛 = (𝑝𝑘) → (𝑛 ∈ ℙ ↔ (𝑝𝑘) ∈ ℙ))
6 fveq2 6906 . . . . . . 7 (𝑛 = (𝑝𝑘) → (log‘𝑛) = (log‘(𝑝𝑘)))
75, 6ifbieq1d 4550 . . . . . 6 (𝑛 = (𝑝𝑘) → if(𝑛 ∈ ℙ, (log‘𝑛), 0) = if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0))
84, 7oveq12d 7449 . . . . 5 (𝑛 = (𝑝𝑘) → ((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) = ((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)))
9 id 22 . . . . 5 (𝑛 = (𝑝𝑘) → 𝑛 = (𝑝𝑘))
108, 9oveq12d 7449 . . . 4 (𝑛 = (𝑝𝑘) → (((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) = (((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)))
11 zre 12617 . . . 4 (𝐴 ∈ ℤ → 𝐴 ∈ ℝ)
12 elfznn 13593 . . . . . . . . 9 (𝑛 ∈ (1...(⌊‘𝐴)) → 𝑛 ∈ ℕ)
1312adantl 481 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝑛 ∈ ℕ)
14 vmacl 27161 . . . . . . . 8 (𝑛 ∈ ℕ → (Λ‘𝑛) ∈ ℝ)
1513, 14syl 17 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (Λ‘𝑛) ∈ ℝ)
1613nnrpd 13075 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝑛 ∈ ℝ+)
1716relogcld 26665 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (log‘𝑛) ∈ ℝ)
18 0re 11263 . . . . . . . 8 0 ∈ ℝ
19 ifcl 4571 . . . . . . . 8 (((log‘𝑛) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑛 ∈ ℙ, (log‘𝑛), 0) ∈ ℝ)
2017, 18, 19sylancl 586 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → if(𝑛 ∈ ℙ, (log‘𝑛), 0) ∈ ℝ)
2115, 20resubcld 11691 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → ((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) ∈ ℝ)
2221, 13nndivred 12320 . . . . 5 ((𝐴 ∈ ℤ ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) ∈ ℝ)
2322recnd 11289 . . . 4 ((𝐴 ∈ ℤ ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) ∈ ℂ)
24 simprr 773 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (Λ‘𝑛) = 0)) → (Λ‘𝑛) = 0)
25 vmaprm 27160 . . . . . . . . . . . . 13 (𝑛 ∈ ℙ → (Λ‘𝑛) = (log‘𝑛))
26 prmnn 16711 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℙ → 𝑛 ∈ ℕ)
2726nnred 12281 . . . . . . . . . . . . . 14 (𝑛 ∈ ℙ → 𝑛 ∈ ℝ)
28 prmgt1 16734 . . . . . . . . . . . . . 14 (𝑛 ∈ ℙ → 1 < 𝑛)
2927, 28rplogcld 26671 . . . . . . . . . . . . 13 (𝑛 ∈ ℙ → (log‘𝑛) ∈ ℝ+)
3025, 29eqeltrd 2841 . . . . . . . . . . . 12 (𝑛 ∈ ℙ → (Λ‘𝑛) ∈ ℝ+)
3130rpne0d 13082 . . . . . . . . . . 11 (𝑛 ∈ ℙ → (Λ‘𝑛) ≠ 0)
3231necon2bi 2971 . . . . . . . . . 10 ((Λ‘𝑛) = 0 → ¬ 𝑛 ∈ ℙ)
3332ad2antll 729 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (Λ‘𝑛) = 0)) → ¬ 𝑛 ∈ ℙ)
3433iffalsed 4536 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (Λ‘𝑛) = 0)) → if(𝑛 ∈ ℙ, (log‘𝑛), 0) = 0)
3524, 34oveq12d 7449 . . . . . . 7 ((𝐴 ∈ ℤ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (Λ‘𝑛) = 0)) → ((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) = (0 − 0))
36 0m0e0 12386 . . . . . . 7 (0 − 0) = 0
3735, 36eqtrdi 2793 . . . . . 6 ((𝐴 ∈ ℤ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (Λ‘𝑛) = 0)) → ((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) = 0)
3837oveq1d 7446 . . . . 5 ((𝐴 ∈ ℤ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (Λ‘𝑛) = 0)) → (((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) = (0 / 𝑛))
3912ad2antrl 728 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (Λ‘𝑛) = 0)) → 𝑛 ∈ ℕ)
4039nnrpd 13075 . . . . . . 7 ((𝐴 ∈ ℤ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (Λ‘𝑛) = 0)) → 𝑛 ∈ ℝ+)
4140rpcnne0d 13086 . . . . . 6 ((𝐴 ∈ ℤ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (Λ‘𝑛) = 0)) → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0))
42 div0 11955 . . . . . 6 ((𝑛 ∈ ℂ ∧ 𝑛 ≠ 0) → (0 / 𝑛) = 0)
4341, 42syl 17 . . . . 5 ((𝐴 ∈ ℤ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (Λ‘𝑛) = 0)) → (0 / 𝑛) = 0)
4438, 43eqtrd 2777 . . . 4 ((𝐴 ∈ ℤ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (Λ‘𝑛) = 0)) → (((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) = 0)
4510, 11, 23, 44fsumvma2 27258 . . 3 (𝐴 ∈ ℤ → Σ𝑛 ∈ (1...(⌊‘𝐴))(((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)))
463, 45eqtr3d 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[,]𝐴) ∩ ℙ))
4948elin2d 4205 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℙ)
50 prmnn 16711 . . . . . . . . . . 11 (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
5149, 50syl 17 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℕ)
5251nnred 12281 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℝ)
5311adantr 480 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝐴 ∈ ℝ)
54 zcn 12618 . . . . . . . . . . . 12 (𝐴 ∈ ℤ → 𝐴 ∈ ℂ)
5554abscld 15475 . . . . . . . . . . 11 (𝐴 ∈ ℤ → (abs‘𝐴) ∈ ℝ)
56 peano2re 11434 . . . . . . . . . . 11 ((abs‘𝐴) ∈ ℝ → ((abs‘𝐴) + 1) ∈ ℝ)
5755, 56syl 17 . . . . . . . . . 10 (𝐴 ∈ ℤ → ((abs‘𝐴) + 1) ∈ ℝ)
5857adantr 480 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((abs‘𝐴) + 1) ∈ ℝ)
59 elinel1 4201 . . . . . . . . . . . 12 (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) → 𝑝 ∈ (0[,]𝐴))
60 elicc2 13452 . . . . . . . . . . . . 13 ((0 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝑝 ∈ (0[,]𝐴) ↔ (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝𝑝𝐴)))
6118, 11, 60sylancr 587 . . . . . . . . . . . 12 (𝐴 ∈ ℤ → (𝑝 ∈ (0[,]𝐴) ↔ (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝𝑝𝐴)))
6259, 61imbitrid 244 . . . . . . . . . . 11 (𝐴 ∈ ℤ → (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) → (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝𝑝𝐴)))
6362imp 406 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝𝑝𝐴))
6463simp3d 1145 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝𝐴)
6554adantr 480 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝐴 ∈ ℂ)
6665abscld 15475 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (abs‘𝐴) ∈ ℝ)
6753leabsd 15453 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝐴 ≤ (abs‘𝐴))
6866lep1d 12199 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (abs‘𝐴) ≤ ((abs‘𝐴) + 1))
6953, 66, 58, 67, 68letrd 11418 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝐴 ≤ ((abs‘𝐴) + 1))
7052, 53, 58, 64, 69letrd 11418 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ≤ ((abs‘𝐴) + 1))
71 prmuz2 16733 . . . . . . . . . 10 (𝑝 ∈ ℙ → 𝑝 ∈ (ℤ‘2))
7249, 71syl 17 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ (ℤ‘2))
73 nn0abscl 15351 . . . . . . . . . . . 12 (𝐴 ∈ ℤ → (abs‘𝐴) ∈ ℕ0)
74 nn0p1nn 12565 . . . . . . . . . . . 12 ((abs‘𝐴) ∈ ℕ0 → ((abs‘𝐴) + 1) ∈ ℕ)
7573, 74syl 17 . . . . . . . . . . 11 (𝐴 ∈ ℤ → ((abs‘𝐴) + 1) ∈ ℕ)
7675nnzd 12640 . . . . . . . . . 10 (𝐴 ∈ ℤ → ((abs‘𝐴) + 1) ∈ ℤ)
7776adantr 480 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((abs‘𝐴) + 1) ∈ ℤ)
78 elfz5 13556 . . . . . . . . 9 ((𝑝 ∈ (ℤ‘2) ∧ ((abs‘𝐴) + 1) ∈ ℤ) → (𝑝 ∈ (2...((abs‘𝐴) + 1)) ↔ 𝑝 ≤ ((abs‘𝐴) + 1)))
7972, 77, 78syl2anc 584 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 ∈ (2...((abs‘𝐴) + 1)) ↔ 𝑝 ≤ ((abs‘𝐴) + 1)))
8070, 79mpbird 257 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ (2...((abs‘𝐴) + 1)))
8180ex 412 . . . . . 6 (𝐴 ∈ ℤ → (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) → 𝑝 ∈ (2...((abs‘𝐴) + 1))))
8281ssrdv 3989 . . . . 5 (𝐴 ∈ ℤ → ((0[,]𝐴) ∩ ℙ) ⊆ (2...((abs‘𝐴) + 1)))
8347, 82ssfid 9301 . . . 4 (𝐴 ∈ ℤ → ((0[,]𝐴) ∩ ℙ) ∈ Fin)
84 fzfid 14014 . . . . 5 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1...(⌊‘((log‘𝐴) / (log‘𝑝)))) ∈ Fin)
85 simprl 771 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → 𝑝 ∈ ((0[,]𝐴) ∩ ℙ))
8685elin2d 4205 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → 𝑝 ∈ ℙ)
87 elfznn 13593 . . . . . . . . . . 11 (𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))) → 𝑘 ∈ ℕ)
8887ad2antll 729 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → 𝑘 ∈ ℕ)
89 vmappw 27159 . . . . . . . . . 10 ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) → (Λ‘(𝑝𝑘)) = (log‘𝑝))
9086, 88, 89syl2anc 584 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → (Λ‘(𝑝𝑘)) = (log‘𝑝))
9151adantrr 717 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → 𝑝 ∈ ℕ)
9291nnrpd 13075 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → 𝑝 ∈ ℝ+)
9392relogcld 26665 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → (log‘𝑝) ∈ ℝ)
9490, 93eqeltrd 2841 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → (Λ‘(𝑝𝑘)) ∈ ℝ)
9588nnnn0d 12587 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → 𝑘 ∈ ℕ0)
96 nnexpcl 14115 . . . . . . . . . . . 12 ((𝑝 ∈ ℕ ∧ 𝑘 ∈ ℕ0) → (𝑝𝑘) ∈ ℕ)
9791, 95, 96syl2anc 584 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → (𝑝𝑘) ∈ ℕ)
9897nnrpd 13075 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → (𝑝𝑘) ∈ ℝ+)
9998relogcld 26665 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → (log‘(𝑝𝑘)) ∈ ℝ)
100 ifcl 4571 . . . . . . . . 9 (((log‘(𝑝𝑘)) ∈ ℝ ∧ 0 ∈ ℝ) → if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0) ∈ ℝ)
10199, 18, 100sylancl 586 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0) ∈ ℝ)
10294, 101resubcld 11691 . . . . . . 7 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → ((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) ∈ ℝ)
103102, 97nndivred 12320 . . . . . 6 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → (((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)) ∈ ℝ)
104103anassrs 467 . . . . 5 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) → (((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)) ∈ ℝ)
10584, 104fsumrecl 15770 . . . 4 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)) ∈ ℝ)
10683, 105fsumrecl 15770 . . 3 (𝐴 ∈ ℤ → Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)) ∈ ℝ)
10751nnrpd 13075 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℝ+)
108107relogcld 26665 . . . . 5 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈ ℝ)
109 uz2m1nn 12965 . . . . . . 7 (𝑝 ∈ (ℤ‘2) → (𝑝 − 1) ∈ ℕ)
11072, 109syl 17 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 − 1) ∈ ℕ)
11151, 110nnmulcld 12319 . . . . 5 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 · (𝑝 − 1)) ∈ ℕ)
112108, 111nndivred 12320 . . . 4 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) / (𝑝 · (𝑝 − 1))) ∈ ℝ)
11383, 112fsumrecl 15770 . . 3 (𝐴 ∈ ℤ → Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)((log‘𝑝) / (𝑝 · (𝑝 − 1))) ∈ ℝ)
114 2re 12340 . . . 4 2 ∈ ℝ
115114a1i 11 . . 3 (𝐴 ∈ ℤ → 2 ∈ ℝ)
11618a1i 11 . . . . . . . . . . . . 13 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 0 ∈ ℝ)
11751nngt0d 12315 . . . . . . . . . . . . 13 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 0 < 𝑝)
118116, 52, 53, 117, 64ltletrd 11421 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 0 < 𝐴)
11953, 118elrpd 13074 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝐴 ∈ ℝ+)
120119relogcld 26665 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝐴) ∈ ℝ)
121 prmgt1 16734 . . . . . . . . . . . 12 (𝑝 ∈ ℙ → 1 < 𝑝)
12249, 121syl 17 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 1 < 𝑝)
12352, 122rplogcld 26671 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈ ℝ+)
124120, 123rerpdivcld 13108 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝐴) / (log‘𝑝)) ∈ ℝ)
125123rpcnd 13079 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈ ℂ)
126125mullidd 11279 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 · (log‘𝑝)) = (log‘𝑝))
127107, 119logled 26669 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝𝐴 ↔ (log‘𝑝) ≤ (log‘𝐴)))
12864, 127mpbid 232 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ≤ (log‘𝐴))
129126, 128eqbrtrd 5165 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 · (log‘𝑝)) ≤ (log‘𝐴))
130 1re 11261 . . . . . . . . . . . 12 1 ∈ ℝ
131130a1i 11 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 1 ∈ ℝ)
132131, 120, 123lemuldivd 13126 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 · (log‘𝑝)) ≤ (log‘𝐴) ↔ 1 ≤ ((log‘𝐴) / (log‘𝑝))))
133129, 132mpbid 232 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 1 ≤ ((log‘𝐴) / (log‘𝑝)))
134 flge1nn 13861 . . . . . . . . 9 ((((log‘𝐴) / (log‘𝑝)) ∈ ℝ ∧ 1 ≤ ((log‘𝐴) / (log‘𝑝))) → (⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℕ)
135124, 133, 134syl2anc 584 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℕ)
136 nnuz 12921 . . . . . . . 8 ℕ = (ℤ‘1)
137135, 136eleqtrdi 2851 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (⌊‘((log‘𝐴) / (log‘𝑝))) ∈ (ℤ‘1))
138103recnd 11289 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → (((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)) ∈ ℂ)
139138anassrs 467 . . . . . . 7 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) → (((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)) ∈ ℂ)
140 oveq2 7439 . . . . . . . . . 10 (𝑘 = 1 → (𝑝𝑘) = (𝑝↑1))
141140fveq2d 6910 . . . . . . . . 9 (𝑘 = 1 → (Λ‘(𝑝𝑘)) = (Λ‘(𝑝↑1)))
142140eleq1d 2826 . . . . . . . . . 10 (𝑘 = 1 → ((𝑝𝑘) ∈ ℙ ↔ (𝑝↑1) ∈ ℙ))
143140fveq2d 6910 . . . . . . . . . 10 (𝑘 = 1 → (log‘(𝑝𝑘)) = (log‘(𝑝↑1)))
144142, 143ifbieq1d 4550 . . . . . . . . 9 (𝑘 = 1 → if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0) = if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0))
145141, 144oveq12d 7449 . . . . . . . 8 (𝑘 = 1 → ((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) = ((Λ‘(𝑝↑1)) − if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0)))
146145, 140oveq12d 7449 . . . . . . 7 (𝑘 = 1 → (((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)) = (((Λ‘(𝑝↑1)) − if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0)) / (𝑝↑1)))
147137, 139, 146fsum1p 15789 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)) = ((((Λ‘(𝑝↑1)) − if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0)) / (𝑝↑1)) + Σ𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘))))
14851nncnd 12282 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℂ)
149148exp1d 14181 . . . . . . . . . . . . 13 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝↑1) = 𝑝)
150149fveq2d 6910 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (Λ‘(𝑝↑1)) = (Λ‘𝑝))
151 vmaprm 27160 . . . . . . . . . . . . 13 (𝑝 ∈ ℙ → (Λ‘𝑝) = (log‘𝑝))
15249, 151syl 17 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (Λ‘𝑝) = (log‘𝑝))
153150, 152eqtrd 2777 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (Λ‘(𝑝↑1)) = (log‘𝑝))
154149, 49eqeltrd 2841 . . . . . . . . . . . . 13 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝↑1) ∈ ℙ)
155154iftrued 4533 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0) = (log‘(𝑝↑1)))
156149fveq2d 6910 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘(𝑝↑1)) = (log‘𝑝))
157155, 156eqtrd 2777 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0) = (log‘𝑝))
158153, 157oveq12d 7449 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((Λ‘(𝑝↑1)) − if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0)) = ((log‘𝑝) − (log‘𝑝)))
159125subidd 11608 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) − (log‘𝑝)) = 0)
160158, 159eqtrd 2777 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((Λ‘(𝑝↑1)) − if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0)) = 0)
161160, 149oveq12d 7449 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((Λ‘(𝑝↑1)) − if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0)) / (𝑝↑1)) = (0 / 𝑝))
162107rpcnne0d 13086 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 ∈ ℂ ∧ 𝑝 ≠ 0))
163 div0 11955 . . . . . . . . 9 ((𝑝 ∈ ℂ ∧ 𝑝 ≠ 0) → (0 / 𝑝) = 0)
164162, 163syl 17 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (0 / 𝑝) = 0)
165161, 164eqtrd 2777 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((Λ‘(𝑝↑1)) − if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0)) / (𝑝↑1)) = 0)
166 1p1e2 12391 . . . . . . . . . 10 (1 + 1) = 2
167166oveq1i 7441 . . . . . . . . 9 ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝)))) = (2...(⌊‘((log‘𝐴) / (log‘𝑝))))
168167a1i 11 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝)))) = (2...(⌊‘((log‘𝐴) / (log‘𝑝)))))
169 elfzuz 13560 . . . . . . . . . . . . . 14 (𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝)))) → 𝑘 ∈ (ℤ‘2))
170 eluz2nn 12924 . . . . . . . . . . . . . 14 (𝑘 ∈ (ℤ‘2) → 𝑘 ∈ ℕ)
171169, 170syl 17 . . . . . . . . . . . . 13 (𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝)))) → 𝑘 ∈ ℕ)
172171, 167eleq2s 2859 . . . . . . . . . . . 12 (𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝)))) → 𝑘 ∈ ℕ)
17349, 172, 89syl2an 596 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → (Λ‘(𝑝𝑘)) = (log‘𝑝))
17451adantr 480 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → 𝑝 ∈ ℕ)
175 nnq 13004 . . . . . . . . . . . . . 14 (𝑝 ∈ ℕ → 𝑝 ∈ ℚ)
176174, 175syl 17 . . . . . . . . . . . . 13 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → 𝑝 ∈ ℚ)
177169, 167eleq2s 2859 . . . . . . . . . . . . . 14 (𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝)))) → 𝑘 ∈ (ℤ‘2))
178177adantl 481 . . . . . . . . . . . . 13 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → 𝑘 ∈ (ℤ‘2))
179 expnprm 16940 . . . . . . . . . . . . 13 ((𝑝 ∈ ℚ ∧ 𝑘 ∈ (ℤ‘2)) → ¬ (𝑝𝑘) ∈ ℙ)
180176, 178, 179syl2anc 584 . . . . . . . . . . . 12 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → ¬ (𝑝𝑘) ∈ ℙ)
181180iffalsed 4536 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0) = 0)
182173, 181oveq12d 7449 . . . . . . . . . 10 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → ((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) = ((log‘𝑝) − 0))
183125subid1d 11609 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) − 0) = (log‘𝑝))
184183adantr 480 . . . . . . . . . 10 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → ((log‘𝑝) − 0) = (log‘𝑝))
185182, 184eqtrd 2777 . . . . . . . . 9 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → ((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) = (log‘𝑝))
186185oveq1d 7446 . . . . . . . 8 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → (((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)) = ((log‘𝑝) / (𝑝𝑘)))
187168, 186sumeq12dv 15742 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)) = Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝𝑘)))
188165, 187oveq12d 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)
190108adantr 480 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → (log‘𝑝) ∈ ℝ)
191 nnnn0 12533 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
19251, 191, 96syl2an 596 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → (𝑝𝑘) ∈ ℕ)
193190, 192nndivred 12320 . . . . . . . . . 10 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → ((log‘𝑝) / (𝑝𝑘)) ∈ ℝ)
194171, 193sylan2 593 . . . . . . . . 9 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))) → ((log‘𝑝) / (𝑝𝑘)) ∈ ℝ)
195189, 194fsumrecl 15770 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝𝑘)) ∈ ℝ)
196195recnd 11289 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝𝑘)) ∈ ℂ)
197196addlidd 11462 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (0 + Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝𝑘))) = Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝𝑘)))
198147, 188, 1973eqtrd 2781 . . . . 5 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)) = Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝𝑘)))
199107rpreccld 13087 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 / 𝑝) ∈ ℝ+)
200124flcld 13838 . . . . . . . . . . . . 13 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℤ)
201200peano2zd 12725 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((⌊‘((log‘𝐴) / (log‘𝑝))) + 1) ∈ ℤ)
202199, 201rpexpcld 14286 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1)) ∈ ℝ+)
203202rpge0d 13081 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 0 ≤ ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1)))
20451nnrecred 12317 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 / 𝑝) ∈ ℝ)
205204resqcld 14165 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 / 𝑝)↑2) ∈ ℝ)
206135peano2nnd 12283 . . . . . . . . . . . . 13 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((⌊‘((log‘𝐴) / (log‘𝑝))) + 1) ∈ ℕ)
207206nnnn0d 12587 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((⌊‘((log‘𝐴) / (log‘𝑝))) + 1) ∈ ℕ0)
208204, 207reexpcld 14203 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1)) ∈ ℝ)
209205, 208subge02d 11855 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (0 ≤ ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1)) ↔ (((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) ≤ ((1 / 𝑝)↑2)))
210203, 209mpbid 232 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) ≤ ((1 / 𝑝)↑2))
211110nnrpd 13075 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 − 1) ∈ ℝ+)
212211rpcnne0d 13086 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((𝑝 − 1) ∈ ℂ ∧ (𝑝 − 1) ≠ 0))
213199rpcnd 13079 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 / 𝑝) ∈ ℂ)
214 dmdcan 11977 . . . . . . . . . . 11 ((((𝑝 − 1) ∈ ℂ ∧ (𝑝 − 1) ≠ 0) ∧ (𝑝 ∈ ℂ ∧ 𝑝 ≠ 0) ∧ (1 / 𝑝) ∈ ℂ) → (((𝑝 − 1) / 𝑝) · ((1 / 𝑝) / (𝑝 − 1))) = ((1 / 𝑝) / 𝑝))
215212, 162, 213, 214syl3anc 1373 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((𝑝 − 1) / 𝑝) · ((1 / 𝑝) / (𝑝 − 1))) = ((1 / 𝑝) / 𝑝))
216131recnd 11289 . . . . . . . . . . . . 13 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 1 ∈ ℂ)
217 divsubdir 11961 . . . . . . . . . . . . 13 ((𝑝 ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝑝 ∈ ℂ ∧ 𝑝 ≠ 0)) → ((𝑝 − 1) / 𝑝) = ((𝑝 / 𝑝) − (1 / 𝑝)))
218148, 216, 162, 217syl3anc 1373 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((𝑝 − 1) / 𝑝) = ((𝑝 / 𝑝) − (1 / 𝑝)))
219 divid 11953 . . . . . . . . . . . . . 14 ((𝑝 ∈ ℂ ∧ 𝑝 ≠ 0) → (𝑝 / 𝑝) = 1)
220162, 219syl 17 . . . . . . . . . . . . 13 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 / 𝑝) = 1)
221220oveq1d 7446 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((𝑝 / 𝑝) − (1 / 𝑝)) = (1 − (1 / 𝑝)))
222218, 221eqtrd 2777 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((𝑝 − 1) / 𝑝) = (1 − (1 / 𝑝)))
223 divdiv1 11978 . . . . . . . . . . . 12 ((1 ∈ ℂ ∧ (𝑝 ∈ ℂ ∧ 𝑝 ≠ 0) ∧ ((𝑝 − 1) ∈ ℂ ∧ (𝑝 − 1) ≠ 0)) → ((1 / 𝑝) / (𝑝 − 1)) = (1 / (𝑝 · (𝑝 − 1))))
224216, 162, 212, 223syl3anc 1373 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 / 𝑝) / (𝑝 − 1)) = (1 / (𝑝 · (𝑝 − 1))))
225222, 224oveq12d 7449 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((𝑝 − 1) / 𝑝) · ((1 / 𝑝) / (𝑝 − 1))) = ((1 − (1 / 𝑝)) · (1 / (𝑝 · (𝑝 − 1)))))
22651nnne0d 12316 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ≠ 0)
227213, 148, 226divrecd 12046 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 / 𝑝) / 𝑝) = ((1 / 𝑝) · (1 / 𝑝)))
228213sqvald 14183 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 / 𝑝)↑2) = ((1 / 𝑝) · (1 / 𝑝)))
229227, 228eqtr4d 2780 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 / 𝑝) / 𝑝) = ((1 / 𝑝)↑2))
230215, 225, 2293eqtr3d 2785 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 − (1 / 𝑝)) · (1 / (𝑝 · (𝑝 − 1)))) = ((1 / 𝑝)↑2))
231210, 230breqtrrd 5171 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) ≤ ((1 − (1 / 𝑝)) · (1 / (𝑝 · (𝑝 − 1)))))
232205, 208resubcld 11691 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) ∈ ℝ)
233111nnrecred 12317 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 / (𝑝 · (𝑝 − 1))) ∈ ℝ)
234 resubcl 11573 . . . . . . . . . 10 ((1 ∈ ℝ ∧ (1 / 𝑝) ∈ ℝ) → (1 − (1 / 𝑝)) ∈ ℝ)
235130, 204, 234sylancr 587 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 − (1 / 𝑝)) ∈ ℝ)
236 recgt1 12164 . . . . . . . . . . . 12 ((𝑝 ∈ ℝ ∧ 0 < 𝑝) → (1 < 𝑝 ↔ (1 / 𝑝) < 1))
23752, 117, 236syl2anc 584 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 < 𝑝 ↔ (1 / 𝑝) < 1))
238122, 237mpbid 232 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 / 𝑝) < 1)
239 posdif 11756 . . . . . . . . . . 11 (((1 / 𝑝) ∈ ℝ ∧ 1 ∈ ℝ) → ((1 / 𝑝) < 1 ↔ 0 < (1 − (1 / 𝑝))))
240204, 130, 239sylancl 586 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 / 𝑝) < 1 ↔ 0 < (1 − (1 / 𝑝))))
241238, 240mpbid 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))))))
243232, 233, 235, 241, 242syl112anc 1376 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 / 𝑝))) ≤ (1 / (𝑝 · (𝑝 − 1))) ↔ (((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) ≤ ((1 − (1 / 𝑝)) · (1 / (𝑝 · (𝑝 − 1))))))
244231, 243mpbird 257 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 / 𝑝))) ≤ (1 / (𝑝 · (𝑝 − 1))))
245235, 241elrpd 13074 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 − (1 / 𝑝)) ∈ ℝ+)
246232, 245rerpdivcld 13108 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 / 𝑝))) ∈ ℝ)
247246, 233, 123lemul2d 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))))))
248244, 247mpbid 232 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) · ((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 / 𝑝)))) ≤ ((log‘𝑝) · (1 / (𝑝 · (𝑝 − 1)))))
249125adantr 480 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → (log‘𝑝) ∈ ℂ)
250192nncnd 12282 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → (𝑝𝑘) ∈ ℂ)
251192nnne0d 12316 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → (𝑝𝑘) ≠ 0)
252249, 250, 251divrecd 12046 . . . . . . . . . 10 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → ((log‘𝑝) / (𝑝𝑘)) = ((log‘𝑝) · (1 / (𝑝𝑘))))
253148adantr 480 . . . . . . . . . . . 12 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → 𝑝 ∈ ℂ)
25451adantr 480 . . . . . . . . . . . . 13 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → 𝑝 ∈ ℕ)
255254nnne0d 12316 . . . . . . . . . . . 12 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → 𝑝 ≠ 0)
256 nnz 12634 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
257256adantl 481 . . . . . . . . . . . 12 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℤ)
258253, 255, 257exprecd 14194 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → ((1 / 𝑝)↑𝑘) = (1 / (𝑝𝑘)))
259258oveq2d 7447 . . . . . . . . . 10 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → ((log‘𝑝) · ((1 / 𝑝)↑𝑘)) = ((log‘𝑝) · (1 / (𝑝𝑘))))
260252, 259eqtr4d 2780 . . . . . . . . 9 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → ((log‘𝑝) / (𝑝𝑘)) = ((log‘𝑝) · ((1 / 𝑝)↑𝑘)))
261171, 260sylan2 593 . . . . . . . 8 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))) → ((log‘𝑝) / (𝑝𝑘)) = ((log‘𝑝) · ((1 / 𝑝)↑𝑘)))
262261sumeq2dv 15738 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝𝑘)) = Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) · ((1 / 𝑝)↑𝑘)))
263171nnnn0d 12587 . . . . . . . . 9 (𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝)))) → 𝑘 ∈ ℕ0)
264 expcl 14120 . . . . . . . . 9 (((1 / 𝑝) ∈ ℂ ∧ 𝑘 ∈ ℕ0) → ((1 / 𝑝)↑𝑘) ∈ ℂ)
265213, 263, 264syl2an 596 . . . . . . . 8 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))) → ((1 / 𝑝)↑𝑘) ∈ ℂ)
266189, 125, 265fsummulc2 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)))
268200, 267syl 17 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (2...(⌊‘((log‘𝐴) / (log‘𝑝)))) = (2..^((⌊‘((log‘𝐴) / (log‘𝑝))) + 1)))
269268sumeq1d 15736 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((1 / 𝑝)↑𝑘) = Σ𝑘 ∈ (2..^((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))((1 / 𝑝)↑𝑘))
270204, 238ltned 11397 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 / 𝑝) ≠ 1)
271 2nn0 12543 . . . . . . . . . . 11 2 ∈ ℕ0
272271a1i 11 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 2 ∈ ℕ0)
273 eluzp1p1 12906 . . . . . . . . . . . 12 ((⌊‘((log‘𝐴) / (log‘𝑝))) ∈ (ℤ‘1) → ((⌊‘((log‘𝐴) / (log‘𝑝))) + 1) ∈ (ℤ‘(1 + 1)))
274137, 273syl 17 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((⌊‘((log‘𝐴) / (log‘𝑝))) + 1) ∈ (ℤ‘(1 + 1)))
275 df-2 12329 . . . . . . . . . . . 12 2 = (1 + 1)
276275fveq2i 6909 . . . . . . . . . . 11 (ℤ‘2) = (ℤ‘(1 + 1))
277274, 276eleqtrrdi 2852 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((⌊‘((log‘𝐴) / (log‘𝑝))) + 1) ∈ (ℤ‘2))
278213, 270, 272, 277geoserg 15902 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈ (2..^((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))((1 / 𝑝)↑𝑘) = ((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 / 𝑝))))
279269, 278eqtrd 2777 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((1 / 𝑝)↑𝑘) = ((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 / 𝑝))))
280279oveq2d 7447 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) · Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((1 / 𝑝)↑𝑘)) = ((log‘𝑝) · ((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 / 𝑝)))))
281262, 266, 2803eqtr2d 2783 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝𝑘)) = ((log‘𝑝) · ((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 / 𝑝)))))
282111nncnd 12282 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 · (𝑝 − 1)) ∈ ℂ)
283111nnne0d 12316 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 · (𝑝 − 1)) ≠ 0)
284125, 282, 283divrecd 12046 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) / (𝑝 · (𝑝 − 1))) = ((log‘𝑝) · (1 / (𝑝 · (𝑝 − 1)))))
285248, 281, 2843brtr4d 5175 . . . . 5 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝𝑘)) ≤ ((log‘𝑝) / (𝑝 · (𝑝 − 1))))
286198, 285eqbrtrd 5165 . . . 4 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)) ≤ ((log‘𝑝) / (𝑝 · (𝑝 − 1))))
28783, 105, 112, 286fsumle 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) → 𝑝 ∈ ℕ)
290288, 289syl 17 . . . . . . . . . 10 (𝑝 ∈ (2...((abs‘𝐴) + 1)) → 𝑝 ∈ ℕ)
291290adantl 481 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → 𝑝 ∈ ℕ)
292291nnred 12281 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → 𝑝 ∈ ℝ)
293288adantl 481 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → 𝑝 ∈ (ℤ‘2))
294 eluz2gt1 12962 . . . . . . . . 9 (𝑝 ∈ (ℤ‘2) → 1 < 𝑝)
295293, 294syl 17 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → 1 < 𝑝)
296292, 295rplogcld 26671 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → (log‘𝑝) ∈ ℝ+)
297293, 109syl 17 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → (𝑝 − 1) ∈ ℕ)
298291, 297nnmulcld 12319 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → (𝑝 · (𝑝 − 1)) ∈ ℕ)
299298nnrpd 13075 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → (𝑝 · (𝑝 − 1)) ∈ ℝ+)
300296, 299rpdivcld 13094 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → ((log‘𝑝) / (𝑝 · (𝑝 − 1))) ∈ ℝ+)
301300rpred 13077 . . . . 5 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → ((log‘𝑝) / (𝑝 · (𝑝 − 1))) ∈ ℝ)
30247, 301fsumrecl 15770 . . . 4 (𝐴 ∈ ℤ → Σ𝑝 ∈ (2...((abs‘𝐴) + 1))((log‘𝑝) / (𝑝 · (𝑝 − 1))) ∈ ℝ)
303300rpge0d 13081 . . . . 5 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → 0 ≤ ((log‘𝑝) / (𝑝 · (𝑝 − 1))))
30447, 301, 303, 82fsumless 15832 . . . 4 (𝐴 ∈ ℤ → Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)((log‘𝑝) / (𝑝 · (𝑝 − 1))) ≤ Σ𝑝 ∈ (2...((abs‘𝐴) + 1))((log‘𝑝) / (𝑝 · (𝑝 − 1))))
305 rplogsumlem1 27528 . . . . 5 (((abs‘𝐴) + 1) ∈ ℕ → Σ𝑝 ∈ (2...((abs‘𝐴) + 1))((log‘𝑝) / (𝑝 · (𝑝 − 1))) ≤ 2)
30675, 305syl 17 . . . 4 (𝐴 ∈ ℤ → Σ𝑝 ∈ (2...((abs‘𝐴) + 1))((log‘𝑝) / (𝑝 · (𝑝 − 1))) ≤ 2)
307113, 302, 115, 304, 306letrd 11418 . . 3 (𝐴 ∈ ℤ → Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)((log‘𝑝) / (𝑝 · (𝑝 − 1))) ≤ 2)
308106, 113, 115, 287, 307letrd 11418 . 2 (𝐴 ∈ ℤ → Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)) ≤ 2)
30946, 308eqbrtrd 5165 1 (𝐴 ∈ ℤ → Σ𝑛 ∈ (1...𝐴)(((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) ≤ 2)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1087   = wceq 1540  wcel 2108  wne 2940  cin 3950  ifcif 4525   class class class wbr 5143  cfv 6561  (class class class)co 7431  cc 11153  cr 11154  0cc0 11155  1c1 11156   + caddc 11158   · cmul 11160   < clt 11295  cle 11296  cmin 11492   / cdiv 11920  cn 12266  2c2 12321  0cn0 12526  cz 12613  cuz 12878  cq 12990  +crp 13034  [,]cicc 13390  ...cfz 13547  ..^cfzo 13694  cfl 13830  cexp 14102  abscabs 15273  Σcsu 15722  cprime 16708  logclog 26596  Λcvma 27135
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233  ax-addf 11234
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-iin 4994  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-om 7888  df-1st 8014  df-2nd 8015  df-supp 8186  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-oadd 8510  df-er 8745  df-map 8868  df-pm 8869  df-ixp 8938  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-fsupp 9402  df-fi 9451  df-sup 9482  df-inf 9483  df-oi 9550  df-dju 9941  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333  df-7 12334  df-8 12335  df-9 12336  df-n0 12527  df-z 12614  df-dec 12734  df-uz 12879  df-q 12991  df-rp 13035  df-xneg 13154  df-xadd 13155  df-xmul 13156  df-ioo 13391  df-ioc 13392  df-ico 13393  df-icc 13394  df-fz 13548  df-fzo 13695  df-fl 13832  df-mod 13910  df-seq 14043  df-exp 14103  df-fac 14313  df-bc 14342  df-hash 14370  df-shft 15106  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-limsup 15507  df-clim 15524  df-rlim 15525  df-sum 15723  df-ef 16103  df-sin 16105  df-cos 16106  df-tan 16107  df-pi 16108  df-dvds 16291  df-gcd 16532  df-prm 16709  df-pc 16875  df-struct 17184  df-sets 17201  df-slot 17219  df-ndx 17231  df-base 17248  df-ress 17275  df-plusg 17310  df-mulr 17311  df-starv 17312  df-sca 17313  df-vsca 17314  df-ip 17315  df-tset 17316  df-ple 17317  df-ds 17319  df-unif 17320  df-hom 17321  df-cco 17322  df-rest 17467  df-topn 17468  df-0g 17486  df-gsum 17487  df-topgen 17488  df-pt 17489  df-prds 17492  df-xrs 17547  df-qtop 17552  df-imas 17553  df-xps 17555  df-mre 17629  df-mrc 17630  df-acs 17632  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-submnd 18797  df-mulg 19086  df-cntz 19335  df-cmn 19800  df-psmet 21356  df-xmet 21357  df-met 21358  df-bl 21359  df-mopn 21360  df-fbas 21361  df-fg 21362  df-cnfld 21365  df-top 22900  df-topon 22917  df-topsp 22939  df-bases 22953  df-cld 23027  df-ntr 23028  df-cls 23029  df-nei 23106  df-lp 23144  df-perf 23145  df-cn 23235  df-cnp 23236  df-haus 23323  df-cmp 23395  df-tx 23570  df-hmeo 23763  df-fil 23854  df-fm 23946  df-flim 23947  df-flf 23948  df-xms 24330  df-ms 24331  df-tms 24332  df-cncf 24904  df-limc 25901  df-dv 25902  df-log 26598  df-cxp 26599  df-vma 27141
This theorem is referenced by:  rplogsum  27571
  Copyright terms: Public domain W3C validator