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 e. NN |-> ( 2 ^ -u ( ! ` a ) ) )
aaliou3lem.d 
|- L = sum_ b e. NN ( F ` b )
aaliou3lem.e 
|- H = ( c e. NN |-> sum_ b e. ( 1 ... c ) ( F ` b ) )
Assertion aaliou3lem9 
|- -. L e. AA

Proof

Step Hyp Ref Expression
1 aaliou3lem.c 
 |-  F = ( a e. NN |-> ( 2 ^ -u ( ! ` a ) ) )
2 aaliou3lem.d 
 |-  L = sum_ b e. NN ( F ` b )
3 aaliou3lem.e 
 |-  H = ( c e. NN |-> sum_ b e. ( 1 ... c ) ( F ` b ) )
4 aaliou3lem8 
 |-  ( ( a e. NN /\ b e. RR+ ) -> E. e e. NN ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) <_ ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) )
5 1 2 3 aaliou3lem6 
 |-  ( e e. NN -> ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) e. ZZ )
6 5 ad2antrl 
 |-  ( ( ( a e. NN /\ b e. RR+ ) /\ ( e e. NN /\ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) <_ ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) ) ) -> ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) e. ZZ )
7 2nn 
 |-  2 e. NN
8 nnnn0 
 |-  ( e e. NN -> e e. NN0 )
9 8 ad2antrl 
 |-  ( ( ( a e. NN /\ b e. RR+ ) /\ ( e e. NN /\ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) <_ ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) ) ) -> e e. NN0 )
10 faccl 
 |-  ( e e. NN0 -> ( ! ` e ) e. NN )
11 nnnn0 
 |-  ( ( ! ` e ) e. NN -> ( ! ` e ) e. NN0 )
12 9 10 11 3syl 
 |-  ( ( ( a e. NN /\ b e. RR+ ) /\ ( e e. NN /\ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) <_ ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) ) ) -> ( ! ` e ) e. NN0 )
13 nnexpcl 
 |-  ( ( 2 e. NN /\ ( ! ` e ) e. NN0 ) -> ( 2 ^ ( ! ` e ) ) e. NN )
14 7 12 13 sylancr 
 |-  ( ( ( a e. NN /\ b e. RR+ ) /\ ( e e. NN /\ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) <_ ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) ) ) -> ( 2 ^ ( ! ` e ) ) e. NN )
15 1 2 3 aaliou3lem5 
 |-  ( e e. NN -> ( H ` e ) e. RR )
16 15 ad2antrl 
 |-  ( ( ( a e. NN /\ b e. RR+ ) /\ ( e e. NN /\ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) <_ ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) ) ) -> ( H ` e ) e. RR )
17 16 recnd 
 |-  ( ( ( a e. NN /\ b e. RR+ ) /\ ( e e. NN /\ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) <_ ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) ) ) -> ( H ` e ) e. CC )
18 14 nncnd 
 |-  ( ( ( a e. NN /\ b e. RR+ ) /\ ( e e. NN /\ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) <_ ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) ) ) -> ( 2 ^ ( ! ` e ) ) e. CC )
19 14 nnne0d 
 |-  ( ( ( a e. NN /\ b e. RR+ ) /\ ( e e. NN /\ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) <_ ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) ) ) -> ( 2 ^ ( ! ` e ) ) =/= 0 )
20 17 18 19 divcan4d 
 |-  ( ( ( a e. NN /\ b e. RR+ ) /\ ( e e. NN /\ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) <_ ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) ) ) -> ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / ( 2 ^ ( ! ` e ) ) ) = ( H ` e ) )
21 1 2 3 aaliou3lem7 
 |-  ( e e. NN -> ( ( H ` e ) =/= L /\ ( abs ` ( L - ( H ` e ) ) ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) ) )
22 21 simpld 
 |-  ( e e. NN -> ( H ` e ) =/= L )
23 22 ad2antrl 
 |-  ( ( ( a e. NN /\ b e. RR+ ) /\ ( e e. NN /\ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) <_ ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) ) ) -> ( H ` e ) =/= L )
24 20 23 eqnetrd 
 |-  ( ( ( a e. NN /\ b e. RR+ ) /\ ( e e. NN /\ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) <_ ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) ) ) -> ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / ( 2 ^ ( ! ` e ) ) ) =/= L )
