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	$$⊢\sum _{k\in \mathbb{N}}{2}^{-k!}\notin 𝔸$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\left(j\in \mathbb{N}⟼2^{-j!}\right)=\left(j\in \mathbb{N}⟼2^{-j!}\right)$$
2		fveq2	$$⊢k=i\to k!=i!$$
3	2	negeqd	$$⊢k=i\to -k!=-i!$$
4	3	oveq2d	$$⊢k=i\to 2^{-k!}=2^{-i!}$$
5	4	cbvsumv	$$⊢\sum _{k\in \mathbb{N}}{2}^{-k!}=\sum _{i\in \mathbb{N}}{2}^{-i!}$$
6		fveq2	$$⊢j=i\to j!=i!$$
7	6	negeqd	$$⊢j=i\to -j!=-i!$$
8	7	oveq2d	$$⊢j=i\to 2^{-j!}=2^{-i!}$$
9		ovex	$$⊢2^{-i!}\in \mathrm{V}$$
10	8 1 9	fvmpt	$$⊢i\in \mathbb{N}\to \left(j\in \mathbb{N}⟼2^{-j!}\right)\left(i\right)=2^{-i!}$$
11	10	eqcomd	$$⊢i\in \mathbb{N}\to 2^{-i!}=\left(j\in \mathbb{N}⟼2^{-j!}\right)\left(i\right)$$
12	11	sumeq2i	$$⊢\sum _{i\in \mathbb{N}}{2}^{-i!}=\sum _{i\in \mathbb{N}}\left(j\in \mathbb{N}⟼2^{-j!}\right)\left(i\right)$$
13	5 12	eqtri	$$⊢\sum _{k\in \mathbb{N}}{2}^{-k!}=\sum _{i\in \mathbb{N}}\left(j\in \mathbb{N}⟼2^{-j!}\right)\left(i\right)$$
14		eqid	$$⊢\left(l\in \mathbb{N}⟼\sum _{i=1}^l\left(j\in \mathbb{N}⟼2^{-j!}\right)\left(i\right)\right)=\left(l\in \mathbb{N}⟼\sum _{i=1}^l\left(j\in \mathbb{N}⟼2^{-j!}\right)\left(i\right)\right)$$
15	1 13 14	aaliou3lem9	$$⊢\neg \sum _{k\in \mathbb{N}}{2}^{-k!}\in 𝔸$$
16	15	nelir	$$⊢\sum _{k\in \mathbb{N}}{2}^{-k!}\notin 𝔸$$