Metamath Proof Explorer

Theorem aaliou3r

Description: The sum presented above is convergent, which means that the "Liouville number" is indeed real. (Contributed by Ender Ting, 21-Jul-2026)

Ref Expression
Assertion aaliou3r ⊢ ∑ k ∈ ℕ 2 − k ! ∈ ℝ

Proof

Step Hyp Ref Expression
1 eqid ⊢ j ∈ ℕ ⟼ 2 − j ! = j ∈ ℕ ⟼ 2 − j !
2 fveq2 ⊢ k = i → k ! = i !
3 2 negeqd ⊢ k = i → − k ! = − i !
4 3 oveq2d ⊢ k = i → 2 − k ! = 2 − i !
5 4 cbvsumv ⊢ ∑ k ∈ ℕ 2 − k ! = ∑ i ∈ ℕ 2 − i !
6 fveq2 ⊢ j = i → j ! = i !
7 6 negeqd ⊢ j = i → − j ! = − i !
8 7 oveq2d ⊢ j = i → 2 − j ! = 2 − i !
9 ovex ⊢ 2 − i ! ∈ V
10 8 1 9 fvmpt ⊢ i ∈ ℕ → j ∈ ℕ ⟼ 2 − j ! ⁡ i = 2 − i !
11 10 eqcomd ⊢ i ∈ ℕ → 2 − i ! = j ∈ ℕ ⟼ 2 − j ! ⁡ i
12 11 sumeq2i ⊢ ∑ i ∈ ℕ 2 − i ! = ∑ i ∈ ℕ j ∈ ℕ ⟼ 2 − j ! ⁡ i
13 5 12 eqtri ⊢ ∑ k ∈ ℕ 2 − k ! = ∑ i ∈ ℕ j ∈ ℕ ⟼ 2 − j ! ⁡ i
14 eqid ⊢ l ∈ ℕ ⟼ ∑ i = 1 l j ∈ ℕ ⟼ 2 − j ! ⁡ i = l ∈ ℕ ⟼ ∑ i = 1 l j ∈ ℕ ⟼ 2 − j ! ⁡ i
15 1 13 14 aaliou3lem4 ⊢ ∑ k ∈ ℕ 2 − k ! ∈ ℝ