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

Axiom ax-ros336 34214
Description: Theorem 13. of [RosserSchoenfeld] p. 71. Theorem chpchtlim 27399 states that the ψ and θ 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.)
Assertion
Ref Expression
ax-ros336 𝑥 ∈ ℝ+ ((ψ‘𝑥) − (θ‘𝑥)) < ((1.4262) · (√‘𝑥))

Detailed syntax breakdown of Axiom ax-ros336
StepHypRef Expression
1 vx . . . . . 6 setvar 𝑥
21cv 1533 . . . . 5 class 𝑥
3 cchp 27012 . . . . 5 class ψ
42, 3cfv 6542 . . . 4 class (ψ‘𝑥)
5 ccht 27010 . . . . 5 class θ
62, 5cfv 6542 . . . 4 class (θ‘𝑥)
7 cmin 11466 . . . 4 class
84, 6, 7co 7414 . . 3 class ((ψ‘𝑥) − (θ‘𝑥))
9 c1 11131 . . . . 5 class 1
10 c4 12291 . . . . . 6 class 4
11 c2 12289 . . . . . . 7 class 2
12 c6 12293 . . . . . . . 8 class 6
1312, 11cdp2 32576 . . . . . . 7 class 62
1411, 13cdp2 32576 . . . . . 6 class 262
1510, 14cdp2 32576 . . . . 5 class 4262
16 cdp 32593 . . . . 5 class .
179, 15, 16co 7414 . . . 4 class (1.4262)
18 csqrt 15204 . . . . 5 class
192, 18cfv 6542 . . . 4 class (√‘𝑥)
20 cmul 11135 . . . 4 class ·
2117, 19, 20co 7414 . . 3 class ((1.4262) · (√‘𝑥))
22 clt 11270 . . 3 class <
238, 21, 22wbr 5142 . 2 wff ((ψ‘𝑥) − (θ‘𝑥)) < ((1.4262) · (√‘𝑥))
24 crp 12998 . 2 class +
2523, 1, 24wral 3056 1 wff 𝑥 ∈ ℝ+ ((ψ‘𝑥) − (θ‘𝑥)) < ((1.4262) · (√‘𝑥))
Colors of variables: wff setvar class
This axiom is referenced by:  hgt750lemd  34216
  Copyright terms: Public domain W3C validator