Metamath Proof Explorer

Theorem relogbcxpb

Description: The logarithm is the inverse of the exponentiation. Observation in Cohen4 p. 348. (Contributed by AV, 11-Jun-2020)

Ref Expression
Assertion relogbcxpb 
|- ( ( ( B e. RR+ /\ B =/= 1 ) /\ X e. RR+ /\ Y e. RR ) -> ( ( B logb X ) = Y <-> ( B ^c Y ) = X ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( Y = ( B logb X ) -> ( B ^c Y ) = ( B ^c ( B logb X ) ) )
2 1 eqcoms 
 |-  ( ( B logb X ) = Y -> ( B ^c Y ) = ( B ^c ( B logb X ) ) )
3 rpcn 
 |-  ( B e. RR+ -> B e. CC )
4 3 adantr 
 |-  ( ( B e. RR+ /\ B =/= 1 ) -> B e. CC )
5 rpne0 
 |-  ( B e. RR+ -> B =/= 0 )
6 5 adantr 
 |-  ( ( B e. RR+ /\ B =/= 1 ) -> B =/= 0 )
7 simpr 
 |-  ( ( B e. RR+ /\ B =/= 1 ) -> B =/= 1 )
8 eldifpr 
 |-  ( B e. ( CC \ { 0 , 1 } ) <-> ( B e. CC /\ B =/= 0 /\ B =/= 1 ) )
9 4 6 7 8 syl3anbrc 
 |-  ( ( B e. RR+ /\ B =/= 1 ) -> B e. ( CC \ { 0 , 1 } ) )
10 rpcndif0 
 |-  ( X e. RR+ -> X e. ( CC \ { 0 } ) )
11 9 10 anim12i 
 |-  ( ( ( B e. RR+ /\ B =/= 1 ) /\ X e. RR+ ) -> ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) )
12 11 3adant3 
 |-  ( ( ( B e. RR+ /\ B =/= 1 ) /\ X e. RR+ /\ Y e. RR ) -> ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) )
13 cxplogb 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( B ^c ( B logb X ) ) = X )
14 12 13 syl 
 |-  ( ( ( B e. RR+ /\ B =/= 1 ) /\ X e. RR+ /\ Y e. RR ) -> ( B ^c ( B logb X ) ) = X )
15 2 14 sylan9eqr 
 |-  ( ( ( ( B e. RR+ /\ B =/= 1 ) /\ X e. RR+ /\ Y e. RR ) /\ ( B logb X ) = Y ) -> ( B ^c Y ) = X )
16 oveq2 
 |-  ( X = ( B ^c Y ) -> ( B logb X ) = ( B logb ( B ^c Y ) ) )
17 16 eqcoms 
 |-  ( ( B ^c Y ) = X -> ( B logb X ) = ( B logb ( B ^c Y ) ) )
18 eldifsn 
 |-  ( B e. ( RR+ \ { 1 } ) <-> ( B e. RR+ /\ B =/= 1 ) )
19 18 biimpri 
 |-  ( ( B e. RR+ /\ B =/= 1 ) -> B e. ( RR+ \ { 1 } ) )
20 19 anim1i 
 |-  ( ( ( B e. RR+ /\ B =/= 1 ) /\ Y e. RR ) -> ( B e. ( RR+ \ { 1 } ) /\ Y e. RR ) )
21 20 3adant2 
 |-  ( ( ( B e. RR+ /\ B =/= 1 ) /\ X e. RR+ /\ Y e. RR ) -> ( B e. ( RR+ \ { 1 } ) /\ Y e. RR ) )
22 relogbcxp 
 |-  ( ( B e. ( RR+ \ { 1 } ) /\ Y e. RR ) -> ( B logb ( B ^c Y ) ) = Y )
23 21 22 syl 
 |-  ( ( ( B e. RR+ /\ B =/= 1 ) /\ X e. RR+ /\ Y e. RR ) -> ( B logb ( B ^c Y ) ) = Y )
24 17 23 sylan9eqr 
 |-  ( ( ( ( B e. RR+ /\ B =/= 1 ) /\ X e. RR+ /\ Y e. RR ) /\ ( B ^c Y ) = X ) -> ( B logb X ) = Y )
25 15 24 impbida 
 |-  ( ( ( B e. RR+ /\ B =/= 1 ) /\ X e. RR+ /\ Y e. RR ) -> ( ( B logb X ) = Y <-> ( B ^c Y ) = X ) )