Skip to main content

En ℝ, (a+b)(a-b) = a²-b²

Números reales

Demostrar con Lean4 que si \(a\) y \(b\) son números reales, entonces \[ (a + b)·(a - b) = a² - b² \]

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

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable (a b : ℝ)

example : (a + b) * (a - b) = a^2 - b^2 :=
sorry

Read more…

En ℝ, (a + b)(c + d) = ac + ad + bc + bd

Números reales

Demostrar con Lean4 que si \(a\), \(b\), \(c\) y \(d\) son números reales, entonces \[ (a + b)(c + d) = ac + ad + bc + bd \]

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

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable (a b c d : ℝ)

example
  : (a + b) * (c + d) = a * c + a * d + b * c + b * d :=
sorry

Read more…

En ℝ, (a + b)(a + b) = aa + 2ab + bb

Números reales

Demostrar con Lean4 que si \(a\) y \(b\) son números reales, entonces \[ (a + b)(a + b) = aa + 2ab + bb \]

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

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable (a b c : ℝ)

example :
  (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=
sorry

Read more…

Si c = ba-d y d = ab, entonces c = 0

Números reales

Demostrar con Lean4 que si \(a\), \(b\), \(c\) y \(d\) son números reales tales \begin{align} &c = ba - d \newline &d = ab \end{align} entonces \[ c = 0 \]

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

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

example
  (a b c d : ℝ)
  (h1 : c = b * a - d)
  (h2 : d = a * b)
  : c = 0 :=
by sorry

Read more…

Si bc = ef, entonces ((ab)c)d = ((ae)f)d

Números reales

Demostrar con Lean4 que si \(bc = ef\), entonces \(((ab)c)d = ((ae)f)d\).

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

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

example
  (a b c d e f : ℝ)
  (h : b * c = e * f)
  : ((a * b) * c) * d = ((a * e) * f) * d :=
by sorry

Read more…

Si ab = cd y e = f, entonces a(be) = c(df)

Números reales

Demostrar con Lean4 que si \(ab = cd\) y \(e = f\), entonces \(a(be) = c(df)\).

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

import Mathlib.Tactic
import Mathlib.Data.Real.Basic

example
  (a b c d e f : ℝ)
  (h1 : a * b = c * d)
  (h2 : e = f)
  : a * (b * e) = c * (d * f) :=
by sorry

Read more…

En ℝ, a(bc) = b(ac)

Números reales

Demostrar con Lean4 que en ℝ, \[ a(bc) = b(ac) \]

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

import Mathlib.Tactic
import Mathlib.Data.Real.Basic

example
  (a b c : ℝ) : a * (b * c) = b * (a * c) :=
by sorry

Read more…

En ℝ, (cb)a = b(ac)

Números reales

Demostrar con Lean4 que los números reales tienen la siguiente propiedad \[ (cb)a = b(ac) \]

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

import Mathlib.Tactic
import Mathlib.Data.Real.Basic

example (a b c : ℝ) : (c * b) * a = b * (a * c) :=
by sorry

Demostración en lenguaje natural

Por la siguiente cadena de igualdades: \begin{align} (cb)a &= (bc)a &&\text{[por la conmutativa]} \newline &= b(ca) &&\text{[por la asociativa]} \newline &= b(ac) &&\text{[por la conmutativa]} \end{align}

Demostraciones con Lean4

import Mathlib.Tactic
import Mathlib.Data.Real.Basic

-- 1ª demostración
example
  (a b c : ℝ)
  : (c * b) * a = b * (a * c) :=
calc
  (c * b) * a
    = (b * c) * a := by rw [mul_comm c b]
  _ = b * (c * a) := by rw [mul_assoc]
  _ = b * (a * c) := by rw [mul_comm c a]

-- 2ª demostración
example
  (a b c : ℝ)
  : (c * b) * a = b * (a * c) :=
by
  rw [mul_comm c b]
  rw [mul_assoc]
  rw [mul_comm c a]

-- 3ª demostración
example
  (a b c : ℝ)
  : (c * b) * a = b * (a * c) :=
by ring

Demostraciones interactivas

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

Referencias

En ℝ, (ab)c = b(ac)

Números reales

Demostrar con Lean4 que los números reales tienen la siguiente propiedad \[ (ab)c = b(ac) \]

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

import Mathlib.Tactic
import Mathlib.Data.Real.Basic

example (a b c : ℝ) : (a * b) * c = b * (a * c) := by
sorry

Demostración en lenguaje natural

Por la siguiente cadena de igualdades \begin{align} (ab)c &= (ba)c &&\text{[por la conmutativa]} \newline &= b(ac) &&\text{[por la asociativa]} \end{align}

Demostraciones con Lean4

import Mathlib.Tactic
import Mathlib.Data.Real.Basic

-- 1ª demostración
example
  (a b c : ℝ)
  : (a * b) * c = b * (a * c) :=
calc
  (a * b) * c = (b * a) * c := by rw [mul_comm a b]
            _ = b * (a * c) := by rw [mul_assoc b a c]

-- 2ª demostración
example (a b c : ℝ) : (a * b) * c = b * (a * c) := by
  rw [mul_comm a b]
  rw [mul_assoc b a c]

-- 3ª demostración
example (a b c : ℝ) : (a * b) * c = b * (a * c) :=
by ring

Demostraciones interactivas

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

Referencias

El producto por un par es par

Números naturales

Demostrar que los productos de los números naturales por números pares son pares.

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

import Mathlib.Algebra.Ring.Parity
import Mathlib.Tactic

open Nat

example : ∀ m n : ℕ, Even n → Even (m * n) := by
  sorry

Demostración en lenguaje natural

Si \(n\) es par, entonces (por la definición de Even) existe un \(k\) tal que \[ \begin{align} n = k + k && (1) \end{align} \] Por tanto, \[ \begin{align} mn &= m(k + k) && (\text{por (1)})\newline &= mk + mk && (\text{por la propiedad distributiva}) \end{align} \] Por consiguiente, \(mn\) es par.

Soluciones con Lean4

import Mathlib.Algebra.Ring.Parity
import Mathlib.Tactic

open Nat

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

example : ∀ m n : ℕ, Even n → Even (m * n) := by
  rintro m n ⟨k, hk⟩
  use m * k
  rw [hk]
  ring

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

example : ∀ m n : ℕ, Even n → Even (m * n) := by
  rintro m n ⟨k, hk⟩
  use m * k
  rw [hk]
  rw [mul_add]

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

example : ∀ m n : ℕ, Even n → Even (m * n) := by
  rintro m n ⟨k, hk⟩
  use m * k
  rw [hk, mul_add]

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

example : ∀ m n : Nat, Even n → Even (m * n) := by
  rintro m n ⟨k, hk⟩; use m * k; rw [hk, mul_add]

-- 5ª demostración
-- ===============

example : ∀ m n : ℕ, Even n → Even (m * n) := by
  rintro m n ⟨k, hk⟩
  exact ⟨m * k, by rw [hk, mul_add]⟩

-- 6ª demostración
-- ===============

example : ∀ m n : Nat, Even n → Even (m * n) :=
fun m n ⟨k, hk⟩ ↦ ⟨m * k, by rw [hk, mul_add]⟩

-- 7ª demostración
-- ===============

example : ∀ m n : ℕ, Even n → Even (m * n) := by
  rintro m n ⟨k, hk⟩
  use m * k
  rw [hk]
  exact mul_add m k k

-- 8ª demostración
-- ===============

example : ∀ m n : ℕ, Even n → Even (m * n) := by
  intros m n hn
  unfold Even at *
  cases hn with
  | intro k hk =>
    use m * k
    rw [hk, mul_add]

-- 9ª demostración
-- ===============

example : ∀ m n : ℕ, Even n → Even (m * n) := by
  intros m n hn
  unfold Even at *
  cases hn with
  | intro k hk =>
    use m * k
    calc m * n
       = m * (k + k)   := by exact congrArg (HMul.hMul m) hk
     _ = m * k + m * k := by exact mul_add m k k

-- 10ª demostración
-- ================

example : ∀ m n : Nat, Even n → Even (m * n) := by
  intros; simp [*, parity_simps]

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

-- #check (mul_add : ∀ a b c : ℕ, a * (b + c) = a * b + a * c)

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

Referencias