Michaelis–Menten kinetics and the quasi-steady state

DefinitionMichaelis constant#✓fully proved

The Michaelis constant K_M = (kb + k₂)/k₁ (Briggs–Haldane). Meaningful for k₁ > 0.

noncomputable def michaelisConstant (k₁ kb k₂ : ℝ) : ℝ :=
  (kb + k₂) / k₁

Used by 8

Used byRigorous QSSA · Quasi-steady-state manifold · Fast transient of the complex with frozen substrate · Fast transient solves the boundary-layer equation · Briggs–Haldane rate law · Quasi-steady-state value of the complex · Substrate consumption at the Michaelis–Menten rate under QSSA · Fast transient converges to the quasi-steady state

DefinitionMass-action rate of the substrate#✓fully proved

The mass-action rate of the substrate, s' = -k₁ e s + kb c.

def substrateRate (k₁ kb s c e : ℝ) : ℝ :=
  -k₁ * e * s + kb * c

Used by 4

Used byRigorous QSSA · Solution of the Michaelis–Menten mass-action system · Mass conservation · Substrate consumption at the Michaelis–Menten rate under QSSA

DefinitionMass-action rate of the enzyme–substrate complex#✓fully proved

The mass-action rate of the complex, c' = k₁ e s - (kb + k₂) c.

def complexRate (k₁ kb k₂ s c e : ℝ) : ℝ :=
  k₁ * e * s - (kb + k₂) * c

Used by 7

Used byRigorous QSSA · Quasi-steady-state manifold · Enzyme conservation · Fast transient solves the boundary-layer equation · Solution of the Michaelis–Menten mass-action system · Mass conservation · Substrate consumption at the Michaelis–Menten rate under QSSA

StructureSolution of the Michaelis–Menten mass-action system#✓fully proved

A solution of the Michaelis–Menten mass-action system on [0, ∞): s' = -k₁ e s + kb c, c' = k₁ e s - (kb + k₂) c, e' = -c', p' = k₂ c.

structure IsSolution (k₁ kb k₂ : ℝ) (s c e p : ℝ → ℝ) : Prop where
  hasDerivAt_substrate : ∀ t, 0 ≤ t → HasDerivAt s (substrateRate k₁ kb (s t) (c t) (e t)) t
  hasDerivAt_complex : ∀ t, 0 ≤ t →
    HasDerivAt c (complexRate k₁ kb k₂ (s t) (c t) (e t)) t
  hasDerivAt_enzyme : ∀ t, 0 ≤ t →
    HasDerivAt e (-complexRate k₁ kb k₂ (s t) (c t) (e t)) t
  hasDerivAt_product : ∀ t, 0 ≤ t → HasDerivAt p (k₂ * c t) t

Uses 2 · Used by 3

Statement usesMass-action rate of the enzyme–substrate complex · Mass-action rate of the substrate

Used byRigorous QSSA · Enzyme conservation · Mass conservation

TheoremEnzyme conservation#✓fully proved

e(t) + c(t) = e(0) + c(0).

theorem IsSolution.enzyme_conservation {k₁ kb k₂ : ℝ} {s c e p : ℝ → ℝ}
    (h : IsSolution k₁ kb k₂ s c e p) {t : ℝ} (ht : 0 ≤ t) : e t + c t = e 0 + c 0

Uses 2 · Used by 1

Statement usesSolution of the Michaelis–Menten mass-action system

Proof usesMass-action rate of the enzyme–substrate complex

Used byRigorous QSSA

TheoremMass conservation#✓fully proved

s(t) + c(t) + p(t) = s(0) + c(0) + p(0).

theorem IsSolution.substrate_conservation {k₁ kb k₂ : ℝ} {s c e p : ℝ → ℝ}
    (h : IsSolution k₁ kb k₂ s c e p) {t : ℝ} (ht : 0 ≤ t) :
    s t + c t + p t = s 0 + c 0 + p 0

Uses 3

Statement usesSolution of the Michaelis–Menten mass-action system

Proof usesMass-action rate of the enzyme–substrate complex · Mass-action rate of the substrate

DefinitionQuasi-steady-state value of the complex#✓fully proved

The quasi-steady-state value of the complex, c = e₀ s / (K_M + s).

noncomputable def qssComplex (k₁ kb k₂ e₀ s : ℝ) : ℝ :=
  e₀ * s / (michaelisConstant k₁ kb k₂ + s)

Uses 1 · Used by 7

Statement usesMichaelis constant

