Divisor_del_mcd.md

Título	Autor
3 divide al máximo común divisor de 6 y 15.	José A. Alonso

[mathjax]

Demostrar con Lean4 que 3 divide al máximo común divisor de 6 y 15.

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

import Mathlib.Data.Real.Basic
import Mathlib.Data.Nat.GCD.Basic

open Nat

example : 3 ∣ gcd 6 15 :=
by sorry

Demostración en lenguaje natural

Se usará el siguiente lema \[ (∀ k, m, n ∈ ℕ)[k ∣ \gcd(m, n) ↔ k ∣ m ∧ k ∣ n] \]

Por el lema, \[ 3 ∣ \gcd(6, 15) \] se reduce a \[ 3 ∣ 6 ∧ 3 ∣ 15 \] que se verifican fácilmente.

Demostraciones con Lean4

import Mathlib.Data.Real.Basic
import Mathlib.Data.Nat.GCD.Basic

open Nat

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

example : 3 ∣ gcd 6 15 :=
by
  rw [dvd_gcd_iff]
  -- ⊢ 3 ∣ 6 ∧ 3 ∣ 15
  constructor
  . -- 3 ∣ 6
    norm_num
  . -- ⊢ 3 ∣ 15
    norm_num

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

example : 3 ∣ gcd 6 15 :=
by
  rw [dvd_gcd_iff]
  -- ⊢ 3 ∣ 6 ∧ 3 ∣ 15
  constructor <;> norm_num

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

-- variable (k m n : ℕ)
-- #check (dvd_gcd_iff : k ∣ gcd m n ↔ k ∣ m ∧ k ∣ n)

Demostraciones interactivas

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

Referencias

• J. Avigad y P. Massot. Mathematics in Lean, p. 37.