Step | Hyp | Ref
| Expression |
1 | | df-logb 24503 |
. . 3
⊢
logb = (𝑥 ∈
(ℂ ∖ {0, 1}), 𝑦
∈ (ℂ ∖ {0}) ↦ ((log‘𝑦) / (log‘𝑥))) |
2 | | ovexd 6680 |
. . . 4
⊢ (((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) ∧ (𝑥 ∈ (ℂ ∖ {0, 1}) ∧ 𝑦 ∈ (ℂ ∖ {0})))
→ ((log‘𝑦) /
(log‘𝑥)) ∈
V) |
3 | 2 | ralrimivva 2971 |
. . 3
⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) → ∀𝑥 ∈ (ℂ ∖ {0, 1})∀𝑦 ∈ (ℂ ∖
{0})((log‘𝑦) /
(log‘𝑥)) ∈
V) |
4 | | ax-1cn 9994 |
. . . . . 6
⊢ 1 ∈
ℂ |
5 | | ax-1ne0 10005 |
. . . . . . 7
⊢ 1 ≠
0 |
6 | | elsng 4191 |
. . . . . . . 8
⊢ (1 ∈
ℂ → (1 ∈ {0} ↔ 1 = 0)) |
7 | 4, 6 | ax-mp 5 |
. . . . . . 7
⊢ (1 ∈
{0} ↔ 1 = 0) |
8 | 5, 7 | nemtbir 2889 |
. . . . . 6
⊢ ¬ 1
∈ {0} |
9 | | eldif 3584 |
. . . . . 6
⊢ (1 ∈
(ℂ ∖ {0}) ↔ (1 ∈ ℂ ∧ ¬ 1 ∈
{0})) |
10 | 4, 8, 9 | mpbir2an 955 |
. . . . 5
⊢ 1 ∈
(ℂ ∖ {0}) |
11 | 10 | ne0ii 3923 |
. . . 4
⊢ (ℂ
∖ {0}) ≠ ∅ |
12 | 11 | a1i 11 |
. . 3
⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) → (ℂ ∖ {0}) ≠
∅) |
13 | | cnex 10017 |
. . . . 5
⊢ ℂ
∈ V |
14 | | difexg 4808 |
. . . . 5
⊢ (ℂ
∈ V → (ℂ ∖ {0}) ∈ V) |
15 | 13, 14 | ax-mp 5 |
. . . 4
⊢ (ℂ
∖ {0}) ∈ V |
16 | 15 | a1i 11 |
. . 3
⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) → (ℂ ∖ {0}) ∈
V) |
17 | | eldifpr 4204 |
. . . 4
⊢ (𝐵 ∈ (ℂ ∖ {0, 1})
↔ (𝐵 ∈ ℂ
∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1)) |
18 | 17 | biimpri 218 |
. . 3
⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) → 𝐵 ∈ (ℂ ∖ {0,
1})) |
19 | 1, 3, 12, 16, 18 | mpt2curryvald 7396 |
. 2
⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) → (curry logb
‘𝐵) = (𝑦 ∈ (ℂ ∖ {0})
↦ ⦋𝐵 /
𝑥⦌((log‘𝑦) / (log‘𝑥)))) |
20 | | csbov2g 6691 |
. . . . 5
⊢ (𝐵 ∈ ℂ →
⦋𝐵 / 𝑥⦌((log‘𝑦) / (log‘𝑥)) = ((log‘𝑦) / ⦋𝐵 / 𝑥⦌(log‘𝑥))) |
21 | | csbfv 6233 |
. . . . . . 7
⊢
⦋𝐵 /
𝑥⦌(log‘𝑥) = (log‘𝐵) |
22 | 21 | a1i 11 |
. . . . . 6
⊢ (𝐵 ∈ ℂ →
⦋𝐵 / 𝑥⦌(log‘𝑥) = (log‘𝐵)) |
23 | 22 | oveq2d 6666 |
. . . . 5
⊢ (𝐵 ∈ ℂ →
((log‘𝑦) /
⦋𝐵 / 𝑥⦌(log‘𝑥)) = ((log‘𝑦) / (log‘𝐵))) |
24 | 20, 23 | eqtrd 2656 |
. . . 4
⊢ (𝐵 ∈ ℂ →
⦋𝐵 / 𝑥⦌((log‘𝑦) / (log‘𝑥)) = ((log‘𝑦) / (log‘𝐵))) |
25 | 24 | 3ad2ant1 1082 |
. . 3
⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) → ⦋𝐵 / 𝑥⦌((log‘𝑦) / (log‘𝑥)) = ((log‘𝑦) / (log‘𝐵))) |
26 | 25 | mpteq2dv 4745 |
. 2
⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) → (𝑦 ∈ (ℂ ∖ {0}) ↦
⦋𝐵 / 𝑥⦌((log‘𝑦) / (log‘𝑥))) = (𝑦 ∈ (ℂ ∖ {0}) ↦
((log‘𝑦) /
(log‘𝐵)))) |
27 | 19, 26 | eqtrd 2656 |
1
⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) → (curry logb
‘𝐵) = (𝑦 ∈ (ℂ ∖ {0})
↦ ((log‘𝑦) /
(log‘𝐵)))) |