Documentation

Projects.Misc.P002.P1

def Misc.P002.P1.Cnd₁ (n : ℕ) :

Equations

Misc.P002.P1.Cnd₁ n = (Nat.digsNum 10 n = 2 ∧ Nat.Prime n ∧ Nat.Prime (Nat.digRev 10 n))

Instances For

noncomputable def Misc.P002.P1.set₁ :

Equations

Misc.P002.P1.set₁ = Set'.ofSet (Set.ofPred Misc.P002.P1.Cnd₁)

Instances For

@[instance_reducible]

instance Misc.P002.P1.instDecidablePredNatCnd₁ :

DecidablePred Cnd₁

Equations

Misc.P002.P1.instDecidablePredNatCnd₁ = id inferInstance

def Misc.P002.P1.list₁ :

Equations

Misc.P002.P1.list₁ = List.filter (fun (b : ℕ) => decide (Misc.P002.P1.Cnd₁ b)) (List.range 100)

Instances For

theorem Misc.P002.P1.ofPred_cnd₁_subset {n : ℕ} (h : n ∈ Set.ofPred Cnd₁) :

n ∈ Finset.range 100

@[simp]

theorem Misc.P002.P1.ofPred_cnd₁ :

(Set.ofPred Cnd₁).Finite

@[simp]

theorem Misc.P002.P1.sortedLT_list₁ :

list₁.SortedLT

theorem Misc.P002.P1.toList_set'_ofList_list₁ :

(Set'.ofList list₁).toList = list₁

@[simp]

theorem Misc.P002.P1.mem_list₁_iff_cnd₁ {n : ℕ} :

n ∈ list₁ ↔ Cnd₁ n

@[simp]

theorem Misc.P002.P1.toList_set₁ :

set₁.toList = list₁

theorem Misc.P002.P1.filter_prime_icc_10_30 :

List.filter (fun (b : ℕ) => decide (Nat.Prime b)) (List.icc 10 30) = [11, 13, 17, 19, 23, 29]

theorem Misc.P002.P1.filter_prime_icc_31_60 :

List.filter (fun (b : ℕ) => decide (Nat.Prime b)) (List.icc 31 60) = [31, 37, 41, 43, 47, 53, 59]

theorem Misc.P002.P1.filter_prime_icc_61_99 :

List.filter (fun (b : ℕ) => decide (Nat.Prime b)) (List.icc 61 99) = [61, 67, 71, 73, 79, 83, 89, 97]

theorem Misc.P002.P1.filter_prime_icc_10_99 :

List.filter (fun (b : ℕ) => decide (Nat.Prime b)) (List.icc 10 99) = [11, 13, 17, 19, 23, 29, 31, 37, 41, 43, 47, 53, 59, 61, 67, 71, 73, 79, 83, 89, 97]

theorem Misc.P002.P1.list₁_eq_aux₁ :

list₁ = List.filter (fun (n : ℕ) => decide (Nat.Prime (Nat.digRev 10 n))) (List.filter (fun (b : ℕ) => decide (Nat.Prime b)) (List.icc 10 99))

theorem Misc.P002.P1.list₁_eq_aux₂ :

list₁ = List.filter (fun (n : ℕ) => decide (Nat.Prime (Nat.digRev 10 n))) [11, 13, 17, 19, 31, 37, 71, 73, 79, 97]

theorem Misc.P002.P1.list₁_eq_aux₃ :

list₁ = List.filter (fun (n : ℕ) => decide (Nat.Prime (n % 10 * 10 + n / 10))) [11, 13, 17, 19, 31, 37, 71, 73, 79, 97]

theorem Misc.P002.P1.list₁_eq :

list₁ = [11, 13, 17, 31, 37, 71, 73, 79, 97]

@[simp]

theorem Misc.P002.P1.length_list₁ :

list₁.length = 9

@[simp]

theorem Misc.P002.P1.size_set₁ :

set₁.size = 9