Axiom ax-ros336

Description: Theorem 13. of RosserSchoenfeld p. 71. Theorem chpchtlim states that the psi and theta 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)

	Ref	Expression
Assertion	ax-ros336	$$⊢\forall x\in {ℝ}^{+}\psi \left(x\right)-\theta \left(x\right)<\mathrm{1\; <mi\; href="df-dp.html">.</mi>4262}\sqrt{x}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1		crp	$$class{ℝ}^{+}$$
2		cchp	$$class\psi$$
3	0	cv	$$setvarx$$
4	3 2	cfv	$$class\psi \left(x\right)$$
5		cmin	$$class-$$
6		ccht	$$class\theta$$
7	3 6	cfv	$$class\theta \left(x\right)$$
8	4 7 5	co	$$class\left(\psi \left(x\right)-\theta \left(x\right)\right)$$
9		clt	$$class<$$
10		c1	$$class1$$
11		cdp	$$class.$$
12		c4	$$class4$$
13		c2	$$class2$$
14		c6	$$class6$$
15	14 13	cdp2	$$class62$$
16	13 15	cdp2	$$class262$$
17	12 16	cdp2	$$class4262$$
18	10 17 11	co	$$class\mathrm{1\; <mi\; href="df-dp.html">.</mi>4262}$$
19		cmul	$$class\times$$
20		csqrt	$$class\surd$$
21	3 20	cfv	$$class\sqrt{x}$$
22	18 21 19	co	$$class\mathrm{1\; <mi\; href="df-dp.html">.</mi>4262}\sqrt{x}$$
23	8 22 9	wbr	$$wff\psi \left(x\right)-\theta \left(x\right)<\mathrm{1\; <mi\; href="df-dp.html">.</mi>4262}\sqrt{x}$$
24	23 0 1	wral	$$wff\forall x\in {ℝ}^{+}\psi \left(x\right)-\theta \left(x\right)<\mathrm{1\; <mi\; href="df-dp.html">.</mi>4262}\sqrt{x}$$