log_nz_of_isNNRat — Mathlib

English

If e is NN rational with given bounds 0 < n/d < 1, then log e ≠ 0.

Русский

Если e является NN рациональным с границами 0 < n/d < 1, то log e ≠ 0.

LaTeX

$$$$ \\log e \\neq 0 \\quad \\text{when } e \\text{ is NN rational with } 0 < n/d < 1. $$$$

Lean4

theorem log_nz_of_isNNRat {n : ℕ} :
    (NormNum.IsNNRat e n d) → (decide ((0 : ℚ) < n / d)) → (decide (n / d < (1 : ℚ))) → (Real.log (e : ℝ) ≠ 0)
  | ⟨inv, eq⟩, h₁, h₂ => by
    rw [eq, invOf_eq_inv, ← div_eq_mul_inv]
    have h₁' : 0 < (n : ℝ) / d := by simpa using (Rat.cast_pos (K := ℝ)).2 (of_decide_eq_true h₁)
    have h₂' : (n : ℝ) / d < 1 := by simpa using (Rat.cast_lt (K := ℝ)).2 (of_decide_eq_true h₂)
    exact ne_of_lt <| Real.log_neg h₁' h₂'

Похожие утверждения