Step |
Hyp |
Ref |
Expression |
1 |
|
df-logb |
⊢ logb = ( 𝑥 ∈ ( ℂ ∖ { 0 , 1 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ( log ‘ 𝑦 ) / ( log ‘ 𝑥 ) ) ) |
2 |
|
ovexd |
⊢ ( ( ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( 𝑥 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) ) → ( ( log ‘ 𝑦 ) / ( log ‘ 𝑥 ) ) ∈ V ) |
3 |
2
|
ralrimivva |
⊢ ( ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ∀ 𝑥 ∈ ( ℂ ∖ { 0 , 1 } ) ∀ 𝑦 ∈ ( ℂ ∖ { 0 } ) ( ( log ‘ 𝑦 ) / ( log ‘ 𝑥 ) ) ∈ V ) |
4 |
|
cnex |
⊢ ℂ ∈ V |
5 |
|
difexg |
⊢ ( ℂ ∈ V → ( ℂ ∖ { 0 } ) ∈ V ) |
6 |
4 5
|
mp1i |
⊢ ( ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( ℂ ∖ { 0 } ) ∈ V ) |
7 |
|
eldifpr |
⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ↔ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) ) |
8 |
7
|
biimpri |
⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ) |
9 |
8
|
adantr |
⊢ ( ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ) |
10 |
|
simpr |
⊢ ( ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → 𝑋 ∈ ( ℂ ∖ { 0 } ) ) |
11 |
1 3 6 9 10
|
fvmpocurryd |
⊢ ( ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( ( curry logb ‘ 𝐵 ) ‘ 𝑋 ) = ( 𝐵 logb 𝑋 ) ) |