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 27183

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 27087	. . . . 5 ⊢ (𝐴 ∈ ℝ → (ψ‘𝐴) ∈ ℝ)
2	1	adantr 480	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (ψ‘𝐴) ∈ ℝ)
3		chtcl 27072	. . . . 5 ⊢ (𝐴 ∈ ℝ → (θ‘𝐴) ∈ ℝ)
4	3	adantr 480	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (θ‘𝐴) ∈ ℝ)
5	2, 4	resubcld 11578	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((ψ‘𝐴) − (θ‘𝐴)) ∈ ℝ)
6		simpl 482	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 𝐴 ∈ ℝ)
7		0red 11147	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 0 ∈ ℝ)
8		1red 11145	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 1 ∈ ℝ)
9		0lt1 11672	. . . . . . . . . 10 ⊢ 0 < 1
10	9	a1i 11	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 0 < 1)
11		simpr 484	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 1 ≤ 𝐴)
12	7, 8, 6, 10, 11	ltletrd 11306	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 0 < 𝐴)
13	6, 12	elrpd 12983	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 𝐴 ∈ ℝ⁺)
14	13	rpge0d 12990	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 0 ≤ 𝐴)
15	6, 14	resqrtcld 15380	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (√‘𝐴) ∈ ℝ)
16		ppifi 27069	. . . . 5 ⊢ ((√‘𝐴) ∈ ℝ → ((0[,](√‘𝐴)) ∩ ℙ) ∈ Fin)
17	15, 16	syl 17	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((0[,](√‘𝐴)) ∩ ℙ) ∈ Fin)
18	13	adantr 480	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 𝐴 ∈ ℝ⁺)
19	18	relogcld 26587	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → (log‘𝐴) ∈ ℝ)
20	17, 19	fsumrecl 15696	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → Σ𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)(log‘𝐴) ∈ ℝ)
21	13	relogcld 26587	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (log‘𝐴) ∈ ℝ)
22	15, 21	remulcld 11175	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((√‘𝐴) · (log‘𝐴)) ∈ ℝ)
23		ppifi 27069	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → ((0[,]𝐴) ∩ ℙ) ∈ Fin)
24	23	adantr 480	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((0[,]𝐴) ∩ ℙ) ∈ Fin)
25		simpr 484	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ((0[,]𝐴) ∩ ℙ))
26	25	elin2d 4146	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℙ)
27		prmnn 16643	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
28	26, 27	syl 17	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℕ)
29	28	nnrpd 12984	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℝ⁺)
30	29	relogcld 26587	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈ ℝ)
31	21	adantr 480	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝐴) ∈ ℝ)
32	28	nnred 12189	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℝ)
33		prmuz2 16665	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ (ℤ_≥‘2))
34	26, 33	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ (ℤ_≥‘2))
35		eluz2gt1 12870	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ (ℤ_≥‘2) → 1 < 𝑝)
36	34, 35	syl 17	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 1 < 𝑝)
37	32, 36	rplogcld 26593	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈ ℝ⁺)
38	31, 37	rerpdivcld 13017	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝐴) / (log‘𝑝)) ∈ ℝ)
39		reflcl 13755	. . . . . . . . 9 ⊢ (((log‘𝐴) / (log‘𝑝)) ∈ ℝ → (⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℝ)
40	38, 39	syl 17	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℝ)
41	30, 40	remulcld 11175	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) ∈ ℝ)
42	41	recnd 11173	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) ∈ ℂ)
43	30	recnd 11173	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈ ℂ)
44	24, 42, 43	fsumsub 15750	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) = (Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑝)))
45		0le0 12282	. . . . . . . . 9 ⊢ 0 ≤ 0
46	45	a1i 11	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 0 ≤ 0)
47	8, 6, 6, 14, 11	lemul2ad 12096	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (𝐴 · 1) ≤ (𝐴 · 𝐴))
48	6	recnd 11173	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 𝐴 ∈ ℂ)
49	48	sqsqrtd 15404	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((√‘𝐴)↑2) = 𝐴)
50	48	mulridd 11162	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (𝐴 · 1) = 𝐴)
51	49, 50	eqtr4d 2775	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((√‘𝐴)↑2) = (𝐴 · 1))
52	48	sqvald 14105	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (𝐴↑2) = (𝐴 · 𝐴))
53	47, 51, 52	3brtr4d 5118	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((√‘𝐴)↑2) ≤ (𝐴↑2))
54	6, 14	sqrtge0d 15383	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 0 ≤ (√‘𝐴))
55	15, 6, 54, 14	le2sqd 14219	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((√‘𝐴) ≤ 𝐴 ↔ ((√‘𝐴)↑2) ≤ (𝐴↑2)))
56	53, 55	mpbird 257	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (√‘𝐴) ≤ 𝐴)
57		iccss 13367	. . . . . . . 8 ⊢ (((0 ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ (0 ≤ 0 ∧ (√‘𝐴) ≤ 𝐴)) → (0[,](√‘𝐴)) ⊆ (0[,]𝐴))
58	7, 6, 46, 56, 57	syl22anc 839	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (0[,](√‘𝐴)) ⊆ (0[,]𝐴))
59	58	ssrind 4185	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((0[,](√‘𝐴)) ∩ ℙ) ⊆ ((0[,]𝐴) ∩ ℙ))
60	59	sselda 3922	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 𝑝 ∈ ((0[,]𝐴) ∩ ℙ))
61	41, 30	resubcld 11578	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ∈ ℝ)
62	61	recnd 11173	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ∈ ℂ)
63	60, 62	syldan 592	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → (((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ∈ ℂ)
64		eldifi 4072	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ)) → 𝑝 ∈ ((0[,]𝐴) ∩ ℙ))
65	64, 43	sylan2 594	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (log‘𝑝) ∈ ℂ)
66	65	mullidd 11163	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (1 · (log‘𝑝)) = (log‘𝑝))
67	25	elin1d 4145	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ (0[,]𝐴))
68		0re 11146	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ ℝ
69	6	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝐴 ∈ ℝ)
70		elicc2 13364	. . . . . . . . . . . . . . . . . 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 26591	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (𝑝 ≤ 𝐴 ↔ (log‘𝑝) ≤ (log‘𝐴)))
78	74, 77	mpbid 232	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (log‘𝑝) ≤ (log‘𝐴))
79	66, 78	eqbrtrd 5108	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (1 · (log‘𝑝)) ≤ (log‘𝐴))
80		1red 11145	. . . . . . . . . . . . 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 13035	. . . . . . . . . . . 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 11173	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 𝐴 ∈ ℂ)
87	86	sqsqrtd 15404	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((√‘𝐴)↑2) = 𝐴)
88		eldifn 4073	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ)) → ¬ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ))
89	88	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ¬ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ))
90	64, 26	sylan2 594	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 𝑝 ∈ ℙ)
91		elin 3906	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ) ↔ (𝑝 ∈ (0[,](√‘𝐴)) ∧ 𝑝 ∈ ℙ))
92	91	rbaib 538	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 ∈ ℙ → (𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ) ↔ 𝑝 ∈ (0[,](√‘𝐴))))
93	90, 92	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ) ↔ 𝑝 ∈ (0[,](√‘𝐴))))
94		0red 11147	. . . . . . . . . . . . . . . . . . . . 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 12189	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 𝑝 ∈ ℝ)
98	75	rpge0d 12990	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 0 ≤ 𝑝)
99		elicc2 13364	. . . . . . . . . . . . . . . . . . . . . . 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 11293	. . . . . . . . . . . . . . . . . 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 14218	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((√‘𝐴) < 𝑝 ↔ ((√‘𝐴)↑2) < (𝑝↑2)))
110	107, 109	mpbid 232	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((√‘𝐴)↑2) < (𝑝↑2))
111	87, 110	eqbrtrrd 5110	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 𝐴 < (𝑝↑2))
112	96	nnsqcld 14206	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (𝑝↑2) ∈ ℕ)
113	112	nnrpd 12984	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (𝑝↑2) ∈ ℝ⁺)
114		logltb 26564	. . . . . . . . . . . . . . . 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 12559	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℤ
118		relogexp 26560	. . . . . . . . . . . . . . 15 ⊢ ((𝑝 ∈ ℝ⁺ ∧ 2 ∈ ℤ) → (log‘(𝑝↑2)) = (2 · (log‘𝑝)))
119	75, 117, 118	sylancl 587	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (log‘(𝑝↑2)) = (2 · (log‘𝑝)))
120	116, 119	breqtrd 5112	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (log‘𝐴) < (2 · (log‘𝑝)))
121		2re 12255	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℝ
122	121	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 2 ∈ ℝ)
123	81, 122, 82	ltdivmul2d 13038	. . . . . . . . . . . . 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 12244	. . . . . . . . . . . 12 ⊢ 2 = (1 + 1)
126	124, 125	breqtrdi 5127	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((log‘𝐴) / (log‘𝑝)) < (1 + 1))
127	64, 38	sylan2 594	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((log‘𝐴) / (log‘𝑝)) ∈ ℝ)
128		1z 12557	. . . . . . . . . . . 12 ⊢ 1 ∈ ℤ
129		flbi 13775	. . . . . . . . . . . 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 7383	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) = ((log‘𝑝) · 1))
133	65	mulridd 11162	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((log‘𝑝) · 1) = (log‘𝑝))
134	132, 133	eqtrd 2772	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) = (log‘𝑝))
135	134	oveq1d 7382	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) = ((log‘𝑝) − (log‘𝑝)))
136	65	subidd 11493	. . . . . . 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 15687	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → Σ𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)(((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)))
139		chpval2 27181	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → (ψ‘𝐴) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))))
140	139	adantr 480	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (ψ‘𝐴) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))))
141		chtval 27073	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → (θ‘𝐴) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑝))
142	141	adantr 480	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (θ‘𝐴) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑝))
143	140, 142	oveq12d 7385	. . . . 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 12990	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 0 ≤ (log‘𝑝))
149		simpr 484	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ))
150	149	elin2d 4146	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 𝑝 ∈ ℙ)
151	150, 27	syl 17	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 𝑝 ∈ ℕ)
152	151	nnrpd 12984	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 𝑝 ∈ ℝ⁺)
153	152	relogcld 26587	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → (log‘𝑝) ∈ ℝ)
154	146, 153	subge02d 11742	. . . . . . 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 13758	. . . . . . . 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 13036	. . . . . . 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 11303	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → (((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ≤ (log‘𝐴))
163	17, 145, 19, 162	fsumle 15762	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → Σ𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)(((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ≤ Σ𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)(log‘𝐴))
164	144, 163	eqbrtrd 5108	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((ψ‘𝐴) − (θ‘𝐴)) ≤ Σ𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)(log‘𝐴))
165	21	recnd 11173	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (log‘𝐴) ∈ ℂ)
166		fsumconst 15752	. . . . 5 ⊢ ((((0[,](√‘𝐴)) ∩ ℙ) ∈ Fin ∧ (log‘𝐴) ∈ ℂ) → Σ𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)(log‘𝐴) = ((♯‘((0[,](√‘𝐴)) ∩ ℙ)) · (log‘𝐴)))
167	17, 165, 166	syl2anc 585	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → Σ𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)(log‘𝐴) = ((♯‘((0[,](√‘𝐴)) ∩ ℙ)) · (log‘𝐴)))
168		hashcl 14318	. . . . . . 7 ⊢ (((0[,](√‘𝐴)) ∩ ℙ) ∈ Fin → (♯‘((0[,](√‘𝐴)) ∩ ℙ)) ∈ ℕ₀)
169	17, 168	syl 17	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (♯‘((0[,](√‘𝐴)) ∩ ℙ)) ∈ ℕ₀)
170	169	nn0red 12499	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (♯‘((0[,](√‘𝐴)) ∩ ℙ)) ∈ ℝ)
171		logge0 26569	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 0 ≤ (log‘𝐴))
172		reflcl 13755	. . . . . . 7 ⊢ ((√‘𝐴) ∈ ℝ → (⌊‘(√‘𝐴)) ∈ ℝ)
173	15, 172	syl 17	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (⌊‘(√‘𝐴)) ∈ ℝ)
174		fzfid 13935	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (1...(⌊‘(√‘𝐴))) ∈ Fin)
175		ppisval 27067	. . . . . . . . . . 11 ⊢ ((√‘𝐴) ∈ ℝ → ((0[,](√‘𝐴)) ∩ ℙ) = ((2...(⌊‘(√‘𝐴))) ∩ ℙ))
176	15, 175	syl 17	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((0[,](√‘𝐴)) ∩ ℙ) = ((2...(⌊‘(√‘𝐴))) ∩ ℙ))
177		inss1 4178	. . . . . . . . . . 11 ⊢ ((2...(⌊‘(√‘𝐴))) ∩ ℙ) ⊆ (2...(⌊‘(√‘𝐴)))
178		2eluzge1 12832	. . . . . . . . . . . 12 ⊢ 2 ∈ (ℤ_≥‘1)
179		fzss1 13517	. . . . . . . . . . . 12 ⊢ (2 ∈ (ℤ_≥‘1) → (2...(⌊‘(√‘𝐴))) ⊆ (1...(⌊‘(√‘𝐴))))
180	178, 179	mp1i 13	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (2...(⌊‘(√‘𝐴))) ⊆ (1...(⌊‘(√‘𝐴))))
181	177, 180	sstrid 3934	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((2...(⌊‘(√‘𝐴))) ∩ ℙ) ⊆ (1...(⌊‘(√‘𝐴))))
182	176, 181	eqsstrd 3957	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((0[,](√‘𝐴)) ∩ ℙ) ⊆ (1...(⌊‘(√‘𝐴))))
183		ssdomg 8947	. . . . . . . . 9 ⊢ ((1...(⌊‘(√‘𝐴))) ∈ Fin → (((0[,](√‘𝐴)) ∩ ℙ) ⊆ (1...(⌊‘(√‘𝐴))) → ((0[,](√‘𝐴)) ∩ ℙ) ≼ (1...(⌊‘(√‘𝐴)))))
184	174, 182, 183	sylc 65	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((0[,](√‘𝐴)) ∩ ℙ) ≼ (1...(⌊‘(√‘𝐴))))
185		hashdom 14341	. . . . . . . . 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 13779	. . . . . . . . 9 ⊢ (((√‘𝐴) ∈ ℝ ∧ 0 ≤ (√‘𝐴)) → (⌊‘(√‘𝐴)) ∈ ℕ₀)
189	15, 54, 188	syl2anc 585	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (⌊‘(√‘𝐴)) ∈ ℕ₀)
190		hashfz1 14308	. . . . . . . 8 ⊢ ((⌊‘(√‘𝐴)) ∈ ℕ₀ → (♯‘(1...(⌊‘(√‘𝐴)))) = (⌊‘(√‘𝐴)))
191	189, 190	syl 17	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (♯‘(1...(⌊‘(√‘𝐴)))) = (⌊‘(√‘𝐴)))
192	187, 191	breqtrd 5112	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (♯‘((0[,](√‘𝐴)) ∩ ℙ)) ≤ (⌊‘(√‘𝐴)))
193		flle 13758	. . . . . . 7 ⊢ ((√‘𝐴) ∈ ℝ → (⌊‘(√‘𝐴)) ≤ (√‘𝐴))
194	15, 193	syl 17	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (⌊‘(√‘𝐴)) ≤ (√‘𝐴))
195	170, 173, 15, 192, 194	letrd 11303	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (♯‘((0[,](√‘𝐴)) ∩ ℙ)) ≤ (√‘𝐴))
196	170, 15, 21, 171, 195	lemul1ad 12095	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((♯‘((0[,](√‘𝐴)) ∩ ℙ)) · (log‘𝐴)) ≤ ((√‘𝐴) · (log‘𝐴)))
197	167, 196	eqbrtrd 5108	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → Σ𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)(log‘𝐴) ≤ ((√‘𝐴) · (log‘𝐴)))
198	5, 20, 22, 164, 197	letrd 11303	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((ψ‘𝐴) − (θ‘𝐴)) ≤ ((√‘𝐴) · (log‘𝐴)))
199	2, 4, 22	lesubadd2d 11749	. 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 3887 ∩ cin 3889 ⊆ wss 3890 class class class wbr 5086 ‘cfv 6499 (class class class)co 7367 ≼ cdom 8891 Fincfn 8893 ℂcc 11036 ℝcr 11037 0cc0 11038 1c1 11039 + caddc 11041 · cmul 11043 < clt 11179 ≤ cle 11180 − cmin 11377 / cdiv 11807 ℕcn 12174 2c2 12236 ℕ₀cn0 12437 ℤcz 12524 ℤ_≥cuz 12788 ℝ⁺crp 12942 [,]cicc 13301 ...cfz 13461 ⌊cfl 13749 ↑cexp 14023 ♯chash 14292 √csqrt 15195 Σcsu 15648 ℙcprime 16640 logclog 26518 θccht 27054 ψcchp 27056

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 5213 ax-sep 5232 ax-nul 5242 ax-pow 5308 ax-pr 5376 ax-un 7689 ax-inf2 9562 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115 ax-pre-sup 11116 ax-addf 11117

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-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-se 5585 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6266 df-ord 6327 df-on 6328 df-lim 6329 df-suc 6330 df-iota 6455 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-isom 6508 df-riota 7324 df-ov 7370 df-oprab 7371 df-mpo 7372 df-of 7631 df-om 7818 df-1st 7942 df-2nd 7943 df-supp 8111 df-frecs 8231 df-wrecs 8262 df-recs 8311 df-rdg 8349 df-1o 8405 df-2o 8406 df-oadd 8409 df-er 8643 df-map 8775 df-pm 8776 df-ixp 8846 df-en 8894 df-dom 8895 df-sdom 8896 df-fin 8897 df-fsupp 9275 df-fi 9324 df-sup 9355 df-inf 9356 df-oi 9425 df-dju 9825 df-card 9863 df-pnf 11181 df-mnf 11182 df-xr 11183 df-ltxr 11184 df-le 11185 df-sub 11379 df-neg 11380 df-div 11808 df-nn 12175 df-2 12244 df-3 12245 df-4 12246 df-5 12247 df-6 12248 df-7 12249 df-8 12250 df-9 12251 df-n0 12438 df-xnn0 12511 df-z 12525 df-dec 12645 df-uz 12789 df-q 12899 df-rp 12943 df-xneg 13063 df-xadd 13064 df-xmul 13065 df-ioo 13302 df-ioc 13303 df-ico 13304 df-icc 13305 df-fz 13462 df-fzo 13609 df-fl 13751 df-mod 13829 df-seq 13964 df-exp 14024 df-fac 14236 df-bc 14265 df-hash 14293 df-shft 15029 df-cj 15061 df-re 15062 df-im 15063 df-sqrt 15197 df-abs 15198 df-limsup 15433 df-clim 15450 df-rlim 15451 df-sum 15649 df-ef 16032 df-sin 16034 df-cos 16035 df-pi 16037 df-dvds 16222 df-gcd 16464 df-prm 16641 df-pc 16808 df-struct 17117 df-sets 17134 df-slot 17152 df-ndx 17164 df-base 17180 df-ress 17201 df-plusg 17233 df-mulr 17234 df-starv 17235 df-sca 17236 df-vsca 17237 df-ip 17238 df-tset 17239 df-ple 17240 df-ds 17242 df-unif 17243 df-hom 17244 df-cco 17245 df-rest 17385 df-topn 17386 df-0g 17404 df-gsum 17405 df-topgen 17406 df-pt 17407 df-prds 17410 df-xrs 17466 df-qtop 17471 df-imas 17472 df-xps 17474 df-mre 17548 df-mrc 17549 df-acs 17551 df-mgm 18608 df-sgrp 18687 df-mnd 18703 df-submnd 18752 df-mulg 19044 df-cntz 19292 df-cmn 19757 df-psmet 21344 df-xmet 21345 df-met 21346 df-bl 21347 df-mopn 21348 df-fbas 21349 df-fg 21350 df-cnfld 21353 df-top 22859 df-topon 22876 df-topsp 22898 df-bases 22911 df-cld 22984 df-ntr 22985 df-cls 22986 df-nei 23063 df-lp 23101 df-perf 23102 df-cn 23192 df-cnp 23193 df-haus 23280 df-tx 23527 df-hmeo 23720 df-fil 23811 df-fm 23903 df-flim 23904 df-flf 23905 df-xms 24285 df-ms 24286 df-tms 24287 df-cncf 24845 df-limc 25833 df-dv 25834 df-log 26520 df-cht 27060 df-vma 27061 df-chp 27062

This theorem is referenced by: chpchtlim 27442

W3C validator