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 + 1 2 1 log 2 R < R

Proof

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