Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ax-ros335 Structured version   Visualization version   GIF version

Axiom ax-ros335 31273
 Description: Theorem 12. of [RosserSchoenfeld] p. 71. Theorem chpo1ubb 25584 states that the ψ 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.)
Assertion
Ref Expression
ax-ros335 𝑥 ∈ ℝ+ (ψ‘𝑥) < ((1.03883) · 𝑥)

Detailed syntax breakdown of Axiom ax-ros335
StepHypRef Expression
1 vx . . . . 5 setvar 𝑥
21cv 1657 . . . 4 class 𝑥
3 cchp 25233 . . . 4 class ψ
42, 3cfv 6124 . . 3 class (ψ‘𝑥)
5 c1 10254 . . . . 5 class 1
6 cc0 10253 . . . . . 6 class 0
7 c3 11408 . . . . . . 7 class 3
8 c8 11413 . . . . . . . 8 class 8
98, 7cdp2 30125 . . . . . . . 8 class 83
108, 9cdp2 30125 . . . . . . 7 class 883
117, 10cdp2 30125 . . . . . 6 class 3883
126, 11cdp2 30125 . . . . 5 class 03883
13 cdp 30142 . . . . 5 class .
145, 12, 13co 6906 . . . 4 class (1.03883)
15 cmul 10258 . . . 4 class ·
1614, 2, 15co 6906 . . 3 class ((1.03883) · 𝑥)
17 clt 10392 . . 3 class <
184, 16, 17wbr 4874 . 2 wff (ψ‘𝑥) < ((1.03883) · 𝑥)
19 crp 12113 . 2 class +
2018, 1, 19wral 3118 1 wff 𝑥 ∈ ℝ+ (ψ‘𝑥) < ((1.03883) · 𝑥)
 Colors of variables: wff setvar class This axiom is referenced by:  hgt750lemc  31275
 Copyright terms: Public domain W3C validator