This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database SUPPLEMENTARY MATERIAL (USERS' MATHBOXES) Mathbox for Thierry Arnoux Number Theory The Ternary Goldbach Conjecture: Final Statement 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 ) · 𝑥 )