Skip to content

Latest commit

 

History

History
187 lines (157 loc) · 3.97 KB

CS_de_divisibilidad_del_producto.md

File metadata and controls

187 lines (157 loc) · 3.97 KB
Título Autor
Si m divide a n o a k, entonces m divide a nk.
José A. Alonso

[mathjax]

Demostrar con Lean4 que si (m) divide a (n) o a (k), entonces (m) divide a (nk).

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Tactic
variable {m n k : ℕ}

example
  (h : m ∣ n ∨ m ∣ k)
  : m ∣ n * k :=
by sorry

Demostración en lenguaje natural

Se demuestra por casos.

Caso 1: Supongamos que (m ∣ n). Entonces, existe un (a ∈ ℕ) tal que [ n = ma ] Por tanto, \begin{align} nk &= (ma)k \ &= m(ak) \end{align} que es divisible por (m).

Caso 2: Supongamos que (m ∣ k). Entonces, existe un (b ∈ ℕ) tal que [ k = mb ] Por tanto, \begin{align} nk &= n(mb) \ &= m(nb) \end{align} que es divisible por (m).

Demostraciones con Lean4

import Mathlib.Tactic
variable {m n k : ℕ}

-- 1ª demostración
-- ===============

example
  (h : m ∣ n ∨ m ∣ k)
  : m ∣ n * k :=
by
  rcases h with h1 | h2
  . -- h1 : m ∣ n
    rcases h1 with ⟨a, ha⟩
    -- a : ℕ
    -- ha : n = m * a
    rw [ha]
    -- ⊢ m ∣ (m * a) * k
    rw [mul_assoc]
    -- ⊢ m ∣ m * (a * k)
    exact dvd_mul_right m (a * k)
  . -- h2 : m ∣ k
    rcases h2 with ⟨b, hb⟩
    -- b : ℕ
    -- hb : k = m * b
    rw [hb]
    -- ⊢ m ∣ n * (m * b)
    rw [mul_comm]
    -- ⊢ m ∣ (m * b) * n
    rw [mul_assoc]
    -- ⊢ m ∣ m * (b * n)
    exact dvd_mul_right m (b * n)

-- 2ª demostración
-- ===============

example
  (h : m ∣ n ∨ m ∣ k)
  : m ∣ n * k :=
by
  rcases h with h1 | h2
  . -- h1 : m ∣ n
    rcases h1 with ⟨a, ha⟩
    -- a : ℕ
    -- ha : n = m * a
    rw [ha, mul_assoc]
    -- ⊢ m ∣ m * (a * k)
    exact dvd_mul_right m (a * k)
  . -- h2 : m ∣ k
    rcases h2 with ⟨b, hb⟩
    -- b : ℕ
    -- hb : k = m * b
    rw [hb, mul_comm, mul_assoc]
    -- ⊢ m ∣ m * (b * n)
    exact dvd_mul_right m (b * n)

-- 3ª demostración
-- ===============

example
  (h : m ∣ n ∨ m ∣ k)
  : m ∣ n * k :=
by
  rcases h with ⟨a, rfl⟩ | ⟨b, rfl⟩
  . -- a : ℕ
    -- ⊢ m ∣ (m * a) * k
    rw [mul_assoc]
    -- ⊢ m ∣ m * (a * k)
    exact dvd_mul_right m (a * k)
  . -- ⊢ m ∣ n * (m * b)
    rw [mul_comm, mul_assoc]
    -- ⊢ m ∣ m * (b * n)
    exact dvd_mul_right m (b * n)

-- 4ª demostración
-- ===============

example
  (h : m ∣ n ∨ m ∣ k)
  : m ∣ n * k :=
by
  rcases h with h1 | h2
  . -- h1 : m ∣ n
    exact dvd_mul_of_dvd_left h1 k
  . -- h2 : m ∣ k
    exact dvd_mul_of_dvd_right h2 n

-- Lemas usados
-- ============

-- #check (dvd_mul_of_dvd_left : m ∣ n → ∀ (c : ℕ), m ∣ n * c)
-- #check (dvd_mul_of_dvd_right : m ∣ n → ∀ (c : ℕ), m ∣ c * n)
-- #check (dvd_mul_right m n : m ∣ m * n)
-- #check (mul_assoc m n k : m * n * k = m * (n * k))
-- #check (mul_comm m n : m * n = n * m)

Demostraciones interactivas

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

Referencias

Demostraciones con Isabelle/HOL

theory CS_de_divisibilidad_del_producto
  imports Main
begin

(* 1ª demostración *)
lemma
  fixes n m k :: nat
  assumes "m dvd n ∨ m dvd k"
  shows "m dvd (n * k)"
using assms
proof
    assume "m dvd n"
    then obtain a where "n = m * a" by auto
    then have "n * k = m * (a * k)" by simp
    then show ?thesis by auto
  next
    assume "m dvd k"
    then obtain b where "k = m * b" by auto
    then have "n * k = m * (n * b)" by simp
    then show ?thesis by auto
qed

(* 2ª demostración *)
lemma
  fixes n m k :: nat
  assumes "m dvd n ∨ m dvd k"
  shows "m dvd (n * k)"
  using assms by auto

end