Axiom ax-ros336 30724

Description: Theorem 13. of [RosserSchoenfeld] p. 71. Theorem chpchtlim 25168 states that the ψ 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.)

Assertion

Ref	Expression
ax-ros336	|- A. x e. RR+ ( (ψ ` x ) - ( theta ` x ) ) < ( ( 1 period_ 4_ 2_ 6 2 ) x. ( sqr ` x ) )

Detailed syntax breakdown of Axiom ax-ros336

Step	Hyp	Ref	Expression
1		vx	. . . . . 6 setvar x
2	1	cv 1482	. . . . 5 class x
3		cchp 24819	. . . . 5 class ψ
4	2, 3	cfv 5888	. . . 4 class (ψ ` x )
5		ccht 24817	. . . . 5 class theta
6	2, 5	cfv 5888	. . . 4 class ( theta ` x )
7		cmin 10266	. . . 4 class -
8	4, 6, 7	co 6650	. . 3 class ( (ψ ` x ) - ( theta ` x ) )
9		c1 9937	. . . . 5 class 1
10		c4 11072	. . . . . 6 class 4
11		c2 11070	. . . . . . 7 class 2
12		c6 11074	. . . . . . . 8 class 6
13	12, 11	cdp2 29577	. . . . . . 7 class _ 6 2
14	11, 13	cdp2 29577	. . . . . 6 class _ 2_ 6 2
15	10, 14	cdp2 29577	. . . . 5 class _ 4_ 2_ 6 2
16		cdp 29595	. . . . 5 class period
17	9, 15, 16	co 6650	. . . 4 class ( 1 period_ 4_ 2_ 6 2 )
18		csqrt 13973	. . . . 5 class sqr
19	2, 18	cfv 5888	. . . 4 class ( sqr ` x )
20		cmul 9941	. . . 4 class x.
21	17, 19, 20	co 6650	. . 3 class ( ( 1 period_ 4_ 2_ 6 2 ) x. ( sqr ` x ) )
22		clt 10074	. . 3 class <
23	8, 21, 22	wbr 4653	. 2 wff ( (ψ ` x ) - ( theta ` x ) ) < ( ( 1 period_ 4_ 2_ 6 2 ) x. ( sqr ` x ) )
24		crp 11832	. 2 class RR+
25	23, 1, 24	wral 2912	1 wff A. x e. RR+ ( (ψ ` x ) - ( theta ` x ) ) < ( ( 1 period_ 4_ 2_ 6 2 ) x. ( sqr ` x ) )

This axiom is referenced by:  hgt750lemd  30726