Metamath Proof Explorer

Theorem dya2ub

Description: An upper bound for a dyadic number. (Contributed by Thierry Arnoux, 19-Sep-2017)

Ref Expression
Assertion dya2ub 
|- ( R e. RR+ -> ( 1 / ( 2 ^ ( |_ ` ( 1 - ( 2 logb R ) ) ) ) ) < R )

Proof

Step Hyp Ref Expression
1 2z 
 |-  2 e. ZZ
2 uzid 
 |-  ( 2 e. ZZ -> 2 e. ( ZZ>= ` 2 ) )
3 1 2 ax-mp 
 |-  2 e. ( ZZ>= ` 2 )
4 relogbzcl 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ R e. RR+ ) -> ( 2 logb R ) e. RR )
5 3 4 mpan 
 |-  ( R e. RR+ -> ( 2 logb R ) e. RR )
6 5 renegcld 
 |-  ( R e. RR+ -> -u ( 2 logb R ) e. RR )
7 flltp1 
 |-  ( -u ( 2 logb R ) e. RR -> -u ( 2 logb R ) < ( ( |_ ` -u ( 2 logb R ) ) + 1 ) )
8 6 7 syl 
 |-  ( R e. RR+ -> -u ( 2 logb R ) < ( ( |_ ` -u ( 2 logb R ) ) + 1 ) )
9 1z 
 |-  1 e. ZZ
10 fladdz 
 |-  ( ( -u ( 2 logb R ) e. RR /\ 1 e. ZZ ) -> ( |_ ` ( -u ( 2 logb R ) + 1 ) ) = ( ( |_ ` -u ( 2 logb R ) ) + 1 ) )
11 6 9 10 sylancl 
 |-  ( R e. RR+ -> ( |_ ` ( -u ( 2 logb R ) + 1 ) ) = ( ( |_ ` -u ( 2 logb R ) ) + 1 ) )
12 5 recnd 
 |-  ( R e. RR+ -> ( 2 logb R ) e. CC )
13 ax-1cn 
 |-  1 e. CC
14 negsubdi 
 |-  ( ( ( 2 logb R ) e. CC /\ 1 e. CC ) -> -u ( ( 2 logb R ) - 1 ) = ( -u ( 2 logb R ) + 1 ) )
15 negsubdi2 
 |-  ( ( ( 2 logb R ) e. CC /\ 1 e. CC ) -> -u ( ( 2 logb R ) - 1 ) = ( 1 - ( 2 logb R ) ) )
16 14 15 eqtr3d 
 |-  ( ( ( 2 logb R ) e. CC /\ 1 e. CC ) -> ( -u ( 2 logb R ) + 1 ) = ( 1 - ( 2 logb R ) ) )
17 12 13 16 sylancl 
 |-  ( R e. RR+ -> ( -u ( 2 logb R ) + 1 ) = ( 1 - ( 2 logb R ) ) )
18 17 fveq2d 
 |-  ( R e. RR+ -> ( |_ ` ( -u ( 2 logb R ) + 1 ) ) = ( |_ ` ( 1 - ( 2 logb R ) ) ) )
19 11 18 eqtr3d 
 |-  ( R e. RR+ -> ( ( |_ ` -u ( 2 logb R ) ) + 1 ) = ( |_ ` ( 1 - ( 2 logb R ) ) ) )
20 8 19 breqtrd 
 |-  ( R e. RR+ -> -u ( 2 logb R ) < ( |_ ` ( 1 - ( 2 logb R ) ) ) )
21 3 a1i 
 |-  ( R e. RR+ -> 2 e. ( ZZ>= ` 2 ) )
22 2rp 
 |-  2 e. RR+
23 22 a1i 
 |-  ( R e. RR+ -> 2 e. RR+ )
24 1red 
 |-  ( R e. RR+ -> 1 e. RR )
25 24 5 resubcld 
 |-  ( R e. RR+ -> ( 1 - ( 2 logb R ) ) e. RR )
26 25 flcld 
 |-  ( R e. RR+ -> ( |_ ` ( 1 - ( 2 logb R ) ) ) e. ZZ )
27 23 26 rpexpcld 
 |-  ( R e. RR+ -> ( 2 ^ ( |_ ` ( 1 - ( 2 logb R ) ) ) ) e. RR+ )
28 27 rpreccld 
 |-  ( R e. RR+ -> ( 1 / ( 2 ^ ( |_ ` ( 1 - ( 2 logb R ) ) ) ) ) e. RR+ )
29 id 
 |-  ( R e. RR+ -> R e. RR+ )
30 logblt 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ ( 1 / ( 2 ^ ( |_ ` ( 1 - ( 2 logb R ) ) ) ) ) e. RR+ /\ R e. RR+ ) -> ( ( 1 / ( 2 ^ ( |_ ` ( 1 - ( 2 logb R ) ) ) ) ) < R <-> ( 2 logb ( 1 / ( 2 ^ ( |_ ` ( 1 - ( 2 logb R ) ) ) ) ) ) < ( 2 logb R ) ) )
31 21 28 29 30 syl3anc 
 |-  ( R e. RR+ -> ( ( 1 / ( 2 ^ ( |_ ` ( 1 - ( 2 logb R ) ) ) ) ) < R <-> ( 2 logb ( 1 / ( 2 ^ ( |_ ` ( 1 - ( 2 logb R ) ) ) ) ) ) < ( 2 logb R ) ) )
32 logbrec 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ ( 2 ^ ( |_ ` ( 1 - ( 2 logb R ) ) ) ) e. RR+ ) -> ( 2 logb ( 1 / ( 2 ^ ( |_ ` ( 1 - ( 2 logb R ) ) ) ) ) ) = -u ( 2 logb ( 2 ^ ( |_ ` ( 1 - ( 2 logb R ) ) ) ) ) )
33 21 27 32 syl2anc 
 |-  ( R e. RR+ -> ( 2 logb ( 1 / ( 2 ^ ( |_ ` ( 1 - ( 2 logb R ) ) ) ) ) ) = -u ( 2 logb ( 2 ^ ( |_ ` ( 1 - ( 2 logb R ) ) ) ) ) )
34 33 breq1d 
 |-  ( R e. RR+ -> ( ( 2 logb ( 1 / ( 2 ^ ( |_ ` ( 1 - ( 2 logb R ) ) ) ) ) ) < ( 2 logb R ) <-> -u ( 2 logb ( 2 ^ ( |_ ` ( 1 - ( 2 logb R ) ) ) ) ) < ( 2 logb R ) ) )
35 relogbzcl 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ ( 2 ^ ( |_ ` ( 1 - ( 2 logb R ) ) ) ) e. RR+ ) -> ( 2 logb ( 2 ^ ( |_ ` ( 1 - ( 2 logb R ) ) ) ) ) e. RR )
36 21 27 35 syl2anc 
 |-  ( R e. RR+ -> ( 2 logb ( 2 ^ ( |_ ` ( 1 - ( 2 logb R ) ) ) ) ) e. RR )
37 ltnegcon1 
 |-  ( ( ( 2 logb ( 2 ^ ( |_ ` ( 1 - ( 2 logb R ) ) ) ) ) e. RR /\ ( 2 logb R ) e. RR ) -> ( -u ( 2 logb ( 2 ^ ( |_ ` ( 1 - ( 2 logb R ) ) ) ) ) < ( 2 logb R ) <-> -u ( 2 logb R ) < ( 2 logb ( 2 ^ ( |_ ` ( 1 - ( 2 logb R ) ) ) ) ) ) )
38 36 5 37 syl2anc 
 |-  ( R e. RR+ -> ( -u ( 2 logb ( 2 ^ ( |_ ` ( 1 - ( 2 logb R ) ) ) ) ) < ( 2 logb R ) <-> -u ( 2 logb R ) < ( 2 logb ( 2 ^ ( |_ ` ( 1 - ( 2 logb R ) ) ) ) ) ) )
39 31 34 38 3bitrd 
 |-  ( R e. RR+ -> ( ( 1 / ( 2 ^ ( |_ ` ( 1 - ( 2 logb R ) ) ) ) ) < R <-> -u ( 2 logb R ) < ( 2 logb ( 2 ^ ( |_ ` ( 1 - ( 2 logb R ) ) ) ) ) ) )
40 nnlogbexp 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ ( |_ ` ( 1 - ( 2 logb R ) ) ) e. ZZ ) -> ( 2 logb ( 2 ^ ( |_ ` ( 1 - ( 2 logb R ) ) ) ) ) = ( |_ ` ( 1 - ( 2 logb R ) ) ) )
41 21 26 40 syl2anc 
 |-  ( R e. RR+ -> ( 2 logb ( 2 ^ ( |_ ` ( 1 - ( 2 logb R ) ) ) ) ) = ( |_ ` ( 1 - ( 2 logb R ) ) ) )
42 41 breq2d 
 |-  ( R e. RR+ -> ( -u ( 2 logb R ) < ( 2 logb ( 2 ^ ( |_ ` ( 1 - ( 2 logb R ) ) ) ) ) <-> -u ( 2 logb R ) < ( |_ ` ( 1 - ( 2 logb R ) ) ) ) )
43 39 42 bitrd 
 |-  ( R e. RR+ -> ( ( 1 / ( 2 ^ ( |_ ` ( 1 - ( 2 logb R ) ) ) ) ) < R <-> -u ( 2 logb R ) < ( |_ ` ( 1 - ( 2 logb R ) ) ) ) )
44 20 43 mpbird 
 |-  ( R e. RR+ -> ( 1 / ( 2 ^ ( |_ ` ( 1 - ( 2 logb R ) ) ) ) ) < R )