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 31274
 Description: Theorem 13. of [RosserSchoenfeld] p. 71. Theorem chpchtlim 25582 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 1657 . . . . 5 class 𝑥
3 cchp 25233 . . . . 5 class ψ
42, 3cfv 6124 . . . 4 class (ψ‘𝑥)
5 ccht 25231 . . . . 5 class θ
62, 5cfv 6124 . . . 4 class (θ‘𝑥)
7 cmin 10586 . . . 4 class
84, 6, 7co 6906 . . 3 class ((ψ‘𝑥) − (θ‘𝑥))
9 c1 10254 . . . . 5 class 1
10 c4 11409 . . . . . 6 class 4
11 c2 11407 . . . . . . 7 class 2
12 c6 11411 . . . . . . . 8 class 6
1312, 11cdp2 30125 . . . . . . 7 class 62
1411, 13cdp2 30125 . . . . . 6 class 262
1510, 14cdp2 30125 . . . . 5 class 4262
16 cdp 30142 . . . . 5 class .
179, 15, 16co 6906 . . . 4 class (1.4262)
18 csqrt 14351 . . . . 5 class
192, 18cfv 6124 . . . 4 class (√‘𝑥)
20 cmul 10258 . . . 4 class ·
2117, 19, 20co 6906 . . 3 class ((1.4262) · (√‘𝑥))
22 clt 10392 . . 3 class <
238, 21, 22wbr 4874 . 2 wff ((ψ‘𝑥) − (θ‘𝑥)) < ((1.4262) · (√‘𝑥))
24 crp 12113 . 2 class +
2523, 1, 24wral 3118 1 wff 𝑥 ∈ ℝ+ ((ψ‘𝑥) − (θ‘𝑥)) < ((1.4262) · (√‘𝑥))
 Colors of variables: wff setvar class This axiom is referenced by:  hgt750lemd  31276
 Copyright terms: Public domain W3C validator