Theorem rplogsum 27509

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 27508	. 2 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑝) / 𝑝)) − (log‘𝑥))) ∈ 𝑂(1))
8	3	phicld 16731	. . . . . . 7 ⊢ (𝜑 → (ϕ‘𝑁) ∈ ℕ)
9	8	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (ϕ‘𝑁) ∈ ℕ)
10	9	nncnd 12179	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (ϕ‘𝑁) ∈ ℂ)
11		fzfid 13924	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (1...(⌊‘𝑥)) ∈ Fin)
12		inss1 4178	. . . . . . . 8 ⊢ ((1...(⌊‘𝑥)) ∩ 𝑇) ⊆ (1...(⌊‘𝑥))
13		ssfi 9098	. . . . . . . 8 ⊢ (((1...(⌊‘𝑥)) ∈ Fin ∧ ((1...(⌊‘𝑥)) ∩ 𝑇) ⊆ (1...(⌊‘𝑥))) → ((1...(⌊‘𝑥)) ∩ 𝑇) ∈ Fin)
14	11, 12, 13	sylancl 587	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((1...(⌊‘𝑥)) ∩ 𝑇) ∈ Fin)
15		simpr 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)) → 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇))
16	15	elin1d 4145	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)) → 𝑝 ∈ (1...(⌊‘𝑥)))
17		elfznn 13496	. . . . . . . . 9 ⊢ (𝑝 ∈ (1...(⌊‘𝑥)) → 𝑝 ∈ ℕ)
18	16, 17	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)) → 𝑝 ∈ ℕ)
19		vmacl 27099	. . . . . . . . 9 ⊢ (𝑝 ∈ ℕ → (Λ‘𝑝) ∈ ℝ)
20		nndivre 12207	. . . . . . . . 9 ⊢ (((Λ‘𝑝) ∈ ℝ ∧ 𝑝 ∈ ℕ) → ((Λ‘𝑝) / 𝑝) ∈ ℝ)
21	19, 20	mpancom 689	. . . . . . . 8 ⊢ (𝑝 ∈ ℕ → ((Λ‘𝑝) / 𝑝) ∈ ℝ)
22	18, 21	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)) → ((Λ‘𝑝) / 𝑝) ∈ ℝ)
23	14, 22	fsumrecl 15685	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑝) / 𝑝) ∈ ℝ)
24	23	recnd 11162	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑝) / 𝑝) ∈ ℂ)
25	10, 24	mulcld 11154	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑝) / 𝑝)) ∈ ℂ)
26		relogcl 26555	. . . . . 6 ⊢ (𝑥 ∈ ℝ+ → (log‘𝑥) ∈ ℝ)
27	26	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℝ)
28	27	recnd 11162	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℂ)
29	25, 28	subcld 11494	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑝) / 𝑝)) − (log‘𝑥)) ∈ ℂ)
30		inss1 4178	. . . . . . . 8 ⊢ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)) ⊆ (1...(⌊‘𝑥))
31		ssfi 9098	. . . . . . . 8 ⊢ (((1...(⌊‘𝑥)) ∈ Fin ∧ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)) ⊆ (1...(⌊‘𝑥))) → ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)) ∈ Fin)
32	11, 30, 31	sylancl 587	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)) ∈ Fin)
33		simpr 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))) → 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)))
34	33	elin1d 4145	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))) → 𝑝 ∈ (1...(⌊‘𝑥)))
35	34, 17	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))) → 𝑝 ∈ ℕ)
36		nnrp 12943	. . . . . . . . . 10 ⊢ (𝑝 ∈ ℕ → 𝑝 ∈ ℝ+)
37	36	relogcld 26603	. . . . . . . . 9 ⊢ (𝑝 ∈ ℕ → (log‘𝑝) ∈ ℝ)
38	37, 36	rerpdivcld 13006	. . . . . . . 8 ⊢ (𝑝 ∈ ℕ → ((log‘𝑝) / 𝑝) ∈ ℝ)
39	35, 38	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))) → ((log‘𝑝) / 𝑝) ∈ ℝ)
40	32, 39	fsumrecl 15685	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑝) / 𝑝) ∈ ℝ)
41	40	recnd 11162	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑝) / 𝑝) ∈ ℂ)
42	10, 41	mulcld 11154	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑝) / 𝑝)) ∈ ℂ)
43	42, 28	subcld 11494	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑝) / 𝑝)) − (log‘𝑥)) ∈ ℂ)
44	10, 24, 41	subdid 11595	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((ϕ‘𝑁) · (Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑝) / 𝑝) − Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑝) / 𝑝))) = (((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑝) / 𝑝)) − ((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑝) / 𝑝))))
45	19	recnd 11162	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ℕ → (Λ‘𝑝) ∈ ℂ)
46		0re 11135	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ
47		ifcl 4513	. . . . . . . . . . . . 13 ⊢ (((log‘𝑝) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑝 ∈ ℙ, (log‘𝑝), 0) ∈ ℝ)
48	37, 46, 47	sylancl 587	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ ℕ → if(𝑝 ∈ ℙ, (log‘𝑝), 0) ∈ ℝ)
49	48	recnd 11162	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ℕ → if(𝑝 ∈ ℙ, (log‘𝑝), 0) ∈ ℂ)
50	36	rpcnne0d 12984	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ℕ → (𝑝 ∈ ℂ ∧ 𝑝 ≠ 0))
51		divsubdir 11837	. . . . . . . . . . 11 ⊢ (((Λ‘𝑝) ∈ ℂ ∧ if(𝑝 ∈ ℙ, (log‘𝑝), 0) ∈ ℂ ∧ (𝑝 ∈ ℂ ∧ 𝑝 ≠ 0)) → (((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝) = (((Λ‘𝑝) / 𝑝) − (if(𝑝 ∈ ℙ, (log‘𝑝), 0) / 𝑝)))
52	45, 49, 50, 51	syl3anc 1374	. . . . . . . . . 10 ⊢ (𝑝 ∈ ℕ → (((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝) = (((Λ‘𝑝) / 𝑝) − (if(𝑝 ∈ ℙ, (log‘𝑝), 0) / 𝑝)))
53	18, 52	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)) → (((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝) = (((Λ‘𝑝) / 𝑝) − (if(𝑝 ∈ ℙ, (log‘𝑝), 0) / 𝑝)))
54	53	sumeq2dv 15653	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝) = Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(((Λ‘𝑝) / 𝑝) − (if(𝑝 ∈ ℙ, (log‘𝑝), 0) / 𝑝)))
55	21	recnd 11162	. . . . . . . . . 10 ⊢ (𝑝 ∈ ℕ → ((Λ‘𝑝) / 𝑝) ∈ ℂ)
56	18, 55	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)) → ((Λ‘𝑝) / 𝑝) ∈ ℂ)
57	48, 36	rerpdivcld 13006	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ℕ → (if(𝑝 ∈ ℙ, (log‘𝑝), 0) / 𝑝) ∈ ℝ)
58	57	recnd 11162	. . . . . . . . . 10 ⊢ (𝑝 ∈ ℕ → (if(𝑝 ∈ ℙ, (log‘𝑝), 0) / 𝑝) ∈ ℂ)
59	18, 58	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)) → (if(𝑝 ∈ ℙ, (log‘𝑝), 0) / 𝑝) ∈ ℂ)
60	14, 56, 59	fsumsub 15739	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(((Λ‘𝑝) / 𝑝) − (if(𝑝 ∈ ℙ, (log‘𝑝), 0) / 𝑝)) = (Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑝) / 𝑝) − Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(if(𝑝 ∈ ℙ, (log‘𝑝), 0) / 𝑝)))
61		inss2 4179	. . . . . . . . . . . 12 ⊢ (ℙ ∩ 𝑇) ⊆ 𝑇
62		sslin 4184	. . . . . . . . . . . 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 4150	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℙ ∩ 𝑇) = (𝑇 ∩ ℙ)
67	66	ineq2i 4158	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)) = ((1...(⌊‘𝑥)) ∩ (𝑇 ∩ ℙ))
68		inass 4169	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((1...(⌊‘𝑥)) ∩ 𝑇) ∩ ℙ) = ((1...(⌊‘𝑥)) ∩ (𝑇 ∩ ℙ))
69	67, 68	eqtr4i 2763	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)) = (((1...(⌊‘𝑥)) ∩ 𝑇) ∩ ℙ)
70	69	elin2 4144	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)) ↔ (𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇) ∧ 𝑝 ∈ ℙ))
71	70	simplbi2 500	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇) → (𝑝 ∈ ℙ → 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))))
72	71	con3dimp 408	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇) ∧ ¬ 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))) → ¬ 𝑝 ∈ ℙ)
73	65, 72	sylbi 217	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ (((1...(⌊‘𝑥)) ∩ 𝑇) ∖ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))) → ¬ 𝑝 ∈ ℙ)
74	73	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ (((1...(⌊‘𝑥)) ∩ 𝑇) ∖ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)))) → ¬ 𝑝 ∈ ℙ)
75	74	iffalsed 4478	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ (((1...(⌊‘𝑥)) ∩ 𝑇) ∖ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)))) → if(𝑝 ∈ ℙ, (log‘𝑝), 0) = 0)
76	75	oveq1d 7373	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ (((1...(⌊‘𝑥)) ∩ 𝑇) ∖ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)))) → (if(𝑝 ∈ ℙ, (log‘𝑝), 0) / 𝑝) = (0 / 𝑝))
77		eldifi 4072	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ (((1...(⌊‘𝑥)) ∩ 𝑇) ∖ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))) → 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇))
78	77, 18	sylan2 594	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ (((1...(⌊‘𝑥)) ∩ 𝑇) ∖ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)))) → 𝑝 ∈ ℕ)
79		div0 11831	. . . . . . . . . . . . . 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 2772	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ (((1...(⌊‘𝑥)) ∩ 𝑇) ∖ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)))) → (if(𝑝 ∈ ℙ, (log‘𝑝), 0) / 𝑝) = 0)
83	63, 64, 82, 14	fsumss 15676	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))(if(𝑝 ∈ ℙ, (log‘𝑝), 0) / 𝑝) = Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(if(𝑝 ∈ ℙ, (log‘𝑝), 0) / 𝑝))
84		inss2 4179	. . . . . . . . . . . . . . 15 ⊢ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)) ⊆ (ℙ ∩ 𝑇)
85		inss1 4178	. . . . . . . . . . . . . . 15 ⊢ (ℙ ∩ 𝑇) ⊆ ℙ
86	84, 85	sstri 3932	. . . . . . . . . . . . . 14 ⊢ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇)) ⊆ ℙ
87	86, 33	sselid 3920	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))) → 𝑝 ∈ ℙ)
88	87	iftrued 4475	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))) → if(𝑝 ∈ ℙ, (log‘𝑝), 0) = (log‘𝑝))
89	88	oveq1d 7373	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))) → (if(𝑝 ∈ ℙ, (log‘𝑝), 0) / 𝑝) = ((log‘𝑝) / 𝑝))
90	89	sumeq2dv 15653	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))(if(𝑝 ∈ ℙ, (log‘𝑝), 0) / 𝑝) = Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑝) / 𝑝))
91	83, 90	eqtr3d 2774	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(if(𝑝 ∈ ℙ, (log‘𝑝), 0) / 𝑝) = Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑝) / 𝑝))
92	91	oveq2d 7374	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑝) / 𝑝) − Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(if(𝑝 ∈ ℙ, (log‘𝑝), 0) / 𝑝)) = (Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑝) / 𝑝) − Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑝) / 𝑝)))
93	54, 60, 92	3eqtrd 2776	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝) = (Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑝) / 𝑝) − Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑝) / 𝑝)))
94	93	oveq2d 7374	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝)) = ((ϕ‘𝑁) · (Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑝) / 𝑝) − Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑝) / 𝑝))))
95	25, 42, 28	nnncan2d 11529	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑝) / 𝑝)) − (log‘𝑥)) − (((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑝) / 𝑝)) − (log‘𝑥))) = (((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑝) / 𝑝)) − ((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑝) / 𝑝))))
96	44, 94, 95	3eqtr4d 2782	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝)) = ((((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑝) / 𝑝)) − (log‘𝑥)) − (((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑝) / 𝑝)) − (log‘𝑥))))
97	96	mpteq2dva 5179	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ ((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝))) = (𝑥 ∈ ℝ+ ↦ ((((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑝) / 𝑝)) − (log‘𝑥)) − (((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑝) / 𝑝)) − (log‘𝑥)))))
98	19, 48	resubcld 11567	. . . . . . . . 9 ⊢ (𝑝 ∈ ℕ → ((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) ∈ ℝ)
99	98, 36	rerpdivcld 13006	. . . . . . . 8 ⊢ (𝑝 ∈ ℕ → (((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝) ∈ ℝ)
100	18, 99	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)) → (((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝) ∈ ℝ)
101	14, 100	fsumrecl 15685	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝) ∈ ℝ)
102	101	recnd 11162	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝) ∈ ℂ)
103		rpssre 12939	. . . . . 6 ⊢ ℝ+ ⊆ ℝ
104	8	nncnd 12179	. . . . . 6 ⊢ (𝜑 → (ϕ‘𝑁) ∈ ℂ)
105		o1const 15571	. . . . . 6 ⊢ ((ℝ+ ⊆ ℝ ∧ (ϕ‘𝑁) ∈ ℂ) → (𝑥 ∈ ℝ+ ↦ (ϕ‘𝑁)) ∈ 𝑂(1))
106	103, 104, 105	sylancr 588	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (ϕ‘𝑁)) ∈ 𝑂(1))
107	103	a1i 11	. . . . . 6 ⊢ (𝜑 → ℝ+ ⊆ ℝ)
108		1red 11134	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℝ)
109		2re 12244	. . . . . . 7 ⊢ 2 ∈ ℝ
110	109	a1i 11	. . . . . 6 ⊢ (𝜑 → 2 ∈ ℝ)
111		breq1 5089	. . . . . . . . . . . . . 14 ⊢ ((log‘𝑝) = if(𝑝 ∈ ℙ, (log‘𝑝), 0) → ((log‘𝑝) ≤ (Λ‘𝑝) ↔ if(𝑝 ∈ ℙ, (log‘𝑝), 0) ≤ (Λ‘𝑝)))
112		breq1 5089	. . . . . . . . . . . . . 14 ⊢ (0 = if(𝑝 ∈ ℙ, (log‘𝑝), 0) → (0 ≤ (Λ‘𝑝) ↔ if(𝑝 ∈ ℙ, (log‘𝑝), 0) ≤ (Λ‘𝑝)))
113	37	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝑝 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (log‘𝑝) ∈ ℝ)
114		vmaprm 27098	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ ℙ → (Λ‘𝑝) = (log‘𝑝))
115	114	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (Λ‘𝑝) = (log‘𝑝))
116	115	eqcomd 2743	. . . . . . . . . . . . . . 15 ⊢ ((𝑝 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (log‘𝑝) = (Λ‘𝑝))
117	113, 116	eqled 11238	. . . . . . . . . . . . . 14 ⊢ ((𝑝 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (log‘𝑝) ≤ (Λ‘𝑝))
118		vmage0 27102	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ ℕ → 0 ≤ (Λ‘𝑝))
119	118	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝑝 ∈ ℕ ∧ ¬ 𝑝 ∈ ℙ) → 0 ≤ (Λ‘𝑝))
120	111, 112, 117, 119	ifbothda 4506	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ ℕ → if(𝑝 ∈ ℙ, (log‘𝑝), 0) ≤ (Λ‘𝑝))
121	19, 48	subge0d 11729	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ ℕ → (0 ≤ ((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) ↔ if(𝑝 ∈ ℙ, (log‘𝑝), 0) ≤ (Λ‘𝑝)))
122	120, 121	mpbird 257	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ ℕ → 0 ≤ ((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)))
123	98, 36, 122	divge0d 13015	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ℕ → 0 ≤ (((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝))
124	18, 123	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)) → 0 ≤ (((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝))
125	14, 100, 124	fsumge0 15747	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 0 ≤ Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝))
126	101, 125	absidd 15374	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (abs‘Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝)) = Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝))
127	17	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ (1...(⌊‘𝑥))) → 𝑝 ∈ ℕ)
128	127, 99	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑝 ∈ (1...(⌊‘𝑥))) → (((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝) ∈ ℝ)
129	11, 128	fsumrecl 15685	. . . . . . . . 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 15748	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝) ≤ Σ𝑝 ∈ (1...(⌊‘𝑥))(((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝))
134	107	sselda 3922	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈ ℝ)
135	134	flcld 13746	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (⌊‘𝑥) ∈ ℤ)
136		rplogsumlem2 27467	. . . . . . . . . 10 ⊢ ((⌊‘𝑥) ∈ ℤ → Σ𝑝 ∈ (1...(⌊‘𝑥))(((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝) ≤ 2)
137	135, 136	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑝 ∈ (1...(⌊‘𝑥))(((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝) ≤ 2)
138	101, 129, 130, 133, 137	letrd 11292	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝) ≤ 2)
139	126, 138	eqbrtrd 5108	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (abs‘Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝)) ≤ 2)
140	139	adantrr 718	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝)) ≤ 2)
141	107, 102, 108, 110, 140	elo1d 15487	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝)) ∈ 𝑂(1))
142	10, 102, 106, 141	o1mul2 15576	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ ((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)(((Λ‘𝑝) − if(𝑝 ∈ ℙ, (log‘𝑝), 0)) / 𝑝))) ∈ 𝑂(1))
143	97, 142	eqeltrrd 2838	. . 3 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ ((((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑝) / 𝑝)) − (log‘𝑥)) − (((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑝) / 𝑝)) − (log‘𝑥)))) ∈ 𝑂(1))
144	29, 43, 143	o1dif 15581	. 2 ⊢ (𝜑 → ((𝑥 ∈ ℝ+ ↦ (((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑝) / 𝑝)) − (log‘𝑥))) ∈ 𝑂(1) ↔ (𝑥 ∈ ℝ+ ↦ (((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑝) / 𝑝)) − (log‘𝑥))) ∈ 𝑂(1)))
145	7, 144	mpbid 232	1 ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑝) / 𝑝)) − (log‘𝑥))) ∈ 𝑂(1))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ≠ wne 2933   ∖ cdif 3887   ∩ cin 3889   ⊆ wss 3890  ifcif 4467  {csn 4568   class class class wbr 5086   ↦ cmpt 5167  ^◡ccnv 5621   “ cima 5625  ‘cfv 6490  (class class class)co 7358  Fincfn 8884  ℂcc 11025  ℝcr 11026  0cc0 11027  1c1 11028   · cmul 11032   ≤ cle 11169   − cmin 11366   / cdiv 11796  ℕcn 12163  2c2 12225  ℤcz 12513  ℝ⁺crp 12931  ...cfz 13450  ⌊cfl 13738  abscabs 15185  𝑂(1)co1 15437  Σcsu 15637  ℙcprime 16629  ϕcphi 16723  Unitcui 20324  ℤRHomczrh 21487  ℤ/nℤczn 21490  logclog 26534  Λcvma 27073

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5300  ax-pr 5368  ax-un 7680  ax-inf2 9551  ax-cnex 11083  ax-resscn 11084  ax-1cn 11085  ax-icn 11086  ax-addcl 11087  ax-addrcl 11088  ax-mulcl 11089  ax-mulrcl 11090  ax-mulcom 11091  ax-addass 11092  ax-mulass 11093  ax-distr 11094  ax-i2m1 11095  ax-1ne0 11096  ax-1rid 11097  ax-rnegex 11098  ax-rrecex 11099  ax-cnre 11100  ax-pre-lttri 11101  ax-pre-lttrn 11102  ax-pre-ltadd 11103  ax-pre-mulgt0 11104  ax-pre-sup 11105  ax-addf 11106  ax-mulf 11107

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-tp 4573  df-op 4575  df-uni 4852  df-int 4891  df-iun 4936  df-iin 4937  df-disj 5054  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5517  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-se 5576  df-we 5577  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-pred 6257  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-isom 6499  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-of 7622  df-rpss 7668  df-om 7809  df-1st 7933  df-2nd 7934  df-supp 8102  df-tpos 8167  df-frecs 8222  df-wrecs 8253  df-recs 8302  df-rdg 8340  df-1o 8396  df-2o 8397  df-oadd 8400  df-omul 8401  df-er 8634  df-ec 8636  df-qs 8640  df-map 8766  df-pm 8767  df-ixp 8837  df-en 8885  df-dom 8886  df-sdom 8887  df-fin 8888  df-fsupp 9266  df-fi 9315  df-sup 9346  df-inf 9347  df-oi 9416  df-dju 9814  df-card 9852  df-acn 9855  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174  df-sub 11368  df-neg 11369  df-div 11797  df-nn 12164  df-2 12233  df-3 12234  df-4 12235  df-5 12236  df-6 12237  df-7 12238  df-8 12239  df-9 12240  df-n0 12427  df-xnn0 12500  df-z 12514  df-dec 12634  df-uz 12778  df-q 12888  df-rp 12932  df-xneg 13052  df-xadd 13053  df-xmul 13054  df-ioo 13291  df-ioc 13292  df-ico 13293  df-icc 13294  df-fz 13451  df-fzo 13598  df-fl 13740  df-mod 13818  df-seq 13953  df-exp 14013  df-fac 14225  df-bc 14254  df-hash 14282  df-word 14465  df-concat 14522  df-s1 14548  df-shft 15018  df-cj 15050  df-re 15051  df-im 15052  df-sqrt 15186  df-abs 15187  df-limsup 15422  df-clim 15439  df-rlim 15440  df-o1 15441  df-lo1 15442  df-sum 15638  df-ef 16021  df-e 16022  df-sin 16023  df-cos 16024  df-tan 16025  df-pi 16026  df-dvds 16211  df-gcd 16453  df-prm 16630  df-numer 16694  df-denom 16695  df-phi 16725  df-pc 16797  df-struct 17106  df-sets 17123  df-slot 17141  df-ndx 17153  df-base 17169  df-ress 17190  df-plusg 17222  df-mulr 17223  df-starv 17224  df-sca 17225  df-vsca 17226  df-ip 17227  df-tset 17228  df-ple 17229  df-ds 17231  df-unif 17232  df-hom 17233  df-cco 17234  df-rest 17374  df-topn 17375  df-0g 17393  df-gsum 17394  df-topgen 17395  df-pt 17396  df-prds 17399  df-xrs 17455  df-qtop 17460  df-imas 17461  df-qus 17462  df-xps 17463  df-mre 17537  df-mrc 17538  df-acs 17540  df-mgm 18597  df-sgrp 18676  df-mnd 18692  df-mhm 18740  df-submnd 18741  df-grp 18901  df-minusg 18902  df-sbg 18903  df-mulg 19033  df-subg 19088  df-nsg 19089  df-eqg 19090  df-ghm 19177  df-gim 19223  df-ga 19254  df-cntz 19281  df-oppg 19310  df-od 19492  df-gex 19493  df-pgp 19494  df-lsm 19600  df-pj1 19601  df-cmn 19746  df-abl 19747  df-cyg 19842  df-dprd 19961  df-dpj 19962  df-mgp 20111  df-rng 20123  df-ur 20152  df-ring 20205  df-cring 20206  df-oppr 20306  df-dvdsr 20326  df-unit 20327  df-invr 20357  df-dvr 20370  df-rhm 20441  df-subrng 20512  df-subrg 20536  df-drng 20697  df-lmod 20846  df-lss 20916  df-lsp 20956  df-sra 21158  df-rgmod 21159  df-lidl 21196  df-rsp 21197  df-2idl 21238  df-psmet 21334  df-xmet 21335  df-met 21336  df-bl 21337  df-mopn 21338  df-fbas 21339  df-fg 21340  df-cnfld 21343  df-zring 21435  df-zrh 21491  df-zn 21494  df-top 22868  df-topon 22885  df-topsp 22907  df-bases 22920  df-cld 22993  df-ntr 22994  df-cls 22995  df-nei 23072  df-lp 23110  df-perf 23111  df-cn 23201  df-cnp 23202  df-haus 23289  df-cmp 23361  df-tx 23536  df-hmeo 23729  df-fil 23820  df-fm 23912  df-flim 23913  df-flf 23914  df-xms 24294  df-ms 24295  df-tms 24296  df-cncf 24854  df-0p 25646  df-limc 25842  df-dv 25843  df-ply 26165  df-idp 26166  df-coe 26167  df-dgr 26168  df-quot 26270  df-ulm 26357  df-log 26536  df-cxp 26537  df-atan 26848  df-em 26974  df-cht 27078  df-vma 27079  df-chp 27080  df-ppi 27081  df-mu 27082  df-dchr 27215

This theorem is referenced by:  dirith2  27510