Axiom ax-ros336 31274

Description: Theorem 13. of [RosserSchoenfeld] p. 71. Theorem chpchtlim 25582 states that the ψ and θ function are asymtotic to each other; this axiom postulates an upper bound for their difference. This is stated as an axiom until a formal proof can be provided. (Contributed by Thierry Arnoux, 28-Dec-2021.)

Assertion

Ref	Expression
ax-ros336	⊢ ∀𝑥 ∈ ℝ+ ((ψ‘𝑥) − (θ‘𝑥)) < ((1._4_2_62) · (√‘𝑥))

Detailed syntax breakdown of Axiom ax-ros336

Step	Hyp	Ref	Expression
1		vx	. . . . . 6 setvar 𝑥
2	1	cv 1657	. . . . 5 class 𝑥
3		cchp 25233	. . . . 5 class ψ
4	2, 3	cfv 6124	. . . 4 class (ψ‘𝑥)
5		ccht 25231	. . . . 5 class θ
6	2, 5	cfv 6124	. . . 4 class (θ‘𝑥)
7		cmin 10586	. . . 4 class −
8	4, 6, 7	co 6906	. . 3 class ((ψ‘𝑥) − (θ‘𝑥))
9		c1 10254	. . . . 5 class 1
10		c4 11409	. . . . . 6 class 4
11		c2 11407	. . . . . . 7 class 2
12		c6 11411	. . . . . . . 8 class 6
13	12, 11	cdp2 30125	. . . . . . 7 class _62
14	11, 13	cdp2 30125	. . . . . 6 class _2_62
15	10, 14	cdp2 30125	. . . . 5 class _4_2_62
16		cdp 30142	. . . . 5 class .
17	9, 15, 16	co 6906	. . . 4 class (1._4_2_62)
18		csqrt 14351	. . . . 5 class √
19	2, 18	cfv 6124	. . . 4 class (√‘𝑥)
20		cmul 10258	. . . 4 class ·
21	17, 19, 20	co 6906	. . 3 class ((1._4_2_62) · (√‘𝑥))
22		clt 10392	. . 3 class <
23	8, 21, 22	wbr 4874	. 2 wff ((ψ‘𝑥) − (θ‘𝑥)) < ((1._4_2_62) · (√‘𝑥))
24		crp 12113	. 2 class ℝ+
25	23, 1, 24	wral 3118	1 wff ∀𝑥 ∈ ℝ+ ((ψ‘𝑥) − (θ‘𝑥)) < ((1._4_2_62) · (√‘𝑥))

This axiom is referenced by:  hgt750lemd  31276