Existen números primos m y n tales que 4 < m < n < 10

Demostrar con Lean4 que existen números primos $m$ y $n$ tales que $4 < m < n < 10$ .

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

import Mathlib.Data.Nat.Prime
import Mathlib.Tactic

example :
  ∃ m n : ℕ, 4 < m ∧ m < n ∧ n < 10 ∧ Nat.Prime m ∧ Nat.Prime n :=
by sorry

import Mathlib.Data.Nat.Prime

import Mathlib.Tactic

example :

∃ m n : ℕ, 4 < m ∧ m < n ∧ n < 10 ∧ Nat.Prime m ∧ Nat.Prime n :=

by sorry

Demostración en lenguaje natural

Basta considerar los números $5$ y $7$ , ya que son primos y $4 < 5 < 7 < 10$ .

Demostraciones con Lean4

import Mathlib.Data.Nat.Prime
import Mathlib.Tactic

example :
  ∃ m n : ℕ, 4 < m ∧ m < n ∧ n < 10 ∧ Nat.Prime m ∧ Nat.Prime n :=
by
  use 5, 7
  norm_num

import Mathlib.Data.Nat.Prime

import Mathlib.Tactic

example :

∃ m n : ℕ, 4 < m ∧ m < n ∧ n < 10 ∧ Nat.Prime m ∧ Nat.Prime n :=

use 5, 7

norm_num

Demostraciones interactivas

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

Referencias

J. Avigad y P. Massot. Mathematics in Lean, p. 36.

Share this:

Escribe un comentarioCancel reply