This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Axiom ax-ros336

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

Ref Expression
Assertion ax-ros336 ⊢ ∀ x ∈ ℝ + ψ ⁡ x − θ ⁡ x < 1.4262 ⁢ 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 cmin class −
6 ccht class θ
7 3 6 cfv class θ ⁡ x
8 4 7 5 co class ψ ⁡ x − θ ⁡ x
9 clt class <
10 c1 class 1
11 cdp class .
12 c4 class 4
13 c2 class 2
14 c6 class 6
15 14 13 cdp2 class 62
16 13 15 cdp2 class 262
17 12 16 cdp2 class 4262
18 10 17 11 co class 1.4262
19 cmul class ×
20 csqrt class √
21 3 20 cfv class x
22 18 21 19 co class 1.4262 ⁢ x
23 8 22 9 wbr wff ψ ⁡ x − θ ⁡ x < 1.4262 ⁢ x
24 23 0 1 wral wff ∀ x ∈ ℝ + ψ ⁡ x − θ ⁡ x < 1.4262 ⁢ x