Theorem chpub

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

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

Proof

Step	Hyp	Ref	Expression
1		chpcl	⊢ ( 𝐴 ∈ ℝ → ( ψ ‘ 𝐴 ) ∈ ℝ )
2	1	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ψ ‘ 𝐴 ) ∈ ℝ )
3		chtcl	⊢ ( 𝐴 ∈ ℝ → ( θ ‘ 𝐴 ) ∈ ℝ )
4	3	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( θ ‘ 𝐴 ) ∈ ℝ )
5	2 4	resubcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( ψ ‘ 𝐴 ) − ( θ ‘ 𝐴 ) ) ∈ ℝ )
6		simpl	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 𝐴 ∈ ℝ )
7		0red	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 0 ∈ ℝ )
8		1red	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 1 ∈ ℝ )
9		0lt1	⊢ 0 < 1
10	9	a1i	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 0 < 1 )
11		simpr	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 1 ≤ 𝐴 )
12	7 8 6 10 11	ltletrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 0 < 𝐴 )
13	6 12	elrpd	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 𝐴 ∈ ℝ+ )
14	13	rpge0d	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 0 ≤ 𝐴 )
15	6 14	resqrtcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( √ ‘ 𝐴 ) ∈ ℝ )
16		ppifi	⊢ ( ( √ ‘ 𝐴 ) ∈ ℝ → ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ∈ Fin )
17	15 16	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ∈ Fin )
18	13	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → 𝐴 ∈ ℝ+ )
19	18	relogcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → ( log ‘ 𝐴 ) ∈ ℝ )
20	17 19	fsumrecl	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → Σ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ( log ‘ 𝐴 ) ∈ ℝ )
21	13	relogcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( log ‘ 𝐴 ) ∈ ℝ )
22	15 21	remulcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( √ ‘ 𝐴 ) · ( log ‘ 𝐴 ) ) ∈ ℝ )
23		ppifi	⊢ ( 𝐴 ∈ ℝ → ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∈ Fin )
24	23	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∈ Fin )
25		simpr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) )
26	25	elin2d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℙ )
27		prmnn	⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℕ )
28	26 27	syl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℕ )
29	28	nnrpd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℝ+ )
30	29	relogcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℝ )
31	21	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝐴 ) ∈ ℝ )
32	28	nnred	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℝ )
33		prmuz2	⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ( ℤ≥ ‘ 2 ) )
34	26 33	syl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ( ℤ≥ ‘ 2 ) )
35		eluz2gt1	⊢ ( 𝑝 ∈ ( ℤ≥ ‘ 2 ) → 1 < 𝑝 )
36	34 35	syl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 1 < 𝑝 )
37	32 36	rplogcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℝ+ )
38	31 37	rerpdivcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ∈ ℝ )
39		reflcl	⊢ ( ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ∈ ℝ → ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ℝ )
40	38 39	syl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ℝ )
41	30 40	remulcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ∈ ℝ )
42	41	recnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ∈ ℂ )
43	30	recnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℂ )
44	24 42 43	fsumsub	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) − ( log ‘ 𝑝 ) ) = ( Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) − Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝑝 ) ) )
45		0le0	⊢ 0 ≤ 0
46	45	a1i	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 0 ≤ 0 )
47	8 6 6 14 11	lemul2ad	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( 𝐴 · 1 ) ≤ ( 𝐴 · 𝐴 ) )
48	6	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 𝐴 ∈ ℂ )
49	48	sqsqrtd	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( √ ‘ 𝐴 ) ↑ 2 ) = 𝐴 )
50	48	mulridd	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( 𝐴 · 1 ) = 𝐴 )
51	49 50	eqtr4d	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( √ ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 · 1 ) )
52	48	sqvald	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 ) )
53	47 51 52	3brtr4d	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( √ ‘ 𝐴 ) ↑ 2 ) ≤ ( 𝐴 ↑ 2 ) )
54	6 14	sqrtge0d	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 0 ≤ ( √ ‘ 𝐴 ) )
55	15 6 54 14	le2sqd	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( √ ‘ 𝐴 ) ≤ 𝐴 ↔ ( ( √ ‘ 𝐴 ) ↑ 2 ) ≤ ( 𝐴 ↑ 2 ) ) )
56	53 55	mpbird	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( √ ‘ 𝐴 ) ≤ 𝐴 )
57		iccss	⊢ ( ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ∧ ( 0 ≤ 0 ∧ ( √ ‘ 𝐴 ) ≤ 𝐴 ) ) → ( 0 [,] ( √ ‘ 𝐴 ) ) ⊆ ( 0 [,] 𝐴 ) )
58	7 6 46 56 57	syl22anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( 0 [,] ( √ ‘ 𝐴 ) ) ⊆ ( 0 [,] 𝐴 ) )
59	58	ssrind	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ⊆ ( ( 0 [,] 𝐴 ) ∩ ℙ ) )
60	59	sselda	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) )
61	41 30	resubcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) − ( log ‘ 𝑝 ) ) ∈ ℝ )
62	61	recnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) − ( log ‘ 𝑝 ) ) ∈ ℂ )
63	60 62	syldan	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → ( ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) − ( log ‘ 𝑝 ) ) ∈ ℂ )
64		eldifi	⊢ ( 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) )
65	64 43	sylan2	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( log ‘ 𝑝 ) ∈ ℂ )
66	65	mullidd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( 1 · ( log ‘ 𝑝 ) ) = ( log ‘ 𝑝 ) )
67	25	elin1d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ( 0 [,] 𝐴 ) )
68		0re	⊢ 0 ∈ ℝ
69	6	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝐴 ∈ ℝ )
70		elicc2	⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝑝 ∈ ( 0 [,] 𝐴 ) ↔ ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴 ) ) )
71	68 69 70	sylancr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 𝑝 ∈ ( 0 [,] 𝐴 ) ↔ ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴 ) ) )
72	67 71	mpbid	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴 ) )
73	72	simp3d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ≤ 𝐴 )
74	64 73	sylan2	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → 𝑝 ≤ 𝐴 )
75	64 29	sylan2	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → 𝑝 ∈ ℝ+ )
76	13	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → 𝐴 ∈ ℝ+ )
77	75 76	logled	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( 𝑝 ≤ 𝐴 ↔ ( log ‘ 𝑝 ) ≤ ( log ‘ 𝐴 ) ) )
78	74 77	mpbid	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( log ‘ 𝑝 ) ≤ ( log ‘ 𝐴 ) )
79	66 78	eqbrtrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( 1 · ( log ‘ 𝑝 ) ) ≤ ( log ‘ 𝐴 ) )
80		1red	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → 1 ∈ ℝ )
81	21	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( log ‘ 𝐴 ) ∈ ℝ )
82	64 37	sylan2	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( log ‘ 𝑝 ) ∈ ℝ+ )
83	80 81 82	lemuldivd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( ( 1 · ( log ‘ 𝑝 ) ) ≤ ( log ‘ 𝐴 ) ↔ 1 ≤ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) )
84	79 83	mpbid	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → 1 ≤ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) )
85	6	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → 𝐴 ∈ ℝ )
86	85	recnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → 𝐴 ∈ ℂ )
87	86	sqsqrtd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( ( √ ‘ 𝐴 ) ↑ 2 ) = 𝐴 )
88		eldifn	⊢ ( 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → ¬ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) )
89	88	adantl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ¬ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) )
90	64 26	sylan2	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → 𝑝 ∈ ℙ )
91		elin	⊢ ( 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ↔ ( 𝑝 ∈ ( 0 [,] ( √ ‘ 𝐴 ) ) ∧ 𝑝 ∈ ℙ ) )
92	91	rbaib	⊢ ( 𝑝 ∈ ℙ → ( 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ↔ 𝑝 ∈ ( 0 [,] ( √ ‘ 𝐴 ) ) ) )
93	90 92	syl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ↔ 𝑝 ∈ ( 0 [,] ( √ ‘ 𝐴 ) ) ) )
94		0red	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → 0 ∈ ℝ )
95	15	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( √ ‘ 𝐴 ) ∈ ℝ )
96	64 28	sylan2	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → 𝑝 ∈ ℕ )
97	96	nnred	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → 𝑝 ∈ ℝ )
98	75	rpge0d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → 0 ≤ 𝑝 )
99		elicc2	⊢ ( ( 0 ∈ ℝ ∧ ( √ ‘ 𝐴 ) ∈ ℝ ) → ( 𝑝 ∈ ( 0 [,] ( √ ‘ 𝐴 ) ) ↔ ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ ( √ ‘ 𝐴 ) ) ) )
100		df-3an	⊢ ( ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ ( √ ‘ 𝐴 ) ) ↔ ( ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ) ∧ 𝑝 ≤ ( √ ‘ 𝐴 ) ) )
101	99 100	bitrdi	⊢ ( ( 0 ∈ ℝ ∧ ( √ ‘ 𝐴 ) ∈ ℝ ) → ( 𝑝 ∈ ( 0 [,] ( √ ‘ 𝐴 ) ) ↔ ( ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ) ∧ 𝑝 ≤ ( √ ‘ 𝐴 ) ) ) )
102	101	baibd	⊢ ( ( ( 0 ∈ ℝ ∧ ( √ ‘ 𝐴 ) ∈ ℝ ) ∧ ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ) ) → ( 𝑝 ∈ ( 0 [,] ( √ ‘ 𝐴 ) ) ↔ 𝑝 ≤ ( √ ‘ 𝐴 ) ) )
103	94 95 97 98 102	syl22anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( 𝑝 ∈ ( 0 [,] ( √ ‘ 𝐴 ) ) ↔ 𝑝 ≤ ( √ ‘ 𝐴 ) ) )
104	93 103	bitrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ↔ 𝑝 ≤ ( √ ‘ 𝐴 ) ) )
105	89 104	mtbid	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ¬ 𝑝 ≤ ( √ ‘ 𝐴 ) )
106	95 97	ltnled	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( ( √ ‘ 𝐴 ) < 𝑝 ↔ ¬ 𝑝 ≤ ( √ ‘ 𝐴 ) ) )
107	105 106	mpbird	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( √ ‘ 𝐴 ) < 𝑝 )
108	54	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → 0 ≤ ( √ ‘ 𝐴 ) )
109	95 97 108 98	lt2sqd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( ( √ ‘ 𝐴 ) < 𝑝 ↔ ( ( √ ‘ 𝐴 ) ↑ 2 ) < ( 𝑝 ↑ 2 ) ) )
110	107 109	mpbid	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( ( √ ‘ 𝐴 ) ↑ 2 ) < ( 𝑝 ↑ 2 ) )
111	87 110	eqbrtrrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → 𝐴 < ( 𝑝 ↑ 2 ) )
112	96	nnsqcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( 𝑝 ↑ 2 ) ∈ ℕ )
113	112	nnrpd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( 𝑝 ↑ 2 ) ∈ ℝ+ )
114		logltb	⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( 𝑝 ↑ 2 ) ∈ ℝ+ ) → ( 𝐴 < ( 𝑝 ↑ 2 ) ↔ ( log ‘ 𝐴 ) < ( log ‘ ( 𝑝 ↑ 2 ) ) ) )
115	76 113 114	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( 𝐴 < ( 𝑝 ↑ 2 ) ↔ ( log ‘ 𝐴 ) < ( log ‘ ( 𝑝 ↑ 2 ) ) ) )
116	111 115	mpbid	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( log ‘ 𝐴 ) < ( log ‘ ( 𝑝 ↑ 2 ) ) )
117		2z	⊢ 2 ∈ ℤ
118		relogexp	⊢ ( ( 𝑝 ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( log ‘ ( 𝑝 ↑ 2 ) ) = ( 2 · ( log ‘ 𝑝 ) ) )
119	75 117 118	sylancl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( log ‘ ( 𝑝 ↑ 2 ) ) = ( 2 · ( log ‘ 𝑝 ) ) )
120	116 119	breqtrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( log ‘ 𝐴 ) < ( 2 · ( log ‘ 𝑝 ) ) )
121		2re	⊢ 2 ∈ ℝ
122	121	a1i	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → 2 ∈ ℝ )
123	81 122 82	ltdivmul2d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) < 2 ↔ ( log ‘ 𝐴 ) < ( 2 · ( log ‘ 𝑝 ) ) ) )
124	120 123	mpbird	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) < 2 )
125		df-2	⊢ 2 = ( 1 + 1 )
126	124 125	breqtrdi	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) < ( 1 + 1 ) )
127	64 38	sylan2	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ∈ ℝ )
128		1z	⊢ 1 ∈ ℤ
129		flbi	⊢ ( ( ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ∈ ℝ ∧ 1 ∈ ℤ ) → ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) = 1 ↔ ( 1 ≤ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ∧ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) < ( 1 + 1 ) ) ) )
130	127 128 129	sylancl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) = 1 ↔ ( 1 ≤ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ∧ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) < ( 1 + 1 ) ) ) )
131	84 126 130	mpbir2and	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) = 1 )
132	131	oveq2d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) = ( ( log ‘ 𝑝 ) · 1 ) )
133	65	mulridd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( ( log ‘ 𝑝 ) · 1 ) = ( log ‘ 𝑝 ) )
134	132 133	eqtrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) = ( log ‘ 𝑝 ) )
135	134	oveq1d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) − ( log ‘ 𝑝 ) ) = ( ( log ‘ 𝑝 ) − ( log ‘ 𝑝 ) ) )
136	65	subidd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( ( log ‘ 𝑝 ) − ( log ‘ 𝑝 ) ) = 0 )
137	135 136	eqtrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) − ( log ‘ 𝑝 ) ) = 0 )
138	59 63 137 24	fsumss	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → Σ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ( ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) − ( log ‘ 𝑝 ) ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) − ( log ‘ 𝑝 ) ) )
139		chpval2	⊢ ( 𝐴 ∈ ℝ → ( ψ ‘ 𝐴 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) )
140	139	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ψ ‘ 𝐴 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) )
141		chtval	⊢ ( 𝐴 ∈ ℝ → ( θ ‘ 𝐴 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝑝 ) )
142	141	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( θ ‘ 𝐴 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝑝 ) )
143	140 142	oveq12d	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( ψ ‘ 𝐴 ) − ( θ ‘ 𝐴 ) ) = ( Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) − Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝑝 ) ) )
144	44 138 143	3eqtr4rd	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( ψ ‘ 𝐴 ) − ( θ ‘ 𝐴 ) ) = Σ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ( ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) − ( log ‘ 𝑝 ) ) )
145	60 61	syldan	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → ( ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) − ( log ‘ 𝑝 ) ) ∈ ℝ )
146	60 41	syldan	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ∈ ℝ )
147	60 37	syldan	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℝ+ )
148	147	rpge0d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → 0 ≤ ( log ‘ 𝑝 ) )
149		simpr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) )
150	149	elin2d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → 𝑝 ∈ ℙ )
151	150 27	syl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → 𝑝 ∈ ℕ )
152	151	nnrpd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → 𝑝 ∈ ℝ+ )
153	152	relogcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℝ )
154	146 153	subge02d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → ( 0 ≤ ( log ‘ 𝑝 ) ↔ ( ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) − ( log ‘ 𝑝 ) ) ≤ ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) )
155	148 154	mpbid	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → ( ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) − ( log ‘ 𝑝 ) ) ≤ ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) )
156	60 38	syldan	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ∈ ℝ )
157		flle	⊢ ( ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ∈ ℝ → ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ≤ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) )
158	156 157	syl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ≤ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) )
159	60 40	syldan	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ℝ )
160	159 19 147	lemuldiv2d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → ( ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ≤ ( log ‘ 𝐴 ) ↔ ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ≤ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) )
161	158 160	mpbird	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ≤ ( log ‘ 𝐴 ) )
162	145 146 19 155 161	letrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → ( ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) − ( log ‘ 𝑝 ) ) ≤ ( log ‘ 𝐴 ) )
163	17 145 19 162	fsumle	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → Σ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ( ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) − ( log ‘ 𝑝 ) ) ≤ Σ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ( log ‘ 𝐴 ) )
164	144 163	eqbrtrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( ψ ‘ 𝐴 ) − ( θ ‘ 𝐴 ) ) ≤ Σ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ( log ‘ 𝐴 ) )
165	21	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( log ‘ 𝐴 ) ∈ ℂ )
166		fsumconst	⊢ ( ( ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ∈ Fin ∧ ( log ‘ 𝐴 ) ∈ ℂ ) → Σ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ( log ‘ 𝐴 ) = ( ( ♯ ‘ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) · ( log ‘ 𝐴 ) ) )
167	17 165 166	syl2anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → Σ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ( log ‘ 𝐴 ) = ( ( ♯ ‘ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) · ( log ‘ 𝐴 ) ) )
168		hashcl	⊢ ( ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ∈ Fin → ( ♯ ‘ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ∈ ℕ0 )
169	17 168	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ♯ ‘ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ∈ ℕ0 )
170	169	nn0red	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ♯ ‘ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ∈ ℝ )
171		logge0	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 0 ≤ ( log ‘ 𝐴 ) )
172		reflcl	⊢ ( ( √ ‘ 𝐴 ) ∈ ℝ → ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ∈ ℝ )
173	15 172	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ∈ ℝ )
174		fzfid	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( 1 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) ∈ Fin )
175		ppisval	⊢ ( ( √ ‘ 𝐴 ) ∈ ℝ → ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) = ( ( 2 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) ∩ ℙ ) )
176	15 175	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) = ( ( 2 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) ∩ ℙ ) )
177		inss1	⊢ ( ( 2 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) ∩ ℙ ) ⊆ ( 2 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) )
178		2eluzge1	⊢ 2 ∈ ( ℤ≥ ‘ 1 )
179		fzss1	⊢ ( 2 ∈ ( ℤ≥ ‘ 1 ) → ( 2 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) ⊆ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) )
180	178 179	mp1i	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( 2 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) ⊆ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) )
181	177 180	sstrid	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( 2 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) ∩ ℙ ) ⊆ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) )
182	176 181	eqsstrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ⊆ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) )
183		ssdomg	⊢ ( ( 1 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) ∈ Fin → ( ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ⊆ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) → ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ≼ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) ) )
184	174 182 183	sylc	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ≼ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) )
185		hashdom	⊢ ( ( ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ∈ Fin ∧ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) ∈ Fin ) → ( ( ♯ ‘ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ≤ ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) ) ↔ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ≼ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) ) )
186	17 174 185	syl2anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( ♯ ‘ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ≤ ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) ) ↔ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ≼ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) ) )
187	184 186	mpbird	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ♯ ‘ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ≤ ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) ) )
188		flge0nn0	⊢ ( ( ( √ ‘ 𝐴 ) ∈ ℝ ∧ 0 ≤ ( √ ‘ 𝐴 ) ) → ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ∈ ℕ0 )
189	15 54 188	syl2anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ∈ ℕ0 )
190		hashfz1	⊢ ( ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) ) = ( ⌊ ‘ ( √ ‘ 𝐴 ) ) )
191	189 190	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) ) = ( ⌊ ‘ ( √ ‘ 𝐴 ) ) )
192	187 191	breqtrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ♯ ‘ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ≤ ( ⌊ ‘ ( √ ‘ 𝐴 ) ) )
193		flle	⊢ ( ( √ ‘ 𝐴 ) ∈ ℝ → ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ≤ ( √ ‘ 𝐴 ) )
194	15 193	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ≤ ( √ ‘ 𝐴 ) )
195	170 173 15 192 194	letrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ♯ ‘ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ≤ ( √ ‘ 𝐴 ) )
196	170 15 21 171 195	lemul1ad	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( ♯ ‘ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) · ( log ‘ 𝐴 ) ) ≤ ( ( √ ‘ 𝐴 ) · ( log ‘ 𝐴 ) ) )
197	167 196	eqbrtrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → Σ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ( log ‘ 𝐴 ) ≤ ( ( √ ‘ 𝐴 ) · ( log ‘ 𝐴 ) ) )
198	5 20 22 164 197	letrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( ψ ‘ 𝐴 ) − ( θ ‘ 𝐴 ) ) ≤ ( ( √ ‘ 𝐴 ) · ( log ‘ 𝐴 ) ) )
199	2 4 22	lesubadd2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( ( ψ ‘ 𝐴 ) − ( θ ‘ 𝐴 ) ) ≤ ( ( √ ‘ 𝐴 ) · ( log ‘ 𝐴 ) ) ↔ ( ψ ‘ 𝐴 ) ≤ ( ( θ ‘ 𝐴 ) + ( ( √ ‘ 𝐴 ) · ( log ‘ 𝐴 ) ) ) ) )
200	198 199	mpbid	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ψ ‘ 𝐴 ) ≤ ( ( θ ‘ 𝐴 ) + ( ( √ ‘ 𝐴 ) · ( log ‘ 𝐴 ) ) ) )