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 | |- A. x e. RR+ ( psi ` x ) < ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) x. x ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | vx | |- x |
|
| 1 | crp | |- RR+ |
|
| 2 | cchp | |- psi |
|
| 3 | 0 | cv | |- x |
| 4 | 3 2 | cfv | |- ( psi ` x ) |
| 5 | clt | |- < |
|
| 6 | c1 | |- 1 |
|
| 7 | cdp | |- . |
|
| 8 | cc0 | |- 0 |
|
| 9 | c3 | |- 3 |
|
| 10 | c8 | |- 8 |
|
| 11 | 10 9 | cdp2 | |- _ 8 3 |
| 12 | 10 11 | cdp2 | |- _ 8 _ 8 3 |
| 13 | 9 12 | cdp2 | |- _ 3 _ 8 _ 8 3 |
| 14 | 8 13 | cdp2 | |- _ 0 _ 3 _ 8 _ 8 3 |
| 15 | 6 14 7 | co | |- ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) |
| 16 | cmul | |- x. |
|
| 17 | 15 3 16 | co | |- ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) x. x ) |
| 18 | 4 17 5 | wbr | |- ( psi ` x ) < ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) x. x ) |
| 19 | 18 0 1 | wral | |- A. x e. RR+ ( psi ` x ) < ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) x. x ) |