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

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 aaliou3lem9 
 |-  -. sum_ k e. NN ( 2 ^ -u ( ! ` k ) ) e. AA
16 15 nelir 
 |-  sum_ k e. NN ( 2 ^ -u ( ! ` k ) ) e/ AA