Metamath Proof Explorer

Theorem aaliou3lem9

Description: Example of a "Liouville number", a very simple definable transcendental real. (Contributed by Stefan O'Rear, 20-Nov-2014)

Ref Expression
Hypotheses aaliou3lem.c ⊢F=a∈ℕ⟼2−a!
aaliou3lem.d ⊢L=∑b∈ℕF⁡b
aaliou3lem.e ⊢H=c∈ℕ⟼∑b=1cF⁡b
Assertion aaliou3lem9 ⊢¬L∈𝔸

Proof

Step Hyp Ref Expression
1 aaliou3lem.c ⊢F=a∈ℕ⟼2−a!
2 aaliou3lem.d ⊢L=∑b∈ℕF⁡b
3 aaliou3lem.e ⊢H=c∈ℕ⟼∑b=1cF⁡b
4 aaliou3lem8 ⊢a∈ℕ∧b∈ℝ+→∃e∈ℕ2⁢2−e+1!≤b2e!a
5 1 2 3 aaliou3lem6 ⊢e∈ℕ→H⁡e⁢2e!∈ℤ
6 5 ad2antrl ⊢a∈ℕ∧b∈ℝ+∧e∈ℕ∧2⁢2−e+1!≤b2e!a→H⁡e⁢2e!∈ℤ
7 2nn ⊢2∈ℕ
8 nnnn0 ⊢e∈ℕ→e∈ℕ0
9 8 ad2antrl ⊢a∈ℕ∧b∈ℝ+∧e∈ℕ∧2⁢2−e+1!≤b2e!a→e∈ℕ0
10 faccl ⊢e∈ℕ0→e!∈ℕ
11 nnnn0 ⊢e!∈ℕ→e!∈ℕ0
12 9 10 11 3syl ⊢a∈ℕ∧b∈ℝ+∧e∈ℕ∧2⁢2−e+1!≤b2e!a→e!∈ℕ0
13 nnexpcl ⊢2∈ℕ∧e!∈ℕ0→2e!∈ℕ
14 7 12 13 sylancr ⊢a∈ℕ∧b∈ℝ+∧e∈ℕ∧2⁢2−e+1!≤b2e!a→2e!∈ℕ
15 1 2 3 aaliou3lem5 ⊢e∈ℕ→H⁡e∈ℝ
16 15 ad2antrl ⊢a∈ℕ∧b∈ℝ+∧e∈ℕ∧2⁢2−e+1!≤b2e!a→H⁡e∈ℝ
17 16 recnd ⊢a∈ℕ∧b∈ℝ+∧e∈ℕ∧2⁢2−e+1!≤b2e!a→H⁡e∈ℂ
18 14 nncnd ⊢a∈ℕ∧b∈ℝ+∧e∈ℕ∧2⁢2−e+1!≤b2e!a→2e!∈ℂ
19 14 nnne0d ⊢a∈ℕ∧b∈ℝ+∧e∈ℕ∧2⁢2−e+1!≤b2e!a→2e!≠0
20 17 18 19 divcan4d ⊢a∈ℕ∧b∈ℝ+∧e∈ℕ∧2⁢2−e+1!≤b2e!a→H⁡e⁢2e!2e!=H⁡e
21 1 2 3 aaliou3lem7 ⊢e∈ℕ→H⁡e≠L∧L−H⁡e≤2⁢2−e+1!
22 21 simpld ⊢e∈ℕ→H⁡e≠L
23 22 ad2antrl ⊢a∈ℕ∧b∈ℝ+∧e∈ℕ∧2⁢2−e+1!≤b2e!a→H⁡e≠L
24 20 23 eqnetrd ⊢a∈ℕ∧b∈ℝ+∧e∈ℕ∧2⁢2−e+1!≤b2e!a→H⁡e⁢2e!2e!≠L
25 24 necomd ⊢a∈ℕ∧b∈ℝ+∧e∈ℕ∧2⁢2−e+1!≤b2e!a→L≠H⁡e⁢2e!2e!
26 25 neneqd ⊢a∈ℕ∧b∈ℝ+∧e∈ℕ∧2⁢2−e+1!≤b2e!a→¬L=H⁡e⁢2e!2e!
27 1 2 3 aaliou3lem4 ⊢L∈ℝ
28 14 nnred ⊢a∈ℕ∧b∈ℝ+∧e∈ℕ∧2⁢2−e+1!≤b2e!a→2e!∈ℝ
29 16 28 remulcld ⊢a∈ℕ∧b∈ℝ+∧e∈ℕ∧2⁢2−e+1!≤b2e!a→H⁡e⁢2e!∈ℝ
30 29 14 nndivred ⊢a∈ℕ∧b∈ℝ+∧e∈ℕ∧2⁢2−e+1!≤b2e!a→H⁡e⁢2e!2e!∈ℝ
31 resubcl ⊢L∈ℝ∧H⁡e⁢2e!2e!∈ℝ→L−H⁡e⁢2e!2e!∈ℝ
32 27 30 31 sylancr ⊢a∈ℕ∧b∈ℝ+∧e∈ℕ∧2⁢2−e+1!≤b2e!a→L−H⁡e⁢2e!2e!∈ℝ
33 32 recnd ⊢a∈ℕ∧b∈ℝ+∧e∈ℕ∧2⁢2−e+1!≤b2e!a→L−H⁡e⁢2e!2e!∈ℂ
34 33 abscld ⊢a∈ℕ∧b∈ℝ+∧e∈ℕ∧2⁢2−e+1!≤b2e!a→L−H⁡e⁢2e!2e!∈ℝ
35 simplr ⊢a∈ℕ∧b∈ℝ+∧e∈ℕ∧2⁢2−e+1!≤b2e!a→b∈ℝ+
36 nnnn0 ⊢a∈ℕ→a∈ℕ0
37 36 ad2antrr ⊢a∈ℕ∧b∈ℝ+∧e∈ℕ∧2⁢2−e+1!≤b2e!a→a∈ℕ0
38 14 37 nnexpcld ⊢a∈ℕ∧b∈ℝ+∧e∈ℕ∧2⁢2−e+1!≤b2e!a→2e!a∈ℕ
39 38 nnrpd ⊢a∈ℕ∧b∈ℝ+∧e∈ℕ∧2⁢2−e+1!≤b2e!a→2e!a∈ℝ+
40 35 39 rpdivcld ⊢a∈ℕ∧b∈ℝ+∧e∈ℕ∧2⁢2−e+1!≤b2e!a→b2e!a∈ℝ+
41 40 rpred ⊢a∈ℕ∧b∈ℝ+∧e∈ℕ∧2⁢2−e+1!≤b2e!a→b2e!a∈ℝ
42 2rp ⊢2∈ℝ+
43 peano2nn0 ⊢e∈ℕ0→e+1∈ℕ0
44 faccl ⊢e+1∈ℕ0→e+1!∈ℕ
45 9 43 44 3syl ⊢a∈ℕ∧b∈ℝ+∧e∈ℕ∧2⁢2−e+1!≤b2e!a→e+1!∈ℕ
46 nnz ⊢e+1!∈ℕ→e+1!∈ℤ
47 znegcl ⊢e+1!∈ℤ→−e+1!∈ℤ
48 45 46 47 3syl ⊢a∈ℕ∧b∈ℝ+∧e∈ℕ∧2⁢2−e+1!≤b2e!a→−e+1!∈ℤ
49 rpexpcl ⊢2∈ℝ+∧−e+1!∈ℤ→2−e+1!∈ℝ+
50 42 48 49 sylancr ⊢a∈ℕ∧b∈ℝ+∧e∈ℕ∧2⁢2−e+1!≤b2e!a→2−e+1!∈ℝ+
51 rpmulcl ⊢2∈ℝ+∧2−e+1!∈ℝ+→2⁢2−e+1!∈ℝ+
52 42 50 51 sylancr ⊢a∈ℕ∧b∈ℝ+∧e∈ℕ∧2⁢2−e+1!≤b2e!a→2⁢2−e+1!∈ℝ+
53 52 rpred ⊢a∈ℕ∧b∈ℝ+∧e∈ℕ∧2⁢2−e+1!≤b2e!a→2⁢2−e+1!∈ℝ
54 20 oveq2d ⊢a∈ℕ∧b∈ℝ+∧e∈ℕ∧2⁢2−e+1!≤b2e!a→L−H⁡e⁢2e!2e!=L−H⁡e
55 54 fveq2d ⊢a∈ℕ∧b∈ℝ+∧e∈ℕ∧2⁢2−e+1!≤b2e!a→L−H⁡e⁢2e!2e!=L−H⁡e
56 21 simprd ⊢e∈ℕ→L−H⁡e≤2⁢2−e+1!
57 56 ad2antrl ⊢a∈ℕ∧b∈ℝ+∧e∈ℕ∧2⁢2−e+1!≤b2e!a→L−H⁡e≤2⁢2−e+1!
58 55 57 eqbrtrd ⊢a∈ℕ∧b∈ℝ+∧e∈ℕ∧2⁢2−e+1!≤b2e!a→L−H⁡e⁢2e!2e!≤2⁢2−e+1!
59 simprr ⊢a∈ℕ∧b∈ℝ+∧e∈ℕ∧2⁢2−e+1!≤b2e!a→2⁢2−e+1!≤b2e!a
60 34 53 41 58 59 letrd ⊢a∈ℕ∧b∈ℝ+∧e∈ℕ∧2⁢2−e+1!≤b2e!a→L−H⁡e⁢2e!2e!≤b2e!a
61 34 41 60 lensymd ⊢a∈ℕ∧b∈ℝ+∧e∈ℕ∧2⁢2−e+1!≤b2e!a→¬b2e!a<L−H⁡e⁢2e!2e!
62 oveq1 ⊢f=H⁡e⁢2e!→fd=H⁡e⁢2e!d
63 62 eqeq2d ⊢f=H⁡e⁢2e!→L=fd↔L=H⁡e⁢2e!d
64 63 notbid ⊢f=H⁡e⁢2e!→¬L=fd↔¬L=H⁡e⁢2e!d
65 62 oveq2d ⊢f=H⁡e⁢2e!→L−fd=L−H⁡e⁢2e!d
66 65 fveq2d ⊢f=H⁡e⁢2e!→L−fd=L−H⁡e⁢2e!d
67 66 breq2d ⊢f=H⁡e⁢2e!→bda<L−fd↔bda<L−H⁡e⁢2e!d
68 67 notbid ⊢f=H⁡e⁢2e!→¬bda<L−fd↔¬bda<L−H⁡e⁢2e!d
69 64 68 anbi12d ⊢f=H⁡e⁢2e!→¬L=fd∧¬bda<L−fd↔¬L=H⁡e⁢2e!d∧¬bda<L−H⁡e⁢2e!d
70 oveq2 ⊢d=2e!→H⁡e⁢2e!d=H⁡e⁢2e!2e!
71 70 eqeq2d ⊢d=2e!→L=H⁡e⁢2e!d↔L=H⁡e⁢2e!2e!
72 71 notbid ⊢d=2e!→¬L=H⁡e⁢2e!d↔¬L=H⁡e⁢2e!2e!
73 oveq1 ⊢d=2e!→da=2e!a
74 73 oveq2d ⊢d=2e!→bda=b2e!a
75 70 oveq2d ⊢d=2e!→L−H⁡e⁢2e!d=L−H⁡e⁢2e!2e!
76 75 fveq2d ⊢d=2e!→L−H⁡e⁢2e!d=L−H⁡e⁢2e!2e!
77 74 76 breq12d ⊢d=2e!→bda<L−H⁡e⁢2e!d↔b2e!a<L−H⁡e⁢2e!2e!
78 77 notbid ⊢d=2e!→¬bda<L−H⁡e⁢2e!d↔¬b2e!a<L−H⁡e⁢2e!2e!
79 72 78 anbi12d ⊢d=2e!→¬L=H⁡e⁢2e!d∧¬bda<L−H⁡e⁢2e!d↔¬L=H⁡e⁢2e!2e!∧¬b2e!a<L−H⁡e⁢2e!2e!
80 69 79 rspc2ev ⊢H⁡e⁢2e!∈ℤ∧2e!∈ℕ∧¬L=H⁡e⁢2e!2e!∧¬b2e!a<L−H⁡e⁢2e!2e!→∃f∈ℤ∃d∈ℕ¬L=fd∧¬bda<L−fd
81 6 14 26 61 80 syl112anc ⊢a∈ℕ∧b∈ℝ+∧e∈ℕ∧2⁢2−e+1!≤b2e!a→∃f∈ℤ∃d∈ℕ¬L=fd∧¬bda<L−fd
82 4 81 rexlimddv ⊢a∈ℕ∧b∈ℝ+→∃f∈ℤ∃d∈ℕ¬L=fd∧¬bda<L−fd
83 pm4.56 ⊢¬L=fd∧¬bda<L−fd↔¬L=fd∨bda<L−fd
84 83 rexbii ⊢∃d∈ℕ¬L=fd∧¬bda<L−fd↔∃d∈ℕ¬L=fd∨bda<L−fd
85 rexnal ⊢∃d∈ℕ¬L=fd∨bda<L−fd↔¬∀d∈ℕL=fd∨bda<L−fd
86 84 85 bitri ⊢∃d∈ℕ¬L=fd∧¬bda<L−fd↔¬∀d∈ℕL=fd∨bda<L−fd
87 86 rexbii ⊢∃f∈ℤ∃d∈ℕ¬L=fd∧¬bda<L−fd↔∃f∈ℤ¬∀d∈ℕL=fd∨bda<L−fd
88 rexnal ⊢∃f∈ℤ¬∀d∈ℕL=fd∨bda<L−fd↔¬∀f∈ℤ∀d∈ℕL=fd∨bda<L−fd
89 87 88 bitri ⊢∃f∈ℤ∃d∈ℕ¬L=fd∧¬bda<L−fd↔¬∀f∈ℤ∀d∈ℕL=fd∨bda<L−fd
90 82 89 sylib ⊢a∈ℕ∧b∈ℝ+→¬∀f∈ℤ∀d∈ℕL=fd∨bda<L−fd
91 90 nrexdv ⊢a∈ℕ→¬∃b∈ℝ+∀f∈ℤ∀d∈ℕL=fd∨bda<L−fd
92 91 nrex ⊢¬∃a∈ℕ∃b∈ℝ+∀f∈ℤ∀d∈ℕL=fd∨bda<L−fd
93 aaliou2b ⊢L∈𝔸→∃a∈ℕ∃b∈ℝ+∀f∈ℤ∀d∈ℕL=fd∨bda<L−fd
94 92 93 mto ⊢¬L∈𝔸