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	⊢ Σ 𝑘 ∈ ℕ ( 2 ↑ - ( ! ‘ 𝑘 ) ) ∉ 𝔸

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝑗 ∈ ℕ ↦ ( 2 ↑ - ( ! ‘ 𝑗 ) ) ) = ( 𝑗 ∈ ℕ ↦ ( 2 ↑ - ( ! ‘ 𝑗 ) ) )
2		fveq2	⊢ ( 𝑘 = 𝑖 → ( ! ‘ 𝑘 ) = ( ! ‘ 𝑖 ) )
3	2	negeqd	⊢ ( 𝑘 = 𝑖 → - ( ! ‘ 𝑘 ) = - ( ! ‘ 𝑖 ) )
4	3	oveq2d	⊢ ( 𝑘 = 𝑖 → ( 2 ↑ - ( ! ‘ 𝑘 ) ) = ( 2 ↑ - ( ! ‘ 𝑖 ) ) )
5	4	cbvsumv	⊢ Σ 𝑘 ∈ ℕ ( 2 ↑ - ( ! ‘ 𝑘 ) ) = Σ 𝑖 ∈ ℕ ( 2 ↑ - ( ! ‘ 𝑖 ) )
6		fveq2	⊢ ( 𝑗 = 𝑖 → ( ! ‘ 𝑗 ) = ( ! ‘ 𝑖 ) )
7	6	negeqd	⊢ ( 𝑗 = 𝑖 → - ( ! ‘ 𝑗 ) = - ( ! ‘ 𝑖 ) )
8	7	oveq2d	⊢ ( 𝑗 = 𝑖 → ( 2 ↑ - ( ! ‘ 𝑗 ) ) = ( 2 ↑ - ( ! ‘ 𝑖 ) ) )
9		ovex	⊢ ( 2 ↑ - ( ! ‘ 𝑖 ) ) ∈ V
10	8 1 9	fvmpt	⊢ ( 𝑖 ∈ ℕ → ( ( 𝑗 ∈ ℕ ↦ ( 2 ↑ - ( ! ‘ 𝑗 ) ) ) ‘ 𝑖 ) = ( 2 ↑ - ( ! ‘ 𝑖 ) ) )
11	10	eqcomd	⊢ ( 𝑖 ∈ ℕ → ( 2 ↑ - ( ! ‘ 𝑖 ) ) = ( ( 𝑗 ∈ ℕ ↦ ( 2 ↑ - ( ! ‘ 𝑗 ) ) ) ‘ 𝑖 ) )
12	11	sumeq2i	⊢ Σ 𝑖 ∈ ℕ ( 2 ↑ - ( ! ‘ 𝑖 ) ) = Σ 𝑖 ∈ ℕ ( ( 𝑗 ∈ ℕ ↦ ( 2 ↑ - ( ! ‘ 𝑗 ) ) ) ‘ 𝑖 )
13	5 12	eqtri	⊢ Σ 𝑘 ∈ ℕ ( 2 ↑ - ( ! ‘ 𝑘 ) ) = Σ 𝑖 ∈ ℕ ( ( 𝑗 ∈ ℕ ↦ ( 2 ↑ - ( ! ‘ 𝑗 ) ) ) ‘ 𝑖 )
14		eqid	⊢ ( 𝑙 ∈ ℕ ↦ Σ 𝑖 ∈ ( 1 ... 𝑙 ) ( ( 𝑗 ∈ ℕ ↦ ( 2 ↑ - ( ! ‘ 𝑗 ) ) ) ‘ 𝑖 ) ) = ( 𝑙 ∈ ℕ ↦ Σ 𝑖 ∈ ( 1 ... 𝑙 ) ( ( 𝑗 ∈ ℕ ↦ ( 2 ↑ - ( ! ‘ 𝑗 ) ) ) ‘ 𝑖 ) )
15	1 13 14	aaliou3lem9	⊢ ¬ Σ 𝑘 ∈ ℕ ( 2 ↑ - ( ! ‘ 𝑘 ) ) ∈ 𝔸
16	15	nelir	⊢ Σ 𝑘 ∈ ℕ ( 2 ↑ - ( ! ‘ 𝑘 ) ) ∉ 𝔸