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

Theorem rplogsumlem2 26060
 Description: Lemma for rplogsum 26102. 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 13177 . . . . 5 (𝐴 ∈ ℤ → (⌊‘𝐴) = 𝐴)
21oveq2d 7171 . . . 4 (𝐴 ∈ ℤ → (1...(⌊‘𝐴)) = (1...𝐴))
32sumeq1d 15057 . . 3 (𝐴 ∈ ℤ → Σ𝑛 ∈ (1...(⌊‘𝐴))(((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) = Σ𝑛 ∈ (1...𝐴)(((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛))
4 fveq2 6669 . . . . . 6 (𝑛 = (𝑝𝑘) → (Λ‘𝑛) = (Λ‘(𝑝𝑘)))
5 eleq1 2900 . . . . . . 7 (𝑛 = (𝑝𝑘) → (𝑛 ∈ ℙ ↔ (𝑝𝑘) ∈ ℙ))
6 fveq2 6669 . . . . . . 7 (𝑛 = (𝑝𝑘) → (log‘𝑛) = (log‘(𝑝𝑘)))
75, 6ifbieq1d 4489 . . . . . 6 (𝑛 = (𝑝𝑘) → if(𝑛 ∈ ℙ, (log‘𝑛), 0) = if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0))
84, 7oveq12d 7173 . . . . 5 (𝑛 = (𝑝𝑘) → ((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) = ((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)))
9 id 22 . . . . 5 (𝑛 = (𝑝𝑘) → 𝑛 = (𝑝𝑘))
108, 9oveq12d 7173 . . . 4 (𝑛 = (𝑝𝑘) → (((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) = (((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)))
11 zre 11984 . . . 4 (𝐴 ∈ ℤ → 𝐴 ∈ ℝ)
12 elfznn 12935 . . . . . . . . 9 (𝑛 ∈ (1...(⌊‘𝐴)) → 𝑛 ∈ ℕ)
1312adantl 484 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝑛 ∈ ℕ)
14 vmacl 25694 . . . . . . . 8 (𝑛 ∈ ℕ → (Λ‘𝑛) ∈ ℝ)
1513, 14syl 17 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (Λ‘𝑛) ∈ ℝ)
1613nnrpd 12428 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝑛 ∈ ℝ+)
1716relogcld 25205 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (log‘𝑛) ∈ ℝ)
18 0re 10642 . . . . . . . 8 0 ∈ ℝ
19 ifcl 4510 . . . . . . . 8 (((log‘𝑛) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑛 ∈ ℙ, (log‘𝑛), 0) ∈ ℝ)
2017, 18, 19sylancl 588 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → if(𝑛 ∈ ℙ, (log‘𝑛), 0) ∈ ℝ)
2115, 20resubcld 11067 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → ((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) ∈ ℝ)
2221, 13nndivred 11690 . . . . 5 ((𝐴 ∈ ℤ ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) ∈ ℝ)
2322recnd 10668 . . . 4 ((𝐴 ∈ ℤ ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) ∈ ℂ)
24 simprr 771 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (Λ‘𝑛) = 0)) → (Λ‘𝑛) = 0)
25 vmaprm 25693 . . . . . . . . . . . . 13 (𝑛 ∈ ℙ → (Λ‘𝑛) = (log‘𝑛))
26 prmnn 16017 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℙ → 𝑛 ∈ ℕ)
2726nnred 11652 . . . . . . . . . . . . . 14 (𝑛 ∈ ℙ → 𝑛 ∈ ℝ)
28 prmgt1 16040 . . . . . . . . . . . . . 14 (𝑛 ∈ ℙ → 1 < 𝑛)
2927, 28rplogcld 25211 . . . . . . . . . . . . 13 (𝑛 ∈ ℙ → (log‘𝑛) ∈ ℝ+)
3025, 29eqeltrd 2913 . . . . . . . . . . . 12 (𝑛 ∈ ℙ → (Λ‘𝑛) ∈ ℝ+)
3130rpne0d 12435 . . . . . . . . . . 11 (𝑛 ∈ ℙ → (Λ‘𝑛) ≠ 0)
3231necon2bi 3046 . . . . . . . . . 10 ((Λ‘𝑛) = 0 → ¬ 𝑛 ∈ ℙ)
3332ad2antll 727 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (Λ‘𝑛) = 0)) → ¬ 𝑛 ∈ ℙ)
3433iffalsed 4477 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (Λ‘𝑛) = 0)) → if(𝑛 ∈ ℙ, (log‘𝑛), 0) = 0)
3524, 34oveq12d 7173 . . . . . . 7 ((𝐴 ∈ ℤ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (Λ‘𝑛) = 0)) → ((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) = (0 − 0))
36 0m0e0 11756 . . . . . . 7 (0 − 0) = 0
3735, 36syl6eq 2872 . . . . . 6 ((𝐴 ∈ ℤ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (Λ‘𝑛) = 0)) → ((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) = 0)
3837oveq1d 7170 . . . . 5 ((𝐴 ∈ ℤ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (Λ‘𝑛) = 0)) → (((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) = (0 / 𝑛))
3912ad2antrl 726 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (Λ‘𝑛) = 0)) → 𝑛 ∈ ℕ)
4039nnrpd 12428 . . . . . . 7 ((𝐴 ∈ ℤ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (Λ‘𝑛) = 0)) → 𝑛 ∈ ℝ+)
4140rpcnne0d 12439 . . . . . 6 ((𝐴 ∈ ℤ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (Λ‘𝑛) = 0)) → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0))
42 div0 11327 . . . . . 6 ((𝑛 ∈ ℂ ∧ 𝑛 ≠ 0) → (0 / 𝑛) = 0)
4341, 42syl 17 . . . . 5 ((𝐴 ∈ ℤ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (Λ‘𝑛) = 0)) → (0 / 𝑛) = 0)
4438, 43eqtrd 2856 . . . 4 ((𝐴 ∈ ℤ ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ (Λ‘𝑛) = 0)) → (((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) = 0)
4510, 11, 23, 44fsumvma2 25789 . . 3 (𝐴 ∈ ℤ → Σ𝑛 ∈ (1...(⌊‘𝐴))(((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)))
463, 45eqtr3d 2858 . 2 (𝐴 ∈ ℤ → Σ𝑛 ∈ (1...𝐴)(((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)))
47 fzfid 13340 . . . . 5 (𝐴 ∈ ℤ → (2...((abs‘𝐴) + 1)) ∈ Fin)
48 simpr 487 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ((0[,]𝐴) ∩ ℙ))
4948elin2d 4175 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℙ)
50 prmnn 16017 . . . . . . . . . . 11 (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
5149, 50syl 17 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℕ)
5251nnred 11652 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℝ)
5311adantr 483 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝐴 ∈ ℝ)
54 zcn 11985 . . . . . . . . . . . 12 (𝐴 ∈ ℤ → 𝐴 ∈ ℂ)
5554abscld 14795 . . . . . . . . . . 11 (𝐴 ∈ ℤ → (abs‘𝐴) ∈ ℝ)
56 peano2re 10812 . . . . . . . . . . 11 ((abs‘𝐴) ∈ ℝ → ((abs‘𝐴) + 1) ∈ ℝ)
5755, 56syl 17 . . . . . . . . . 10 (𝐴 ∈ ℤ → ((abs‘𝐴) + 1) ∈ ℝ)
5857adantr 483 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((abs‘𝐴) + 1) ∈ ℝ)
59 elinel1 4171 . . . . . . . . . . . 12 (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) → 𝑝 ∈ (0[,]𝐴))
60 elicc2 12800 . . . . . . . . . . . . 13 ((0 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝑝 ∈ (0[,]𝐴) ↔ (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝𝑝𝐴)))
6118, 11, 60sylancr 589 . . . . . . . . . . . 12 (𝐴 ∈ ℤ → (𝑝 ∈ (0[,]𝐴) ↔ (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝𝑝𝐴)))
6259, 61syl5ib 246 . . . . . . . . . . 11 (𝐴 ∈ ℤ → (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) → (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝𝑝𝐴)))
6362imp 409 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝𝑝𝐴))
6463simp3d 1140 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝𝐴)
6554adantr 483 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝐴 ∈ ℂ)
6665abscld 14795 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (abs‘𝐴) ∈ ℝ)
6753leabsd 14773 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝐴 ≤ (abs‘𝐴))
6866lep1d 11570 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (abs‘𝐴) ≤ ((abs‘𝐴) + 1))
6953, 66, 58, 67, 68letrd 10796 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝐴 ≤ ((abs‘𝐴) + 1))
7052, 53, 58, 64, 69letrd 10796 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ≤ ((abs‘𝐴) + 1))
71 prmuz2 16039 . . . . . . . . . 10 (𝑝 ∈ ℙ → 𝑝 ∈ (ℤ‘2))
7249, 71syl 17 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ (ℤ‘2))
73 nn0abscl 14671 . . . . . . . . . . . 12 (𝐴 ∈ ℤ → (abs‘𝐴) ∈ ℕ0)
74 nn0p1nn 11935 . . . . . . . . . . . 12 ((abs‘𝐴) ∈ ℕ0 → ((abs‘𝐴) + 1) ∈ ℕ)
7573, 74syl 17 . . . . . . . . . . 11 (𝐴 ∈ ℤ → ((abs‘𝐴) + 1) ∈ ℕ)
7675nnzd 12085 . . . . . . . . . 10 (𝐴 ∈ ℤ → ((abs‘𝐴) + 1) ∈ ℤ)
7776adantr 483 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((abs‘𝐴) + 1) ∈ ℤ)
78 elfz5 12899 . . . . . . . . 9 ((𝑝 ∈ (ℤ‘2) ∧ ((abs‘𝐴) + 1) ∈ ℤ) → (𝑝 ∈ (2...((abs‘𝐴) + 1)) ↔ 𝑝 ≤ ((abs‘𝐴) + 1)))
7972, 77, 78syl2anc 586 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 ∈ (2...((abs‘𝐴) + 1)) ↔ 𝑝 ≤ ((abs‘𝐴) + 1)))
8070, 79mpbird 259 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ (2...((abs‘𝐴) + 1)))
8180ex 415 . . . . . 6 (𝐴 ∈ ℤ → (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) → 𝑝 ∈ (2...((abs‘𝐴) + 1))))
8281ssrdv 3972 . . . . 5 (𝐴 ∈ ℤ → ((0[,]𝐴) ∩ ℙ) ⊆ (2...((abs‘𝐴) + 1)))
8347, 82ssfid 8740 . . . 4 (𝐴 ∈ ℤ → ((0[,]𝐴) ∩ ℙ) ∈ Fin)
84 fzfid 13340 . . . . 5 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1...(⌊‘((log‘𝐴) / (log‘𝑝)))) ∈ Fin)
85 simprl 769 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → 𝑝 ∈ ((0[,]𝐴) ∩ ℙ))
8685elin2d 4175 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → 𝑝 ∈ ℙ)
87 elfznn 12935 . . . . . . . . . . 11 (𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))) → 𝑘 ∈ ℕ)
8887ad2antll 727 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → 𝑘 ∈ ℕ)
89 vmappw 25692 . . . . . . . . . 10 ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) → (Λ‘(𝑝𝑘)) = (log‘𝑝))
9086, 88, 89syl2anc 586 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → (Λ‘(𝑝𝑘)) = (log‘𝑝))
9151adantrr 715 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → 𝑝 ∈ ℕ)
9291nnrpd 12428 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → 𝑝 ∈ ℝ+)
9392relogcld 25205 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → (log‘𝑝) ∈ ℝ)
9490, 93eqeltrd 2913 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → (Λ‘(𝑝𝑘)) ∈ ℝ)
9588nnnn0d 11954 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → 𝑘 ∈ ℕ0)
96 nnexpcl 13441 . . . . . . . . . . . 12 ((𝑝 ∈ ℕ ∧ 𝑘 ∈ ℕ0) → (𝑝𝑘) ∈ ℕ)
9791, 95, 96syl2anc 586 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → (𝑝𝑘) ∈ ℕ)
9897nnrpd 12428 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → (𝑝𝑘) ∈ ℝ+)
9998relogcld 25205 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → (log‘(𝑝𝑘)) ∈ ℝ)
100 ifcl 4510 . . . . . . . . 9 (((log‘(𝑝𝑘)) ∈ ℝ ∧ 0 ∈ ℝ) → if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0) ∈ ℝ)
10199, 18, 100sylancl 588 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0) ∈ ℝ)
10294, 101resubcld 11067 . . . . . . 7 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → ((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) ∈ ℝ)
103102, 97nndivred 11690 . . . . . 6 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → (((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)) ∈ ℝ)
104103anassrs 470 . . . . 5 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) → (((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)) ∈ ℝ)
10584, 104fsumrecl 15090 . . . 4 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)) ∈ ℝ)
10683, 105fsumrecl 15090 . . 3 (𝐴 ∈ ℤ → Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)) ∈ ℝ)
10751nnrpd 12428 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℝ+)
108107relogcld 25205 . . . . 5 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈ ℝ)
109 uz2m1nn 12322 . . . . . . 7 (𝑝 ∈ (ℤ‘2) → (𝑝 − 1) ∈ ℕ)
11072, 109syl 17 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 − 1) ∈ ℕ)
11151, 110nnmulcld 11689 . . . . 5 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 · (𝑝 − 1)) ∈ ℕ)
112108, 111nndivred 11690 . . . 4 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) / (𝑝 · (𝑝 − 1))) ∈ ℝ)
11383, 112fsumrecl 15090 . . 3 (𝐴 ∈ ℤ → Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)((log‘𝑝) / (𝑝 · (𝑝 − 1))) ∈ ℝ)
114 2re 11710 . . . 4 2 ∈ ℝ
115114a1i 11 . . 3 (𝐴 ∈ ℤ → 2 ∈ ℝ)
11618a1i 11 . . . . . . . . . . . . 13 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 0 ∈ ℝ)
11751nngt0d 11685 . . . . . . . . . . . . 13 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 0 < 𝑝)
118116, 52, 53, 117, 64ltletrd 10799 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 0 < 𝐴)
11953, 118elrpd 12427 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝐴 ∈ ℝ+)
120119relogcld 25205 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝐴) ∈ ℝ)
121 prmgt1 16040 . . . . . . . . . . . 12 (𝑝 ∈ ℙ → 1 < 𝑝)
12249, 121syl 17 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 1 < 𝑝)
12352, 122rplogcld 25211 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈ ℝ+)
124120, 123rerpdivcld 12461 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝐴) / (log‘𝑝)) ∈ ℝ)
125123rpcnd 12432 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈ ℂ)
126125mulid2d 10658 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 · (log‘𝑝)) = (log‘𝑝))
127107, 119logled 25209 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝𝐴 ↔ (log‘𝑝) ≤ (log‘𝐴)))
12864, 127mpbid 234 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ≤ (log‘𝐴))
129126, 128eqbrtrd 5087 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 · (log‘𝑝)) ≤ (log‘𝐴))
130 1re 10640 . . . . . . . . . . . 12 1 ∈ ℝ
131130a1i 11 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 1 ∈ ℝ)
132131, 120, 123lemuldivd 12479 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 · (log‘𝑝)) ≤ (log‘𝐴) ↔ 1 ≤ ((log‘𝐴) / (log‘𝑝))))
133129, 132mpbid 234 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 1 ≤ ((log‘𝐴) / (log‘𝑝)))
134 flge1nn 13190 . . . . . . . . 9 ((((log‘𝐴) / (log‘𝑝)) ∈ ℝ ∧ 1 ≤ ((log‘𝐴) / (log‘𝑝))) → (⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℕ)
135124, 133, 134syl2anc 586 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℕ)
136 nnuz 12280 . . . . . . . 8 ℕ = (ℤ‘1)
137135, 136eleqtrdi 2923 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (⌊‘((log‘𝐴) / (log‘𝑝))) ∈ (ℤ‘1))
138103recnd 10668 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) → (((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)) ∈ ℂ)
139138anassrs 470 . . . . . . 7 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) → (((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)) ∈ ℂ)
140 oveq2 7163 . . . . . . . . . 10 (𝑘 = 1 → (𝑝𝑘) = (𝑝↑1))
141140fveq2d 6673 . . . . . . . . 9 (𝑘 = 1 → (Λ‘(𝑝𝑘)) = (Λ‘(𝑝↑1)))
142140eleq1d 2897 . . . . . . . . . 10 (𝑘 = 1 → ((𝑝𝑘) ∈ ℙ ↔ (𝑝↑1) ∈ ℙ))
143140fveq2d 6673 . . . . . . . . . 10 (𝑘 = 1 → (log‘(𝑝𝑘)) = (log‘(𝑝↑1)))
144142, 143ifbieq1d 4489 . . . . . . . . 9 (𝑘 = 1 → if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0) = if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0))
145141, 144oveq12d 7173 . . . . . . . 8 (𝑘 = 1 → ((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) = ((Λ‘(𝑝↑1)) − if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0)))
146145, 140oveq12d 7173 . . . . . . 7 (𝑘 = 1 → (((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)) = (((Λ‘(𝑝↑1)) − if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0)) / (𝑝↑1)))
147137, 139, 146fsum1p 15107 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)) = ((((Λ‘(𝑝↑1)) − if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0)) / (𝑝↑1)) + Σ𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘))))
14851nncnd 11653 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℂ)
149148exp1d 13504 . . . . . . . . . . . . 13 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝↑1) = 𝑝)
150149fveq2d 6673 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (Λ‘(𝑝↑1)) = (Λ‘𝑝))
151 vmaprm 25693 . . . . . . . . . . . . 13 (𝑝 ∈ ℙ → (Λ‘𝑝) = (log‘𝑝))
15249, 151syl 17 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (Λ‘𝑝) = (log‘𝑝))
153150, 152eqtrd 2856 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (Λ‘(𝑝↑1)) = (log‘𝑝))
154149, 49eqeltrd 2913 . . . . . . . . . . . . 13 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝↑1) ∈ ℙ)
155154iftrued 4474 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0) = (log‘(𝑝↑1)))
156149fveq2d 6673 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘(𝑝↑1)) = (log‘𝑝))
157155, 156eqtrd 2856 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0) = (log‘𝑝))
158153, 157oveq12d 7173 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((Λ‘(𝑝↑1)) − if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0)) = ((log‘𝑝) − (log‘𝑝)))
159125subidd 10984 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) − (log‘𝑝)) = 0)
160158, 159eqtrd 2856 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((Λ‘(𝑝↑1)) − if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0)) = 0)
161160, 149oveq12d 7173 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((Λ‘(𝑝↑1)) − if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0)) / (𝑝↑1)) = (0 / 𝑝))
162107rpcnne0d 12439 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 ∈ ℂ ∧ 𝑝 ≠ 0))
163 div0 11327 . . . . . . . . 9 ((𝑝 ∈ ℂ ∧ 𝑝 ≠ 0) → (0 / 𝑝) = 0)
164162, 163syl 17 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (0 / 𝑝) = 0)
165161, 164eqtrd 2856 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((Λ‘(𝑝↑1)) − if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0)) / (𝑝↑1)) = 0)
166 1p1e2 11761 . . . . . . . . . 10 (1 + 1) = 2
167166oveq1i 7165 . . . . . . . . 9 ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝)))) = (2...(⌊‘((log‘𝐴) / (log‘𝑝))))
168167a1i 11 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝)))) = (2...(⌊‘((log‘𝐴) / (log‘𝑝)))))
169 elfzuz 12903 . . . . . . . . . . . . . 14 (𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝)))) → 𝑘 ∈ (ℤ‘2))
170 eluz2nn 12283 . . . . . . . . . . . . . 14 (𝑘 ∈ (ℤ‘2) → 𝑘 ∈ ℕ)
171169, 170syl 17 . . . . . . . . . . . . 13 (𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝)))) → 𝑘 ∈ ℕ)
172171, 167eleq2s 2931 . . . . . . . . . . . 12 (𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝)))) → 𝑘 ∈ ℕ)
17349, 172, 89syl2an 597 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → (Λ‘(𝑝𝑘)) = (log‘𝑝))
17451adantr 483 . . . . . . . . . . . . . 14 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → 𝑝 ∈ ℕ)
175 nnq 12360 . . . . . . . . . . . . . 14 (𝑝 ∈ ℕ → 𝑝 ∈ ℚ)
176174, 175syl 17 . . . . . . . . . . . . 13 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → 𝑝 ∈ ℚ)
177169, 167eleq2s 2931 . . . . . . . . . . . . . 14 (𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝)))) → 𝑘 ∈ (ℤ‘2))
178177adantl 484 . . . . . . . . . . . . 13 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → 𝑘 ∈ (ℤ‘2))
179 expnprm 16237 . . . . . . . . . . . . 13 ((𝑝 ∈ ℚ ∧ 𝑘 ∈ (ℤ‘2)) → ¬ (𝑝𝑘) ∈ ℙ)
180176, 178, 179syl2anc 586 . . . . . . . . . . . 12 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → ¬ (𝑝𝑘) ∈ ℙ)
181180iffalsed 4477 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0) = 0)
182173, 181oveq12d 7173 . . . . . . . . . 10 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → ((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) = ((log‘𝑝) − 0))
183125subid1d 10985 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) − 0) = (log‘𝑝))
184183adantr 483 . . . . . . . . . 10 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → ((log‘𝑝) − 0) = (log‘𝑝))
185182, 184eqtrd 2856 . . . . . . . . 9 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → ((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) = (log‘𝑝))
186185oveq1d 7170 . . . . . . . 8 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝))))) → (((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)) = ((log‘𝑝) / (𝑝𝑘)))
187168, 186sumeq12dv 15062 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)) = Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝𝑘)))
188165, 187oveq12d 7173 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((((Λ‘(𝑝↑1)) − if((𝑝↑1) ∈ ℙ, (log‘(𝑝↑1)), 0)) / (𝑝↑1)) + Σ𝑘 ∈ ((1 + 1)...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘))) = (0 + Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝𝑘))))
189 fzfid 13340 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (2...(⌊‘((log‘𝐴) / (log‘𝑝)))) ∈ Fin)
190108adantr 483 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → (log‘𝑝) ∈ ℝ)
191 nnnn0 11903 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
19251, 191, 96syl2an 597 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → (𝑝𝑘) ∈ ℕ)
193190, 192nndivred 11690 . . . . . . . . . 10 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → ((log‘𝑝) / (𝑝𝑘)) ∈ ℝ)
194171, 193sylan2 594 . . . . . . . . 9 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))) → ((log‘𝑝) / (𝑝𝑘)) ∈ ℝ)
195189, 194fsumrecl 15090 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝𝑘)) ∈ ℝ)
196195recnd 10668 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝𝑘)) ∈ ℂ)
197196addid2d 10840 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (0 + Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝𝑘))) = Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝𝑘)))
198147, 188, 1973eqtrd 2860 . . . . 5 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)) = Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝𝑘)))
199107rpreccld 12440 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 / 𝑝) ∈ ℝ+)
200124flcld 13167 . . . . . . . . . . . . 13 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℤ)
201200peano2zd 12089 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((⌊‘((log‘𝐴) / (log‘𝑝))) + 1) ∈ ℤ)
202199, 201rpexpcld 13607 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1)) ∈ ℝ+)
203202rpge0d 12434 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 0 ≤ ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1)))
20451nnrecred 11687 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 / 𝑝) ∈ ℝ)
205204resqcld 13610 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 / 𝑝)↑2) ∈ ℝ)
206135peano2nnd 11654 . . . . . . . . . . . . 13 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((⌊‘((log‘𝐴) / (log‘𝑝))) + 1) ∈ ℕ)
207206nnnn0d 11954 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((⌊‘((log‘𝐴) / (log‘𝑝))) + 1) ∈ ℕ0)
208204, 207reexpcld 13526 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1)) ∈ ℝ)
209205, 208subge02d 11231 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (0 ≤ ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1)) ↔ (((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) ≤ ((1 / 𝑝)↑2)))
210203, 209mpbid 234 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) ≤ ((1 / 𝑝)↑2))
211110nnrpd 12428 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 − 1) ∈ ℝ+)
212211rpcnne0d 12439 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((𝑝 − 1) ∈ ℂ ∧ (𝑝 − 1) ≠ 0))
213199rpcnd 12432 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 / 𝑝) ∈ ℂ)
214 dmdcan 11349 . . . . . . . . . . 11 ((((𝑝 − 1) ∈ ℂ ∧ (𝑝 − 1) ≠ 0) ∧ (𝑝 ∈ ℂ ∧ 𝑝 ≠ 0) ∧ (1 / 𝑝) ∈ ℂ) → (((𝑝 − 1) / 𝑝) · ((1 / 𝑝) / (𝑝 − 1))) = ((1 / 𝑝) / 𝑝))
215212, 162, 213, 214syl3anc 1367 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((𝑝 − 1) / 𝑝) · ((1 / 𝑝) / (𝑝 − 1))) = ((1 / 𝑝) / 𝑝))
216131recnd 10668 . . . . . . . . . . . . 13 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 1 ∈ ℂ)
217 divsubdir 11333 . . . . . . . . . . . . 13 ((𝑝 ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝑝 ∈ ℂ ∧ 𝑝 ≠ 0)) → ((𝑝 − 1) / 𝑝) = ((𝑝 / 𝑝) − (1 / 𝑝)))
218148, 216, 162, 217syl3anc 1367 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((𝑝 − 1) / 𝑝) = ((𝑝 / 𝑝) − (1 / 𝑝)))
219 divid 11326 . . . . . . . . . . . . . 14 ((𝑝 ∈ ℂ ∧ 𝑝 ≠ 0) → (𝑝 / 𝑝) = 1)
220162, 219syl 17 . . . . . . . . . . . . 13 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 / 𝑝) = 1)
221220oveq1d 7170 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((𝑝 / 𝑝) − (1 / 𝑝)) = (1 − (1 / 𝑝)))
222218, 221eqtrd 2856 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((𝑝 − 1) / 𝑝) = (1 − (1 / 𝑝)))
223 divdiv1 11350 . . . . . . . . . . . 12 ((1 ∈ ℂ ∧ (𝑝 ∈ ℂ ∧ 𝑝 ≠ 0) ∧ ((𝑝 − 1) ∈ ℂ ∧ (𝑝 − 1) ≠ 0)) → ((1 / 𝑝) / (𝑝 − 1)) = (1 / (𝑝 · (𝑝 − 1))))
224216, 162, 212, 223syl3anc 1367 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 / 𝑝) / (𝑝 − 1)) = (1 / (𝑝 · (𝑝 − 1))))
225222, 224oveq12d 7173 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((𝑝 − 1) / 𝑝) · ((1 / 𝑝) / (𝑝 − 1))) = ((1 − (1 / 𝑝)) · (1 / (𝑝 · (𝑝 − 1)))))
22651nnne0d 11686 . . . . . . . . . . . 12 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ≠ 0)
227213, 148, 226divrecd 11418 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 / 𝑝) / 𝑝) = ((1 / 𝑝) · (1 / 𝑝)))
228213sqvald 13506 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 / 𝑝)↑2) = ((1 / 𝑝) · (1 / 𝑝)))
229227, 228eqtr4d 2859 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 / 𝑝) / 𝑝) = ((1 / 𝑝)↑2))
230215, 225, 2293eqtr3d 2864 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 − (1 / 𝑝)) · (1 / (𝑝 · (𝑝 − 1)))) = ((1 / 𝑝)↑2))
231210, 230breqtrrd 5093 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) ≤ ((1 − (1 / 𝑝)) · (1 / (𝑝 · (𝑝 − 1)))))
232205, 208resubcld 11067 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) ∈ ℝ)
233111nnrecred 11687 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 / (𝑝 · (𝑝 − 1))) ∈ ℝ)
234 resubcl 10949 . . . . . . . . . 10 ((1 ∈ ℝ ∧ (1 / 𝑝) ∈ ℝ) → (1 − (1 / 𝑝)) ∈ ℝ)
235130, 204, 234sylancr 589 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 − (1 / 𝑝)) ∈ ℝ)
236 recgt1 11535 . . . . . . . . . . . 12 ((𝑝 ∈ ℝ ∧ 0 < 𝑝) → (1 < 𝑝 ↔ (1 / 𝑝) < 1))
23752, 117, 236syl2anc 586 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 < 𝑝 ↔ (1 / 𝑝) < 1))
238122, 237mpbid 234 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 / 𝑝) < 1)
239 posdif 11132 . . . . . . . . . . 11 (((1 / 𝑝) ∈ ℝ ∧ 1 ∈ ℝ) → ((1 / 𝑝) < 1 ↔ 0 < (1 − (1 / 𝑝))))
240204, 130, 239sylancl 588 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((1 / 𝑝) < 1 ↔ 0 < (1 − (1 / 𝑝))))
241238, 240mpbid 234 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 0 < (1 − (1 / 𝑝)))
242 ledivmul 11515 . . . . . . . . 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 1370 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 / 𝑝))) ≤ (1 / (𝑝 · (𝑝 − 1))) ↔ (((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) ≤ ((1 − (1 / 𝑝)) · (1 / (𝑝 · (𝑝 − 1))))))
244231, 243mpbird 259 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 / 𝑝))) ≤ (1 / (𝑝 · (𝑝 − 1))))
245235, 241elrpd 12427 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 − (1 / 𝑝)) ∈ ℝ+)
246232, 245rerpdivcld 12461 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 / 𝑝))) ∈ ℝ)
247246, 233, 123lemul2d 12474 . . . . . . 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 234 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) · ((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 / 𝑝)))) ≤ ((log‘𝑝) · (1 / (𝑝 · (𝑝 − 1)))))
249125adantr 483 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → (log‘𝑝) ∈ ℂ)
250192nncnd 11653 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → (𝑝𝑘) ∈ ℂ)
251192nnne0d 11686 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → (𝑝𝑘) ≠ 0)
252249, 250, 251divrecd 11418 . . . . . . . . . 10 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → ((log‘𝑝) / (𝑝𝑘)) = ((log‘𝑝) · (1 / (𝑝𝑘))))
253148adantr 483 . . . . . . . . . . . 12 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → 𝑝 ∈ ℂ)
25451adantr 483 . . . . . . . . . . . . 13 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → 𝑝 ∈ ℕ)
255254nnne0d 11686 . . . . . . . . . . . 12 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → 𝑝 ≠ 0)
256 nnz 12003 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → 𝑘 ∈ ℤ)
257256adantl 484 . . . . . . . . . . . 12 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℤ)
258253, 255, 257exprecd 13517 . . . . . . . . . . 11 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → ((1 / 𝑝)↑𝑘) = (1 / (𝑝𝑘)))
259258oveq2d 7171 . . . . . . . . . 10 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → ((log‘𝑝) · ((1 / 𝑝)↑𝑘)) = ((log‘𝑝) · (1 / (𝑝𝑘))))
260252, 259eqtr4d 2859 . . . . . . . . 9 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ ℕ) → ((log‘𝑝) / (𝑝𝑘)) = ((log‘𝑝) · ((1 / 𝑝)↑𝑘)))
261171, 260sylan2 594 . . . . . . . 8 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))) → ((log‘𝑝) / (𝑝𝑘)) = ((log‘𝑝) · ((1 / 𝑝)↑𝑘)))
262261sumeq2dv 15059 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝𝑘)) = Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) · ((1 / 𝑝)↑𝑘)))
263171nnnn0d 11954 . . . . . . . . 9 (𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝)))) → 𝑘 ∈ ℕ0)
264 expcl 13446 . . . . . . . . 9 (((1 / 𝑝) ∈ ℂ ∧ 𝑘 ∈ ℕ0) → ((1 / 𝑝)↑𝑘) ∈ ℂ)
265213, 263, 264syl2an 597 . . . . . . . 8 (((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))) → ((1 / 𝑝)↑𝑘) ∈ ℂ)
266189, 125, 265fsummulc2 15138 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) · Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((1 / 𝑝)↑𝑘)) = Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) · ((1 / 𝑝)↑𝑘)))
267 fzval3 13105 . . . . . . . . . . 11 ((⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℤ → (2...(⌊‘((log‘𝐴) / (log‘𝑝)))) = (2..^((⌊‘((log‘𝐴) / (log‘𝑝))) + 1)))
268200, 267syl 17 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (2...(⌊‘((log‘𝐴) / (log‘𝑝)))) = (2..^((⌊‘((log‘𝐴) / (log‘𝑝))) + 1)))
269268sumeq1d 15057 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((1 / 𝑝)↑𝑘) = Σ𝑘 ∈ (2..^((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))((1 / 𝑝)↑𝑘))
270204, 238ltned 10775 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (1 / 𝑝) ≠ 1)
271 2nn0 11913 . . . . . . . . . . 11 2 ∈ ℕ0
272271a1i 11 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 2 ∈ ℕ0)
273 eluzp1p1 12269 . . . . . . . . . . . 12 ((⌊‘((log‘𝐴) / (log‘𝑝))) ∈ (ℤ‘1) → ((⌊‘((log‘𝐴) / (log‘𝑝))) + 1) ∈ (ℤ‘(1 + 1)))
274137, 273syl 17 . . . . . . . . . . 11 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((⌊‘((log‘𝐴) / (log‘𝑝))) + 1) ∈ (ℤ‘(1 + 1)))
275 df-2 11699 . . . . . . . . . . . 12 2 = (1 + 1)
276275fveq2i 6672 . . . . . . . . . . 11 (ℤ‘2) = (ℤ‘(1 + 1))
277274, 276eleqtrrdi 2924 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((⌊‘((log‘𝐴) / (log‘𝑝))) + 1) ∈ (ℤ‘2))
278213, 270, 272, 277geoserg 15220 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈ (2..^((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))((1 / 𝑝)↑𝑘) = ((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 / 𝑝))))
279269, 278eqtrd 2856 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((1 / 𝑝)↑𝑘) = ((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 / 𝑝))))
280279oveq2d 7171 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) · Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((1 / 𝑝)↑𝑘)) = ((log‘𝑝) · ((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 / 𝑝)))))
281262, 266, 2803eqtr2d 2862 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝𝑘)) = ((log‘𝑝) · ((((1 / 𝑝)↑2) − ((1 / 𝑝)↑((⌊‘((log‘𝐴) / (log‘𝑝))) + 1))) / (1 − (1 / 𝑝)))))
282111nncnd 11653 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 · (𝑝 − 1)) ∈ ℂ)
283111nnne0d 11686 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 · (𝑝 − 1)) ≠ 0)
284125, 282, 283divrecd 11418 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) / (𝑝 · (𝑝 − 1))) = ((log‘𝑝) · (1 / (𝑝 · (𝑝 − 1)))))
285248, 281, 2843brtr4d 5097 . . . . 5 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈ (2...(⌊‘((log‘𝐴) / (log‘𝑝))))((log‘𝑝) / (𝑝𝑘)) ≤ ((log‘𝑝) / (𝑝 · (𝑝 − 1))))
286198, 285eqbrtrd 5087 . . . 4 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)) ≤ ((log‘𝑝) / (𝑝 · (𝑝 − 1))))
28783, 105, 112, 286fsumle 15153 . . 3 (𝐴 ∈ ℤ → Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)) ≤ Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)((log‘𝑝) / (𝑝 · (𝑝 − 1))))
288 elfzuz 12903 . . . . . . . . . . 11 (𝑝 ∈ (2...((abs‘𝐴) + 1)) → 𝑝 ∈ (ℤ‘2))
289 eluz2nn 12283 . . . . . . . . . . 11 (𝑝 ∈ (ℤ‘2) → 𝑝 ∈ ℕ)
290288, 289syl 17 . . . . . . . . . 10 (𝑝 ∈ (2...((abs‘𝐴) + 1)) → 𝑝 ∈ ℕ)
291290adantl 484 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → 𝑝 ∈ ℕ)
292291nnred 11652 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → 𝑝 ∈ ℝ)
293288adantl 484 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → 𝑝 ∈ (ℤ‘2))
294 eluz2gt1 12319 . . . . . . . . 9 (𝑝 ∈ (ℤ‘2) → 1 < 𝑝)
295293, 294syl 17 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → 1 < 𝑝)
296292, 295rplogcld 25211 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → (log‘𝑝) ∈ ℝ+)
297293, 109syl 17 . . . . . . . . 9 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → (𝑝 − 1) ∈ ℕ)
298291, 297nnmulcld 11689 . . . . . . . 8 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → (𝑝 · (𝑝 − 1)) ∈ ℕ)
299298nnrpd 12428 . . . . . . 7 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → (𝑝 · (𝑝 − 1)) ∈ ℝ+)
300296, 299rpdivcld 12447 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → ((log‘𝑝) / (𝑝 · (𝑝 − 1))) ∈ ℝ+)
301300rpred 12430 . . . . 5 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → ((log‘𝑝) / (𝑝 · (𝑝 − 1))) ∈ ℝ)
30247, 301fsumrecl 15090 . . . 4 (𝐴 ∈ ℤ → Σ𝑝 ∈ (2...((abs‘𝐴) + 1))((log‘𝑝) / (𝑝 · (𝑝 − 1))) ∈ ℝ)
303300rpge0d 12434 . . . . 5 ((𝐴 ∈ ℤ ∧ 𝑝 ∈ (2...((abs‘𝐴) + 1))) → 0 ≤ ((log‘𝑝) / (𝑝 · (𝑝 − 1))))
30447, 301, 303, 82fsumless 15150 . . . 4 (𝐴 ∈ ℤ → Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)((log‘𝑝) / (𝑝 · (𝑝 − 1))) ≤ Σ𝑝 ∈ (2...((abs‘𝐴) + 1))((log‘𝑝) / (𝑝 · (𝑝 − 1))))
305 rplogsumlem1 26059 . . . . 5 (((abs‘𝐴) + 1) ∈ ℕ → Σ𝑝 ∈ (2...((abs‘𝐴) + 1))((log‘𝑝) / (𝑝 · (𝑝 − 1))) ≤ 2)
30675, 305syl 17 . . . 4 (𝐴 ∈ ℤ → Σ𝑝 ∈ (2...((abs‘𝐴) + 1))((log‘𝑝) / (𝑝 · (𝑝 − 1))) ≤ 2)
307113, 302, 115, 304, 306letrd 10796 . . 3 (𝐴 ∈ ℤ → Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)((log‘𝑝) / (𝑝 · (𝑝 − 1))) ≤ 2)
308106, 113, 115, 287, 307letrd 10796 . 2 (𝐴 ∈ ℤ → Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))(((Λ‘(𝑝𝑘)) − if((𝑝𝑘) ∈ ℙ, (log‘(𝑝𝑘)), 0)) / (𝑝𝑘)) ≤ 2)
30946, 308eqbrtrd 5087 1 (𝐴 ∈ ℤ → Σ𝑛 ∈ (1...𝐴)(((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) ≤ 2)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083   = wceq 1533   ∈ wcel 2110   ≠ wne 3016   ∩ cin 3934  ifcif 4466   class class class wbr 5065  ‘cfv 6354  (class class class)co 7155  ℂcc 10534  ℝcr 10535  0cc0 10536  1c1 10537   + caddc 10539   · cmul 10541   < clt 10674   ≤ cle 10675   − cmin 10869   / cdiv 11296  ℕcn 11637  2c2 11691  ℕ0cn0 11896  ℤcz 11980  ℤ≥cuz 12242  ℚcq 12347  ℝ+crp 12388  [,]cicc 12740  ...cfz 12891  ..^cfzo 13032  ⌊cfl 13159  ↑cexp 13428  abscabs 14592  Σcsu 15041  ℙcprime 16014  logclog 25137  Λcvma 25668 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-rep 5189  ax-sep 5202  ax-nul 5209  ax-pow 5265  ax-pr 5329  ax-un 7460  ax-inf2 9103  ax-cnex 10592  ax-resscn 10593  ax-1cn 10594  ax-icn 10595  ax-addcl 10596  ax-addrcl 10597  ax-mulcl 10598  ax-mulrcl 10599  ax-mulcom 10600  ax-addass 10601  ax-mulass 10602  ax-distr 10603  ax-i2m1 10604  ax-1ne0 10605  ax-1rid 10606  ax-rnegex 10607  ax-rrecex 10608  ax-cnre 10609  ax-pre-lttri 10610  ax-pre-lttrn 10611  ax-pre-ltadd 10612  ax-pre-mulgt0 10613  ax-pre-sup 10614  ax-addf 10615  ax-mulf 10616 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-fal 1546  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4567  df-pr 4569  df-tp 4571  df-op 4573  df-uni 4838  df-int 4876  df-iun 4920  df-iin 4921  df-br 5066  df-opab 5128  df-mpt 5146  df-tr 5172  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-se 5514  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6147  df-ord 6193  df-on 6194  df-lim 6195  df-suc 6196  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-isom 6363  df-riota 7113  df-ov 7158  df-oprab 7159  df-mpo 7160  df-of 7408  df-om 7580  df-1st 7688  df-2nd 7689  df-supp 7830  df-wrecs 7946  df-recs 8007  df-rdg 8045  df-1o 8101  df-2o 8102  df-oadd 8105  df-er 8288  df-map 8407  df-pm 8408  df-ixp 8461  df-en 8509  df-dom 8510  df-sdom 8511  df-fin 8512  df-fsupp 8833  df-fi 8874  df-sup 8905  df-inf 8906  df-oi 8973  df-dju 9329  df-card 9367  df-pnf 10676  df-mnf 10677  df-xr 10678  df-ltxr 10679  df-le 10680  df-sub 10871  df-neg 10872  df-div 11297  df-nn 11638  df-2 11699  df-3 11700  df-4 11701  df-5 11702  df-6 11703  df-7 11704  df-8 11705  df-9 11706  df-n0 11897  df-z 11981  df-dec 12098  df-uz 12243  df-q 12348  df-rp 12389  df-xneg 12506  df-xadd 12507  df-xmul 12508  df-ioo 12741  df-ioc 12742  df-ico 12743  df-icc 12744  df-fz 12892  df-fzo 13033  df-fl 13161  df-mod 13237  df-seq 13369  df-exp 13429  df-fac 13633  df-bc 13662  df-hash 13690  df-shft 14425  df-cj 14457  df-re 14458  df-im 14459  df-sqrt 14593  df-abs 14594  df-limsup 14827  df-clim 14844  df-rlim 14845  df-sum 15042  df-ef 15420  df-sin 15422  df-cos 15423  df-tan 15424  df-pi 15425  df-dvds 15607  df-gcd 15843  df-prm 16015  df-pc 16173  df-struct 16484  df-ndx 16485  df-slot 16486  df-base 16488  df-sets 16489  df-ress 16490  df-plusg 16577  df-mulr 16578  df-starv 16579  df-sca 16580  df-vsca 16581  df-ip 16582  df-tset 16583  df-ple 16584  df-ds 16586  df-unif 16587  df-hom 16588  df-cco 16589  df-rest 16695  df-topn 16696  df-0g 16714  df-gsum 16715  df-topgen 16716  df-pt 16717  df-prds 16720  df-xrs 16774  df-qtop 16779  df-imas 16780  df-xps 16782  df-mre 16856  df-mrc 16857  df-acs 16859  df-mgm 17851  df-sgrp 17900  df-mnd 17911  df-submnd 17956  df-mulg 18224  df-cntz 18446  df-cmn 18907  df-psmet 20536  df-xmet 20537  df-met 20538  df-bl 20539  df-mopn 20540  df-fbas 20541  df-fg 20542  df-cnfld 20545  df-top 21501  df-topon 21518  df-topsp 21540  df-bases 21553  df-cld 21626  df-ntr 21627  df-cls 21628  df-nei 21705  df-lp 21743  df-perf 21744  df-cn 21834  df-cnp 21835  df-haus 21922  df-cmp 21994  df-tx 22169  df-hmeo 22362  df-fil 22453  df-fm 22545  df-flim 22546  df-flf 22547  df-xms 22929  df-ms 22930  df-tms 22931  df-cncf 23485  df-limc 24463  df-dv 24464  df-log 25139  df-cxp 25140  df-vma 25674 This theorem is referenced by:  rplogsum  26102
 Copyright terms: Public domain W3C validator