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+121log2R<R

Proof

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