chpub - Metamath Proof Explorer

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

Theorem chpub 27192

Description: An upper bound on the second Chebyshev function. (Contributed by Mario Carneiro, 8-Apr-2016.)

**Assertion**
Ref	Expression
chpub	⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (ψ‘𝐴) ≤ ((θ‘𝐴) + ((√‘𝐴) · (log‘𝐴))))

Proof of Theorem chpub Dummy variable 𝑝 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		chpcl 27095	. . . . 5 ⊢ (𝐴 ∈ ℝ → (ψ‘𝐴) ∈ ℝ)
2	1	adantr 480	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (ψ‘𝐴) ∈ ℝ)
3		chtcl 27080	. . . . 5 ⊢ (𝐴 ∈ ℝ → (θ‘𝐴) ∈ ℝ)
4	3	adantr 480	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (θ‘𝐴) ∈ ℝ)
5	2, 4	resubcld 11570	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((ψ‘𝐴) − (θ‘𝐴)) ∈ ℝ)
6		simpl 482	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 𝐴 ∈ ℝ)
7		0red 11140	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 0 ∈ ℝ)
8		1red 11138	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 1 ∈ ℝ)
9		0lt1 11664	. . . . . . . . . 10 ⊢ 0 < 1
10	9	a1i 11	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 0 < 1)
11		simpr 484	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 1 ≤ 𝐴)
12	7, 8, 6, 10, 11	ltletrd 11298	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 0 < 𝐴)
13	6, 12	elrpd 12951	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 𝐴 ∈ ℝ⁺)
14	13	rpge0d 12958	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 0 ≤ 𝐴)
15	6, 14	resqrtcld 15346	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (√‘𝐴) ∈ ℝ)
16		ppifi 27077	. . . . 5 ⊢ ((√‘𝐴) ∈ ℝ → ((0[,](√‘𝐴)) ∩ ℙ) ∈ Fin)
17	15, 16	syl 17	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((0[,](√‘𝐴)) ∩ ℙ) ∈ Fin)
18	13	adantr 480	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 𝐴 ∈ ℝ⁺)
19	18	relogcld 26593	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → (log‘𝐴) ∈ ℝ)
20	17, 19	fsumrecl 15662	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → Σ𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)(log‘𝐴) ∈ ℝ)
21	13	relogcld 26593	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (log‘𝐴) ∈ ℝ)
22	15, 21	remulcld 11167	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((√‘𝐴) · (log‘𝐴)) ∈ ℝ)
23		ppifi 27077	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → ((0[,]𝐴) ∩ ℙ) ∈ Fin)
24	23	adantr 480	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((0[,]𝐴) ∩ ℙ) ∈ Fin)
25		simpr 484	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ((0[,]𝐴) ∩ ℙ))
26	25	elin2d 4158	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℙ)
27		prmnn 16606	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
28	26, 27	syl 17	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℕ)
29	28	nnrpd 12952	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℝ⁺)
30	29	relogcld 26593	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈ ℝ)
31	21	adantr 480	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝐴) ∈ ℝ)
32	28	nnred 12165	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℝ)
33		prmuz2 16628	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ (ℤ_≥‘2))
34	26, 33	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ (ℤ_≥‘2))
35		eluz2gt1 12838	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ (ℤ_≥‘2) → 1 < 𝑝)
36	34, 35	syl 17	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 1 < 𝑝)
37	32, 36	rplogcld 26599	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈ ℝ⁺)
38	31, 37	rerpdivcld 12985	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝐴) / (log‘𝑝)) ∈ ℝ)
39		reflcl 13721	. . . . . . . . 9 ⊢ (((log‘𝐴) / (log‘𝑝)) ∈ ℝ → (⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℝ)
40	38, 39	syl 17	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℝ)
41	30, 40	remulcld 11167	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) ∈ ℝ)
42	41	recnd 11165	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) ∈ ℂ)
43	30	recnd 11165	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈ ℂ)
44	24, 42, 43	fsumsub 15716	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) = (Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑝)))
45		0le0 12251	. . . . . . . . 9 ⊢ 0 ≤ 0
46	45	a1i 11	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 0 ≤ 0)
47	8, 6, 6, 14, 11	lemul2ad 12087	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (𝐴 · 1) ≤ (𝐴 · 𝐴))
48	6	recnd 11165	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 𝐴 ∈ ℂ)
49	48	sqsqrtd 15370	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((√‘𝐴)↑2) = 𝐴)
50	48	mulridd 11154	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (𝐴 · 1) = 𝐴)
51	49, 50	eqtr4d 2775	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((√‘𝐴)↑2) = (𝐴 · 1))
52	48	sqvald 14071	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (𝐴↑2) = (𝐴 · 𝐴))
53	47, 51, 52	3brtr4d 5131	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((√‘𝐴)↑2) ≤ (𝐴↑2))
54	6, 14	sqrtge0d 15349	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 0 ≤ (√‘𝐴))
55	15, 6, 54, 14	le2sqd 14185	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((√‘𝐴) ≤ 𝐴 ↔ ((√‘𝐴)↑2) ≤ (𝐴↑2)))
56	53, 55	mpbird 257	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (√‘𝐴) ≤ 𝐴)
57		iccss 13335	. . . . . . . 8 ⊢ (((0 ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ (0 ≤ 0 ∧ (√‘𝐴) ≤ 𝐴)) → (0[,](√‘𝐴)) ⊆ (0[,]𝐴))
58	7, 6, 46, 56, 57	syl22anc 839	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (0[,](√‘𝐴)) ⊆ (0[,]𝐴))
59	58	ssrind 4197	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((0[,](√‘𝐴)) ∩ ℙ) ⊆ ((0[,]𝐴) ∩ ℙ))
60	59	sselda 3934	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 𝑝 ∈ ((0[,]𝐴) ∩ ℙ))
61	41, 30	resubcld 11570	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ∈ ℝ)
62	61	recnd 11165	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ∈ ℂ)
63	60, 62	syldan 592	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → (((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ∈ ℂ)
64		eldifi 4084	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ)) → 𝑝 ∈ ((0[,]𝐴) ∩ ℙ))
65	64, 43	sylan2 594	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (log‘𝑝) ∈ ℂ)
66	65	mullidd 11155	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (1 · (log‘𝑝)) = (log‘𝑝))
67	25	elin1d 4157	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ (0[,]𝐴))
68		0re 11139	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ ℝ
69	6	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝐴 ∈ ℝ)
70		elicc2 13332	. . . . . . . . . . . . . . . . . 18 ⊢ ((0 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝑝 ∈ (0[,]𝐴) ↔ (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴)))
71	68, 69, 70	sylancr 588	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 ∈ (0[,]𝐴) ↔ (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴)))
72	67, 71	mpbid 232	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴))
73	72	simp3d 1145	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ≤ 𝐴)
74	64, 73	sylan2 594	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 𝑝 ≤ 𝐴)
75	64, 29	sylan2 594	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 𝑝 ∈ ℝ⁺)
76	13	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 𝐴 ∈ ℝ⁺)
77	75, 76	logled 26597	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (𝑝 ≤ 𝐴 ↔ (log‘𝑝) ≤ (log‘𝐴)))
78	74, 77	mpbid 232	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (log‘𝑝) ≤ (log‘𝐴))
79	66, 78	eqbrtrd 5121	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (1 · (log‘𝑝)) ≤ (log‘𝐴))
80		1red 11138	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 1 ∈ ℝ)
81	21	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (log‘𝐴) ∈ ℝ)
82	64, 37	sylan2 594	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (log‘𝑝) ∈ ℝ⁺)
83	80, 81, 82	lemuldivd 13003	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((1 · (log‘𝑝)) ≤ (log‘𝐴) ↔ 1 ≤ ((log‘𝐴) / (log‘𝑝))))
84	79, 83	mpbid 232	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 1 ≤ ((log‘𝐴) / (log‘𝑝)))
85	6	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 𝐴 ∈ ℝ)
86	85	recnd 11165	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 𝐴 ∈ ℂ)
87	86	sqsqrtd 15370	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((√‘𝐴)↑2) = 𝐴)
88		eldifn 4085	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ)) → ¬ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ))
89	88	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ¬ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ))
90	64, 26	sylan2 594	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 𝑝 ∈ ℙ)
91		elin 3918	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ) ↔ (𝑝 ∈ (0[,](√‘𝐴)) ∧ 𝑝 ∈ ℙ))
92	91	rbaib 538	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 ∈ ℙ → (𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ) ↔ 𝑝 ∈ (0[,](√‘𝐴))))
93	90, 92	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ) ↔ 𝑝 ∈ (0[,](√‘𝐴))))
94		0red 11140	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 0 ∈ ℝ)
95	15	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (√‘𝐴) ∈ ℝ)
96	64, 28	sylan2 594	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 𝑝 ∈ ℕ)
97	96	nnred 12165	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 𝑝 ∈ ℝ)
98	75	rpge0d 12958	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 0 ≤ 𝑝)
99		elicc2 13332	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((0 ∈ ℝ ∧ (√‘𝐴) ∈ ℝ) → (𝑝 ∈ (0[,](√‘𝐴)) ↔ (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ (√‘𝐴))))
100		df-3an 1089	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ (√‘𝐴)) ↔ ((𝑝 ∈ ℝ ∧ 0 ≤ 𝑝) ∧ 𝑝 ≤ (√‘𝐴)))
101	99, 100	bitrdi 287	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((0 ∈ ℝ ∧ (√‘𝐴) ∈ ℝ) → (𝑝 ∈ (0[,](√‘𝐴)) ↔ ((𝑝 ∈ ℝ ∧ 0 ≤ 𝑝) ∧ 𝑝 ≤ (√‘𝐴))))
102	101	baibd 539	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((0 ∈ ℝ ∧ (√‘𝐴) ∈ ℝ) ∧ (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝)) → (𝑝 ∈ (0[,](√‘𝐴)) ↔ 𝑝 ≤ (√‘𝐴)))
103	94, 95, 97, 98, 102	syl22anc 839	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (𝑝 ∈ (0[,](√‘𝐴)) ↔ 𝑝 ≤ (√‘𝐴)))
104	93, 103	bitrd 279	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ) ↔ 𝑝 ≤ (√‘𝐴)))
105	89, 104	mtbid 324	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ¬ 𝑝 ≤ (√‘𝐴))
106	95, 97	ltnled 11285	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((√‘𝐴) < 𝑝 ↔ ¬ 𝑝 ≤ (√‘𝐴)))
107	105, 106	mpbird 257	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (√‘𝐴) < 𝑝)
108	54	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 0 ≤ (√‘𝐴))
109	95, 97, 108, 98	lt2sqd 14184	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((√‘𝐴) < 𝑝 ↔ ((√‘𝐴)↑2) < (𝑝↑2)))
110	107, 109	mpbid 232	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((√‘𝐴)↑2) < (𝑝↑2))
111	87, 110	eqbrtrrd 5123	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 𝐴 < (𝑝↑2))
112	96	nnsqcld 14172	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (𝑝↑2) ∈ ℕ)
113	112	nnrpd 12952	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (𝑝↑2) ∈ ℝ⁺)
114		logltb 26570	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℝ⁺ ∧ (𝑝↑2) ∈ ℝ⁺) → (𝐴 < (𝑝↑2) ↔ (log‘𝐴) < (log‘(𝑝↑2))))
115	76, 113, 114	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (𝐴 < (𝑝↑2) ↔ (log‘𝐴) < (log‘(𝑝↑2))))
116	111, 115	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (log‘𝐴) < (log‘(𝑝↑2)))
117		2z 12528	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℤ
118		relogexp 26566	. . . . . . . . . . . . . . 15 ⊢ ((𝑝 ∈ ℝ⁺ ∧ 2 ∈ ℤ) → (log‘(𝑝↑2)) = (2 · (log‘𝑝)))
119	75, 117, 118	sylancl 587	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (log‘(𝑝↑2)) = (2 · (log‘𝑝)))
120	116, 119	breqtrd 5125	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (log‘𝐴) < (2 · (log‘𝑝)))
121		2re 12224	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℝ
122	121	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 2 ∈ ℝ)
123	81, 122, 82	ltdivmul2d 13006	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (((log‘𝐴) / (log‘𝑝)) < 2 ↔ (log‘𝐴) < (2 · (log‘𝑝))))
124	120, 123	mpbird 257	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((log‘𝐴) / (log‘𝑝)) < 2)
125		df-2 12213	. . . . . . . . . . . 12 ⊢ 2 = (1 + 1)
126	124, 125	breqtrdi 5140	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((log‘𝐴) / (log‘𝑝)) < (1 + 1))
127	64, 38	sylan2 594	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((log‘𝐴) / (log‘𝑝)) ∈ ℝ)
128		1z 12526	. . . . . . . . . . . 12 ⊢ 1 ∈ ℤ
129		flbi 13741	. . . . . . . . . . . 12 ⊢ ((((log‘𝐴) / (log‘𝑝)) ∈ ℝ ∧ 1 ∈ ℤ) → ((⌊‘((log‘𝐴) / (log‘𝑝))) = 1 ↔ (1 ≤ ((log‘𝐴) / (log‘𝑝)) ∧ ((log‘𝐴) / (log‘𝑝)) < (1 + 1))))
130	127, 128, 129	sylancl 587	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((⌊‘((log‘𝐴) / (log‘𝑝))) = 1 ↔ (1 ≤ ((log‘𝐴) / (log‘𝑝)) ∧ ((log‘𝐴) / (log‘𝑝)) < (1 + 1))))
131	84, 126, 130	mpbir2and 714	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (⌊‘((log‘𝐴) / (log‘𝑝))) = 1)
132	131	oveq2d 7377	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) = ((log‘𝑝) · 1))
133	65	mulridd 11154	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((log‘𝑝) · 1) = (log‘𝑝))
134	132, 133	eqtrd 2772	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) = (log‘𝑝))
135	134	oveq1d 7376	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) = ((log‘𝑝) − (log‘𝑝)))
136	65	subidd 11485	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((log‘𝑝) − (log‘𝑝)) = 0)
137	135, 136	eqtrd 2772	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) = 0)
138	59, 63, 137, 24	fsumss 15653	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → Σ𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)(((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)))
139		chpval2 27190	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → (ψ‘𝐴) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))))
140	139	adantr 480	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (ψ‘𝐴) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))))
141		chtval 27081	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → (θ‘𝐴) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑝))
142	141	adantr 480	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (θ‘𝐴) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑝))
143	140, 142	oveq12d 7379	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((ψ‘𝐴) − (θ‘𝐴)) = (Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑝)))
144	44, 138, 143	3eqtr4rd 2783	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((ψ‘𝐴) − (θ‘𝐴)) = Σ𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)(((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)))
145	60, 61	syldan 592	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → (((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ∈ ℝ)
146	60, 41	syldan 592	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) ∈ ℝ)
147	60, 37	syldan 592	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → (log‘𝑝) ∈ ℝ⁺)
148	147	rpge0d 12958	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 0 ≤ (log‘𝑝))
149		simpr 484	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ))
150	149	elin2d 4158	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 𝑝 ∈ ℙ)
151	150, 27	syl 17	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 𝑝 ∈ ℕ)
152	151	nnrpd 12952	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 𝑝 ∈ ℝ⁺)
153	152	relogcld 26593	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → (log‘𝑝) ∈ ℝ)
154	146, 153	subge02d 11734	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → (0 ≤ (log‘𝑝) ↔ (((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ≤ ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝))))))
155	148, 154	mpbid 232	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → (((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ≤ ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))))
156	60, 38	syldan 592	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → ((log‘𝐴) / (log‘𝑝)) ∈ ℝ)
157		flle 13724	. . . . . . . 8 ⊢ (((log‘𝐴) / (log‘𝑝)) ∈ ℝ → (⌊‘((log‘𝐴) / (log‘𝑝))) ≤ ((log‘𝐴) / (log‘𝑝)))
158	156, 157	syl 17	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → (⌊‘((log‘𝐴) / (log‘𝑝))) ≤ ((log‘𝐴) / (log‘𝑝)))
159	60, 40	syldan 592	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → (⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℝ)
160	159, 19, 147	lemuldiv2d 13004	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → (((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) ≤ (log‘𝐴) ↔ (⌊‘((log‘𝐴) / (log‘𝑝))) ≤ ((log‘𝐴) / (log‘𝑝))))
161	158, 160	mpbird 257	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) ≤ (log‘𝐴))
162	145, 146, 19, 155, 161	letrd 11295	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → (((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ≤ (log‘𝐴))
163	17, 145, 19, 162	fsumle 15727	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → Σ𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)(((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ≤ Σ𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)(log‘𝐴))
164	144, 163	eqbrtrd 5121	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((ψ‘𝐴) − (θ‘𝐴)) ≤ Σ𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)(log‘𝐴))
165	21	recnd 11165	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (log‘𝐴) ∈ ℂ)
166		fsumconst 15718	. . . . 5 ⊢ ((((0[,](√‘𝐴)) ∩ ℙ) ∈ Fin ∧ (log‘𝐴) ∈ ℂ) → Σ𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)(log‘𝐴) = ((♯‘((0[,](√‘𝐴)) ∩ ℙ)) · (log‘𝐴)))
167	17, 165, 166	syl2anc 585	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → Σ𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)(log‘𝐴) = ((♯‘((0[,](√‘𝐴)) ∩ ℙ)) · (log‘𝐴)))
168		hashcl 14284	. . . . . . 7 ⊢ (((0[,](√‘𝐴)) ∩ ℙ) ∈ Fin → (♯‘((0[,](√‘𝐴)) ∩ ℙ)) ∈ ℕ₀)
169	17, 168	syl 17	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (♯‘((0[,](√‘𝐴)) ∩ ℙ)) ∈ ℕ₀)
170	169	nn0red 12468	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (♯‘((0[,](√‘𝐴)) ∩ ℙ)) ∈ ℝ)
171		logge0 26575	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 0 ≤ (log‘𝐴))
172		reflcl 13721	. . . . . . 7 ⊢ ((√‘𝐴) ∈ ℝ → (⌊‘(√‘𝐴)) ∈ ℝ)
173	15, 172	syl 17	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (⌊‘(√‘𝐴)) ∈ ℝ)
174		fzfid 13901	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (1...(⌊‘(√‘𝐴))) ∈ Fin)
175		ppisval 27075	. . . . . . . . . . 11 ⊢ ((√‘𝐴) ∈ ℝ → ((0[,](√‘𝐴)) ∩ ℙ) = ((2...(⌊‘(√‘𝐴))) ∩ ℙ))
176	15, 175	syl 17	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((0[,](√‘𝐴)) ∩ ℙ) = ((2...(⌊‘(√‘𝐴))) ∩ ℙ))
177		inss1 4190	. . . . . . . . . . 11 ⊢ ((2...(⌊‘(√‘𝐴))) ∩ ℙ) ⊆ (2...(⌊‘(√‘𝐴)))
178		2eluzge1 12800	. . . . . . . . . . . 12 ⊢ 2 ∈ (ℤ_≥‘1)
179		fzss1 13484	. . . . . . . . . . . 12 ⊢ (2 ∈ (ℤ_≥‘1) → (2...(⌊‘(√‘𝐴))) ⊆ (1...(⌊‘(√‘𝐴))))
180	178, 179	mp1i 13	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (2...(⌊‘(√‘𝐴))) ⊆ (1...(⌊‘(√‘𝐴))))
181	177, 180	sstrid 3946	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((2...(⌊‘(√‘𝐴))) ∩ ℙ) ⊆ (1...(⌊‘(√‘𝐴))))
182	176, 181	eqsstrd 3969	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((0[,](√‘𝐴)) ∩ ℙ) ⊆ (1...(⌊‘(√‘𝐴))))
183		ssdomg 8942	. . . . . . . . 9 ⊢ ((1...(⌊‘(√‘𝐴))) ∈ Fin → (((0[,](√‘𝐴)) ∩ ℙ) ⊆ (1...(⌊‘(√‘𝐴))) → ((0[,](√‘𝐴)) ∩ ℙ) ≼ (1...(⌊‘(√‘𝐴)))))
184	174, 182, 183	sylc 65	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((0[,](√‘𝐴)) ∩ ℙ) ≼ (1...(⌊‘(√‘𝐴))))
185		hashdom 14307	. . . . . . . . 9 ⊢ ((((0[,](√‘𝐴)) ∩ ℙ) ∈ Fin ∧ (1...(⌊‘(√‘𝐴))) ∈ Fin) → ((♯‘((0[,](√‘𝐴)) ∩ ℙ)) ≤ (♯‘(1...(⌊‘(√‘𝐴)))) ↔ ((0[,](√‘𝐴)) ∩ ℙ) ≼ (1...(⌊‘(√‘𝐴)))))
186	17, 174, 185	syl2anc 585	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((♯‘((0[,](√‘𝐴)) ∩ ℙ)) ≤ (♯‘(1...(⌊‘(√‘𝐴)))) ↔ ((0[,](√‘𝐴)) ∩ ℙ) ≼ (1...(⌊‘(√‘𝐴)))))
187	184, 186	mpbird 257	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (♯‘((0[,](√‘𝐴)) ∩ ℙ)) ≤ (♯‘(1...(⌊‘(√‘𝐴)))))
188		flge0nn0 13745	. . . . . . . . 9 ⊢ (((√‘𝐴) ∈ ℝ ∧ 0 ≤ (√‘𝐴)) → (⌊‘(√‘𝐴)) ∈ ℕ₀)
189	15, 54, 188	syl2anc 585	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (⌊‘(√‘𝐴)) ∈ ℕ₀)
190		hashfz1 14274	. . . . . . . 8 ⊢ ((⌊‘(√‘𝐴)) ∈ ℕ₀ → (♯‘(1...(⌊‘(√‘𝐴)))) = (⌊‘(√‘𝐴)))
191	189, 190	syl 17	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (♯‘(1...(⌊‘(√‘𝐴)))) = (⌊‘(√‘𝐴)))
192	187, 191	breqtrd 5125	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (♯‘((0[,](√‘𝐴)) ∩ ℙ)) ≤ (⌊‘(√‘𝐴)))
193		flle 13724	. . . . . . 7 ⊢ ((√‘𝐴) ∈ ℝ → (⌊‘(√‘𝐴)) ≤ (√‘𝐴))
194	15, 193	syl 17	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (⌊‘(√‘𝐴)) ≤ (√‘𝐴))
195	170, 173, 15, 192, 194	letrd 11295	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (♯‘((0[,](√‘𝐴)) ∩ ℙ)) ≤ (√‘𝐴))
196	170, 15, 21, 171, 195	lemul1ad 12086	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((♯‘((0[,](√‘𝐴)) ∩ ℙ)) · (log‘𝐴)) ≤ ((√‘𝐴) · (log‘𝐴)))
197	167, 196	eqbrtrd 5121	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → Σ𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)(log‘𝐴) ≤ ((√‘𝐴) · (log‘𝐴)))
198	5, 20, 22, 164, 197	letrd 11295	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((ψ‘𝐴) − (θ‘𝐴)) ≤ ((√‘𝐴) · (log‘𝐴)))
199	2, 4, 22	lesubadd2d 11741	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (((ψ‘𝐴) − (θ‘𝐴)) ≤ ((√‘𝐴) · (log‘𝐴)) ↔ (ψ‘𝐴) ≤ ((θ‘𝐴) + ((√‘𝐴) · (log‘𝐴)))))
200	198, 199	mpbid 232	1 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (ψ‘𝐴) ≤ ((θ‘𝐴) + ((√‘𝐴) · (log‘𝐴))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ∖ cdif 3899 ∩ cin 3901 ⊆ wss 3902 class class class wbr 5099 ‘cfv 6493 (class class class)co 7361 ≼ cdom 8886 Fincfn 8888 ℂcc 11029 ℝcr 11030 0cc0 11031 1c1 11032 + caddc 11034 · cmul 11036 < clt 11171 ≤ cle 11172 − cmin 11369 / cdiv 11799 ℕcn 12150 2c2 12205 ℕ₀cn0 12406 ℤcz 12493 ℤ_≥cuz 12756 ℝ⁺crp 12910 [,]cicc 13269 ...cfz 13428 ⌊cfl 13715 ↑cexp 13989 ♯chash 14258 √csqrt 15161 Σcsu 15614 ℙcprime 16603 logclog 26524 θccht 27062 ψcchp 27064

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 5225 ax-sep 5242 ax-nul 5252 ax-pow 5311 ax-pr 5378 ax-un 7683 ax-inf2 9555 ax-cnex 11087 ax-resscn 11088 ax-1cn 11089 ax-icn 11090 ax-addcl 11091 ax-addrcl 11092 ax-mulcl 11093 ax-mulrcl 11094 ax-mulcom 11095 ax-addass 11096 ax-mulass 11097 ax-distr 11098 ax-i2m1 11099 ax-1ne0 11100 ax-1rid 11101 ax-rnegex 11102 ax-rrecex 11103 ax-cnre 11104 ax-pre-lttri 11105 ax-pre-lttrn 11106 ax-pre-ltadd 11107 ax-pre-mulgt0 11108 ax-pre-sup 11109 ax-addf 11110

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 3062 df-rmo 3351 df-reu 3352 df-rab 3401 df-v 3443 df-sbc 3742 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4287 df-if 4481 df-pw 4557 df-sn 4582 df-pr 4584 df-tp 4586 df-op 4588 df-uni 4865 df-int 4904 df-iun 4949 df-iin 4950 df-br 5100 df-opab 5162 df-mpt 5181 df-tr 5207 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 6260 df-ord 6321 df-on 6322 df-lim 6323 df-suc 6324 df-iota 6449 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500 df-fv 6501 df-isom 6502 df-riota 7318 df-ov 7364 df-oprab 7365 df-mpo 7366 df-of 7625 df-om 7812 df-1st 7936 df-2nd 7937 df-supp 8106 df-frecs 8226 df-wrecs 8257 df-recs 8306 df-rdg 8344 df-1o 8400 df-2o 8401 df-oadd 8404 df-er 8638 df-map 8770 df-pm 8771 df-ixp 8841 df-en 8889 df-dom 8890 df-sdom 8891 df-fin 8892 df-fsupp 9270 df-fi 9319 df-sup 9350 df-inf 9351 df-oi 9420 df-dju 9818 df-card 9856 df-pnf 11173 df-mnf 11174 df-xr 11175 df-ltxr 11176 df-le 11177 df-sub 11371 df-neg 11372 df-div 11800 df-nn 12151 df-2 12213 df-3 12214 df-4 12215 df-5 12216 df-6 12217 df-7 12218 df-8 12219 df-9 12220 df-n0 12407 df-xnn0 12480 df-z 12494 df-dec 12613 df-uz 12757 df-q 12867 df-rp 12911 df-xneg 13031 df-xadd 13032 df-xmul 13033 df-ioo 13270 df-ioc 13271 df-ico 13272 df-icc 13273 df-fz 13429 df-fzo 13576 df-fl 13717 df-mod 13795 df-seq 13930 df-exp 13990 df-fac 14202 df-bc 14231 df-hash 14259 df-shft 14995 df-cj 15027 df-re 15028 df-im 15029 df-sqrt 15163 df-abs 15164 df-limsup 15399 df-clim 15416 df-rlim 15417 df-sum 15615 df-ef 15995 df-sin 15997 df-cos 15998 df-pi 16000 df-dvds 16185 df-gcd 16427 df-prm 16604 df-pc 16770 df-struct 17079 df-sets 17096 df-slot 17114 df-ndx 17126 df-base 17142 df-ress 17163 df-plusg 17195 df-mulr 17196 df-starv 17197 df-sca 17198 df-vsca 17199 df-ip 17200 df-tset 17201 df-ple 17202 df-ds 17204 df-unif 17205 df-hom 17206 df-cco 17207 df-rest 17347 df-topn 17348 df-0g 17366 df-gsum 17367 df-topgen 17368 df-pt 17369 df-prds 17372 df-xrs 17428 df-qtop 17433 df-imas 17434 df-xps 17436 df-mre 17510 df-mrc 17511 df-acs 17513 df-mgm 18570 df-sgrp 18649 df-mnd 18665 df-submnd 18714 df-mulg 19003 df-cntz 19251 df-cmn 19716 df-psmet 21306 df-xmet 21307 df-met 21308 df-bl 21309 df-mopn 21310 df-fbas 21311 df-fg 21312 df-cnfld 21315 df-top 22843 df-topon 22860 df-topsp 22882 df-bases 22895 df-cld 22968 df-ntr 22969 df-cls 22970 df-nei 23047 df-lp 23085 df-perf 23086 df-cn 23176 df-cnp 23177 df-haus 23264 df-tx 23511 df-hmeo 23704 df-fil 23795 df-fm 23887 df-flim 23888 df-flf 23889 df-xms 24269 df-ms 24270 df-tms 24271 df-cncf 24832 df-limc 25828 df-dv 25829 df-log 26526 df-cht 27068 df-vma 27069 df-chp 27070

This theorem is referenced by: chpchtlim 27451

W3C validator