Axiom ax-ros335

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	⊢ ∀ 𝑥 ∈ ℝ+ ( ψ ‘ 𝑥 ) < ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) · 𝑥 )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	⊢ 𝑥
1		crp	⊢ ℝ+
2		cchp	⊢ ψ
3	0	cv	⊢ 𝑥
4	3 2	cfv	⊢ ( ψ ‘ 𝑥 )
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	⊢ ·
17	15 3 16	co	⊢ ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) · 𝑥 )
18	4 17 5	wbr	⊢ ( ψ ‘ 𝑥 ) < ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) · 𝑥 )
19	18 0 1	wral	⊢ ∀ 𝑥 ∈ ℝ+ ( ψ ‘ 𝑥 ) < ( ( 1 . _ 0 _ 3 _ 8 _ 8 3 ) · 𝑥 )