English
The minimal p found is a prime number.
Русский
Минимальное найденное число p является простым.
LaTeX
$$p \\text{ is prime}$$
Lean4
/-- The minimal positive integer with absolute value smaller than 1 is a prime number. -/
theorem is_prime_of_minimal_nat_zero_lt_and_lt_one : p.Prime :=
by
rw [← Nat.irreducible_iff_nat_prime]
constructor -- Two goals: p is not a unit and any product giving p must contain a unit.
· rw [Nat.isUnit_iff]
rintro rfl
simp only [Nat.cast_one, map_one, lt_self_iff_false] at hp1
· rintro a b rfl
rw [Nat.isUnit_iff, Nat.isUnit_iff]
by_contra! con
obtain ⟨ha₁, hb₁⟩ := con
obtain ⟨ha₀, hb₀⟩ : a ≠ 0 ∧ b ≠ 0 := by
refine mul_ne_zero_iff.mp fun h ↦ ?_
rwa [h, Nat.cast_zero, map_zero, lt_self_iff_false] at hp0
have hap : a < a * b := lt_mul_of_one_lt_right (by cutsat) (by cutsat)
have hbp : b < a * b := lt_mul_of_one_lt_left (by cutsat) (by cutsat)
have ha := le_of_not_gt <| not_and.mp ((hmin a).mt hap.not_ge) (map_pos_of_ne_zero f (mod_cast ha₀))
have hb := le_of_not_gt <| not_and.mp ((hmin b).mt hbp.not_ge) (map_pos_of_ne_zero f (mod_cast hb₀))
rw [Nat.cast_mul, map_mul] at hp1
exact ((one_le_mul_of_one_le_of_one_le ha hb).trans_lt hp1).false
