Two small large C seventh power

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

section
namespace D1Bound5






theorem _root_.D1Bound5.two_small_large_C_seventh_power
    (A B S T C D Z : ℝ) (hA : 1 ≤ A) (hB : 0 < B) (hB3 : B < 3)
    (hS : 0 < S) (hT : 0 < T) (hS8 : S < (10 : ℝ)^8) (hT8 : T < (10 : ℝ)^8)
    (hC : (10 : ℝ)^100 ≤ C) (hZ : 0 < Z) (hCZ : C/2 < Z)
    (hroot : Z^2 ≤ 2*C*D)
    (hform : 1 < 13*B*S^2*T^3/Z+49*S*T^2*Z/(50*A*C^4)) :
    C^7/(10 : ℝ)^50 < D := by sorry

end D1Bound5
end