def Misc.P002.P2.CndX (n : ℕ) : Prop

Equations

• Misc.P002.P2.CndX n = (Nat.Prime n ∧ ∃ (a : ℕ) (b : ℕ), Nat.Prime a ∧ Nat.Prime b ∧ n = a + b ∧ ↑n = ↑a - ↑b)

def Misc.P002.P2.Cnd₁ (n : ℕ) : Prop

Equations

• Misc.P002.P2.Cnd₁ n = (Nat.Prime n ∧ (∃ (a : ℕ) (b : ℕ), Nat.Prime a ∧ Nat.Prime b ∧ n = a + b) ∧ ∃ (a : ℕ) (b : ℕ), Nat.Prime a ∧ Nat.Prime b ∧ ↑n = ↑a - ↑b)

def Misc.P002.P2.setX : Set ℕ

Equations

• Misc.P002.P2.setX = Set.ofPred Misc.P002.P2.CndX

def Misc.P002.P2.set₁ : Set ℕ

Equations

• Misc.P002.P2.set₁ = Set.ofPred Misc.P002.P2.Cnd₁

noncomputable def Misc.P002.P2.n₁ : ℕ

Equations

• Misc.P002.P2.n₁ = Classical.epsilon fun (n : ℕ) => Misc.P002.P2.Cnd₁ n

theorem Misc.P002.P2.cnd₁_of_cndX {n : ℕ} (h : CndX n) : Cnd₁ n

@[simp]

theorem Misc.P002.P2.setX_eq : setX = ∅

@[simp]

theorem Misc.P002.P2.set₁_eq : set₁ = {5}

@[simp]

theorem Misc.P002.P2.n₁_eq : n₁ = 5