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 ( ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( 𝐵 logb 𝑋 ) = 𝑌 ↔ ( 𝐵 ↑𝑐 𝑌 ) = 𝑋 ) )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑌 = ( 𝐵 logb 𝑋 ) → ( 𝐵 ↑𝑐 𝑌 ) = ( 𝐵 ↑𝑐 ( 𝐵 logb 𝑋 ) ) )
2 1 eqcoms ⊢ ( ( 𝐵 logb 𝑋 ) = 𝑌 → ( 𝐵 ↑𝑐 𝑌 ) = ( 𝐵 ↑𝑐 ( 𝐵 logb 𝑋 ) ) )
3 rpcn ⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ∈ ℂ )
4 3 adantr ⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) → 𝐵 ∈ ℂ )
5 rpne0 ⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ≠ 0 )
6 5 adantr ⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) → 𝐵 ≠ 0 )
7 simpr ⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) → 𝐵 ≠ 1 )
8 eldifpr ⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ↔ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) )
9 4 6 7 8 syl3anbrc ⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) → 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) )
10 rpcndif0 ⊢ ( 𝑋 ∈ ℝ+ → 𝑋 ∈ ( ℂ ∖ { 0 } ) )
11 9 10 anim12i ⊢ ( ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) ∧ 𝑋 ∈ ℝ+ ) → ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) )
12 11 3adant3 ⊢ ( ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) )
13 cxplogb ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐵 ↑𝑐 ( 𝐵 logb 𝑋 ) ) = 𝑋 )
14 12 13 syl ⊢ ( ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( 𝐵 ↑𝑐 ( 𝐵 logb 𝑋 ) ) = 𝑋 )
15 2 14 sylan9eqr ⊢ ( ( ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ ( 𝐵 logb 𝑋 ) = 𝑌 ) → ( 𝐵 ↑𝑐 𝑌 ) = 𝑋 )
16 oveq2 ⊢ ( 𝑋 = ( 𝐵 ↑𝑐 𝑌 ) → ( 𝐵 logb 𝑋 ) = ( 𝐵 logb ( 𝐵 ↑𝑐 𝑌 ) ) )
17 16 eqcoms ⊢ ( ( 𝐵 ↑𝑐 𝑌 ) = 𝑋 → ( 𝐵 logb 𝑋 ) = ( 𝐵 logb ( 𝐵 ↑𝑐 𝑌 ) ) )
18 eldifsn ⊢ ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ↔ ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) )
19 18 biimpri ⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) → 𝐵 ∈ ( ℝ+ ∖ { 1 } ) )
20 19 anim1i ⊢ ( ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) ∧ 𝑌 ∈ ℝ ) → ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ∧ 𝑌 ∈ ℝ ) )
21 20 3adant2 ⊢ ( ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ∧ 𝑌 ∈ ℝ ) )
22 relogbcxp ⊢ ( ( 𝐵 ∈ ( ℝ+ ∖ { 1 } ) ∧ 𝑌 ∈ ℝ ) → ( 𝐵 logb ( 𝐵 ↑𝑐 𝑌 ) ) = 𝑌 )
23 21 22 syl ⊢ ( ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( 𝐵 logb ( 𝐵 ↑𝑐 𝑌 ) ) = 𝑌 )
24 17 23 sylan9eqr ⊢ ( ( ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ ( 𝐵 ↑𝑐 𝑌 ) = 𝑋 ) → ( 𝐵 logb 𝑋 ) = 𝑌 )
25 15 24 impbida ⊢ ( ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( 𝐵 logb 𝑋 ) = 𝑌 ↔ ( 𝐵 ↑𝑐 𝑌 ) = 𝑋 ) )