BKLNW.buthe_eq_1_7

@[blueprint  "from-buthe-eq-1-7"  (title := "A consequence of Buthe equation (1.7)")  (statement := /-- $\theta(x) < x$ for all $1 \leq x \leq 10^{19}$. -/)  (latexEnv := "sublemma")  (proof := /-- This follows from Theorem \ref{buthe-theorem-2c}. -/)  (discussion := 787)]theorem buthe_eq_1_7 : ∀ x ∈ Set.Ioc 0 1e19, θ x < x := by  intro x hx  have hx':= (Set.mem_Ioc).1 hx  have hlb := hx'.left  have hub:= hx'.right  have hub' : x ≤ 10^19 := by linarith  by_cases h : x < 1  · have hworse: x < 2 := by linarith    have htheta: theta x = 0 := by apply Chebyshev.theta_eq_zero_of_lt_two hworse    linarith  · have hnewlb : x≥ 1 := by simpa using h    have hineq : x - θ x > 5e-2 * √x := by exact Buthe.theorem_2c hnewlb hub'    have hsqrtpos: 0 < sqrt x := by exact Real.sqrt_pos.mpr hlb    linarith