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 k2k!𝔸

Proof

Step Hyp Ref Expression
1 eqid j2j!=j2j!
2 fveq2 k=ik!=i!
3 2 negeqd k=ik!=i!
4 3 oveq2d k=i2k!=2i!
5 4 cbvsumv k2k!=i2i!
6 fveq2 j=ij!=i!
7 6 negeqd j=ij!=i!
8 7 oveq2d j=i2j!=2i!
9 ovex 2i!V
10 8 1 9 fvmpt ij2j!i=2i!
11 10 eqcomd i2i!=j2j!i
12 11 sumeq2i i2i!=ij2j!i
13 5 12 eqtri k2k!=ij2j!i
14 eqid li=1lj2j!i=li=1lj2j!i
15 1 13 14 aaliou3lem9 ¬k2k!𝔸
16 15 nelir k2k!𝔸