Metamath Proof Explorer


Theorem relogbf

Description: The general logarithm to a real base greater than 1 regarded as function restricted to the positive integers. Property in Cohen4 p. 349. (Contributed by AV, 12-Jun-2020)

Ref Expression
Assertion relogbf B + 1 < B curry logb B + : +

Proof

Step Hyp Ref Expression
1 rpcndif0 x + x 0
2 1 adantl B + 1 < B x + x 0
3 rpcn B + B
4 3 adantr B + 1 < B B
5 rpne0 B + B 0
6 5 adantr B + 1 < B B 0
7 animorr B + 1 < B B < 1 1 < B
8 rpre B + B
9 1red 1 < B 1
10 lttri2 B 1 B 1 B < 1 1 < B
11 8 9 10 syl2an B + 1 < B B 1 B < 1 1 < B
12 7 11 mpbird B + 1 < B B 1
13 4 6 12 3jca B + 1 < B B B 0 B 1
14 logbmpt B B 0 B 1 curry logb B = x 0 log x log B
15 13 14 syl B + 1 < B curry logb B = x 0 log x log B
16 15 dmeqd B + 1 < B dom curry logb B = dom x 0 log x log B
17 ovexd B + 1 < B x 0 log x log B V
18 17 ralrimiva B + 1 < B x 0 log x log B V
19 dmmptg x 0 log x log B V dom x 0 log x log B = 0
20 18 19 syl B + 1 < B dom x 0 log x log B = 0
21 16 20 eqtrd B + 1 < B dom curry logb B = 0
22 21 adantr B + 1 < B x + dom curry logb B = 0
23 2 22 eleqtrrd B + 1 < B x + x dom curry logb B
24 logbfval B B 0 B 1 x 0 curry logb B x = log B x
25 13 1 24 syl2an B + 1 < B x + curry logb B x = log B x
26 simpll B + 1 < B x + B +
27 simpr B + 1 < B x + x +
28 12 adantr B + 1 < B x + B 1
29 26 27 28 3jca B + 1 < B x + B + x + B 1
30 relogbcl B + x + B 1 log B x
31 29 30 syl B + 1 < B x + log B x
32 25 31 eqeltrd B + 1 < B x + curry logb B x
33 23 32 jca B + 1 < B x + x dom curry logb B curry logb B x
34 33 ralrimiva B + 1 < B x + x dom curry logb B curry logb B x
35 logbf B B 0 B 1 curry logb B : 0
36 13 35 syl B + 1 < B curry logb B : 0
37 ffun curry logb B : 0 Fun curry logb B
38 ffvresb Fun curry logb B curry logb B + : + x + x dom curry logb B curry logb B x
39 36 37 38 3syl B + 1 < B curry logb B + : + x + x dom curry logb B curry logb B x
40 34 39 mpbird B + 1 < B curry logb B + : +