Axiom ax-ros335 30723

Description: Theorem 12. of [RosserSchoenfeld] p. 71. Theorem chpo1ubb 25170 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	|- A. x e. RR+ (ψ ` x ) < ( ( 1 period_ 0_ 3_ 8_ 8 3 ) x. x )

Detailed syntax breakdown of Axiom ax-ros335

Step	Hyp	Ref	Expression
1		vx	. . . . 5 setvar x
2	1	cv 1482	. . . 4 class x
3		cchp 24819	. . . 4 class ψ
4	2, 3	cfv 5888	. . 3 class (ψ ` x )
5		c1 9937	. . . . 5 class 1
6		cc0 9936	. . . . . 6 class 0
7		c3 11071	. . . . . . 7 class 3
8		c8 11076	. . . . . . . 8 class 8
9	8, 7	cdp2 29577	. . . . . . . 8 class _ 8 3
10	8, 9	cdp2 29577	. . . . . . 7 class _ 8_ 8 3
11	7, 10	cdp2 29577	. . . . . 6 class _ 3_ 8_ 8 3
12	6, 11	cdp2 29577	. . . . 5 class _ 0_ 3_ 8_ 8 3
13		cdp 29595	. . . . 5 class period
14	5, 12, 13	co 6650	. . . 4 class ( 1 period_ 0_ 3_ 8_ 8 3 )
15		cmul 9941	. . . 4 class x.
16	14, 2, 15	co 6650	. . 3 class ( ( 1 period_ 0_ 3_ 8_ 8 3 ) x. x )
17		clt 10074	. . 3 class <
18	4, 16, 17	wbr 4653	. 2 wff (ψ ` x ) < ( ( 1 period_ 0_ 3_ 8_ 8 3 ) x. x )
19		crp 11832	. 2 class RR+
20	18, 1, 19	wral 2912	1 wff A. x e. RR+ (ψ ` x ) < ( ( 1 period_ 0_ 3_ 8_ 8 3 ) x. x )

This axiom is referenced by:  hgt750lemc  30725