25 24 necomd 
 |-  ( ( ( a e. NN /\ b e. RR+ ) /\ ( e e. NN /\ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) <_ ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) ) ) -> L =/= ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / ( 2 ^ ( ! ` e ) ) ) )
26 25 neneqd 
 |-  ( ( ( a e. NN /\ b e. RR+ ) /\ ( e e. NN /\ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) <_ ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) ) ) -> -. L = ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / ( 2 ^ ( ! ` e ) ) ) )
27 1 2 3 aaliou3lem4 
 |-  L e. RR
28 14 nnred 
 |-  ( ( ( a e. NN /\ b e. RR+ ) /\ ( e e. NN /\ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) <_ ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) ) ) -> ( 2 ^ ( ! ` e ) ) e. RR )
29 16 28 remulcld 
 |-  ( ( ( a e. NN /\ b e. RR+ ) /\ ( e e. NN /\ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) <_ ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) ) ) -> ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) e. RR )
30 29 14 nndivred 
 |-  ( ( ( a e. NN /\ b e. RR+ ) /\ ( e e. NN /\ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) <_ ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) ) ) -> ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / ( 2 ^ ( ! ` e ) ) ) e. RR )
31 resubcl 
 |-  ( ( L e. RR /\ ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / ( 2 ^ ( ! ` e ) ) ) e. RR ) -> ( L - ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / ( 2 ^ ( ! ` e ) ) ) ) e. RR )
32 27 30 31 sylancr 
 |-  ( ( ( a e. NN /\ b e. RR+ ) /\ ( e e. NN /\ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) <_ ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) ) ) -> ( L - ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / ( 2 ^ ( ! ` e ) ) ) ) e. RR )
33 32 recnd 
 |-  ( ( ( a e. NN /\ b e. RR+ ) /\ ( e e. NN /\ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) <_ ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) ) ) -> ( L - ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / ( 2 ^ ( ! ` e ) ) ) ) e. CC )
34 33 abscld 
 |-  ( ( ( a e. NN /\ b e. RR+ ) /\ ( e e. NN /\ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) <_ ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) ) ) -> ( abs ` ( L - ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / ( 2 ^ ( ! ` e ) ) ) ) ) e. RR )
35 simplr 
 |-  ( ( ( a e. NN /\ b e. RR+ ) /\ ( e e. NN /\ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) <_ ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) ) ) -> b e. RR+ )
36 nnnn0 
 |-  ( a e. NN -> a e. NN0 )
37 36 ad2antrr 
 |-  ( ( ( a e. NN /\ b e. RR+ ) /\ ( e e. NN /\ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) <_ ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) ) ) -> a e. NN0 )
38 14 37 nnexpcld 
 |-  ( ( ( a e. NN /\ b e. RR+ ) /\ ( e e. NN /\ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) <_ ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) ) ) -> ( ( 2 ^ ( ! ` e ) ) ^ a ) e. NN )
39 38 nnrpd 
 |-  ( ( ( a e. NN /\ b e. RR+ ) /\ ( e e. NN /\ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) <_ ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) ) ) -> ( ( 2 ^ ( ! ` e ) ) ^ a ) e. RR+ )
40 35 39 rpdivcld 
 |-  ( ( ( a e. NN /\ b e. RR+ ) /\ ( e e. NN /\ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) <_ ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) ) ) -> ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) e. RR+ )
41 40 rpred 
 |-  ( ( ( a e. NN /\ b e. RR+ ) /\ ( e e. NN /\ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) <_ ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) ) ) -> ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) e. RR )
42 2rp 
 |-  2 e. RR+
43 peano2nn0 
 |-  ( e e. NN0 -> ( e + 1 ) e. NN0 )
44 faccl 
 |-  ( ( e + 1 ) e. NN0 -> ( ! ` ( e + 1 ) ) e. NN )
45 9 43 44 3syl 
 |-  ( ( ( a e. NN /\ b e. RR+ ) /\ ( e e. NN /\ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) <_ ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) ) ) -> ( ! ` ( e + 1 ) ) e. NN )
46 nnz 
 |-  ( ( ! ` ( e + 1 ) ) e. NN -> ( ! ` ( e + 1 ) ) e. ZZ )
