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 25799

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 25704	. . . . 5 ⊢ (𝐴 ∈ ℝ → (ψ‘𝐴) ∈ ℝ)
2	1	adantr 483	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (ψ‘𝐴) ∈ ℝ)
3		chtcl 25689	. . . . 5 ⊢ (𝐴 ∈ ℝ → (θ‘𝐴) ∈ ℝ)
4	3	adantr 483	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (θ‘𝐴) ∈ ℝ)
5	2, 4	resubcld 11071	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((ψ‘𝐴) − (θ‘𝐴)) ∈ ℝ)
6		simpl 485	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 𝐴 ∈ ℝ)
7		0red 10647	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 0 ∈ ℝ)
8		1red 10645	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 1 ∈ ℝ)
9		0lt1 11165	. . . . . . . . . 10 ⊢ 0 < 1
10	9	a1i 11	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 0 < 1)
11		simpr 487	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 1 ≤ 𝐴)
12	7, 8, 6, 10, 11	ltletrd 10803	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 0 < 𝐴)
13	6, 12	elrpd 12431	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 𝐴 ∈ ℝ⁺)
14	13	rpge0d 12438	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 0 ≤ 𝐴)
15	6, 14	resqrtcld 14780	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (√‘𝐴) ∈ ℝ)
16		ppifi 25686	. . . . 5 ⊢ ((√‘𝐴) ∈ ℝ → ((0[,](√‘𝐴)) ∩ ℙ) ∈ Fin)
17	15, 16	syl 17	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((0[,](√‘𝐴)) ∩ ℙ) ∈ Fin)
18	13	adantr 483	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 𝐴 ∈ ℝ⁺)
19	18	relogcld 25209	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → (log‘𝐴) ∈ ℝ)
20	17, 19	fsumrecl 15094	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → Σ𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)(log‘𝐴) ∈ ℝ)
21	13	relogcld 25209	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (log‘𝐴) ∈ ℝ)
22	15, 21	remulcld 10674	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((√‘𝐴) · (log‘𝐴)) ∈ ℝ)
23		ppifi 25686	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → ((0[,]𝐴) ∩ ℙ) ∈ Fin)
24	23	adantr 483	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((0[,]𝐴) ∩ ℙ) ∈ Fin)
25		simpr 487	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ((0[,]𝐴) ∩ ℙ))
26	25	elin2d 4179	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℙ)
27		prmnn 16021	. . . . . . . . . . 11 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
28	26, 27	syl 17	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℕ)
29	28	nnrpd 12432	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℝ⁺)
30	29	relogcld 25209	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈ ℝ)
31	21	adantr 483	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝐴) ∈ ℝ)
32	28	nnred 11656	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℝ)
33		prmuz2 16043	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ (ℤ_≥‘2))
34	26, 33	syl 17	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ (ℤ_≥‘2))
35		eluz2gt1 12323	. . . . . . . . . . . 12 ⊢ (𝑝 ∈ (ℤ_≥‘2) → 1 < 𝑝)
36	34, 35	syl 17	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 1 < 𝑝)
37	32, 36	rplogcld 25215	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈ ℝ⁺)
38	31, 37	rerpdivcld 12465	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝐴) / (log‘𝑝)) ∈ ℝ)
39		reflcl 13169	. . . . . . . . 9 ⊢ (((log‘𝐴) / (log‘𝑝)) ∈ ℝ → (⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℝ)
40	38, 39	syl 17	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℝ)
41	30, 40	remulcld 10674	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) ∈ ℝ)
42	41	recnd 10672	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) ∈ ℂ)
43	30	recnd 10672	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈ ℂ)
44	24, 42, 43	fsumsub 15146	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) = (Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑝)))
45		0le0 11741	. . . . . . . . 9 ⊢ 0 ≤ 0
46	45	a1i 11	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 0 ≤ 0)
47	8, 6, 6, 14, 11	lemul2ad 11583	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (𝐴 · 1) ≤ (𝐴 · 𝐴))
48	6	recnd 10672	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 𝐴 ∈ ℂ)
49	48	sqsqrtd 14802	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((√‘𝐴)↑2) = 𝐴)
50	48	mulid1d 10661	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (𝐴 · 1) = 𝐴)
51	49, 50	eqtr4d 2862	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((√‘𝐴)↑2) = (𝐴 · 1))
52	48	sqvald 13510	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (𝐴↑2) = (𝐴 · 𝐴))
53	47, 51, 52	3brtr4d 5101	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((√‘𝐴)↑2) ≤ (𝐴↑2))
54	6, 14	sqrtge0d 14783	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 0 ≤ (√‘𝐴))
55	15, 6, 54, 14	le2sqd 13623	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((√‘𝐴) ≤ 𝐴 ↔ ((√‘𝐴)↑2) ≤ (𝐴↑2)))
56	53, 55	mpbird 259	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (√‘𝐴) ≤ 𝐴)
57		iccss 12807	. . . . . . . 8 ⊢ (((0 ∈ ℝ ∧ 𝐴 ∈ ℝ) ∧ (0 ≤ 0 ∧ (√‘𝐴) ≤ 𝐴)) → (0[,](√‘𝐴)) ⊆ (0[,]𝐴))
58	7, 6, 46, 56, 57	syl22anc 836	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (0[,](√‘𝐴)) ⊆ (0[,]𝐴))
59	58	ssrind 4215	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((0[,](√‘𝐴)) ∩ ℙ) ⊆ ((0[,]𝐴) ∩ ℙ))
60	59	sselda 3970	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 𝑝 ∈ ((0[,]𝐴) ∩ ℙ))
61	41, 30	resubcld 11071	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ∈ ℝ)
62	61	recnd 10672	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ∈ ℂ)
63	60, 62	syldan 593	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → (((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ∈ ℂ)
64		eldifi 4106	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ)) → 𝑝 ∈ ((0[,]𝐴) ∩ ℙ))
65	64, 43	sylan2 594	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (log‘𝑝) ∈ ℂ)
66	65	mulid2d 10662	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (1 · (log‘𝑝)) = (log‘𝑝))
67	25	elin1d 4178	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ (0[,]𝐴))
68		0re 10646	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ ℝ
69	6	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝐴 ∈ ℝ)
70		elicc2 12804	. . . . . . . . . . . . . . . . . 18 ⊢ ((0 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝑝 ∈ (0[,]𝐴) ↔ (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴)))
71	68, 69, 70	sylancr 589	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 ∈ (0[,]𝐴) ↔ (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴)))
72	67, 71	mpbid 234	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴))
73	72	simp3d 1140	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ≤ 𝐴)
74	64, 73	sylan2 594	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 𝑝 ≤ 𝐴)
75	64, 29	sylan2 594	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 𝑝 ∈ ℝ⁺)
76	13	adantr 483	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 𝐴 ∈ ℝ⁺)
77	75, 76	logled 25213	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (𝑝 ≤ 𝐴 ↔ (log‘𝑝) ≤ (log‘𝐴)))
78	74, 77	mpbid 234	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (log‘𝑝) ≤ (log‘𝐴))
79	66, 78	eqbrtrd 5091	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (1 · (log‘𝑝)) ≤ (log‘𝐴))
80		1red 10645	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 1 ∈ ℝ)
81	21	adantr 483	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (log‘𝐴) ∈ ℝ)
82	64, 37	sylan2 594	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (log‘𝑝) ∈ ℝ⁺)
83	80, 81, 82	lemuldivd 12483	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((1 · (log‘𝑝)) ≤ (log‘𝐴) ↔ 1 ≤ ((log‘𝐴) / (log‘𝑝))))
84	79, 83	mpbid 234	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 1 ≤ ((log‘𝐴) / (log‘𝑝)))
85	6	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 𝐴 ∈ ℝ)
86	85	recnd 10672	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 𝐴 ∈ ℂ)
87	86	sqsqrtd 14802	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((√‘𝐴)↑2) = 𝐴)
88		eldifn 4107	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ)) → ¬ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ))
89	88	adantl 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ¬ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ))
90	64, 26	sylan2 594	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 𝑝 ∈ ℙ)
91		elin 4172	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ) ↔ (𝑝 ∈ (0[,](√‘𝐴)) ∧ 𝑝 ∈ ℙ))
92	91	rbaib 541	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 ∈ ℙ → (𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ) ↔ 𝑝 ∈ (0[,](√‘𝐴))))
93	90, 92	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ) ↔ 𝑝 ∈ (0[,](√‘𝐴))))
94		0red 10647	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 0 ∈ ℝ)
95	15	adantr 483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (√‘𝐴) ∈ ℝ)
96	64, 28	sylan2 594	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 𝑝 ∈ ℕ)
97	96	nnred 11656	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 𝑝 ∈ ℝ)
98	75	rpge0d 12438	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 0 ≤ 𝑝)
99		elicc2 12804	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((0 ∈ ℝ ∧ (√‘𝐴) ∈ ℝ) → (𝑝 ∈ (0[,](√‘𝐴)) ↔ (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ (√‘𝐴))))
100		df-3an 1085	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ (√‘𝐴)) ↔ ((𝑝 ∈ ℝ ∧ 0 ≤ 𝑝) ∧ 𝑝 ≤ (√‘𝐴)))
101	99, 100	syl6bb 289	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((0 ∈ ℝ ∧ (√‘𝐴) ∈ ℝ) → (𝑝 ∈ (0[,](√‘𝐴)) ↔ ((𝑝 ∈ ℝ ∧ 0 ≤ 𝑝) ∧ 𝑝 ≤ (√‘𝐴))))
102	101	baibd 542	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((0 ∈ ℝ ∧ (√‘𝐴) ∈ ℝ) ∧ (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝)) → (𝑝 ∈ (0[,](√‘𝐴)) ↔ 𝑝 ≤ (√‘𝐴)))
103	94, 95, 97, 98, 102	syl22anc 836	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (𝑝 ∈ (0[,](√‘𝐴)) ↔ 𝑝 ≤ (√‘𝐴)))
104	93, 103	bitrd 281	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ) ↔ 𝑝 ≤ (√‘𝐴)))
105	89, 104	mtbid 326	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ¬ 𝑝 ≤ (√‘𝐴))
106	95, 97	ltnled 10790	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((√‘𝐴) < 𝑝 ↔ ¬ 𝑝 ≤ (√‘𝐴)))
107	105, 106	mpbird 259	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (√‘𝐴) < 𝑝)
108	54	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 0 ≤ (√‘𝐴))
109	95, 97, 108, 98	lt2sqd 13622	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((√‘𝐴) < 𝑝 ↔ ((√‘𝐴)↑2) < (𝑝↑2)))
110	107, 109	mpbid 234	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((√‘𝐴)↑2) < (𝑝↑2))
111	87, 110	eqbrtrrd 5093	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 𝐴 < (𝑝↑2))
112	96	nnsqcld 13608	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (𝑝↑2) ∈ ℕ)
113	112	nnrpd 12432	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (𝑝↑2) ∈ ℝ⁺)
114		logltb 25186	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℝ⁺ ∧ (𝑝↑2) ∈ ℝ⁺) → (𝐴 < (𝑝↑2) ↔ (log‘𝐴) < (log‘(𝑝↑2))))
115	76, 113, 114	syl2anc 586	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (𝐴 < (𝑝↑2) ↔ (log‘𝐴) < (log‘(𝑝↑2))))
116	111, 115	mpbid 234	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (log‘𝐴) < (log‘(𝑝↑2)))
117		2z 12017	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℤ
118		relogexp 25182	. . . . . . . . . . . . . . 15 ⊢ ((𝑝 ∈ ℝ⁺ ∧ 2 ∈ ℤ) → (log‘(𝑝↑2)) = (2 · (log‘𝑝)))
119	75, 117, 118	sylancl 588	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (log‘(𝑝↑2)) = (2 · (log‘𝑝)))
120	116, 119	breqtrd 5095	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (log‘𝐴) < (2 · (log‘𝑝)))
121		2re 11714	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℝ
122	121	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → 2 ∈ ℝ)
123	81, 122, 82	ltdivmul2d 12486	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (((log‘𝐴) / (log‘𝑝)) < 2 ↔ (log‘𝐴) < (2 · (log‘𝑝))))
124	120, 123	mpbird 259	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((log‘𝐴) / (log‘𝑝)) < 2)
125		df-2 11703	. . . . . . . . . . . 12 ⊢ 2 = (1 + 1)
126	124, 125	breqtrdi 5110	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((log‘𝐴) / (log‘𝑝)) < (1 + 1))
127	64, 38	sylan2 594	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((log‘𝐴) / (log‘𝑝)) ∈ ℝ)
128		1z 12015	. . . . . . . . . . . 12 ⊢ 1 ∈ ℤ
129		flbi 13189	. . . . . . . . . . . 12 ⊢ ((((log‘𝐴) / (log‘𝑝)) ∈ ℝ ∧ 1 ∈ ℤ) → ((⌊‘((log‘𝐴) / (log‘𝑝))) = 1 ↔ (1 ≤ ((log‘𝐴) / (log‘𝑝)) ∧ ((log‘𝐴) / (log‘𝑝)) < (1 + 1))))
130	127, 128, 129	sylancl 588	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((⌊‘((log‘𝐴) / (log‘𝑝))) = 1 ↔ (1 ≤ ((log‘𝐴) / (log‘𝑝)) ∧ ((log‘𝐴) / (log‘𝑝)) < (1 + 1))))
131	84, 126, 130	mpbir2and 711	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (⌊‘((log‘𝐴) / (log‘𝑝))) = 1)
132	131	oveq2d 7175	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) = ((log‘𝑝) · 1))
133	65	mulid1d 10661	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((log‘𝑝) · 1) = (log‘𝑝))
134	132, 133	eqtrd 2859	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) = (log‘𝑝))
135	134	oveq1d 7174	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) = ((log‘𝑝) − (log‘𝑝)))
136	65	subidd 10988	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → ((log‘𝑝) − (log‘𝑝)) = 0)
137	135, 136	eqtrd 2859	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖ ((0[,](√‘𝐴)) ∩ ℙ))) → (((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) = 0)
138	59, 63, 137, 24	fsumss 15085	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → Σ𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)(((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)))
139		chpval2 25797	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → (ψ‘𝐴) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))))
140	139	adantr 483	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (ψ‘𝐴) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))))
141		chtval 25690	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → (θ‘𝐴) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑝))
142	141	adantr 483	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (θ‘𝐴) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑝))
143	140, 142	oveq12d 7177	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((ψ‘𝐴) − (θ‘𝐴)) = (Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑝)))
144	44, 138, 143	3eqtr4rd 2870	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((ψ‘𝐴) − (θ‘𝐴)) = Σ𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)(((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)))
145	60, 61	syldan 593	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → (((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ∈ ℝ)
146	60, 41	syldan 593	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) ∈ ℝ)
147	60, 37	syldan 593	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → (log‘𝑝) ∈ ℝ⁺)
148	147	rpge0d 12438	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 0 ≤ (log‘𝑝))
149		simpr 487	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ))
150	149	elin2d 4179	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 𝑝 ∈ ℙ)
151	150, 27	syl 17	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 𝑝 ∈ ℕ)
152	151	nnrpd 12432	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 𝑝 ∈ ℝ⁺)
153	152	relogcld 25209	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → (log‘𝑝) ∈ ℝ)
154	146, 153	subge02d 11235	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → (0 ≤ (log‘𝑝) ↔ (((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ≤ ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝))))))
155	148, 154	mpbid 234	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → (((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ≤ ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))))
156	60, 38	syldan 593	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → ((log‘𝐴) / (log‘𝑝)) ∈ ℝ)
157		flle 13172	. . . . . . . 8 ⊢ (((log‘𝐴) / (log‘𝑝)) ∈ ℝ → (⌊‘((log‘𝐴) / (log‘𝑝))) ≤ ((log‘𝐴) / (log‘𝑝)))
158	156, 157	syl 17	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → (⌊‘((log‘𝐴) / (log‘𝑝))) ≤ ((log‘𝐴) / (log‘𝑝)))
159	60, 40	syldan 593	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → (⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℝ)
160	159, 19, 147	lemuldiv2d 12484	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → (((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) ≤ (log‘𝐴) ↔ (⌊‘((log‘𝐴) / (log‘𝑝))) ≤ ((log‘𝐴) / (log‘𝑝))))
161	158, 160	mpbird 259	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) ≤ (log‘𝐴))
162	145, 146, 19, 155, 161	letrd 10800	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → (((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ≤ (log‘𝐴))
163	17, 145, 19, 162	fsumle 15157	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → Σ𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)(((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ≤ Σ𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)(log‘𝐴))
164	144, 163	eqbrtrd 5091	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((ψ‘𝐴) − (θ‘𝐴)) ≤ Σ𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)(log‘𝐴))
165	21	recnd 10672	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (log‘𝐴) ∈ ℂ)
166		fsumconst 15148	. . . . 5 ⊢ ((((0[,](√‘𝐴)) ∩ ℙ) ∈ Fin ∧ (log‘𝐴) ∈ ℂ) → Σ𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)(log‘𝐴) = ((♯‘((0[,](√‘𝐴)) ∩ ℙ)) · (log‘𝐴)))
167	17, 165, 166	syl2anc 586	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → Σ𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)(log‘𝐴) = ((♯‘((0[,](√‘𝐴)) ∩ ℙ)) · (log‘𝐴)))
168		hashcl 13720	. . . . . . 7 ⊢ (((0[,](√‘𝐴)) ∩ ℙ) ∈ Fin → (♯‘((0[,](√‘𝐴)) ∩ ℙ)) ∈ ℕ₀)
169	17, 168	syl 17	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (♯‘((0[,](√‘𝐴)) ∩ ℙ)) ∈ ℕ₀)
170	169	nn0red 11959	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (♯‘((0[,](√‘𝐴)) ∩ ℙ)) ∈ ℝ)
171		logge0 25191	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → 0 ≤ (log‘𝐴))
172		reflcl 13169	. . . . . . 7 ⊢ ((√‘𝐴) ∈ ℝ → (⌊‘(√‘𝐴)) ∈ ℝ)
173	15, 172	syl 17	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (⌊‘(√‘𝐴)) ∈ ℝ)
174		fzfid 13344	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (1...(⌊‘(√‘𝐴))) ∈ Fin)
175		ppisval 25684	. . . . . . . . . . 11 ⊢ ((√‘𝐴) ∈ ℝ → ((0[,](√‘𝐴)) ∩ ℙ) = ((2...(⌊‘(√‘𝐴))) ∩ ℙ))
176	15, 175	syl 17	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((0[,](√‘𝐴)) ∩ ℙ) = ((2...(⌊‘(√‘𝐴))) ∩ ℙ))
177		inss1 4208	. . . . . . . . . . 11 ⊢ ((2...(⌊‘(√‘𝐴))) ∩ ℙ) ⊆ (2...(⌊‘(√‘𝐴)))
178		2eluzge1 12297	. . . . . . . . . . . 12 ⊢ 2 ∈ (ℤ_≥‘1)
179		fzss1 12949	. . . . . . . . . . . 12 ⊢ (2 ∈ (ℤ_≥‘1) → (2...(⌊‘(√‘𝐴))) ⊆ (1...(⌊‘(√‘𝐴))))
180	178, 179	mp1i 13	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (2...(⌊‘(√‘𝐴))) ⊆ (1...(⌊‘(√‘𝐴))))
181	177, 180	sstrid 3981	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((2...(⌊‘(√‘𝐴))) ∩ ℙ) ⊆ (1...(⌊‘(√‘𝐴))))
182	176, 181	eqsstrd 4008	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((0[,](√‘𝐴)) ∩ ℙ) ⊆ (1...(⌊‘(√‘𝐴))))
183		ssdomg 8558	. . . . . . . . 9 ⊢ ((1...(⌊‘(√‘𝐴))) ∈ Fin → (((0[,](√‘𝐴)) ∩ ℙ) ⊆ (1...(⌊‘(√‘𝐴))) → ((0[,](√‘𝐴)) ∩ ℙ) ≼ (1...(⌊‘(√‘𝐴)))))
184	174, 182, 183	sylc 65	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((0[,](√‘𝐴)) ∩ ℙ) ≼ (1...(⌊‘(√‘𝐴))))
185		hashdom 13743	. . . . . . . . 9 ⊢ ((((0[,](√‘𝐴)) ∩ ℙ) ∈ Fin ∧ (1...(⌊‘(√‘𝐴))) ∈ Fin) → ((♯‘((0[,](√‘𝐴)) ∩ ℙ)) ≤ (♯‘(1...(⌊‘(√‘𝐴)))) ↔ ((0[,](√‘𝐴)) ∩ ℙ) ≼ (1...(⌊‘(√‘𝐴)))))
186	17, 174, 185	syl2anc 586	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((♯‘((0[,](√‘𝐴)) ∩ ℙ)) ≤ (♯‘(1...(⌊‘(√‘𝐴)))) ↔ ((0[,](√‘𝐴)) ∩ ℙ) ≼ (1...(⌊‘(√‘𝐴)))))
187	184, 186	mpbird 259	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (♯‘((0[,](√‘𝐴)) ∩ ℙ)) ≤ (♯‘(1...(⌊‘(√‘𝐴)))))
188		flge0nn0 13193	. . . . . . . . 9 ⊢ (((√‘𝐴) ∈ ℝ ∧ 0 ≤ (√‘𝐴)) → (⌊‘(√‘𝐴)) ∈ ℕ₀)
189	15, 54, 188	syl2anc 586	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (⌊‘(√‘𝐴)) ∈ ℕ₀)
190		hashfz1 13709	. . . . . . . 8 ⊢ ((⌊‘(√‘𝐴)) ∈ ℕ₀ → (♯‘(1...(⌊‘(√‘𝐴)))) = (⌊‘(√‘𝐴)))
191	189, 190	syl 17	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (♯‘(1...(⌊‘(√‘𝐴)))) = (⌊‘(√‘𝐴)))
192	187, 191	breqtrd 5095	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (♯‘((0[,](√‘𝐴)) ∩ ℙ)) ≤ (⌊‘(√‘𝐴)))
193		flle 13172	. . . . . . 7 ⊢ ((√‘𝐴) ∈ ℝ → (⌊‘(√‘𝐴)) ≤ (√‘𝐴))
194	15, 193	syl 17	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (⌊‘(√‘𝐴)) ≤ (√‘𝐴))
195	170, 173, 15, 192, 194	letrd 10800	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (♯‘((0[,](√‘𝐴)) ∩ ℙ)) ≤ (√‘𝐴))
196	170, 15, 21, 171, 195	lemul1ad 11582	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((♯‘((0[,](√‘𝐴)) ∩ ℙ)) · (log‘𝐴)) ≤ ((√‘𝐴) · (log‘𝐴)))
197	167, 196	eqbrtrd 5091	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → Σ𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)(log‘𝐴) ≤ ((√‘𝐴) · (log‘𝐴)))
198	5, 20, 22, 164, 197	letrd 10800	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ((ψ‘𝐴) − (θ‘𝐴)) ≤ ((√‘𝐴) · (log‘𝐴)))
199	2, 4, 22	lesubadd2d 11242	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (((ψ‘𝐴) − (θ‘𝐴)) ≤ ((√‘𝐴) · (log‘𝐴)) ↔ (ψ‘𝐴) ≤ ((θ‘𝐴) + ((√‘𝐴) · (log‘𝐴)))))
200	198, 199	mpbid 234	1 ⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → (ψ‘𝐴) ≤ ((θ‘𝐴) + ((√‘𝐴) · (log‘𝐴))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1536 ∈ wcel 2113 ∖ cdif 3936 ∩ cin 3938 ⊆ wss 3939 class class class wbr 5069 ‘cfv 6358 (class class class)co 7159 ≼ cdom 8510 Fincfn 8512 ℂcc 10538 ℝcr 10539 0cc0 10540 1c1 10541 + caddc 10543 · cmul 10545 < clt 10678 ≤ cle 10679 − cmin 10873 / cdiv 11300 ℕcn 11641 2c2 11695 ℕ₀cn0 11900 ℤcz 11984 ℤ_≥cuz 12246 ℝ⁺crp 12392 [,]cicc 12744 ...cfz 12895 ⌊cfl 13163 ↑cexp 13432 ♯chash 13693 √csqrt 14595 Σcsu 15045 ℙcprime 16018 logclog 25141 θccht 25671 ψcchp 25673

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2160 ax-12 2176 ax-ext 2796 ax-rep 5193 ax-sep 5206 ax-nul 5213 ax-pow 5269 ax-pr 5333 ax-un 7464 ax-inf2 9107 ax-cnex 10596 ax-resscn 10597 ax-1cn 10598 ax-icn 10599 ax-addcl 10600 ax-addrcl 10601 ax-mulcl 10602 ax-mulrcl 10603 ax-mulcom 10604 ax-addass 10605 ax-mulass 10606 ax-distr 10607 ax-i2m1 10608 ax-1ne0 10609 ax-1rid 10610 ax-rnegex 10611 ax-rrecex 10612 ax-cnre 10613 ax-pre-lttri 10614 ax-pre-lttrn 10615 ax-pre-ltadd 10616 ax-pre-mulgt0 10617 ax-pre-sup 10618 ax-addf 10619 ax-mulf 10620

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1539 df-fal 1549 df-ex 1780 df-nf 1784 df-sb 2069 df-mo 2621 df-eu 2653 df-clab 2803 df-cleq 2817 df-clel 2896 df-nfc 2966 df-ne 3020 df-nel 3127 df-ral 3146 df-rex 3147 df-reu 3148 df-rmo 3149 df-rab 3150 df-v 3499 df-sbc 3776 df-csb 3887 df-dif 3942 df-un 3944 df-in 3946 df-ss 3955 df-pss 3957 df-nul 4295 df-if 4471 df-pw 4544 df-sn 4571 df-pr 4573 df-tp 4575 df-op 4577 df-uni 4842 df-int 4880 df-iun 4924 df-iin 4925 df-br 5070 df-opab 5132 df-mpt 5150 df-tr 5176 df-id 5463 df-eprel 5468 df-po 5477 df-so 5478 df-fr 5517 df-se 5518 df-we 5519 df-xp 5564 df-rel 5565 df-cnv 5566 df-co 5567 df-dm 5568 df-rn 5569 df-res 5570 df-ima 5571 df-pred 6151 df-ord 6197 df-on 6198 df-lim 6199 df-suc 6200 df-iota 6317 df-fun 6360 df-fn 6361 df-f 6362 df-f1 6363 df-fo 6364 df-f1o 6365 df-fv 6366 df-isom 6367 df-riota 7117 df-ov 7162 df-oprab 7163 df-mpo 7164 df-of 7412 df-om 7584 df-1st 7692 df-2nd 7693 df-supp 7834 df-wrecs 7950 df-recs 8011 df-rdg 8049 df-1o 8105 df-2o 8106 df-oadd 8109 df-er 8292 df-map 8411 df-pm 8412 df-ixp 8465 df-en 8513 df-dom 8514 df-sdom 8515 df-fin 8516 df-fsupp 8837 df-fi 8878 df-sup 8909 df-inf 8910 df-oi 8977 df-dju 9333 df-card 9371 df-pnf 10680 df-mnf 10681 df-xr 10682 df-ltxr 10683 df-le 10684 df-sub 10875 df-neg 10876 df-div 11301 df-nn 11642 df-2 11703 df-3 11704 df-4 11705 df-5 11706 df-6 11707 df-7 11708 df-8 11709 df-9 11710 df-n0 11901 df-xnn0 11971 df-z 11985 df-dec 12102 df-uz 12247 df-q 12352 df-rp 12393 df-xneg 12510 df-xadd 12511 df-xmul 12512 df-ioo 12745 df-ioc 12746 df-ico 12747 df-icc 12748 df-fz 12896 df-fzo 13037 df-fl 13165 df-mod 13241 df-seq 13373 df-exp 13433 df-fac 13637 df-bc 13666 df-hash 13694 df-shft 14429 df-cj 14461 df-re 14462 df-im 14463 df-sqrt 14597 df-abs 14598 df-limsup 14831 df-clim 14848 df-rlim 14849 df-sum 15046 df-ef 15424 df-sin 15426 df-cos 15427 df-pi 15429 df-dvds 15611 df-gcd 15847 df-prm 16019 df-pc 16177 df-struct 16488 df-ndx 16489 df-slot 16490 df-base 16492 df-sets 16493 df-ress 16494 df-plusg 16581 df-mulr 16582 df-starv 16583 df-sca 16584 df-vsca 16585 df-ip 16586 df-tset 16587 df-ple 16588 df-ds 16590 df-unif 16591 df-hom 16592 df-cco 16593 df-rest 16699 df-topn 16700 df-0g 16718 df-gsum 16719 df-topgen 16720 df-pt 16721 df-prds 16724 df-xrs 16778 df-qtop 16783 df-imas 16784 df-xps 16786 df-mre 16860 df-mrc 16861 df-acs 16863 df-mgm 17855 df-sgrp 17904 df-mnd 17915 df-submnd 17960 df-mulg 18228 df-cntz 18450 df-cmn 18911 df-psmet 20540 df-xmet 20541 df-met 20542 df-bl 20543 df-mopn 20544 df-fbas 20545 df-fg 20546 df-cnfld 20549 df-top 21505 df-topon 21522 df-topsp 21544 df-bases 21557 df-cld 21630 df-ntr 21631 df-cls 21632 df-nei 21709 df-lp 21747 df-perf 21748 df-cn 21838 df-cnp 21839 df-haus 21926 df-tx 22173 df-hmeo 22366 df-fil 22457 df-fm 22549 df-flim 22550 df-flf 22551 df-xms 22933 df-ms 22934 df-tms 22935 df-cncf 23489 df-limc 24467 df-dv 24468 df-log 25143 df-cht 25677 df-vma 25678 df-chp 25679

This theorem is referenced by: chpchtlim 26058

W3C validator