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 27360

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 27264	. . . . 5 ⊢ (𝐴 ∈ ℝ → (ψ‘𝐴) ∈ ℝ)
2	1	adantr 485	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (ψ‘𝐴) ∈ ℝ)
3		chtcl 27249	. . . . 5 ⊢ (𝐴 ∈ ℝ → (θ‘𝐴) ∈ ℝ)
4	3	adantr 485	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (θ‘𝐴) ∈ ℝ)
5	2, 4	resubcld 11641	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((ψ‘𝐴) − (θ‘𝐴)) ∈ ℝ)
6		simpl 487	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 𝐴 ∈ ℝ)
7		0red 11210	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 0 ∈ ℝ)
8		1red 11208	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 1 ∈ ℝ)
9		0lt1 11735	. . . . . . . . . 10 ⊢ 0 < 1
10	9	a1i 11	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 0 < 1)
11		simpr 489	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 1 ≤ 𝐴)
12	7, 8, 6, 10, 11	ltletrd 11369	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 0 < 𝐴)
13	6, 12	elrpd 13056	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 𝐴 ∈ ℝ⁺)
14	13	rpge0d 13063	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 0 ≤ 𝐴)
15	6, 14	resqrtcld 15468	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (√‘𝐴) ∈ ℝ)
16		ppifi 27246	. . . . 5 ⊢ ((√‘𝐴) ∈ ℝ → ((0[,](√‘𝐴)) ∩ ℙ) ∈ Fin)
17	15, 16	syl 18	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((0[,](√‘𝐴)) ∩ ℙ) ∈ Fin)
18	13	adantr 485	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 𝐴 ∈ ℝ⁺)
19	18	relogcld 26764	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → (log‘𝐴) ∈ ℝ)
20	17, 19	fsumrecl 15784	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → Σ𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)(log‘𝐴) ∈ ℝ)
21	13	relogcld 26764	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (log‘𝐴) ∈ ℝ)
22	15, 21	remulcld 11238	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((√‘𝐴) · (log‘𝐴)) ∈ ℝ)
23		ppifi 27246	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → ((0[,]𝐴) ∩ ℙ) ∈ Fin)
24	23	adantr 485	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((0[,]𝐴) ∩ ℙ) ∈ Fin)
25		simpr 489	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ((0[,]𝐴) ∩ ℙ))
26	25	elin2d 4157	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℙ)
27		prmnn 16731	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
28	26, 27	syl 18	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℕ)
29	28	nnrpd 13057	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℝ⁺)
30	29	relogcld 26764	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈ ℝ)
31	21	adantr 485	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝐴) ∈ ℝ)
32	28	nnred 12247	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℝ)
33		prmuz2 16753	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ (ℤ_≥‘2))
34	26, 33	syl 18	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ (ℤ_≥‘2))
35		eluz2gt1 12943	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ (ℤ_≥‘2) → 1 < 𝑝)
36	34, 35	syl 18	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 1 < 𝑝)
37	32, 36	rplogcld 26770	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈ ℝ⁺)
38	31, 37	rerpdivcld 13090	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝐴) / (log‘𝑝)) ∈ ℝ)
39		reflcl 13828	. . . . . . . . 9 ⊢ (((log‘𝐴) / (log‘𝑝)) ∈ ℝ → (⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℝ)
40	38, 39	syl 18	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℝ)
41	30, 40	remulcld 11238	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) ∈ ℝ)
42	41	recnd 11236	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) ∈ ℂ)
43	30	recnd 11236	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈ ℂ)
44	24, 42, 43	fsumsub 15838	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) = (Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑝)))
45		0le0 12341	. . . . . . . . 9 ⊢ 0 ≤ 0
46	45	a1i 11	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 0 ≤ 0)
47	8, 6, 6, 14, 11	lemul2ad 12154	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (𝐴 · 1) ≤ (𝐴 · 𝐴))
48	6	recnd 11236	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 𝐴 ∈ ℂ)
49	48	sqsqrtd 15492	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((√‘𝐴)↑2) = 𝐴)
50	48	mulridd 11225	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (𝐴 · 1) = 𝐴)
51	49, 50	eqtr4d 2799	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((√‘𝐴)↑2) = (𝐴 · 1))
52	48	sqvald 14178	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (𝐴↑2) = (𝐴 · 𝐴))
53	47, 51, 52	3brtr4d 5142	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((√‘𝐴)↑2) ≤ (𝐴↑2))
54	6, 14	sqrtge0d 15471	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 0 ≤ (√‘𝐴))
55	15, 6, 54, 14	le2sqd 14292	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((√‘𝐴) ≤ 𝐴 ↔ ((√‘𝐴)↑2) ≤ (𝐴↑2)))
56	53, 55	mpbird 260	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (√‘𝐴) ≤ 𝐴)
57		iccss 13440	. . . . . . . 8 ⊢ (((0 ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ (0 ≤ 0 ∧ (√‘𝐴) ≤ 𝐴)) → (0[,](√‘𝐴)) ⊆ (0[,]𝐴))
58	7, 6, 46, 56, 57	syl22anc 851	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (0[,](√‘𝐴)) ⊆ (0[,]𝐴))
59	58	ssrind 4195	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((0[,](√‘𝐴)) ∩ ℙ) ⊆ ((0[,]𝐴) ∩ ℙ))
60	59	sselda 3936	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 𝑝 ∈ ((0[,]𝐴) ∩ ℙ))
61	41, 30	resubcld 11641	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ∈ ℝ)
62	61	recnd 11236	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ∈ ℂ)
63	60, 62	syldan 602	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → (((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ∈ ℂ)
64		eldifi 4084	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ)) → 𝑝 ∈ ((0[,]𝐴) ∩ ℙ))
65	64, 43	sylan2 604	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (log‘𝑝) ∈ ℂ)
66	65	mullidd 11226	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (1 · (log‘𝑝)) = (log‘𝑝))
67	25	elin1d 4156	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ (0[,]𝐴))
68		0re 11209	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ ℝ
69	6	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝐴 ∈ ℝ)
70		elicc2 13437	. . . . . . . . . . . . . . . . . 18 ⊢ ((0 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝑝 ∈ (0[,]𝐴) ↔ (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴)))
71	68, 69, 70	sylancr 598	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 ∈ (0[,]𝐴) ↔ (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴)))
72	67, 71	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴))
73	72	simp3d 1160	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ≤ 𝐴)
74	64, 73	sylan2 604	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 𝑝 ≤ 𝐴)
75	64, 29	sylan2 604	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 𝑝 ∈ ℝ⁺)
76	13	adantr 485	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 𝐴 ∈ ℝ⁺)
77	75, 76	logled 26768	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (𝑝 ≤ 𝐴 ↔ (log‘𝑝) ≤ (log‘𝐴)))
78	74, 77	mpbid 235	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (log‘𝑝) ≤ (log‘𝐴))
79	66, 78	eqbrtrd 5132	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (1 · (log‘𝑝)) ≤ (log‘𝐴))
80		1red 11208	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 1 ∈ ℝ)
81	21	adantr 485	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (log‘𝐴) ∈ ℝ)
82	64, 37	sylan2 604	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (log‘𝑝) ∈ ℝ⁺)
83	80, 81, 82	lemuldivd 13108	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((1 · (log‘𝑝)) ≤ (log‘𝐴) ↔ 1 ≤ ((log‘𝐴) / (log‘𝑝))))
84	79, 83	mpbid 235	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 1 ≤ ((log‘𝐴) / (log‘𝑝)))
85	6	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 𝐴 ∈ ℝ)
86	85	recnd 11236	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 𝐴 ∈ ℂ)
87	86	sqsqrtd 15492	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((√‘𝐴)↑2) = 𝐴)
88		eldifn 4085	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ)) → ¬ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ))
89	88	adantl 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ¬ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ))
90	64, 26	sylan2 604	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 𝑝 ∈ ℙ)
91		elin 3920	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ) ↔ (𝑝 ∈ (0[,](√‘𝐴)) ∧ 𝑝 ∈ ℙ))
92	91	rbaib 547	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 ∈ ℙ → (𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ) ↔ 𝑝 ∈ (0[,](√‘𝐴))))
93	90, 92	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ) ↔ 𝑝 ∈ (0[,](√‘𝐴))))
94		0red 11210	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 0 ∈ ℝ)
95	15	adantr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (√‘𝐴) ∈ ℝ)
96	64, 28	sylan2 604	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 𝑝 ∈ ℕ)
97	96	nnred 12247	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 𝑝 ∈ ℝ)
98	75	rpge0d 13063	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 0 ≤ 𝑝)
99		elicc2 13437	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((0 ∈ ℝ ∧ (√‘𝐴) ∈ ℝ) → (𝑝 ∈ (0[,](√‘𝐴)) ↔ (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ (√‘𝐴))))
100		df-3an 1103	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ (√‘𝐴)) ↔ ((𝑝 ∈ ℝ ∧ 0 ≤ 𝑝) ∧ 𝑝 ≤ (√‘𝐴)))
101	99, 100	bitrdi 290	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((0 ∈ ℝ ∧ (√‘𝐴) ∈ ℝ) → (𝑝 ∈ (0[,](√‘𝐴)) ↔ ((𝑝 ∈ ℝ ∧ 0 ≤ 𝑝) ∧ 𝑝 ≤ (√‘𝐴))))
102	101	baibd 548	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((0 ∈ ℝ ∧ (√‘𝐴) ∈ ℝ) ∧ (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝)) → (𝑝 ∈ (0[,](√‘𝐴)) ↔ 𝑝 ≤ (√‘𝐴)))
103	94, 95, 97, 98, 102	syl22anc 851	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (𝑝 ∈ (0[,](√‘𝐴)) ↔ 𝑝 ≤ (√‘𝐴)))
104	93, 103	bitrd 282	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ) ↔ 𝑝 ≤ (√‘𝐴)))
105	89, 104	mtbid 327	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ¬ 𝑝 ≤ (√‘𝐴))
106	95, 97	ltnled 11356	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((√‘𝐴) < 𝑝 ↔ ¬ 𝑝 ≤ (√‘𝐴)))
107	105, 106	mpbird 260	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (√‘𝐴) < 𝑝)
108	54	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 0 ≤ (√‘𝐴))
109	95, 97, 108, 98	lt2sqd 14291	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((√‘𝐴) < 𝑝 ↔ ((√‘𝐴)↑2) < (𝑝↑2)))
110	107, 109	mpbid 235	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((√‘𝐴)↑2) < (𝑝↑2))
111	87, 110	eqbrtrrd 5134	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 𝐴 < (𝑝↑2))
112	96	nnsqcld 14279	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (𝑝↑2) ∈ ℕ)
113	112	nnrpd 13057	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (𝑝↑2) ∈ ℝ⁺)
114		logltb 26741	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℝ⁺ ∧ (𝑝↑2) ∈ ℝ⁺) → (𝐴 < (𝑝↑2) ↔ (log‘𝐴) < (log‘(𝑝↑2))))
115	76, 113, 114	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (𝐴 < (𝑝↑2) ↔ (log‘𝐴) < (log‘(𝑝↑2))))
116	111, 115	mpbid 235	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (log‘𝐴) < (log‘(𝑝↑2)))
117		2z 12625	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℤ
118		relogexp 26737	. . . . . . . . . . . . . . 15 ⊢ ((𝑝 ∈ ℝ⁺ ∧ 2 ∈ ℤ) → (log‘(𝑝↑2)) = (2 · (log‘𝑝)))
119	75, 117, 118	sylancl 597	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (log‘(𝑝↑2)) = (2 · (log‘𝑝)))
120	116, 119	breqtrd 5136	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (log‘𝐴) < (2 · (log‘𝑝)))
121		2re 12314	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℝ
122	121	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 2 ∈ ℝ)
123	81, 122, 82	ltdivmul2d 13111	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (((log‘𝐴) / (log‘𝑝)) < 2 ↔ (log‘𝐴) < (2 · (log‘𝑝))))
124	120, 123	mpbird 260	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((log‘𝐴) / (log‘𝑝)) < 2)
125		df-2 12302	. . . . . . . . . . . 12 ⊢ 2 = (1 + 1)
126	124, 125	breqtrdi 5151	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((log‘𝐴) / (log‘𝑝)) < (1 + 1))
127	64, 38	sylan2 604	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((log‘𝐴) / (log‘𝑝)) ∈ ℝ)
128		1z 12623	. . . . . . . . . . . 12 ⊢ 1 ∈ ℤ
129		flbi 13848	. . . . . . . . . . . 12 ⊢ ((((log‘𝐴) / (log‘𝑝)) ∈ ℝ ∧ 1 ∈ ℤ) → ((⌊‘((log‘𝐴) / (log‘𝑝))) = 1 ↔ (1 ≤ ((log‘𝐴) / (log‘𝑝)) ∧ ((log‘𝐴) / (log‘𝑝)) < (1 + 1))))
130	127, 128, 129	sylancl 597	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((⌊‘((log‘𝐴) / (log‘𝑝))) = 1 ↔ (1 ≤ ((log‘𝐴) / (log‘𝑝)) ∧ ((log‘𝐴) / (log‘𝑝)) < (1 + 1))))
131	84, 126, 130	mpbir2and 725	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (⌊‘((log‘𝐴) / (log‘𝑝))) = 1)
132	131	oveq2d 7426	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) = ((log‘𝑝) · 1))
133	65	mulridd 11225	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((log‘𝑝) · 1) = (log‘𝑝))
134	132, 133	eqtrd 2796	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) = (log‘𝑝))
135	134	oveq1d 7425	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) = ((log‘𝑝) − (log‘𝑝)))
136	65	subidd 11556	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((log‘𝑝) − (log‘𝑝)) = 0)
137	135, 136	eqtrd 2796	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) = 0)
138	59, 63, 137, 24	fsumss 15775	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → Σ𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)(((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)))
139		chpval2 27358	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → (ψ‘𝐴) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))))
140	139	adantr 485	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (ψ‘𝐴) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))))
141		chtval 27250	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → (θ‘𝐴) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑝))
142	141	adantr 485	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (θ‘𝐴) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑝))
143	140, 142	oveq12d 7428	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((ψ‘𝐴) − (θ‘𝐴)) = (Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑝)))
144	44, 138, 143	3eqtr4rd 2807	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((ψ‘𝐴) − (θ‘𝐴)) = Σ𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)(((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)))
145	60, 61	syldan 602	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → (((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ∈ ℝ)
146	60, 41	syldan 602	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) ∈ ℝ)
147	60, 37	syldan 602	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → (log‘𝑝) ∈ ℝ⁺)
148	147	rpge0d 13063	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 0 ≤ (log‘𝑝))
149		simpr 489	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ))
150	149	elin2d 4157	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 𝑝 ∈ ℙ)
151	150, 27	syl 18	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 𝑝 ∈ ℕ)
152	151	nnrpd 13057	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 𝑝 ∈ ℝ⁺)
153	152	relogcld 26764	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → (log‘𝑝) ∈ ℝ)
154	146, 153	subge02d 11805	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → (0 ≤ (log‘𝑝) ↔ (((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ≤ ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝))))))
155	148, 154	mpbid 235	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → (((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ≤ ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))))
156	60, 38	syldan 602	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → ((log‘𝐴) / (log‘𝑝)) ∈ ℝ)
157		flle 13831	. . . . . . . 8 ⊢ (((log‘𝐴) / (log‘𝑝)) ∈ ℝ → (⌊‘((log‘𝐴) / (log‘𝑝))) ≤ ((log‘𝐴) / (log‘𝑝)))
158	156, 157	syl 18	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → (⌊‘((log‘𝐴) / (log‘𝑝))) ≤ ((log‘𝐴) / (log‘𝑝)))
159	60, 40	syldan 602	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → (⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℝ)
160	159, 19, 147	lemuldiv2d 13109	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → (((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) ≤ (log‘𝐴) ↔ (⌊‘((log‘𝐴) / (log‘𝑝))) ≤ ((log‘𝐴) / (log‘𝑝))))
161	158, 160	mpbird 260	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) ≤ (log‘𝐴))
162	145, 146, 19, 155, 161	letrd 11366	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → (((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ≤ (log‘𝐴))
163	17, 145, 19, 162	fsumle 15850	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → Σ𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)(((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ≤ Σ𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)(log‘𝐴))
164	144, 163	eqbrtrd 5132	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((ψ‘𝐴) − (θ‘𝐴)) ≤ Σ𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)(log‘𝐴))
165	21	recnd 11236	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (log‘𝐴) ∈ ℂ)
166		fsumconst 15840	. . . . 5 ⊢ ((((0[,](√‘𝐴)) ∩ ℙ) ∈ Fin ∧ (log‘𝐴) ∈ ℂ) → Σ𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)(log‘𝐴) = ((♯‘((0[,](√‘𝐴)) ∩ ℙ)) · (log‘𝐴)))
167	17, 165, 166	syl2anc 595	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → Σ𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)(log‘𝐴) = ((♯‘((0[,](√‘𝐴)) ∩ ℙ)) · (log‘𝐴)))
168		hashcl 14391	. . . . . . 7 ⊢ (((0[,](√‘𝐴)) ∩ ℙ) ∈ Fin → (♯‘((0[,](√‘𝐴)) ∩ ℙ)) ∈ ℕ₀)
169	17, 168	syl 18	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (♯‘((0[,](√‘𝐴)) ∩ ℙ)) ∈ ℕ₀)
170	169	nn0red 12565	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (♯‘((0[,](√‘𝐴)) ∩ ℙ)) ∈ ℝ)
171		logge0 26746	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 0 ≤ (log‘𝐴))
172		reflcl 13828	. . . . . . 7 ⊢ ((√‘𝐴) ∈ ℝ → (⌊‘(√‘𝐴)) ∈ ℝ)
173	15, 172	syl 18	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (⌊‘(√‘𝐴)) ∈ ℝ)
174		fzfid 14008	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (1...(⌊‘(√‘𝐴))) ∈ Fin)
175		ppisval 27244	. . . . . . . . . . 11 ⊢ ((√‘𝐴) ∈ ℝ → ((0[,](√‘𝐴)) ∩ ℙ) = ((2...(⌊‘(√‘𝐴))) ∩ ℙ))
176	15, 175	syl 18	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((0[,](√‘𝐴)) ∩ ℙ) = ((2...(⌊‘(√‘𝐴))) ∩ ℙ))
177		inss1 4188	. . . . . . . . . . 11 ⊢ ((2...(⌊‘(√‘𝐴))) ∩ ℙ) ⊆ (2...(⌊‘(√‘𝐴)))
178		2eluzge1 12905	. . . . . . . . . . . 12 ⊢ 2 ∈ (ℤ_≥‘1)
179		fzss1 13590	. . . . . . . . . . . 12 ⊢ (2 ∈ (ℤ_≥‘1) → (2...(⌊‘(√‘𝐴))) ⊆ (1...(⌊‘(√‘𝐴))))
180	178, 179	mp1i 14	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (2...(⌊‘(√‘𝐴))) ⊆ (1...(⌊‘(√‘𝐴))))
181	177, 180	sstrid 3947	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((2...(⌊‘(√‘𝐴))) ∩ ℙ) ⊆ (1...(⌊‘(√‘𝐴))))
182	176, 181	eqsstrd 3970	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((0[,](√‘𝐴)) ∩ ℙ) ⊆ (1...(⌊‘(√‘𝐴))))
183		ssdomg 8996	. . . . . . . . 9 ⊢ ((1...(⌊‘(√‘𝐴))) ∈ Fin → (((0[,](√‘𝐴)) ∩ ℙ) ⊆ (1...(⌊‘(√‘𝐴))) → ((0[,](√‘𝐴)) ∩ ℙ) ≼ (1...(⌊‘(√‘𝐴)))))
184	174, 182, 183	sylc 66	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((0[,](√‘𝐴)) ∩ ℙ) ≼ (1...(⌊‘(√‘𝐴))))
185		hashdom 14414	. . . . . . . . 9 ⊢ ((((0[,](√‘𝐴)) ∩ ℙ) ∈ Fin ∧ (1...(⌊‘(√‘𝐴))) ∈ Fin) → ((♯‘((0[,](√‘𝐴)) ∩ ℙ)) ≤ (♯‘(1...(⌊‘(√‘𝐴)))) ↔ ((0[,](√‘𝐴)) ∩ ℙ) ≼ (1...(⌊‘(√‘𝐴)))))
186	17, 174, 185	syl2anc 595	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((♯‘((0[,](√‘𝐴)) ∩ ℙ)) ≤ (♯‘(1...(⌊‘(√‘𝐴)))) ↔ ((0[,](√‘𝐴)) ∩ ℙ) ≼ (1...(⌊‘(√‘𝐴)))))
187	184, 186	mpbird 260	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (♯‘((0[,](√‘𝐴)) ∩ ℙ)) ≤ (♯‘(1...(⌊‘(√‘𝐴)))))
188		flge0nn0 13852	. . . . . . . . 9 ⊢ (((√‘𝐴) ∈ ℝ ∧ 0 ≤ (√‘𝐴)) → (⌊‘(√‘𝐴)) ∈ ℕ₀)
189	15, 54, 188	syl2anc 595	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (⌊‘(√‘𝐴)) ∈ ℕ₀)
190		hashfz1 14381	. . . . . . . 8 ⊢ ((⌊‘(√‘𝐴)) ∈ ℕ₀ → (♯‘(1...(⌊‘(√‘𝐴)))) = (⌊‘(√‘𝐴)))
191	189, 190	syl 18	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (♯‘(1...(⌊‘(√‘𝐴)))) = (⌊‘(√‘𝐴)))
192	187, 191	breqtrd 5136	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (♯‘((0[,](√‘𝐴)) ∩ ℙ)) ≤ (⌊‘(√‘𝐴)))
193		flle 13831	. . . . . . 7 ⊢ ((√‘𝐴) ∈ ℝ → (⌊‘(√‘𝐴)) ≤ (√‘𝐴))
194	15, 193	syl 18	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (⌊‘(√‘𝐴)) ≤ (√‘𝐴))
195	170, 173, 15, 192, 194	letrd 11366	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (♯‘((0[,](√‘𝐴)) ∩ ℙ)) ≤ (√‘𝐴))
196	170, 15, 21, 171, 195	lemul1ad 12153	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((♯‘((0[,](√‘𝐴)) ∩ ℙ)) · (log‘𝐴)) ≤ ((√‘𝐴) · (log‘𝐴)))
197	167, 196	eqbrtrd 5132	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → Σ𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)(log‘𝐴) ≤ ((√‘𝐴) · (log‘𝐴)))
198	5, 20, 22, 164, 197	letrd 11366	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((ψ‘𝐴) − (θ‘𝐴)) ≤ ((√‘𝐴) · (log‘𝐴)))
199	2, 4, 22	lesubadd2d 11812	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (((ψ‘𝐴) − (θ‘𝐴)) ≤ ((√‘𝐴) · (log‘𝐴)) ↔ (ψ‘𝐴) ≤ ((θ‘𝐴) + ((√‘𝐴) · (log‘𝐴)))))
200	198, 199	mpbid 235	1 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (ψ‘𝐴) ≤ ((θ‘𝐴) + ((√‘𝐴) · (log‘𝐴))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1101 = wceq 1568 ∈ wcel 2141 ∖ cdif 3901 ∩ cin 3903 ⊆ wss 3904 class class class wbr 5108 ‘cfv 6536 (class class class)co 7410 ≼ cdom 8940 Fincfn 8942 ℂcc 11097 ℝcr 11098 0cc0 11099 1c1 11100 + caddc 11102 · cmul 11104 < clt 11242 ≤ cle 11243 − cmin 11440 / cdiv 11870 ℕcn 12232 2c2 12294 ℕ₀cn0 12503 ℤcz 12590 ℤ_≥cuz 12861 ℝ⁺crp 13015 [,]cicc 13374 ...cfz 13534 ⌊cfl 13822 ↑cexp 14096 ♯chash 14365 √csqrt 15283 Σcsu 15736 ℙcprime 16728 logclog 26695 θccht 27231 ψcchp 27233

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1823 ax-4 1837 ax-5 1938 ax-6 1995 ax-7 2036 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5237 ax-sep 5256 ax-nul 5268 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-inf2 9609 ax-cnex 11155 ax-resscn 11156 ax-1cn 11157 ax-icn 11158 ax-addcl 11159 ax-addrcl 11160 ax-mulcl 11161 ax-mulrcl 11162 ax-mulcom 11163 ax-addass 11164 ax-mulass 11165 ax-distr 11166 ax-i2m1 11167 ax-1ne0 11168 ax-1rid 11169 ax-rnegex 11170 ax-rrecex 11171 ax-cnre 11172 ax-pre-lttri 11173 ax-pre-lttrn 11174 ax-pre-ltadd 11175 ax-pre-mulgt0 11176 ax-pre-sup 11177 ax-addf 11178

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1571 df-fal 1581 df-ex 1808 df-nf 1812 df-sb 2095 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3744 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4487 df-pw 4563 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4595 df-uni 4872 df-int 4912 df-iun 4957 df-iin 4958 df-br 5109 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-se 5615 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-isom 6545 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-of 7674 df-om 7862 df-1st 7985 df-2nd 7986 df-supp 8156 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-1o 8452 df-2o 8453 df-oadd 8456 df-er 8693 df-map 8825 df-pm 8826 df-ixp 8895 df-en 8943 df-dom 8944 df-sdom 8945 df-fin 8946 df-fsupp 9321 df-fi 9370 df-sup 9401 df-inf 9402 df-oi 9471 df-dju 9886 df-card 9924 df-pnf 11244 df-mnf 11245 df-xr 11246 df-ltxr 11247 df-le 11248 df-sub 11442 df-neg 11443 df-div 11871 df-nn 12233 df-2 12302 df-3 12303 df-4 12304 df-5 12305 df-6 12306 df-7 12307 df-8 12308 df-9 12309 df-n0 12504 df-xnn0 12577 df-z 12591 df-dec 12711 df-uz 12862 df-q 12972 df-rp 13016 df-xneg 13136 df-xadd 13137 df-xmul 13138 df-ioo 13375 df-ioc 13376 df-ico 13377 df-icc 13378 df-fz 13535 df-fzo 13682 df-fl 13824 df-mod 13902 df-seq 14037 df-exp 14097 df-fac 14309 df-bc 14338 df-hash 14366 df-shft 15103 df-cj 15149 df-re 15150 df-im 15151 df-sqrt 15285 df-abs 15286 df-limsup 15521 df-clim 15538 df-rlim 15539 df-sum 15737 df-ef 16120 df-sin 16122 df-cos 16123 df-pi 16125 df-dvds 16310 df-gcd 16552 df-prm 16729 df-pc 16896 df-struct 17206 df-sets 17223 df-slot 17241 df-ndx 17253 df-base 17269 df-ress 17290 df-plusg 17322 df-mulr 17323 df-starv 17324 df-sca 17325 df-vsca 17326 df-ip 17327 df-tset 17328 df-ple 17329 df-ds 17331 df-unif 17332 df-hom 17333 df-cco 17334 df-rest 17474 df-topn 17475 df-0g 17493 df-gsum 17494 df-topgen 17495 df-pt 17496 df-prds 17499 df-xrs 17555 df-qtop 17560 df-imas 17561 df-xps 17563 df-mre 17637 df-mrc 17638 df-acs 17640 df-mgm 18697 df-sgrp 18776 df-mnd 18792 df-submnd 18841 df-mulg 19133 df-cntz 19386 df-cmn 19851 df-psmet 21493 df-xmet 21494 df-met 21495 df-bl 21496 df-mopn 21497 df-fbas 21498 df-fg 21499 df-cnfld 21502 df-top 23030 df-topon 23047 df-topsp 23069 df-bases 23082 df-cld 23155 df-ntr 23156 df-cls 23157 df-nei 23234 df-lp 23272 df-perf 23273 df-cn 23363 df-cnp 23364 df-haus 23451 df-tx 23698 df-hmeo 23891 df-fil 23982 df-fm 24074 df-flim 24075 df-flf 24076 df-xms 24456 df-ms 24457 df-tms 24458 df-cncf 25016 df-limc 26004 df-dv 26005 df-log 26697 df-cht 27237 df-vma 27238 df-chp 27239

This theorem is referenced by: chpchtlim 27619

W3C validator