Metamath Proof Explorer


Theorem logblt

Description: The general logarithm function is strictly monotone/increasing. Property 2 of Cohen4 p. 377. See logltb . (Contributed by Stefan O'Rear, 19-Oct-2014) (Revised by Thierry Arnoux, 27-Sep-2017)

Ref Expression
Assertion logblt B 2 X + Y + X < Y log B X < log B Y

Proof

Step Hyp Ref Expression
1 simp2 B 2 X + Y + X +
2 1 relogcld B 2 X + Y + log X
3 simp3 B 2 X + Y + Y +
4 3 relogcld B 2 X + Y + log Y
5 simp1 B 2 X + Y + B 2
6 eluzelz B 2 B
7 5 6 syl B 2 X + Y + B
8 7 zred B 2 X + Y + B
9 1z 1
10 1p1e2 1 + 1 = 2
11 10 fveq2i 1 + 1 = 2
12 5 11 syl6eleqr B 2 X + Y + B 1 + 1
13 eluzp1l 1 B 1 + 1 1 < B
14 9 12 13 sylancr B 2 X + Y + 1 < B
15 8 14 rplogcld B 2 X + Y + log B +
16 2 4 15 ltdiv1d B 2 X + Y + log X < log Y log X log B < log Y log B
17 logltb X + Y + X < Y log X < log Y
18 17 3adant1 B 2 X + Y + X < Y log X < log Y
19 relogbval B 2 X + log B X = log X log B
20 19 3adant3 B 2 X + Y + log B X = log X log B
21 relogbval B 2 Y + log B Y = log Y log B
22 21 3adant2 B 2 X + Y + log B Y = log Y log B
23 20 22 breq12d B 2 X + Y + log B X < log B Y log X log B < log Y log B
24 16 18 23 3bitr4d B 2 X + Y + X < Y log B X < log B Y