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	|- sum_ k e. NN ( 2 ^ -u ( ! ` k ) ) e. RR

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( j e. NN |-> ( 2 ^ -u ( ! ` j ) ) ) = ( j e. NN |-> ( 2 ^ -u ( ! ` j ) ) )
2		fveq2	|- ( k = i -> ( ! ` k ) = ( ! ` i ) )
3	2	negeqd	|- ( k = i -> -u ( ! ` k ) = -u ( ! ` i ) )
4	3	oveq2d	|- ( k = i -> ( 2 ^ -u ( ! ` k ) ) = ( 2 ^ -u ( ! ` i ) ) )
5	4	cbvsumv	|- sum_ k e. NN ( 2 ^ -u ( ! ` k ) ) = sum_ i e. NN ( 2 ^ -u ( ! ` i ) )
6		fveq2	|- ( j = i -> ( ! ` j ) = ( ! ` i ) )
7	6	negeqd	|- ( j = i -> -u ( ! ` j ) = -u ( ! ` i ) )
8	7	oveq2d	|- ( j = i -> ( 2 ^ -u ( ! ` j ) ) = ( 2 ^ -u ( ! ` i ) ) )
9		ovex	|- ( 2 ^ -u ( ! ` i ) ) e. _V
10	8 1 9	fvmpt	|- ( i e. NN -> ( ( j e. NN |-> ( 2 ^ -u ( ! ` j ) ) ) ` i ) = ( 2 ^ -u ( ! ` i ) ) )
11	10	eqcomd	|- ( i e. NN -> ( 2 ^ -u ( ! ` i ) ) = ( ( j e. NN |-> ( 2 ^ -u ( ! ` j ) ) ) ` i ) )
12	11	sumeq2i	|- sum_ i e. NN ( 2 ^ -u ( ! ` i ) ) = sum_ i e. NN ( ( j e. NN |-> ( 2 ^ -u ( ! ` j ) ) ) ` i )
13	5 12	eqtri	|- sum_ k e. NN ( 2 ^ -u ( ! ` k ) ) = sum_ i e. NN ( ( j e. NN |-> ( 2 ^ -u ( ! ` j ) ) ) ` i )
14		eqid	|- ( l e. NN |-> sum_ i e. ( 1 ... l ) ( ( j e. NN |-> ( 2 ^ -u ( ! ` j ) ) ) ` i ) ) = ( l e. NN |-> sum_ i e. ( 1 ... l ) ( ( j e. NN |-> ( 2 ^ -u ( ! ` j ) ) ) ` i ) )
15	1 13 14	aaliou3lem4	|- sum_ k e. NN ( 2 ^ -u ( ! ` k ) ) e. RR