Theorem rplogsum 27515

Description: The sum of log𝑝 / 𝑝 over the primes 𝑝≡𝐴 (mod 𝑁) is asymptotic to log𝑥 / ϕ(𝑥) + 𝑂(1). Equation 9.4.3 of [Shapiro], p. 375. (Contributed by Mario Carneiro, 16-Apr-2016.)

Hypotheses

Ref	Expression
rpvmasum.z	⊢ 𝑍 = (ℤ/nℤ‘𝑁)
rpvmasum.l	⊢ 𝐿 = (ℤRHom‘𝑍)
rpvmasum.a	⊢ (𝜑 → 𝑁 ∈ ℕ)
rpvmasum.u	⊢ 𝑈 = (Unit‘𝑍)
rpvmasum.b	⊢ (𝜑 → 𝐴 ∈ 𝑈)
rpvmasum.t	⊢ 𝑇 = (◡𝐿 “ {𝐴})

Assertion

Ref	Expression
rplogsum	⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑝) / 𝑝)) − (log‘𝑥))) ∈ 𝑂(1))

Distinct variable groups:   𝑥,𝑝,𝐴   𝑁,𝑝,𝑥   𝜑,𝑝,𝑥   𝑇,𝑝,𝑥   𝑈,𝑝,𝑥   𝑍,𝑝,𝑥   𝐿,𝑝,𝑥

Proof of Theorem rplogsum

