Axiom ax-ros335

Description: Theorem 12. of RosserSchoenfeld p. 71. Theorem chpo1ubb states that the psi function is bounded by a linear term; this axiom postulates an upper bound for that linear term. This is stated as an axiom until a formal proof can be provided. (Contributed by Thierry Arnoux, 28-Dec-2021)

	Ref	Expression
Assertion	ax-ros335	$$⊢\forall x\in {ℝ}^{+}\psi \left(x\right)<\mathrm{1\; <mi\; href="df-dp.html">.</mi>03883}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		clt	$$class<$$
6		c1	$$class1$$
7		cdp	$$class.$$
8		cc0	$$class0$$
9		c3	$$class3$$
10		c8	$$class8$$
11	10 9	cdp2	$$class83$$
12	10 11	cdp2	$$class883$$
13	9 12	cdp2	$$class3883$$
14	8 13	cdp2	$$class03883$$
15	6 14 7	co	$$class\mathrm{1\; <mi\; href="df-dp.html">.</mi>03883}$$
16		cmul	$$class\times$$
17	15 3 16	co	$$class\mathrm{1\; <mi\; href="df-dp.html">.</mi>03883}x$$
18	4 17 5	wbr	$$wff\psi \left(x\right)<\mathrm{1\; <mi\; href="df-dp.html">.</mi>03883}x$$
19	18 0 1	wral	$$wff\forall x\in {ℝ}^{+}\psi \left(x\right)<\mathrm{1\; <mi\; href="df-dp.html">.</mi>03883}x$$