Skip to content

Erdős problem 68

Start work

∑n=2∞1n!−1=∑n=2∞∑k=1∞1(n!)k\sum_{n=2}^\infty \frac{1}{n!-1} = \sum_{n=2}^\infty \sum_{k=1}^\infty \frac{1}{(n!)^k}

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

68.lean

Retained formal statement2 of 2

∑n=2∞1n!−1=∑n=2∞∑k=1∞1(n!)k\sum_{n=2}^\infty \frac{1}{n!-1} = \sum_{n=2}^\infty \sum_{k=1}^\infty \frac{1}{(n!)^k}

FormalConjectures/ErdosProblems/68.leanErdos68.sum_factorial_inv_eq_geometric2 linesExact file
have f := fun n k => 1 / ↑(n + 2).factorial ^ (k + 1);∑' (n : ℕ), 1 / (↑(n + 2).factorial - 1) = ∑' (n : ℕ) (k : ℕ), f n k
TextbookStatement only, no proof