Metamath Proof Explorer

Theorem rplogsum

Description: The sum of log p / p over the primes p == A (mod N ) is asymptotic to log x / phi ( x ) + O(1) . Equation 9.4.3 of Shapiro, p. 375. (Contributed by Mario Carneiro, 16-Apr-2016)

Ref Expression
Hypotheses rpvmasum.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
rpvmasum.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
rpvmasum.a ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
rpvmasum.u ⊢ 𝑈 = ( Unit ‘ 𝑍 )
rpvmasum.b ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
rpvmasum.t ⊢ 𝑇 = ( ◡ 𝐿 “ { 𝐴 } )
Assertion rplogsum ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ( ( log ‘ 𝑝 ) / 𝑝 ) ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) )

Proof

Step Hyp Ref Expression
1 rpvmasum.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
2 rpvmasum.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
3 rpvmasum.a ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4 rpvmasum.u ⊢ 𝑈 = ( Unit ‘ 𝑍 )
5 rpvmasum.b ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
6 rpvmasum.t ⊢ 𝑇 = ( ◡ 𝐿 “ { 𝐴 } )
7 1 2 3 4 5 6 rpvmasum ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑝 ) / 𝑝 ) ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
8 3 phicld ⊢ ( 𝜑 → ( ϕ ‘ 𝑁 ) ∈ ℕ )
9 8 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ϕ ‘ 𝑁 ) ∈ ℕ )
10 9 nncnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ϕ ‘ 𝑁 ) ∈ ℂ )
11 fzfid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
12 inss1 ⊢ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ⊆ ( 1 ... ( ⌊ ‘ 𝑥 ) )
13 ssfi ⊢ ( ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin ∧ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ⊆ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ∈ Fin )
14 11 12 13 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ∈ Fin )
15 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ) → 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) )
16 15 elin1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ) → 𝑝 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) )
17 elfznn ⊢ ( 𝑝 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑝 ∈ ℕ )
18 16 17 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ) → 𝑝 ∈ ℕ )
19 vmacl ⊢ ( 𝑝 ∈ ℕ → ( Λ ‘ 𝑝 ) ∈ ℝ )
20 nndivre ⊢ ( ( ( Λ ‘ 𝑝 ) ∈ ℝ ∧ 𝑝 ∈ ℕ ) → ( ( Λ ‘ 𝑝 ) / 𝑝 ) ∈ ℝ )
21 19 20 mpancom ⊢ ( 𝑝 ∈ ℕ → ( ( Λ ‘ 𝑝 ) / 𝑝 ) ∈ ℝ )
22 18 21 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ) → ( ( Λ ‘ 𝑝 ) / 𝑝 ) ∈ ℝ )
23 14 22 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑝 ) / 𝑝 ) ∈ ℝ )
24 23 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑝 ) / 𝑝 ) ∈ ℂ )
25 10 24 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( ϕ ‘ 𝑁 ) · Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑝 ) / 𝑝 ) ) ∈ ℂ )
26 relogcl ⊢ ( 𝑥 ∈ ℝ+ → ( log ‘ 𝑥 ) ∈ ℝ )
27 26 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℝ )
28 27 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℂ )
29 25 28 subcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑝 ) / 𝑝 ) ) − ( log ‘ 𝑥 ) ) ∈ ℂ )
30 inss1 ⊢ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ⊆ ( 1 ... ( ⌊ ‘ 𝑥 ) )
31 ssfi ⊢ ( ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin ∧ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ⊆ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ∈ Fin )
32 11 30 31 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ∈ Fin )
33 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ) → 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) )
34 33 elin1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ) → 𝑝 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) )
35 34 17 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ) → 𝑝 ∈ ℕ )
36 nnrp ⊢ ( 𝑝 ∈ ℕ → 𝑝 ∈ ℝ+ )
37 36 relogcld ⊢ ( 𝑝 ∈ ℕ → ( log ‘ 𝑝 ) ∈ ℝ )
38 37 36 rerpdivcld ⊢ ( 𝑝 ∈ ℕ → ( ( log ‘ 𝑝 ) / 𝑝 ) ∈ ℝ )
39 35 38 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ) → ( ( log ‘ 𝑝 ) / 𝑝 ) ∈ ℝ )
40 32 39 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ( ( log ‘ 𝑝 ) / 𝑝 ) ∈ ℝ )
41 40 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ( ( log ‘ 𝑝 ) / 𝑝 ) ∈ ℂ )
42 10 41 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( ϕ ‘ 𝑁 ) · Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ( ( log ‘ 𝑝 ) / 𝑝 ) ) ∈ ℂ )
43 42 28 subcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ( ( log ‘ 𝑝 ) / 𝑝 ) ) − ( log ‘ 𝑥 ) ) ∈ ℂ )
44 10 24 41 subdid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( ϕ ‘ 𝑁 ) · ( Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑝 ) / 𝑝 ) − Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ( ( log ‘ 𝑝 ) / 𝑝 ) ) ) = ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑝 ) / 𝑝 ) ) − ( ( ϕ ‘ 𝑁 ) · Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ( ( log ‘ 𝑝 ) / 𝑝 ) ) ) )
45 19 recnd ⊢ ( 𝑝 ∈ ℕ → ( Λ ‘ 𝑝 ) ∈ ℂ )
46 0re ⊢ 0 ∈ ℝ
47 ifcl ⊢ ( ( ( log ‘ 𝑝 ) ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) ∈ ℝ )
48 37 46 47 sylancl ⊢ ( 𝑝 ∈ ℕ → if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) ∈ ℝ )
49 48 recnd ⊢ ( 𝑝 ∈ ℕ → if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) ∈ ℂ )
50 36 rpcnne0d ⊢ ( 𝑝 ∈ ℕ → ( 𝑝 ∈ ℂ ∧ 𝑝 ≠ 0 ) )
51 divsubdir ⊢ ( ( ( Λ ‘ 𝑝 ) ∈ ℂ ∧ if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) ∈ ℂ ∧ ( 𝑝 ∈ ℂ ∧ 𝑝 ≠ 0 ) ) → ( ( ( Λ ‘ 𝑝 ) − if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) ) / 𝑝 ) = ( ( ( Λ ‘ 𝑝 ) / 𝑝 ) − ( if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) / 𝑝 ) ) )
52 45 49 50 51 syl3anc ⊢ ( 𝑝 ∈ ℕ → ( ( ( Λ ‘ 𝑝 ) − if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) ) / 𝑝 ) = ( ( ( Λ ‘ 𝑝 ) / 𝑝 ) − ( if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) / 𝑝 ) ) )
53 18 52 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ) → ( ( ( Λ ‘ 𝑝 ) − if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) ) / 𝑝 ) = ( ( ( Λ ‘ 𝑝 ) / 𝑝 ) − ( if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) / 𝑝 ) ) )
54 53 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( ( Λ ‘ 𝑝 ) − if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) ) / 𝑝 ) = Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( ( Λ ‘ 𝑝 ) / 𝑝 ) − ( if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) / 𝑝 ) ) )
55 21 recnd ⊢ ( 𝑝 ∈ ℕ → ( ( Λ ‘ 𝑝 ) / 𝑝 ) ∈ ℂ )
56 18 55 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ) → ( ( Λ ‘ 𝑝 ) / 𝑝 ) ∈ ℂ )
57 48 36 rerpdivcld ⊢ ( 𝑝 ∈ ℕ → ( if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) / 𝑝 ) ∈ ℝ )
58 57 recnd ⊢ ( 𝑝 ∈ ℕ → ( if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) / 𝑝 ) ∈ ℂ )
59 18 58 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ) → ( if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) / 𝑝 ) ∈ ℂ )
60 14 56 59 fsumsub ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( ( Λ ‘ 𝑝 ) / 𝑝 ) − ( if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) / 𝑝 ) ) = ( Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑝 ) / 𝑝 ) − Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) / 𝑝 ) ) )
61 inss2 ⊢ ( ℙ ∩ 𝑇 ) ⊆ 𝑇
62 sslin ⊢ ( ( ℙ ∩ 𝑇 ) ⊆ 𝑇 → ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ⊆ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) )
63 61 62 mp1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ⊆ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) )
64 35 58 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ) → ( if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) / 𝑝 ) ∈ ℂ )
65 eldif ⊢ ( 𝑝 ∈ ( ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ∖ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ) ↔ ( 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ∧ ¬ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ) )
66 incom ⊢ ( ℙ ∩ 𝑇 ) = ( 𝑇 ∩ ℙ )
67 66 ineq2i ⊢ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) = ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( 𝑇 ∩ ℙ ) )
68 inass ⊢ ( ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ∩ ℙ ) = ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( 𝑇 ∩ ℙ ) )
69 67 68 eqtr4i ⊢ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) = ( ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ∩ ℙ )
70 69 elin2 ⊢ ( 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ↔ ( 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ∧ 𝑝 ∈ ℙ ) )
71 70 simplbi2 ⊢ ( 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) → ( 𝑝 ∈ ℙ → 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ) )
72 71 con3dimp ⊢ ( ( 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ∧ ¬ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ) → ¬ 𝑝 ∈ ℙ )
73 65 72 sylbi ⊢ ( 𝑝 ∈ ( ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ∖ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ) → ¬ 𝑝 ∈ ℙ )
74 73 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑝 ∈ ( ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ∖ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ) ) → ¬ 𝑝 ∈ ℙ )
75 74 iffalsed ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑝 ∈ ( ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ∖ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ) ) → if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) = 0 )
76 75 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑝 ∈ ( ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ∖ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ) ) → ( if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) / 𝑝 ) = ( 0 / 𝑝 ) )
77 eldifi ⊢ ( 𝑝 ∈ ( ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ∖ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ) → 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) )
78 77 18 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑝 ∈ ( ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ∖ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ) ) → 𝑝 ∈ ℕ )
79 div0 ⊢ ( ( 𝑝 ∈ ℂ ∧ 𝑝 ≠ 0 ) → ( 0 / 𝑝 ) = 0 )
80 50 79 syl ⊢ ( 𝑝 ∈ ℕ → ( 0 / 𝑝 ) = 0 )
81 78 80 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑝 ∈ ( ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ∖ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ) ) → ( 0 / 𝑝 ) = 0 )
82 76 81 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑝 ∈ ( ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ∖ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ) ) → ( if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) / 𝑝 ) = 0 )
83 63 64 82 14 fsumss ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ( if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) / 𝑝 ) = Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) / 𝑝 ) )
84 inss2 ⊢ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ⊆ ( ℙ ∩ 𝑇 )
85 inss1 ⊢ ( ℙ ∩ 𝑇 ) ⊆ ℙ
86 84 85 sstri ⊢ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ⊆ ℙ
87 86 33 sseldi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ) → 𝑝 ∈ ℙ )
88 87 iftrued ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ) → if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) = ( log ‘ 𝑝 ) )
89 88 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ) → ( if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) / 𝑝 ) = ( ( log ‘ 𝑝 ) / 𝑝 ) )
90 89 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ( if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) / 𝑝 ) = Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ( ( log ‘ 𝑝 ) / 𝑝 ) )
91 83 90 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) / 𝑝 ) = Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ( ( log ‘ 𝑝 ) / 𝑝 ) )
92 91 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑝 ) / 𝑝 ) − Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) / 𝑝 ) ) = ( Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑝 ) / 𝑝 ) − Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ( ( log ‘ 𝑝 ) / 𝑝 ) ) )
93 54 60 92 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( ( Λ ‘ 𝑝 ) − if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) ) / 𝑝 ) = ( Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑝 ) / 𝑝 ) − Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ( ( log ‘ 𝑝 ) / 𝑝 ) ) )
94 93 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( ϕ ‘ 𝑁 ) · Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( ( Λ ‘ 𝑝 ) − if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) ) / 𝑝 ) ) = ( ( ϕ ‘ 𝑁 ) · ( Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑝 ) / 𝑝 ) − Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ( ( log ‘ 𝑝 ) / 𝑝 ) ) ) )
95 25 42 28 nnncan2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑝 ) / 𝑝 ) ) − ( log ‘ 𝑥 ) ) − ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ( ( log ‘ 𝑝 ) / 𝑝 ) ) − ( log ‘ 𝑥 ) ) ) = ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑝 ) / 𝑝 ) ) − ( ( ϕ ‘ 𝑁 ) · Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ( ( log ‘ 𝑝 ) / 𝑝 ) ) ) )
96 44 94 95 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( ϕ ‘ 𝑁 ) · Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( ( Λ ‘ 𝑝 ) − if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) ) / 𝑝 ) ) = ( ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑝 ) / 𝑝 ) ) − ( log ‘ 𝑥 ) ) − ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ( ( log ‘ 𝑝 ) / 𝑝 ) ) − ( log ‘ 𝑥 ) ) ) )
97 96 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( ϕ ‘ 𝑁 ) · Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( ( Λ ‘ 𝑝 ) − if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) ) / 𝑝 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑝 ) / 𝑝 ) ) − ( log ‘ 𝑥 ) ) − ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ( ( log ‘ 𝑝 ) / 𝑝 ) ) − ( log ‘ 𝑥 ) ) ) ) )
98 19 48 resubcld ⊢ ( 𝑝 ∈ ℕ → ( ( Λ ‘ 𝑝 ) − if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) ) ∈ ℝ )
99 98 36 rerpdivcld ⊢ ( 𝑝 ∈ ℕ → ( ( ( Λ ‘ 𝑝 ) − if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) ) / 𝑝 ) ∈ ℝ )
100 18 99 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ) → ( ( ( Λ ‘ 𝑝 ) − if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) ) / 𝑝 ) ∈ ℝ )
101 14 100 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( ( Λ ‘ 𝑝 ) − if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) ) / 𝑝 ) ∈ ℝ )
102 101 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( ( Λ ‘ 𝑝 ) − if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) ) / 𝑝 ) ∈ ℂ )
103 rpssre ⊢ ℝ+ ⊆ ℝ
104 8 nncnd ⊢ ( 𝜑 → ( ϕ ‘ 𝑁 ) ∈ ℂ )
105 o1const ⊢ ( ( ℝ+ ⊆ ℝ ∧ ( ϕ ‘ 𝑁 ) ∈ ℂ ) → ( 𝑥 ∈ ℝ+ ↦ ( ϕ ‘ 𝑁 ) ) ∈ 𝑂(1) )
106 103 104 105 sylancr ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ϕ ‘ 𝑁 ) ) ∈ 𝑂(1) )
107 103 a1i ⊢ ( 𝜑 → ℝ+ ⊆ ℝ )
108 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
109 2re ⊢ 2 ∈ ℝ
110 109 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
111 breq1 ⊢ ( ( log ‘ 𝑝 ) = if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) → ( ( log ‘ 𝑝 ) ≤ ( Λ ‘ 𝑝 ) ↔ if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) ≤ ( Λ ‘ 𝑝 ) ) )
112 breq1 ⊢ ( 0 = if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) → ( 0 ≤ ( Λ ‘ 𝑝 ) ↔ if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) ≤ ( Λ ‘ 𝑝 ) ) )
113 37 adantr ⊢ ( ( 𝑝 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( log ‘ 𝑝 ) ∈ ℝ )
114 vmaprm ⊢ ( 𝑝 ∈ ℙ → ( Λ ‘ 𝑝 ) = ( log ‘ 𝑝 ) )
115 114 adantl ⊢ ( ( 𝑝 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( Λ ‘ 𝑝 ) = ( log ‘ 𝑝 ) )
116 115 eqcomd ⊢ ( ( 𝑝 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( log ‘ 𝑝 ) = ( Λ ‘ 𝑝 ) )
117 113 116 eqled ⊢ ( ( 𝑝 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( log ‘ 𝑝 ) ≤ ( Λ ‘ 𝑝 ) )
118 vmage0 ⊢ ( 𝑝 ∈ ℕ → 0 ≤ ( Λ ‘ 𝑝 ) )
119 118 adantr ⊢ ( ( 𝑝 ∈ ℕ ∧ ¬ 𝑝 ∈ ℙ ) → 0 ≤ ( Λ ‘ 𝑝 ) )
120 111 112 117 119 ifbothda ⊢ ( 𝑝 ∈ ℕ → if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) ≤ ( Λ ‘ 𝑝 ) )
121 19 48 subge0d ⊢ ( 𝑝 ∈ ℕ → ( 0 ≤ ( ( Λ ‘ 𝑝 ) − if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) ) ↔ if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) ≤ ( Λ ‘ 𝑝 ) ) )
122 120 121 mpbird ⊢ ( 𝑝 ∈ ℕ → 0 ≤ ( ( Λ ‘ 𝑝 ) − if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) ) )
123 98 36 122 divge0d ⊢ ( 𝑝 ∈ ℕ → 0 ≤ ( ( ( Λ ‘ 𝑝 ) − if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) ) / 𝑝 ) )
124 18 123 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ) → 0 ≤ ( ( ( Λ ‘ 𝑝 ) − if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) ) / 𝑝 ) )
125 14 100 124 fsumge0 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 0 ≤ Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( ( Λ ‘ 𝑝 ) − if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) ) / 𝑝 ) )
126 101 125 absidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( ( Λ ‘ 𝑝 ) − if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) ) / 𝑝 ) ) = Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( ( Λ ‘ 𝑝 ) − if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) ) / 𝑝 ) )
127 17 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑝 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑝 ∈ ℕ )
128 127 99 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑝 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑝 ) − if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) ) / 𝑝 ) ∈ ℝ )
129 11 128 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑝 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑝 ) − if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) ) / 𝑝 ) ∈ ℝ )
130 109 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 2 ∈ ℝ )
131 127 123 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑝 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( ( ( Λ ‘ 𝑝 ) − if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) ) / 𝑝 ) )
132 12 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ⊆ ( 1 ... ( ⌊ ‘ 𝑥 ) ) )
133 11 128 131 132 fsumless ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( ( Λ ‘ 𝑝 ) − if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) ) / 𝑝 ) ≤ Σ 𝑝 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑝 ) − if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) ) / 𝑝 ) )
134 107 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ )
135 134 flcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ⌊ ‘ 𝑥 ) ∈ ℤ )
136 rplogsumlem2 ⊢ ( ( ⌊ ‘ 𝑥 ) ∈ ℤ → Σ 𝑝 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑝 ) − if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) ) / 𝑝 ) ≤ 2 )
137 135 136 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑝 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑝 ) − if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) ) / 𝑝 ) ≤ 2 )
138 101 129 130 133 137 letrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( ( Λ ‘ 𝑝 ) − if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) ) / 𝑝 ) ≤ 2 )
139 126 138 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( ( Λ ‘ 𝑝 ) − if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) ) / 𝑝 ) ) ≤ 2 )
140 139 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( ( Λ ‘ 𝑝 ) − if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) ) / 𝑝 ) ) ≤ 2 )
141 107 102 108 110 140 elo1d ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( ( Λ ‘ 𝑝 ) − if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) ) / 𝑝 ) ) ∈ 𝑂(1) )
142 10 102 106 141 o1mul2 ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( ϕ ‘ 𝑁 ) · Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( ( Λ ‘ 𝑝 ) − if ( 𝑝 ∈ ℙ , ( log ‘ 𝑝 ) , 0 ) ) / 𝑝 ) ) ) ∈ 𝑂(1) )
143 97 142 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑝 ) / 𝑝 ) ) − ( log ‘ 𝑥 ) ) − ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ( ( log ‘ 𝑝 ) / 𝑝 ) ) − ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
144 29 43 143 o1dif ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ+ ↦ ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑝 ) / 𝑝 ) ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ ℝ+ ↦ ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ( ( log ‘ 𝑝 ) / 𝑝 ) ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) ) )
145 7 144 mpbid ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑝 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ ( ℙ ∩ 𝑇 ) ) ( ( log ‘ 𝑝 ) / 𝑝 ) ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) )