Axiom ax-ros335 31916

Description: Theorem 12. of [RosserSchoenfeld] p. 71. Theorem chpo1ubb 26057 states that the ψ 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.)

Assertion

Ref	Expression
ax-ros335	⊢ ∀𝑥 ∈ ℝ+ (ψ‘𝑥) < ((1._0_3_8_83) · 𝑥)

Detailed syntax breakdown of Axiom ax-ros335

Step	Hyp	Ref	Expression
1		vx	. . . . 5 setvar 𝑥
2	1	cv 1536	. . . 4 class 𝑥
3		cchp 25670	. . . 4 class ψ
4	2, 3	cfv 6355	. . 3 class (ψ‘𝑥)
5		c1 10538	. . . . 5 class 1
6		cc0 10537	. . . . . 6 class 0
7		c3 11694	. . . . . . 7 class 3
8		c8 11699	. . . . . . . 8 class 8
9	8, 7	cdp2 30547	. . . . . . . 8 class _83
10	8, 9	cdp2 30547	. . . . . . 7 class _8_83
11	7, 10	cdp2 30547	. . . . . 6 class _3_8_83
12	6, 11	cdp2 30547	. . . . 5 class _0_3_8_83
13		cdp 30564	. . . . 5 class .
14	5, 12, 13	co 7156	. . . 4 class (1._0_3_8_83)
15		cmul 10542	. . . 4 class ·
16	14, 2, 15	co 7156	. . 3 class ((1._0_3_8_83) · 𝑥)
17		clt 10675	. . 3 class <
18	4, 16, 17	wbr 5066	. 2 wff (ψ‘𝑥) < ((1._0_3_8_83) · 𝑥)
19		crp 12390	. 2 class ℝ+
20	18, 1, 19	wral 3138	1 wff ∀𝑥 ∈ ℝ+ (ψ‘𝑥) < ((1._0_3_8_83) · 𝑥)

This axiom is referenced by:  hgt750lemc  31918