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	sselid	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑝 ∈ ( ( 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) )