Step	Hyp	Ref	Expression
1		rpvmasum.z	. . 3 ⊢ 𝑍 = (ℤ/nℤ‘𝑁)
2		rpvmasum.l	. . 3 ⊢ 𝐿 = (ℤRHom‘𝑍)
3		rpvmasum.a	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℕ)
4		rpvmasum.u	. . 3 ⊢ 𝑈 = (Unit‘𝑍)
5		rpvmasum.b	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑈)
6		rpvmasum.t	. . 3 ⊢ 𝑇 = (◡𝐿 “ {𝐴})
7	1, 2, 3, 4, 5, 6	rpvmasum 27514	. 2 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑝) / 𝑝)) − (log‘𝑥))) ∈ 𝑂(1))
8	3	phicld 16740	. . . . . . 7 ⊢ (𝜑 → (ϕ‘𝑁) ∈ ℕ)
9	8	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (ϕ‘𝑁) ∈ ℕ)
10	9	nncnd 12188	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (ϕ‘𝑁) ∈ ℂ)
11		fzfid 13933	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (1...(⌊‘𝑥)) ∈ Fin)
12		inss1 4172	. . . . . . . 8 ⊢ ((1...(⌊‘𝑥)) ∩ 𝑇) ⊆ (1...(⌊‘𝑥))
13		ssfi 9104	. . . . . . . 8 ⊢ (((1...(⌊‘𝑥)) ∈ Fin ∧ ((1...(⌊‘𝑥)) ∩ 𝑇) ⊆ (1...(⌊‘𝑥))) → ((1...(⌊‘𝑥)) ∩ 𝑇) ∈ Fin)
14	11, 12, 13	sylancl 592	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((1...(⌊‘𝑥)) ∩ 𝑇) ∈ Fin)
15		simpr 485	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)) → 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇))
16	15	elin1d 4140	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)) → 𝑝 ∈ (1...(⌊‘𝑥)))
17		elfznn 13505	. . . . . . . . 9 ⊢ (𝑝 ∈ (1...(⌊‘𝑥)) → 𝑝 ∈ ℕ)
18	16, 17	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)) → 𝑝 ∈ ℕ)
19		vmacl 27106	. . . . . . . . 9 ⊢ (𝑝 ∈ ℕ → (Λ‘𝑝) ∈ ℝ)
20		nndivre 12216	. . . . . . . . 9 ⊢ (((Λ‘𝑝) ∈ ℝ ∧ 𝑝 ∈ ℕ) → ((Λ‘𝑝) / 𝑝) ∈ ℝ)
21	19, 20	mpancom 694	. . . . . . . 8 ⊢ (𝑝 ∈ ℕ → ((Λ‘𝑝) / 𝑝) ∈ ℝ)
22	18, 21	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)) → ((Λ‘𝑝) / 𝑝) ∈ ℝ)
23	14, 22	fsumrecl 15694	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑝) / 𝑝) ∈ ℝ)
24	23	recnd 11171	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑝) / 𝑝) ∈ ℂ)
25	10, 24	mulcld 11163	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑝) / 𝑝)) ∈ ℂ)
26		relogcl 26564	. . . . . 6 ⊢ (𝑥 ∈ ℝ+ → (log‘𝑥) ∈ ℝ)
27	26	adantl 482	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℝ)
28	27	recnd 11171	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℂ)
29	25, 28	subcld 11503	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑝) / 𝑝)) − (log‘𝑥)) ∈ ℂ)
30		inss1 4172	. . . . . . . 8 ⊢ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)) ⊆ (1...(⌊‘𝑥))
31		ssfi 9104	. . . . . . . 8 ⊢ (((1...(⌊‘𝑥)) ∈ Fin ∧ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)) ⊆ (1...(⌊‘𝑥))) → ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)) ∈ Fin)
32	11, 30, 31	sylancl 592	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)) ∈ Fin)
33		simpr 485	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))) → 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)))
34	33	elin1d 4140	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))) → 𝑝 ∈ (1...(⌊‘𝑥)))
35	34, 17	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))) → 𝑝 ∈ ℕ)
36		nnrp 12952	. . . . . . . . . 10 ⊢ (𝑝 ∈ ℕ → 𝑝 ∈ ℝ+)
37	36	relogcld 26612	. . . . . . . . 9 ⊢ (𝑝 ∈ ℕ → (log‘𝑝) ∈ ℝ)
38	37, 36	rerpdivcld 13015	. . . . . . . 8 ⊢ (𝑝 ∈ ℕ → ((log‘𝑝) / 𝑝) ∈ ℝ)
39	35, 38	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))) → ((log‘𝑝) / 𝑝) ∈ ℝ)
40	32, 39	fsumrecl 15694	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑝) / 𝑝) ∈ ℝ)
41	40	recnd 11171	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑝) / 𝑝) ∈ ℂ)
42	10, 41	mulcld 11163	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑝) / 𝑝)) ∈ ℂ)
43	42, 28	subcld 11503	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑝) / 𝑝)) − (log‘𝑥)) ∈ ℂ)
44	10, 24, 41	subdid 11604	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((ϕ‘𝑁) · (Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑝) / 𝑝) − Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑝) / 𝑝))) = (((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑝) / 𝑝)) − ((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑝) / 𝑝))))
45	19	recnd 11171	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ℕ → (Λ‘𝑝) ∈ ℂ)
46		0re 11144	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ
47		ifcl 4507	. . . . . . . . . . . . 13 ⊢ (((log‘𝑝) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑝 ∈ ℙ, (log‘𝑝), 0) ∈ ℝ)
48	37, 46, 47	sylancl 592	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ ℕ → if(𝑝 ∈ ℙ, (log‘𝑝), 0) ∈ ℝ)
49	48	recnd 11171	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ℕ → if(𝑝 ∈ ℙ, (log‘𝑝), 0) ∈ ℂ)
50	36	rpcnne0d 12993	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ℕ → (𝑝 ∈ ℂ ∧ 𝑝 ≠ 0))
51		divsubdir 11846	. . . . . . . . . . 11 ⊢ (((Λ‘𝑝) ∈ ℂ ∧ if(𝑝 ∈ ℙ, (log‘𝑝), 0) ∈ ℂ ∧ (𝑝 ∈ ℂ ∧ 𝑝 ≠ 0)) → (((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝) = (((Λ‘𝑝) / 𝑝) − (if(𝑝 ∈ ℙ, (log‘𝑝), 0) / 𝑝)))
52	45, 49, 50, 51	syl3anc 1379	. . . . . . . . . 10 ⊢ (𝑝 ∈ ℕ → (((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝) = (((Λ‘𝑝) / 𝑝) − (if(𝑝 ∈ ℙ, (log‘𝑝), 0) / 𝑝)))
53	18, 52	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)) → (((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝) = (((Λ‘𝑝) / 𝑝) − (if(𝑝 ∈ ℙ, (log‘𝑝), 0) / 𝑝)))
54	53	sumeq2dv 15662	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝) = Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(((Λ‘𝑝) / 𝑝) − (if(𝑝 ∈ ℙ, (log‘𝑝), 0) / 𝑝)))
55	21	recnd 11171	. . . . . . . . . 10 ⊢ (𝑝 ∈ ℕ → ((Λ‘𝑝) / 𝑝) ∈ ℂ)
56	18, 55	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)) → ((Λ‘𝑝) / 𝑝) ∈ ℂ)
57	48, 36	rerpdivcld 13015	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ℕ → (if(𝑝 ∈ ℙ, (log‘𝑝), 0) / 𝑝) ∈ ℝ)
58	57	recnd 11171	. . . . . . . . . 10 ⊢ (𝑝 ∈ ℕ → (if(𝑝 ∈ ℙ, (log‘𝑝), 0) / 𝑝) ∈ ℂ)
59	18, 58	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)) → (if(𝑝 ∈ ℙ, (log‘𝑝), 0) / 𝑝) ∈ ℂ)
60	14, 56, 59	fsumsub 15748	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(((Λ‘𝑝) / 𝑝) − (if(𝑝 ∈ ℙ, (log‘𝑝), 0) / 𝑝)) = (Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑝) / 𝑝) − Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(if(𝑝 ∈ ℙ, (log‘𝑝), 0) / 𝑝)))
61		inss2 4173	. . . . . . . . . . . 12 ⊢ (ℙ ∩ 𝑇) ⊆ 𝑇
62		sslin 4178	. . . . . . . . . . . 12 ⊢ ((ℙ ∩ 𝑇) ⊆ 𝑇 → ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)) ⊆ ((1...(⌊‘𝑥)) ∩ 𝑇))
63	61, 62	mp1i 13	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)) ⊆ ((1...(⌊‘𝑥)) ∩ 𝑇))
64	35, 58	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))) → (if(𝑝 ∈ ℙ, (log‘𝑝), 0) / 𝑝) ∈ ℂ)
65		eldif 3900	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 ∈ (((1...(⌊‘𝑥)) ∩ 𝑇) ∖ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))) ↔ (𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇) ∧ ¬ 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))))
66		incom 4145	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℙ ∩ 𝑇) = (𝑇 ∩ ℙ)
67	66	ineq2i 4153	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)) = ((1...(⌊‘𝑥)) ∩ (𝑇 ∩ ℙ))
68		inass 4163	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((1...(⌊‘𝑥)) ∩ 𝑇) ∩ ℙ) = ((1...(⌊‘𝑥)) ∩ (𝑇 ∩ ℙ))
69	67, 68	eqtr4i 2766	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)) = (((1...(⌊‘𝑥)) ∩ 𝑇) ∩ ℙ)
70	69	elin2 4139	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)) ↔ (𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇) ∧ 𝑝 ∈ ℙ))
71	70	simplbi2 501	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇) → (𝑝 ∈ ℙ → 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))))
72	71	con3dimp 409	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇) ∧ ¬ 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))) → ¬ 𝑝 ∈ ℙ)
73	65, 72	sylbi 218	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ (((1...(⌊‘𝑥)) ∩ 𝑇) ∖ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))) → ¬ 𝑝 ∈ ℙ)
74	73	adantl 482	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ (((1...(⌊‘𝑥)) ∩ 𝑇) ∖ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)))) → ¬ 𝑝 ∈ ℙ)
75	74	iffalsed 4472	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ (((1...(⌊‘𝑥)) ∩ 𝑇) ∖ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)))) → if(𝑝 ∈ ℙ, (log‘𝑝), 0) = 0)
76	75	oveq1d 7378	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ (((1...(⌊‘𝑥)) ∩ 𝑇) ∖ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)))) → (if(𝑝 ∈ ℙ, (log‘𝑝), 0) / 𝑝) = (0 / 𝑝))
77		eldifi 4068	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ (((1...(⌊‘𝑥)) ∩ 𝑇) ∖ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))) → 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇))
78	77, 18	sylan2 599	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ (((1...(⌊‘𝑥)) ∩ 𝑇) ∖ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)))) → 𝑝 ∈ ℕ)
79		div0 11840	. . . . . . . . . . . . . 14 ⊢ ((𝑝 ∈ ℂ ∧ 𝑝 ≠ 0) → (0 / 𝑝) = 0)
80	50, 79	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ ℕ → (0 / 𝑝) = 0)
81	78, 80	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ (((1...(⌊‘𝑥)) ∩ 𝑇) ∖ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)))) → (0 / 𝑝) = 0)
82	76, 81	eqtrd 2775	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ (((1...(⌊‘𝑥)) ∩ 𝑇) ∖ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)))) → (if(𝑝 ∈ ℙ, (log‘𝑝), 0) / 𝑝) = 0)
83	63, 64, 82, 14	fsumss 15685	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))(if(𝑝 ∈ ℙ, (log‘𝑝), 0) / 𝑝) = Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(if(𝑝 ∈ ℙ, (log‘𝑝), 0) / 𝑝))
84		inss2 4173	. . . . . . . . . . . . . . 15 ⊢ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)) ⊆ (ℙ ∩ 𝑇)
85		inss1 4172	. . . . . . . . . . . . . . 15 ⊢ (ℙ ∩ 𝑇) ⊆ ℙ
86	84, 85	sstri 3931	. . . . . . . . . . . . . 14 ⊢ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)) ⊆ ℙ
87	86, 33	sselid 3920	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))) → 𝑝 ∈ ℙ)
88	87	iftrued 4469	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))) → if(𝑝 ∈ ℙ, (log‘𝑝), 0) = (log‘𝑝))
89	88	oveq1d 7378	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))) → (if(𝑝 ∈ ℙ, (log‘𝑝), 0) / 𝑝) = ((log‘𝑝) / 𝑝))
90	89	sumeq2dv 15662	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))(if(𝑝 ∈ ℙ, (log‘𝑝), 0) / 𝑝) = Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑝) / 𝑝))
91	83, 90	eqtr3d 2777	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(if(𝑝 ∈ ℙ, (log‘𝑝), 0) / 𝑝) = Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑝) / 𝑝))
92	91	oveq2d 7379	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑝) / 𝑝) − Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(if(𝑝 ∈ ℙ, (log‘𝑝), 0) / 𝑝)) = (Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑝) / 𝑝) − Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑝) / 𝑝)))
93	54, 60, 92	3eqtrd 2779	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝) = (Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑝) / 𝑝) − Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑝) / 𝑝)))
94	93	oveq2d 7379	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝)) = ((ϕ‘𝑁) · (Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑝) / 𝑝) − Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑝) / 𝑝))))
95	25, 42, 28	nnncan2d 11538	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑝) / 𝑝)) − (log‘𝑥)) − (((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑝) / 𝑝)) − (log‘𝑥))) = (((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑝) / 𝑝)) − ((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑝) / 𝑝))))
96	44, 94, 95	3eqtr4d 2785	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝)) = ((((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑝) / 𝑝)) − (log‘𝑥)) − (((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑝) / 𝑝)) − (log‘𝑥))))
97	96	mpteq2dva 5172	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ ((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝))) = (𝑥 ∈ ℝ+ ↦ ((((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑝) / 𝑝)) − (log‘𝑥)) − (((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑝) / 𝑝)) − (log‘𝑥)))))
98	19, 48	resubcld 11576	. . . . . . . . 9 ⊢ (𝑝 ∈ ℕ → ((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) ∈ ℝ)
99	98, 36	rerpdivcld 13015	. . . . . . . 8 ⊢ (𝑝 ∈ ℕ → (((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝) ∈ ℝ)
100	18, 99	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)) → (((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝) ∈ ℝ)
101	14, 100	fsumrecl 15694	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝) ∈ ℝ)
102	101	recnd 11171	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝) ∈ ℂ)
103		rpssre 12948	. . . . . 6 ⊢ ℝ+ ⊆ ℝ
104	8	nncnd 12188	. . . . . 6 ⊢ (𝜑 → (ϕ‘𝑁) ∈ ℂ)
105		o1const 15580	. . . . . 6 ⊢ ((ℝ+ ⊆ ℝ ∧ (ϕ‘𝑁) ∈ ℂ) → (𝑥 ∈ ℝ+ ↦ (ϕ‘𝑁)) ∈ 𝑂(1))
106	103, 104, 105	sylancr 593	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (ϕ‘𝑁)) ∈ 𝑂(1))
107	103	a1i 11	. . . . . 6 ⊢ (𝜑 → ℝ+ ⊆ ℝ)
108		1red 11143	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℝ)
109		2re 12253	. . . . . . 7 ⊢ 2 ∈ ℝ
110	109	a1i 11	. . . . . 6 ⊢ (𝜑 → 2 ∈ ℝ)
111		breq1 5082	. . . . . . . . . . . . . 14 ⊢ ((log‘𝑝) = if(𝑝 ∈ ℙ, (log‘𝑝), 0) → ((log‘𝑝) ≤ (Λ‘𝑝) ↔ if(𝑝 ∈ ℙ, (log‘𝑝), 0) ≤ (Λ‘𝑝)))
112		breq1 5082	. . . . . . . . . . . . . 14 ⊢ (0 = if(𝑝 ∈ ℙ, (log‘𝑝), 0) → (0 ≤ (Λ‘𝑝) ↔ if(𝑝 ∈ ℙ, (log‘𝑝), 0) ≤ (Λ‘𝑝)))
113	37	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑝 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (log‘𝑝) ∈ ℝ)
114		vmaprm 27105	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ ℙ → (Λ‘𝑝) = (log‘𝑝))
115	114	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (Λ‘𝑝) = (log‘𝑝))
116	115	eqcomd 2746	. . . . . . . . . . . . . . 15 ⊢ ((𝑝 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (log‘𝑝) = (Λ‘𝑝))
117	113, 116	eqled 11247	. . . . . . . . . . . . . 14 ⊢ ((𝑝 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (log‘𝑝) ≤ (Λ‘𝑝))
118		vmage0 27109	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ ℕ → 0 ≤ (Λ‘𝑝))
119	118	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝑝 ∈ ℕ ∧ ¬ 𝑝 ∈ ℙ) → 0 ≤ (Λ‘𝑝))
120	111, 112, 117, 119	ifbothda 4500	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ ℕ → if(𝑝 ∈ ℙ, (log‘𝑝), 0) ≤ (Λ‘𝑝))
121	19, 48	subge0d 11738	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ ℕ → (0 ≤ ((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) ↔ if(𝑝 ∈ ℙ, (log‘𝑝), 0) ≤ (Λ‘𝑝)))
122	120, 121	mpbird 258	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ ℕ → 0 ≤ ((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)))
123	98, 36, 122	divge0d 13024	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ℕ → 0 ≤ (((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝))
124	18, 123	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)) → 0 ≤ (((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝))
125	14, 100, 124	fsumge0 15756	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 0 ≤ Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝))
126	101, 125	absidd 15383	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (abs‘Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝)) = Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝))
127	17	adantl 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ (1...(⌊‘𝑥))) → 𝑝 ∈ ℕ)
128	127, 99	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝) ∈ ℝ)
129	11, 128	fsumrecl 15694	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑝 ∈ (1...(⌊‘𝑥))(((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝) ∈ ℝ)
130	109	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 2 ∈ ℝ)
131	127, 123	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ (1...(⌊‘𝑥))) → 0 ≤ (((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝))
132	12	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((1...(⌊‘𝑥)) ∩ 𝑇) ⊆ (1...(⌊‘𝑥)))
133	11, 128, 131, 132	fsumless 15757	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝) ≤ Σ𝑝 ∈ (1...(⌊‘𝑥))(((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝))
134	107	sselda 3922	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ)
135	134	flcld 13755	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (⌊‘𝑥) ∈ ℤ)
136		rplogsumlem2 27473	. . . . . . . . . 10 ⊢ ((⌊‘𝑥) ∈ ℤ → Σ𝑝 ∈ (1...(⌊‘𝑥))(((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝) ≤ 2)
137	135, 136	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑝 ∈ (1...(⌊‘𝑥))(((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝) ≤ 2)
138	101, 129, 130, 133, 137	letrd 11301	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝) ≤ 2)
139	126, 138	eqbrtrd 5101	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (abs‘Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝)) ≤ 2)
140	139	adantrr 723	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝)) ≤ 2)
141	107, 102, 108, 110, 140	elo1d 15496	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝)) ∈ 𝑂(1))
142	10, 102, 106, 141	o1mul2 15585	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ ((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝))) ∈ 𝑂(1))
143	97, 142	eqeltrrd 2841	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ ((((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑝) / 𝑝)) − (log‘𝑥)) − (((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑝) / 𝑝)) − (log‘𝑥)))) ∈ 𝑂(1))
144	29, 43, 143	o1dif 15590	. 2 ⊢ (𝜑 → ((𝑥 ∈ ℝ+ ↦ (((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑝) / 𝑝)) − (log‘𝑥))) ∈ 𝑂(1) ↔ (𝑥 ∈ ℝ+ ↦ (((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑝) / 𝑝)) − (log‘𝑥))) ∈ 𝑂(1)))
145	7, 144	mpbid 233	1 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑝) / 𝑝)) − (log‘𝑥))) ∈ 𝑂(1))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119   ≠ wne 2935   ∖ cdif 3887   ∩ cin 3889   ⊆ wss 3890  ifcif 4461  {csn 4562   class class class wbr 5079   ↦ cmpt 5160  ^◡ccnv 5624   “ cima 5628  ‘cfv 6492  (class class class)co 7363  Fincfn 8890  ℂcc 11034  ℝcr 11035  0cc0 11036  1c1 11037   · cmul 11041   ≤ cle 11178   − cmin 11375   / cdiv 11805  ℕcn 12172  2c2 12234  ℤcz 12522  ℝ⁺crp 12940  ...cfz 13459  ⌊cfl 13747  abscabs 15194  𝑂(1)co1 15446  Σcsu 15646  ℙcprime 16638  ϕcphi 16732  Unitcui 20333  ℤRHomczrh 21481  ℤ/nℤczn 21484  logclog 26543  Λcvma 27080

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-rep 5206  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685  ax-inf2 9560  ax-cnex 11092  ax-resscn 11093  ax-1cn 11094  ax-icn 11095  ax-addcl 11096  ax-addrcl 11097  ax-mulcl 11098  ax-mulrcl 11099  ax-mulcom 11100  ax-addass 11101  ax-mulass 11102  ax-distr 11103  ax-i2m1 11104  ax-1ne0 11105  ax-1rid 11106  ax-rnegex 11107  ax-rrecex 11108  ax-cnre 11109  ax-pre-lttri 11110  ax-pre-lttrn 11111  ax-pre-ltadd 11112  ax-pre-mulgt0 11113  ax-pre-sup 11114  ax-addf 11115  ax-mulf 11116

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-nel 3040  df-ral 3055  df-rex 3065  df-rmo 3345  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-tp 4567  df-op 4569  df-uni 4846  df-int 4885  df-iun 4930  df-iin 4931  df-disj 5047  df-br 5080  df-opab 5142  df-mpt 5161  df-tr 5187  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-se 5579  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-isom 6501  df-riota 7320  df-ov 7366  df-oprab 7367  df-mpo 7368  df-of 7627  df-rpss 7673  df-om 7814  df-1st 7938  df-2nd 7939  df-supp 8108  df-tpos 8173  df-frecs 8228  df-wrecs 8259  df-recs 8308  df-rdg 8346  df-1o 8402  df-2o 8403  df-oadd 8406  df-omul 8407  df-er 8640  df-ec 8642  df-qs 8646  df-map 8772  df-pm 8773  df-ixp 8843  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-fsupp 9272  df-fi 9321  df-sup 9352  df-inf 9353  df-oi 9422  df-dju 9823  df-card 9861  df-acn 9864  df-pnf 11179  df-mnf 11180  df-xr 11181  df-ltxr 11182  df-le 11183  df-sub 11377  df-neg 11378  df-div 11806  df-nn 12173  df-2 12242  df-3 12243  df-4 12244  df-5 12245  df-6 12246  df-7 12247  df-8 12248  df-9 12249  df-n0 12436  df-xnn0 12509  df-z 12523  df-dec 12643  df-uz 12787  df-q 12897  df-rp 12941  df-xneg 13061  df-xadd 13062  df-xmul 13063  df-ioo 13300  df-ioc 13301  df-ico 13302  df-icc 13303  df-fz 13460  df-fzo 13607  df-fl 13749  df-mod 13827  df-seq 13962  df-exp 14022  df-fac 14234  df-bc 14263  df-hash 14291  df-word 14474  df-concat 14531  df-s1 14557  df-shft 15027  df-cj 15059  df-re 15060  df-im 15061  df-sqrt 15195  df-abs 15196  df-limsup 15431  df-clim 15448  df-rlim 15449  df-o1 15450  df-lo1 15451  df-sum 15647  df-ef 16030  df-e 16031  df-sin 16032  df-cos 16033  df-tan 16034  df-pi 16035  df-dvds 16220  df-gcd 16462  df-prm 16639  df-numer 16703  df-denom 16704  df-phi 16734  df-pc 16806  df-struct 17115  df-sets 17132  df-slot 17150  df-ndx 17162  df-base 17178  df-ress 17199  df-plusg 17231  df-mulr 17232  df-starv 17233  df-sca 17234  df-vsca 17235  df-ip 17236  df-tset 17237  df-ple 17238  df-ds 17240  df-unif 17241  df-hom 17242  df-cco 17243  df-rest 17383  df-topn 17384  df-0g 17402  df-gsum 17403  df-topgen 17404  df-pt 17405  df-prds 17408  df-xrs 17464  df-qtop 17469  df-imas 17470  df-qus 17471  df-xps 17472  df-mre 17546  df-mrc 17547  df-acs 17549  df-mgm 18606  df-sgrp 18685  df-mnd 18701  df-mhm 18749  df-submnd 18750  df-grp 18910  df-minusg 18911  df-sbg 18912  df-mulg 19042  df-subg 19097  df-nsg 19098  df-eqg 19099  df-ghm 19186  df-gim 19232  df-ga 19263  df-cntz 19290  df-oppg 19319  df-od 19501  df-gex 19502  df-pgp 19503  df-lsm 19609  df-pj1 19610  df-cmn 19755  df-abl 19756  df-cyg 19851  df-dprd 19970  df-dpj 19971  df-mgp 20120  df-rng 20132  df-ur 20161  df-ring 20214  df-cring 20215  df-oppr 20315  df-dvdsr 20335  df-unit 20336  df-invr 20366  df-dvr 20379  df-rhm 20450  df-subrng 20525  df-subrg 20549  df-drng 20710  df-lmod 20859  df-lss 20929  df-lsp 20969  df-sra 21170  df-rgmod 21171  df-lidl 21208  df-rsp 21209  df-2idl 21250  df-psmet 21346  df-xmet 21347  df-met 21348  df-bl 21349  df-mopn 21350  df-fbas 21351  df-fg 21352  df-cnfld 21355  df-zring 21429  df-zrh 21485  df-zn 21488  df-top 22884  df-topon 22901  df-topsp 22923  df-bases 22936  df-cld 23009  df-ntr 23010  df-cls 23011  df-nei 23088  df-lp 23126  df-perf 23127  df-cn 23217  df-cnp 23218  df-haus 23305  df-cmp 23377  df-tx 23552  df-hmeo 23745  df-fil 23836  df-fm 23928  df-flim 23929  df-flf 23930  df-xms 24310  df-ms 24311  df-tms 24312  df-cncf 24870  df-0p 25662  df-limc 25858  df-dv 25859  df-ply 26178  df-idp 26179  df-coe 26180  df-dgr 26181  df-quot 26282  df-ulm 26367  df-log 26545  df-cxp 26546  df-atan 26856  df-em 26981  df-cht 27085  df-vma 27086  df-chp 27087  df-ppi 27088  df-mu 27089  df-dchr 27221

This theorem is referenced by:  dirith2  27516