Step | Hyp | Ref
| Expression |
1 | | df-logb 24303 |
. . 3
⊢
logb = (𝑥 ∈
(ℂ ∖ {0, 1}), 𝑦
∈ (ℂ ∖ {0}) ↦ ((log‘𝑦) / (log‘𝑥))) |
2 | | ovex 6577 |
. . . . 5
⊢
((log‘𝑦) /
(log‘𝑥)) ∈
V |
3 | 2 | a1i 11 |
. . . 4
⊢ (((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) ∧ (𝑥 ∈ (ℂ ∖ {0, 1}) ∧ 𝑦 ∈ (ℂ ∖ {0})))
→ ((log‘𝑦) /
(log‘𝑥)) ∈
V) |
4 | 3 | ralrimivva 2954 |
. . 3
⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) → ∀𝑥 ∈ (ℂ ∖ {0, 1})∀𝑦 ∈ (ℂ ∖
{0})((log‘𝑦) /
(log‘𝑥)) ∈
V) |
5 | | ax-1cn 9873 |
. . . . . 6
⊢ 1 ∈
ℂ |
6 | | ax-1ne0 9884 |
. . . . . . 7
⊢ 1 ≠
0 |
7 | | elsng 4139 |
. . . . . . . 8
⊢ (1 ∈
ℂ → (1 ∈ {0} ↔ 1 = 0)) |
8 | 5, 7 | ax-mp 5 |
. . . . . . 7
⊢ (1 ∈
{0} ↔ 1 = 0) |
9 | 6, 8 | nemtbir 2877 |
. . . . . 6
⊢ ¬ 1
∈ {0} |
10 | | eldif 3550 |
. . . . . 6
⊢ (1 ∈
(ℂ ∖ {0}) ↔ (1 ∈ ℂ ∧ ¬ 1 ∈
{0})) |
11 | 5, 9, 10 | mpbir2an 957 |
. . . . 5
⊢ 1 ∈
(ℂ ∖ {0}) |
12 | 11 | ne0ii 3882 |
. . . 4
⊢ (ℂ
∖ {0}) ≠ ∅ |
13 | 12 | a1i 11 |
. . 3
⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) → (ℂ ∖ {0}) ≠
∅) |
14 | | cnex 9896 |
. . . . 5
⊢ ℂ
∈ V |
15 | | difexg 4735 |
. . . . 5
⊢ (ℂ
∈ V → (ℂ ∖ {0}) ∈ V) |
16 | 14, 15 | ax-mp 5 |
. . . 4
⊢ (ℂ
∖ {0}) ∈ V |
17 | 16 | a1i 11 |
. . 3
⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) → (ℂ ∖ {0}) ∈
V) |
18 | | eldifpr 4152 |
. . . 4
⊢ (𝐵 ∈ (ℂ ∖ {0, 1})
↔ (𝐵 ∈ ℂ
∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1)) |
19 | 18 | biimpri 217 |
. . 3
⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) → 𝐵 ∈ (ℂ ∖ {0,
1})) |
20 | 1, 4, 13, 17, 19 | mpt2curryvald 7283 |
. 2
⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) → (curry logb
‘𝐵) = (𝑦 ∈ (ℂ ∖ {0})
↦ ⦋𝐵 /
𝑥⦌((log‘𝑦) / (log‘𝑥)))) |
21 | | csbov2g 6589 |
. . . . 5
⊢ (𝐵 ∈ ℂ →
⦋𝐵 / 𝑥⦌((log‘𝑦) / (log‘𝑥)) = ((log‘𝑦) / ⦋𝐵 / 𝑥⦌(log‘𝑥))) |
22 | | csbfv 6143 |
. . . . . . 7
⊢
⦋𝐵 /
𝑥⦌(log‘𝑥) = (log‘𝐵) |
23 | 22 | a1i 11 |
. . . . . 6
⊢ (𝐵 ∈ ℂ →
⦋𝐵 / 𝑥⦌(log‘𝑥) = (log‘𝐵)) |
24 | 23 | oveq2d 6565 |
. . . . 5
⊢ (𝐵 ∈ ℂ →
((log‘𝑦) /
⦋𝐵 / 𝑥⦌(log‘𝑥)) = ((log‘𝑦) / (log‘𝐵))) |
25 | 21, 24 | eqtrd 2644 |
. . . 4
⊢ (𝐵 ∈ ℂ →
⦋𝐵 / 𝑥⦌((log‘𝑦) / (log‘𝑥)) = ((log‘𝑦) / (log‘𝐵))) |
26 | 25 | 3ad2ant1 1075 |
. . 3
⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) → ⦋𝐵 / 𝑥⦌((log‘𝑦) / (log‘𝑥)) = ((log‘𝑦) / (log‘𝐵))) |
27 | 26 | mpteq2dv 4673 |
. 2
⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) → (𝑦 ∈ (ℂ ∖ {0}) ↦
⦋𝐵 / 𝑥⦌((log‘𝑦) / (log‘𝑥))) = (𝑦 ∈ (ℂ ∖ {0}) ↦
((log‘𝑦) /
(log‘𝐵)))) |
28 | 20, 27 | eqtrd 2644 |
1
⊢ ((𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1) → (curry logb
‘𝐵) = (𝑦 ∈ (ℂ ∖ {0})
↦ ((log‘𝑦) /
(log‘𝐵)))) |