47 znegcl 
 |-  ( ( ! ` ( e + 1 ) ) e. ZZ -> -u ( ! ` ( e + 1 ) ) e. ZZ )
48 45 46 47 3syl 
 |-  ( ( ( a e. NN /\ b e. RR+ ) /\ ( e e. NN /\ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) <_ ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) ) ) -> -u ( ! ` ( e + 1 ) ) e. ZZ )
49 rpexpcl 
 |-  ( ( 2 e. RR+ /\ -u ( ! ` ( e + 1 ) ) e. ZZ ) -> ( 2 ^ -u ( ! ` ( e + 1 ) ) ) e. RR+ )
50 42 48 49 sylancr 
 |-  ( ( ( a e. NN /\ b e. RR+ ) /\ ( e e. NN /\ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) <_ ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) ) ) -> ( 2 ^ -u ( ! ` ( e + 1 ) ) ) e. RR+ )
51 rpmulcl 
 |-  ( ( 2 e. RR+ /\ ( 2 ^ -u ( ! ` ( e + 1 ) ) ) e. RR+ ) -> ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) e. RR+ )
52 42 50 51 sylancr 
 |-  ( ( ( a e. NN /\ b e. RR+ ) /\ ( e e. NN /\ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) <_ ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) ) ) -> ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) e. RR+ )
53 52 rpred 
 |-  ( ( ( a e. NN /\ b e. RR+ ) /\ ( e e. NN /\ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) <_ ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) ) ) -> ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) e. RR )
54 20 oveq2d 
 |-  ( ( ( a e. NN /\ b e. RR+ ) /\ ( e e. NN /\ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) <_ ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) ) ) -> ( L - ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / ( 2 ^ ( ! ` e ) ) ) ) = ( L - ( H ` e ) ) )
55 54 fveq2d 
 |-  ( ( ( a e. NN /\ b e. RR+ ) /\ ( e e. NN /\ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) <_ ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) ) ) -> ( abs ` ( L - ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / ( 2 ^ ( ! ` e ) ) ) ) ) = ( abs ` ( L - ( H ` e ) ) ) )
56 21 simprd 
 |-  ( e e. NN -> ( abs ` ( L - ( H ` e ) ) ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) )
57 56 ad2antrl 
 |-  ( ( ( a e. NN /\ b e. RR+ ) /\ ( e e. NN /\ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) <_ ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) ) ) -> ( abs ` ( L - ( H ` e ) ) ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) )
58 55 57 eqbrtrd 
 |-  ( ( ( a e. NN /\ b e. RR+ ) /\ ( e e. NN /\ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) <_ ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) ) ) -> ( abs ` ( L - ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / ( 2 ^ ( ! ` e ) ) ) ) ) <_ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) )
59 simprr 
 |-  ( ( ( a e. NN /\ b e. RR+ ) /\ ( e e. NN /\ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) <_ ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) ) ) -> ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) <_ ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) )
60 34 53 41 58 59 letrd 
 |-  ( ( ( a e. NN /\ b e. RR+ ) /\ ( e e. NN /\ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) <_ ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) ) ) -> ( abs ` ( L - ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / ( 2 ^ ( ! ` e ) ) ) ) ) <_ ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) )
61 34 41 60 lensymd 
 |-  ( ( ( a e. NN /\ b e. RR+ ) /\ ( e e. NN /\ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) <_ ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) ) ) -> -. ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) < ( abs ` ( L - ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / ( 2 ^ ( ! ` e ) ) ) ) ) )
62 oveq1 
 |-  ( f = ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) -> ( f / d ) = ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / d ) )
63 62 eqeq2d 
 |-  ( f = ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) -> ( L = ( f / d ) <-> L = ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / d ) ) )
64 63 notbid 
 |-  ( f = ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) -> ( -. L = ( f / d ) <-> -. L = ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / d ) ) )
65 62 oveq2d 
 |-  ( f = ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) -> ( L - ( f / d ) ) = ( L - ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / d ) ) )
66 65 fveq2d 
 |-  ( f = ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) -> ( abs ` ( L - ( f / d ) ) ) = ( abs ` ( L - ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / d ) ) ) )
67 66 breq2d 
 |-  ( f = ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) -> ( ( b / ( d ^ a ) ) < ( abs ` ( L - ( f / d ) ) ) <-> ( b / ( d ^ a ) ) < ( abs ` ( L - ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / d ) ) ) ) )
68 67 notbid 
 |-  ( f = ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) -> ( -. ( b / ( d ^ a ) ) < ( abs ` ( L - ( f / d ) ) ) <-> -. ( b / ( d ^ a ) ) < ( abs ` ( L - ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / d ) ) ) ) )
69 64 68 anbi12d 
 |-  ( f = ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) -> ( ( -. L = ( f / d ) /\ -. ( b / ( d ^ a ) ) < ( abs ` ( L - ( f / d ) ) ) ) <-> ( -. L = ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / d ) /\ -. ( b / ( d ^ a ) ) < ( abs ` ( L - ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / d ) ) ) ) ) )
70 oveq2 
 |-  ( d = ( 2 ^ ( ! ` e ) ) -> ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / d ) = ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / ( 2 ^ ( ! ` e ) ) ) )
71 70 eqeq2d 
 |-  ( d = ( 2 ^ ( ! ` e ) ) -> ( L = ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / d ) <-> L = ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / ( 2 ^ ( ! ` e ) ) ) ) )
72 71 notbid 
 |-  ( d = ( 2 ^ ( ! ` e ) ) -> ( -. L = ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / d ) <-> -. L = ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / ( 2 ^ ( ! ` e ) ) ) ) )
73 oveq1 
 |-  ( d = ( 2 ^ ( ! ` e ) ) -> ( d ^ a ) = ( ( 2 ^ ( ! ` e ) ) ^ a ) )
74 73 oveq2d 
 |-  ( d = ( 2 ^ ( ! ` e ) ) -> ( b / ( d ^ a ) ) = ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) )
75 70 oveq2d 
 |-  ( d = ( 2 ^ ( ! ` e ) ) -> ( L - ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / d ) ) = ( L - ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / ( 2 ^ ( ! ` e ) ) ) ) )
76 75 fveq2d 
 |-  ( d = ( 2 ^ ( ! ` e ) ) -> ( abs ` ( L - ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / d ) ) ) = ( abs ` ( L - ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / ( 2 ^ ( ! ` e ) ) ) ) ) )
77 74 76 breq12d 
 |-  ( d = ( 2 ^ ( ! ` e ) ) -> ( ( b / ( d ^ a ) ) < ( abs ` ( L - ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / d ) ) ) <-> ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) < ( abs ` ( L - ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / ( 2 ^ ( ! ` e ) ) ) ) ) ) )
78 77 notbid 
 |-  ( d = ( 2 ^ ( ! ` e ) ) -> ( -. ( b / ( d ^ a ) ) < ( abs ` ( L - ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / d ) ) ) <-> -. ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) < ( abs ` ( L - ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / ( 2 ^ ( ! ` e ) ) ) ) ) ) )
