Conjectures associated with A56777

A56777 lists composite numbers $n$ satisfying both $\varphi(n+12) = \varphi(n) + 12$ and $\sigma(n+12) = \sigma(n) + 12$.

The conjectures state identities connecting A56777 and prime quadruples (A7530), as well as congruences satisfied by the members of A56777.

References: A56777

def OeisA56777.a (n : ℕ) : Prop

A composite number $n$ is in the sequence A56777 if it satisfies both $\varphi(n+12) = \varphi(n) + 12$ and $\sigma(n+12) = \sigma(n) + 12$.

Equations

• OeisA56777.a n = (¬Nat.Prime n ∧ 1 < n ∧ (n + 12).totient = n.totient + 12 ∧ (ArithmeticFunction.sigma 1) (n + 12) = (ArithmeticFunction.sigma 1) n + 12)

def OeisA56777.ComesFromPrimeQuadruple (n : ℕ) : Prop

A number $n$ comes from a prime quadruple $(p, p+2, p+6, p+8)$ if $n = p(p+8)$ for some prime $p$ where $p$, $p+2$, $p+6$, $p+8$ are all prime.

Equations

• OeisA56777.ComesFromPrimeQuadruple n = ∃ (p : ℕ), Nat.Prime p ∧ Nat.Prime (p + 2) ∧ Nat.Prime (p + 6) ∧ Nat.Prime (p + 8) ∧ n = p * (p + 8)

theorem OeisA56777.a_65 : a 65

$65$ is in the sequence A56777.

theorem OeisA56777.a_209 : a 209

$209$ is in the sequence A56777.

theorem OeisA56777.a_of_comesFromPrimeQuadruple {n : ℕ} (h : ComesFromPrimeQuadruple n) : a n

Numbers coming from prime quadruples are in the sequence A56777.

theorem OeisA56777.comesFromPrimeQuadruple_of_a {n : ℕ} (h : a n) : ComesFromPrimeQuadruple n

All members of the sequence A56777 come from prime quadruples.

theorem OeisA56777.mod_72_of_comesFromPrimeQuadruple {n : ℕ} (h : ComesFromPrimeQuadruple n) : n % 72 = 65

Numbers coming from prime quadruples satisfy $n \equiv 65 \pmod{72}$.

theorem OeisA56777.mod_100_of_comesFromPrimeQuadruple {n : ℕ} (h : ComesFromPrimeQuadruple n) : n % 100 = 9

Numbers coming from prime quadruples satisfy $n \equiv 9 \pmod{100}$.