Description: An upper bound for a dyadic number. (Contributed by Thierry Arnoux, 19-Sep-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | dya2ub | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2z | |
|
2 | uzid | |
|
3 | 1 2 | ax-mp | |
4 | relogbzcl | |
|
5 | 3 4 | mpan | |
6 | 5 | renegcld | |
7 | flltp1 | |
|
8 | 6 7 | syl | |
9 | 1z | |
|
10 | fladdz | |
|
11 | 6 9 10 | sylancl | |
12 | 5 | recnd | |
13 | ax-1cn | |
|
14 | negsubdi | |
|
15 | negsubdi2 | |
|
16 | 14 15 | eqtr3d | |
17 | 12 13 16 | sylancl | |
18 | 17 | fveq2d | |
19 | 11 18 | eqtr3d | |
20 | 8 19 | breqtrd | |
21 | 3 | a1i | |
22 | 2rp | |
|
23 | 22 | a1i | |
24 | 1red | |
|
25 | 24 5 | resubcld | |
26 | 25 | flcld | |
27 | 23 26 | rpexpcld | |
28 | 27 | rpreccld | |
29 | id | |
|
30 | logblt | |
|
31 | 21 28 29 30 | syl3anc | |
32 | logbrec | |
|
33 | 21 27 32 | syl2anc | |
34 | 33 | breq1d | |
35 | relogbzcl | |
|
36 | 21 27 35 | syl2anc | |
37 | ltnegcon1 | |
|
38 | 36 5 37 | syl2anc | |
39 | 31 34 38 | 3bitrd | |
40 | nnlogbexp | |
|
41 | 21 26 40 | syl2anc | |
42 | 41 | breq2d | |
43 | 39 42 | bitrd | |
44 | 20 43 | mpbird | |