79 72 78 anbi12d 
 |-  ( d = ( 2 ^ ( ! ` e ) ) -> ( ( -. L = ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / d ) /\ -. ( b / ( d ^ a ) ) < ( abs ` ( L - ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / d ) ) ) ) <-> ( -. L = ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / ( 2 ^ ( ! ` e ) ) ) /\ -. ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) < ( abs ` ( L - ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / ( 2 ^ ( ! ` e ) ) ) ) ) ) ) )
80 69 79 rspc2ev 
 |-  ( ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) e. ZZ /\ ( 2 ^ ( ! ` e ) ) e. NN /\ ( -. L = ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / ( 2 ^ ( ! ` e ) ) ) /\ -. ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) < ( abs ` ( L - ( ( ( H ` e ) x. ( 2 ^ ( ! ` e ) ) ) / ( 2 ^ ( ! ` e ) ) ) ) ) ) ) -> E. f e. ZZ E. d e. NN ( -. L = ( f / d ) /\ -. ( b / ( d ^ a ) ) < ( abs ` ( L - ( f / d ) ) ) ) )
81 6 14 26 61 80 syl112anc 
 |-  ( ( ( a e. NN /\ b e. RR+ ) /\ ( e e. NN /\ ( 2 x. ( 2 ^ -u ( ! ` ( e + 1 ) ) ) ) <_ ( b / ( ( 2 ^ ( ! ` e ) ) ^ a ) ) ) ) -> E. f e. ZZ E. d e. NN ( -. L = ( f / d ) /\ -. ( b / ( d ^ a ) ) < ( abs ` ( L - ( f / d ) ) ) ) )
82 4 81 rexlimddv 
 |-  ( ( a e. NN /\ b e. RR+ ) -> E. f e. ZZ E. d e. NN ( -. L = ( f / d ) /\ -. ( b / ( d ^ a ) ) < ( abs ` ( L - ( f / d ) ) ) ) )
83 pm4.56 
 |-  ( ( -. L = ( f / d ) /\ -. ( b / ( d ^ a ) ) < ( abs ` ( L - ( f / d ) ) ) ) <-> -. ( L = ( f / d ) \/ ( b / ( d ^ a ) ) < ( abs ` ( L - ( f / d ) ) ) ) )
84 83 rexbii 
 |-  ( E. d e. NN ( -. L = ( f / d ) /\ -. ( b / ( d ^ a ) ) < ( abs ` ( L - ( f / d ) ) ) ) <-> E. d e. NN -. ( L = ( f / d ) \/ ( b / ( d ^ a ) ) < ( abs ` ( L - ( f / d ) ) ) ) )
85 rexnal 
 |-  ( E. d e. NN -. ( L = ( f / d ) \/ ( b / ( d ^ a ) ) < ( abs ` ( L - ( f / d ) ) ) ) <-> -. A. d e. NN ( L = ( f / d ) \/ ( b / ( d ^ a ) ) < ( abs ` ( L - ( f / d ) ) ) ) )
86 84 85 bitri 
 |-  ( E. d e. NN ( -. L = ( f / d ) /\ -. ( b / ( d ^ a ) ) < ( abs ` ( L - ( f / d ) ) ) ) <-> -. A. d e. NN ( L = ( f / d ) \/ ( b / ( d ^ a ) ) < ( abs ` ( L - ( f / d ) ) ) ) )
87 86 rexbii 
 |-  ( E. f e. ZZ E. d e. NN ( -. L = ( f / d ) /\ -. ( b / ( d ^ a ) ) < ( abs ` ( L - ( f / d ) ) ) ) <-> E. f e. ZZ -. A. d e. NN ( L = ( f / d ) \/ ( b / ( d ^ a ) ) < ( abs ` ( L - ( f / d ) ) ) ) )
88 rexnal 
 |-  ( E. f e. ZZ -. A. d e. NN ( L = ( f / d ) \/ ( b / ( d ^ a ) ) < ( abs ` ( L - ( f / d ) ) ) ) <-> -. A. f e. ZZ A. d e. NN ( L = ( f / d ) \/ ( b / ( d ^ a ) ) < ( abs ` ( L - ( f / d ) ) ) ) )
89 87 88 bitri 
 |-  ( E. f e. ZZ E. d e. NN ( -. L = ( f / d ) /\ -. ( b / ( d ^ a ) ) < ( abs ` ( L - ( f / d ) ) ) ) <-> -. A. f e. ZZ A. d e. NN ( L = ( f / d ) \/ ( b / ( d ^ a ) ) < ( abs ` ( L - ( f / d ) ) ) ) )
90 82 89 sylib 
 |-  ( ( a e. NN /\ b e. RR+ ) -> -. A. f e. ZZ A. d e. NN ( L = ( f / d ) \/ ( b / ( d ^ a ) ) < ( abs ` ( L - ( f / d ) ) ) ) )
91 90 nrexdv 
 |-  ( a e. NN -> -. E. b e. RR+ A. f e. ZZ A. d e. NN ( L = ( f / d ) \/ ( b / ( d ^ a ) ) < ( abs ` ( L - ( f / d ) ) ) ) )
92 91 nrex 
 |-  -. E. a e. NN E. b e. RR+ A. f e. ZZ A. d e. NN ( L = ( f / d ) \/ ( b / ( d ^ a ) ) < ( abs ` ( L - ( f / d ) ) ) )
93 aaliou2b 
 |-  ( L e. AA -> E. a e. NN E. b e. RR+ A. f e. ZZ A. d e. NN ( L = ( f / d ) \/ ( b / ( d ^ a ) ) < ( abs ` ( L - ( f / d ) ) ) ) )
94 92 93 mto 
 |-  -. L e. AA