lt_of_sum_four_squares_eq_mul — Mathlib

English

If a^2 + b^2 + c^2 + d^2 = k m with ha hb hc hd: 2a<m, 2b<m, 2c<m, 2d<m, then k < m.

Русский

Если сумма квадратов четырех чисел равна k m и каждая пара (2a, m), (2b, m), (2c, m), (2d, m) удовлетворяет неравенствам, то k < m.

LaTeX

$$$a^2+b^2+c^2+d^2 = k m,\; 2a

Lean4

theorem lt_of_sum_four_squares_eq_mul {a b c d k m : ℕ} (h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = k * m) (ha : 2 * a < m)
    (hb : 2 * b < m) (hc : 2 * c < m) (hd : 2 * d < m) : k < m := by nlinarith

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