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:
|
1 2 3 4 5 6 |
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
|
1 2 3 4 5 6 7 8 |
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 |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 36.
