prime_of_aleph0_le — Mathlib

English

If aleph_0 ≤ a, then a is prime.

Русский

Если aleph_0 ≤ a, то a простое.

LaTeX

$$$\aleph_0 \le a \Rightarrow \mathrm{Prime}(a)$$$

Lean4

@[simp]
theorem prime_of_aleph0_le (ha : ℵ₀ ≤ a) : Prime a :=
  by
  refine ⟨(aleph0_pos.trans_le ha).ne', ?_, fun b c hbc => ?_⟩
  · rw [isUnit_iff]
    exact (one_lt_aleph0.trans_le ha).ne'
  rcases eq_or_ne (b * c) 0 with hz | hz
  · rcases mul_eq_zero.mp hz with (rfl | rfl) <;> simp
  wlog h : c ≤ b
  · cases le_total c b <;> [solve_by_elim; rw [or_comm]]
    apply_assumption
    assumption'
    all_goals rwa [mul_comm]
  left
  have habc := le_of_dvd hz hbc
  rwa [mul_eq_max' <| ha.trans <| habc, max_def', if_pos h] at hbc

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