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	⊢ ∀ 𝑥 ∈ ℝ⁺ ( ( ψ ‘ 𝑥 ) − ( θ ‘ 𝑥 ) ) < ( ( 1 . _ 4 _ 2 _ 6 2 ) · ( √ ‘ 𝑥 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	⊢ 𝑥
1		crp	⊢ ℝ⁺
2		cchp	⊢ ψ
3	0	cv	⊢ 𝑥
4	3 2	cfv	⊢ ( ψ ‘ 𝑥 )
5		cmin	⊢ −
6		ccht	⊢ θ
7	3 6	cfv	⊢ ( θ ‘ 𝑥 )
8	4 7 5	co	⊢ ( ( ψ ‘ 𝑥 ) − ( θ ‘ 𝑥 ) )
9		clt	⊢ <
10		c1	⊢ 1
11		cdp	⊢ .
12		c4	⊢ 4
13		c2	⊢ 2
14		c6	⊢ 6
15	14 13	cdp2	⊢ _ 6 2
16	13 15	cdp2	⊢ _ 2 _ 6 2
17	12 16	cdp2	⊢ _ 4 _ 2 _ 6 2
18	10 17 11	co	⊢ ( 1 . _ 4 _ 2 _ 6 2 )
19		cmul	⊢ ·
20		csqrt	⊢ √
21	3 20	cfv	⊢ ( √ ‘ 𝑥 )
22	18 21 19	co	⊢ ( ( 1 . _ 4 _ 2 _ 6 2 ) · ( √ ‘ 𝑥 ) )
23	8 22 9	wbr	⊢ ( ( ψ ‘ 𝑥 ) − ( θ ‘ 𝑥 ) ) < ( ( 1 . _ 4 _ 2 _ 6 2 ) · ( √ ‘ 𝑥 ) )
24	23 0 1	wral	⊢ ∀ 𝑥 ∈ ℝ⁺ ( ( ψ ‘ 𝑥 ) − ( θ ‘ 𝑥 ) ) < ( ( 1 . _ 4 _ 2 _ 6 2 ) · ( √ ‘ 𝑥 ) )

Metamath Proof Explorer

Axiom ax-ros336

Detailed syntax breakdown