Step | Hyp | Ref
| Expression |
1 | | redivcl 11551 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) ∈ ℝ) |
2 | | recn 10819 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
3 | | recn 10819 |
. . . . . 6
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℂ) |
4 | | id 22 |
. . . . . 6
⊢ (𝐵 ≠ 0 → 𝐵 ≠ 0) |
5 | 2, 3, 4 | 3anim123i 1153 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0)) |
6 | | divcan2 11498 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐵 · (𝐴 / 𝐵)) = 𝐴) |
7 | 5, 6 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐵 · (𝐴 / 𝐵)) = 𝐴) |
8 | | oveq2 7221 |
. . . . . 6
⊢ (𝑥 = (𝐴 / 𝐵) → (𝐵 · 𝑥) = (𝐵 · (𝐴 / 𝐵))) |
9 | 8 | eqeq1d 2739 |
. . . . 5
⊢ (𝑥 = (𝐴 / 𝐵) → ((𝐵 · 𝑥) = 𝐴 ↔ (𝐵 · (𝐴 / 𝐵)) = 𝐴)) |
10 | 9 | rspcev 3537 |
. . . 4
⊢ (((𝐴 / 𝐵) ∈ ℝ ∧ (𝐵 · (𝐴 / 𝐵)) = 𝐴) → ∃𝑥 ∈ ℝ (𝐵 · 𝑥) = 𝐴) |
11 | 1, 7, 10 | syl2anc 587 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → ∃𝑥 ∈ ℝ (𝐵 · 𝑥) = 𝐴) |
12 | | receu 11477 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ∃!𝑥 ∈ ℂ (𝐵 · 𝑥) = 𝐴) |
13 | 5, 12 | syl 17 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → ∃!𝑥 ∈ ℂ (𝐵 · 𝑥) = 𝐴) |
14 | | ax-resscn 10786 |
. . . 4
⊢ ℝ
⊆ ℂ |
15 | | id 22 |
. . . . 5
⊢ ((𝐵 · 𝑥) = 𝐴 → (𝐵 · 𝑥) = 𝐴) |
16 | 15 | rgenw 3073 |
. . . 4
⊢
∀𝑥 ∈
ℝ ((𝐵 · 𝑥) = 𝐴 → (𝐵 · 𝑥) = 𝐴) |
17 | | riotass2 7201 |
. . . 4
⊢
(((ℝ ⊆ ℂ ∧ ∀𝑥 ∈ ℝ ((𝐵 · 𝑥) = 𝐴 → (𝐵 · 𝑥) = 𝐴)) ∧ (∃𝑥 ∈ ℝ (𝐵 · 𝑥) = 𝐴 ∧ ∃!𝑥 ∈ ℂ (𝐵 · 𝑥) = 𝐴)) → (℩𝑥 ∈ ℝ (𝐵 · 𝑥) = 𝐴) = (℩𝑥 ∈ ℂ (𝐵 · 𝑥) = 𝐴)) |
18 | 14, 16, 17 | mpanl12 702 |
. . 3
⊢
((∃𝑥 ∈
ℝ (𝐵 · 𝑥) = 𝐴 ∧ ∃!𝑥 ∈ ℂ (𝐵 · 𝑥) = 𝐴) → (℩𝑥 ∈ ℝ (𝐵 · 𝑥) = 𝐴) = (℩𝑥 ∈ ℂ (𝐵 · 𝑥) = 𝐴)) |
19 | 11, 13, 18 | syl2anc 587 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) →
(℩𝑥 ∈
ℝ (𝐵 · 𝑥) = 𝐴) = (℩𝑥 ∈ ℂ (𝐵 · 𝑥) = 𝐴)) |
20 | | rexr 10879 |
. . . 4
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℝ*) |
21 | | xdivval 30913 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ
∧ 𝐵 ≠ 0) →
(𝐴 /𝑒
𝐵) = (℩𝑥 ∈ ℝ*
(𝐵 ·e
𝑥) = 𝐴)) |
22 | 20, 21 | syl3an1 1165 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 /𝑒 𝐵) = (℩𝑥 ∈ ℝ*
(𝐵 ·e
𝑥) = 𝐴)) |
23 | | ressxr 10877 |
. . . . 5
⊢ ℝ
⊆ ℝ* |
24 | 23 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → ℝ ⊆
ℝ*) |
25 | | rexmul 12861 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝐵 ·e 𝑥) = (𝐵 · 𝑥)) |
26 | 25 | eqeq1d 2739 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((𝐵 ·e 𝑥) = 𝐴 ↔ (𝐵 · 𝑥) = 𝐴)) |
27 | 26 | biimprd 251 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((𝐵 · 𝑥) = 𝐴 → (𝐵 ·e 𝑥) = 𝐴)) |
28 | 27 | ralrimiva 3105 |
. . . . 5
⊢ (𝐵 ∈ ℝ →
∀𝑥 ∈ ℝ
((𝐵 · 𝑥) = 𝐴 → (𝐵 ·e 𝑥) = 𝐴)) |
29 | 28 | 3ad2ant2 1136 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → ∀𝑥 ∈ ℝ ((𝐵 · 𝑥) = 𝐴 → (𝐵 ·e 𝑥) = 𝐴)) |
30 | | xreceu 30916 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ
∧ 𝐵 ≠ 0) →
∃!𝑥 ∈
ℝ* (𝐵
·e 𝑥) =
𝐴) |
31 | 20, 30 | syl3an1 1165 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → ∃!𝑥 ∈ ℝ*
(𝐵 ·e
𝑥) = 𝐴) |
32 | | riotass2 7201 |
. . . 4
⊢
(((ℝ ⊆ ℝ* ∧ ∀𝑥 ∈ ℝ ((𝐵 · 𝑥) = 𝐴 → (𝐵 ·e 𝑥) = 𝐴)) ∧ (∃𝑥 ∈ ℝ (𝐵 · 𝑥) = 𝐴 ∧ ∃!𝑥 ∈ ℝ* (𝐵 ·e 𝑥) = 𝐴)) → (℩𝑥 ∈ ℝ (𝐵 · 𝑥) = 𝐴) = (℩𝑥 ∈ ℝ* (𝐵 ·e 𝑥) = 𝐴)) |
33 | 24, 29, 11, 31, 32 | syl22anc 839 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) →
(℩𝑥 ∈
ℝ (𝐵 · 𝑥) = 𝐴) = (℩𝑥 ∈ ℝ* (𝐵 ·e 𝑥) = 𝐴)) |
34 | 22, 33 | eqtr4d 2780 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 /𝑒 𝐵) = (℩𝑥 ∈ ℝ (𝐵 · 𝑥) = 𝐴)) |
35 | | divval 11492 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) = (℩𝑥 ∈ ℂ (𝐵 · 𝑥) = 𝐴)) |
36 | 5, 35 | syl 17 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 / 𝐵) = (℩𝑥 ∈ ℂ (𝐵 · 𝑥) = 𝐴)) |
37 | 19, 34, 36 | 3eqtr4d 2787 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 /𝑒 𝐵) = (𝐴 / 𝐵)) |