Used byRigorous QSSA · Quasi-steady-state manifold · Fast transient of the complex with frozen substrate · Fast transient solves the boundary-layer equation · Briggs–Haldane rate law · Substrate consumption at the Michaelis–Menten rate under QSSA · Fast transient converges to the quasi-steady state

DefinitionMichaelis–Menten rate law#✓fully proved

The Michaelis–Menten rate law v(s) = V_max s / (K_M + s).

noncomputable def mmRate (Vmax KM s : ℝ) : ℝ :=
  Vmax * s / (KM + s)

Used by 7

Used byRigorous QSSA · Michaelis–Menten rate stays below its maximum · Michaelis constant is the half-saturation substrate level · Michaelis–Menten rate is strictly increasing · Briggs–Haldane rate law · Substrate consumption at the Michaelis–Menten rate under QSSA · Saturation of the Michaelis–Menten rate

TheoremQuasi-steady-state manifold#✓fully proved

With total enzyme e₀ (so e = e₀ - c), k₁ > 0 and K_M + s ≠ 0, the complex is stationary iff c = e₀ s / (K_M + s).

theorem complexRate_eq_zero_iff {k₁ kb k₂ e₀ s c : ℝ} (hk₁ : 0 < k₁)
    (hs : michaelisConstant k₁ kb k₂ + s ≠ 0) :
    complexRate k₁ kb k₂ s c (e₀ - c) = 0 ↔ c = qssComplex k₁ kb k₂ e₀ s

Uses 3 · Used by 1

Statement usesMass-action rate of the enzyme–substrate complex · Michaelis constant · Quasi-steady-state value of the complex

Used bySubstrate consumption at the Michaelis–Menten rate under QSSA

TheoremBriggs–Haldane rate law#✓fully proved

On the quasi-steady-state manifold the product forms at rate k₂ c = V_max s / (K_M + s), V_max = k₂ e₀.

theorem productRate_qss (k₁ kb k₂ e₀ s : ℝ) :
    k₂ * qssComplex k₁ kb k₂ e₀ s = mmRate (k₂ * e₀) (michaelisConstant k₁ kb k₂) s

Uses 3 · Used by 1

Statement usesMichaelis constant · Michaelis–Menten rate law · Quasi-steady-state value of the complex

Used bySubstrate consumption at the Michaelis–Menten rate under QSSA

TheoremSubstrate consumption at the Michaelis–Menten rate under QSSA#✓fully proved

On the quasi-steady-state manifold the substrate is consumed at the Michaelis–Menten rate: s' = -V_max s / (K_M + s).

theorem substrateRate_qss {k₁ kb k₂ e₀ s : ℝ} (hk₁ : 0 < k₁)
    (hs : michaelisConstant k₁ kb k₂ + s ≠ 0) :
    substrateRate k₁ kb s (qssComplex k₁ kb k₂ e₀ s) (e₀ - qssComplex k₁ kb k₂ e₀ s) =
      -mmRate (k₂ * e₀) (michaelisConstant k₁ kb k₂) s

Uses 7

Statement usesMichaelis constant · Michaelis–Menten rate law · Quasi-steady-state value of the complex · Mass-action rate of the substrate

Proof usesMass-action rate of the enzyme–substrate complex · Quasi-steady-state manifold · Briggs–Haldane rate law

TheoremMichaelis–Menten rate is strictly increasing#✓fully proved

The rate law is strictly increasing on s ≥ 0 for V_max, K_M > 0.

theorem mmRate_strictMono {Vmax KM : ℝ} (hV : 0 < Vmax) (hK : 0 < KM) :
    StrictMonoOn (mmRate Vmax KM) (Ici 0)

Uses 1 · Used by 1

Statement usesMichaelis–Menten rate law

Used byRigorous QSSA

TheoremMichaelis constant is the half-saturation substrate level#✓fully proved

The Michaelis constant is the half-saturation substrate level: v(K_M) = V_max / 2.

theorem mmRate_michaelisConstant {Vmax KM : ℝ} (hK : KM ≠ 0) :
    mmRate Vmax KM KM = Vmax / 2

Uses 1

Statement usesMichaelis–Menten rate law

TheoremMichaelis–Menten rate stays below its maximum#✓fully proved

The rate law is below its maximum: v(s) < V_max for s ≥ 0, V_max, K_M > 0.

theorem mmRate_lt {Vmax KM s : ℝ} (hV : 0 < Vmax) (hK : 0 < KM) (hs : 0 ≤ s) :
    mmRate Vmax KM s < Vmax

Uses 1

Statement usesMichaelis–Menten rate law

