ack_add_one_sq_lt_ack_add_four — Mathlib

English

For all m,n, ack(m, (n+1)^2) < ack(m+4, n).

Русский

Для всех m,n: ack(m, (n+1)^2) < ack(m+4, n).

LaTeX

$$$$\\forall m,n \\in \\mathbb{N}, \\operatorname{ack}(m, (n+1)^2) \\lt \\operatorname{ack}(m+4, n).$$$$

Lean4

theorem ack_add_one_sq_lt_ack_add_four (m n : ℕ) : ack m ((n + 1) ^ 2) < ack (m + 4) n :=
  calc
    ack m ((n + 1) ^ 2) < ack m ((ack m n + 1) ^ 2) :=
      ack_strictMono_right m <| Nat.pow_lt_pow_left (succ_lt_succ <| lt_ack_right m n) two_ne_zero
    _ ≤ ack m (ack (m + 3) n) := (ack_mono_right m <| ack_add_one_sq_lt_ack_add_three m n)
    _ ≤ ack (m + 2) (ack (m + 3) n) := (ack_mono_left _ <| by cutsat)
    _ = ack (m + 3) (n + 1) := (ack_succ_succ _ n).symm
    _ ≤ ack (m + 4) n := ack_succ_right_le_ack_succ_left _ n

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