Metamath Proof Explorer


Theorem relogbcl

Description: Closure of the general logarithm with a positive real base on positive reals. (Contributed by Stefan O'Rear, 19-Sep-2014) (Revised by Thierry Arnoux, 27-Sep-2017)

Ref Expression
Assertion relogbcl B+X+B1logBX

Proof

Step Hyp Ref Expression
1 simp1 B+X+B1B+
2 1 rpcnne0d B+X+B1BB0
3 simp3 B+X+B1B1
4 df-3an BB0B1BB0B1
5 2 3 4 sylanbrc B+X+B1BB0B1
6 eldifpr B01BB0B1
7 5 6 sylibr B+X+B1B01
8 simp2 B+X+B1X+
9 8 rpcnne0d B+X+B1XX0
10 eldifsn X0XX0
11 9 10 sylibr B+X+B1X0
12 logbval B01X0logBX=logXlogB
13 7 11 12 syl2anc B+X+B1logBX=logXlogB
14 relogcl X+logX
15 14 3ad2ant2 B+X+B1logX
16 relogcl B+logB
17 16 3ad2ant1 B+X+B1logB
18 logne0 B+B1logB0
19 18 3adant2 B+X+B1logB0
20 15 17 19 redivcld B+X+B1logXlogB
21 13 20 eqeltrd B+X+B1logBX