Metamath Proof Explorer

Theorem aaliou3

Description: Example of a "Liouville number", a very simple definable transcendental real. (Contributed by Stefan O'Rear, 23-Nov-2014)

Ref Expression
Assertion aaliou3 ⊢ ∑ 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 aaliou3lem9 ⊢ ¬ ∑ k ∈ ℕ 2 − k ! ∈ 𝔸
16 15 nelir ⊢ ∑ k ∈ ℕ 2 − k ! ∉ 𝔸