Ordinary Log10 lt of pow lt

import Mathlib.Algebra.Order.Floor.Semiring
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Tactic
import Definitions.Def_D1Bound5_OrdinaryLog10_Definitions

section
namespace D1Bound5


















theorem _root_.D1Bound5.ordinaryLog10_lt_of_pow_lt (x : ℝ) (m n : ℕ)
    (hx : 0 < x) (hpow : x^n < (10 : ℝ)^m) :
    (n : ℝ)*ordinaryLog10 x < m := by sorry





end D1Bound5
end