minFacHelper_1

Mathlib.Tactic.NormNum.Prime

URI: https://scilib.ai/kg/mathlib#Mathlib.Meta.NormNum.minFacHelper_1

Lean4

theorem minFacHelper_1 {n k k' : ℕ} (e : k + 2 = k') (h : MinFacHelper n k) (np : minFac n ≠ k) : MinFacHelper n k' :=
  by
  rw [← e]
  refine ⟨Nat.lt_add_right _ h.1, ?_, ?_⟩
  · rw [add_mod, mod_self, add_zero, mod_mod]
    exact h.2.1
  rcases h.2.2.eq_or_lt with rfl | h2
  · exact (np rfl).elim
  rcases (succ_le_of_lt h2).eq_or_lt with h2 | h2
  · refine ((h.1.trans_le h.2.2).ne ?_).elim
    have h3 : 2 ∣ minFac n := by rw [Nat.dvd_iff_mod_eq_zero, ← h2, succ_eq_add_one, add_mod, h.2.1]
    rw [dvd_prime <| minFac_prime h.one_lt.ne'] at h3
    norm_num at h3
    exact h3
  exact h2

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

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

Разделы

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

Аффилиация

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