TheoremSaturation of the Michaelis–Menten rate#✓fully proved

Saturation: v(s) → V_max as s → ∞.

theorem tendsto_mmRate (Vmax KM : ℝ) :
    Tendsto (mmRate Vmax KM) atTop (𝓝 Vmax)

Uses 1

Statement usesMichaelis–Menten rate law

DefinitionFast transient of the complex with frozen substrate#✓fully proved

The fast transient of the complex with the substrate frozen at s̄: c(t) = c* + (c₀ - c*) e^{-k₁ (s̄ + K_M) t}, where c* = e₀ s̄ / (K_M + s̄).

noncomputable def fastTransient (k₁ kb k₂ e₀ s c₀ t : ℝ) : ℝ :=
  qssComplex k₁ kb k₂ e₀ s + (c₀ - qssComplex k₁ kb k₂ e₀ s) *
    exp (-(k₁ * (s + michaelisConstant k₁ kb k₂)) * t)

Uses 2 · Used by 2

Statement usesMichaelis constant · Quasi-steady-state value of the complex

Used byFast transient solves the boundary-layer equation · Fast transient converges to the quasi-steady state

TheoremFast transient solves the boundary-layer equation#✓fully proved

The fast transient solves the boundary-layer equation c' = k₁ (e₀ - c) s̄ - (kb + k₂) c for k₁ > 0 and K_M + s̄ ≠ 0.

theorem hasDerivAt_fastTransient {k₁ kb k₂ e₀ s : ℝ} (hk₁ : 0 < k₁)
    (hs : michaelisConstant k₁ kb k₂ + s ≠ 0) (c₀ t : ℝ) :
    HasDerivAt (fastTransient k₁ kb k₂ e₀ s c₀)
      (complexRate k₁ kb k₂ s (fastTransient k₁ kb k₂ e₀ s c₀ t)
        (e₀ - fastTransient k₁ kb k₂ e₀ s c₀ t)) t

Uses 4

Statement usesMass-action rate of the enzyme–substrate complex · Fast transient of the complex with frozen substrate · Michaelis constant

Proof usesQuasi-steady-state value of the complex

TheoremFast transient converges to the quasi-steady state#✓fully proved

The fast transient converges to the quasi-steady-state value for k₁ > 0 and s̄ + K_M > 0.

theorem tendsto_fastTransient {k₁ kb k₂ e₀ s : ℝ} (hk₁ : 0 < k₁)
    (hs : 0 < s + michaelisConstant k₁ kb k₂) (c₀ : ℝ) :
    Tendsto (fastTransient k₁ kb k₂ e₀ s c₀) atTop (𝓝 (qssComplex k₁ kb k₂ e₀ s))

Uses 3

Statement usesFast transient of the complex with frozen substrate · Michaelis constant · Quasi-steady-state value of the complex

TheoremRigorous QSSA#✓fully proved

Rigorous QSSA (Tikhonov 1952; Heineken–Tsuchiya–Aris 1967). On the slow time scale τ = e₀ t, the substrate of the full Michaelis–Menten system with s(0) = s₀, c(0) = 0, e(0) = e₀ stays within C e₀ of the solution S̄ of the reduced equation dS̄/dτ = -k₂ S̄ / (K_M + S̄), S̄(0) = s₀, uniformly on [0, T].

theorem abs_sub_reduced_le {k₁ kb k₂ s₀ T : ℝ} (hk₁ : 0 < k₁) (hkb : 0 ≤ kb)
    (hk₂ : 0 < k₂) (hs₀ : 0 < s₀) (hT : 0 < T) {S : ℝ → ℝ}
    (hS : ∀ τ, 0 ≤ τ → HasDerivAt S (-mmRate k₂ (michaelisConstant k₁ kb k₂) (S τ)) τ)
    (hS₀ : S 0 = s₀) :
    ∃ C : ℝ, ∀ e₀ : ℝ, 0 < e₀ → e₀ ≤ 1 → ∀ s c e p : ℝ → ℝ, IsSolution k₁ kb k₂ s c e p →
      s 0 = s₀ → c 0 = 0 → e 0 = e₀ → ∀ τ ∈ Icc 0 T, |s (τ / e₀) - S τ| ≤ C * e₀

Uses 8

Statement usesSolution of the Michaelis–Menten mass-action system · Michaelis constant · Michaelis–Menten rate law

Proof usesEnzyme conservation · Mass-action rate of the enzyme–substrate complex · Michaelis–Menten rate is strictly increasing · Quasi-steady-state value of the complex · Mass-action rate of the substrate

19 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.