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 ℝ^{+} ψ (x) < 1.03883 x$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$setvar x$
1		crp	$class ℝ^{+}$
2		cchp	$class ψ$
3	0	cv	$setvar x$
4	3 2	cfv	$class ψ (x)$
5		clt	$class <$
6		c1	$class 1$
7		cdp	$class .$
8		cc0	$class 0$
9		c3	$class 3$
10		c8	$class 8$
11	10 9	cdp2	$class 83$
12	10 11	cdp2	$class 883$
13	9 12	cdp2	$class 3883$
14	8 13	cdp2	$class 03883$
15	6 14 7	co	$class 1.03883$
16		cmul	$class \times$
17	15 3 16	co	$class 1.03883 x$
18	4 17 5	wbr	$wff ψ (x) < 1.03883 x$
19	18 0 1	wral	$wff \forall x \in ℝ^{+} ψ (x) < 1.03883 x$

Metamath Proof Explorer

Axiom ax-ros335

Detailed syntax breakdown