five_le_of_ne_two_of_ne_three

Mathlib.Data.Nat.Prime.Basic

URI: https://scilib.ai/kg/mathlib#Nat.Prime.five_le_of_ne_two_of_ne_three

← MathLib Explorer

English

If p is prime and p ≠ 2 and p ≠ 3, then p ≥ 5.

Русский

Если p простое и p не равно 2 и не равно 3, то p ≥ 5.

LaTeX

$$$$ \text{Prime}(p) \land p \neq 2 \land p \neq 3 \Rightarrow 5 \le p. $$$$

Lean4

theorem five_le_of_ne_two_of_ne_three {p : ℕ} (hp : p.Prime) (h_two : p ≠ 2) (h_three : p ≠ 3) : 5 ≤ p :=
  by
  by_contra! h
  revert h_two h_three hp
  decide +revert

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru