no goals
⊢ 0 ≠ 1 ↔ ∃ p, Prime p ∧ p ∣ 0
simpa using Exists.intro 2 Nat.prime_two
no goals
⊢ 1 ≠ 1 ↔ ∃ p, Prime p ∧ p ∣ 1
simp [Nat.not_prime_one]
n : ℕ
a : ℕ := n + 2
⊢ n + 2 ≠ 1 ↔ ∃ p, Prime p ∧ p ∣ n + 2
n : ℕ
⊢ n + 2 ≠ 1 ↔ ∃ p, Prime p ∧ p ∣ n + 2
let a := n + 2
n : ℕ
a : ℕ := n + 2
ha : a ≠ 1 := succ_succ_ne_one n
⊢ n + 2 ≠ 1 ↔ ∃ p, Prime p ∧ p ∣ n + 2
n : ℕ
a : ℕ := n + 2
⊢ n + 2 ≠ 1 ↔ ∃ p, Prime p ∧ p ∣ n + 2
let ha : a ≠ 1 := Nat.succ_succ_ne_one n
n : ℕ
a : ℕ := n + 2
ha : a ≠ 1 := succ_succ_ne_one n
⊢ ∃ p, Prime p ∧ p ∣ n + 2
n : ℕ
a : ℕ := n + 2
ha : a ≠ 1 := succ_succ_ne_one n
⊢ n + 2 ≠ 1 ↔ ∃ p, Prime p ∧ p ∣ n + 2
simp only [true_iff_iff, Ne.def, not_false_iff, ha]
no goals
n : ℕ
a : ℕ := n + 2
ha : a ≠ 1 := succ_succ_ne_one n
⊢ ∃ p, Prime p ∧ p ∣ n + 2
exact ⟨a.minFac, Nat.minFac_prime ha, a.minFac_dvd⟩