factorial_lt — Mathlib

English

For all m,n ∈ ℕ with 0 < n, n! < m! iff n < m.

Русский

Для любых m,n ∈ ℕ с n > 0 выполняется: n! < m! ⇔ n < m.

LaTeX

$$$\forall {m,n:\mathbb{N}}, 0 < n \rightarrow (n! < m! \leftrightarrow n < m)$$$

Lean4

theorem factorial_lt (hn : 0 < n) : n ! < m ! ↔ n < m :=
  by
  refine ⟨fun h => not_le.mp fun hmn => Nat.not_le_of_gt h (factorial_le hmn), fun h => ?_⟩
  have : ∀ {n}, 0 < n → n ! < (n + 1)! := by
    intro k hk
    rw [factorial_succ, succ_mul, Nat.lt_add_left_iff_pos]
    exact Nat.mul_pos hk k.factorial_pos
  induction h generalizing hn with
  | refl => exact this hn
  | step hnk ih => exact lt_trans (ih hn) <| this <| lt_trans hn <| lt_of_succ_le hnk

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