Metamath Proof Explorer

Theorem divval

Description: Value of division: if A and B are complex numbers with B nonzero, then ( A / B ) is the (unique) complex number such that ( B x. x ) = A . (Contributed by NM, 8-May-1999) (Revised by Mario Carneiro, 17-Feb-2014)

Ref Expression
Assertion divval ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B = ι x ∈ ℂ | B ⁢ x = A

Proof

Step Hyp Ref Expression
1 eldifsn ⊢ B ∈ ℂ ∖ 0 ↔ B ∈ ℂ ∧ B ≠ 0
2 eqeq2 ⊢ z = A → y ⁢ x = z ↔ y ⁢ x = A
3 2 riotabidv ⊢ z = A → ι x ∈ ℂ | y ⁢ x = z = ι x ∈ ℂ | y ⁢ x = A
4 oveq1 ⊢ y = B → y ⁢ x = B ⁢ x
5 4 eqeq1d ⊢ y = B → y ⁢ x = A ↔ B ⁢ x = A
6 5 riotabidv ⊢ y = B → ι x ∈ ℂ | y ⁢ x = A = ι x ∈ ℂ | B ⁢ x = A
7 df-div ⊢ ÷ = z ∈ ℂ , y ∈ ℂ ∖ 0 ⟼ ι x ∈ ℂ | y ⁢ x = z
8 riotaex ⊢ ι x ∈ ℂ | B ⁢ x = A ∈ V
9 3 6 7 8 ovmpo ⊢ A ∈ ℂ ∧ B ∈ ℂ ∖ 0 → A B = ι x ∈ ℂ | B ⁢ x = A
10 1 9 sylan2br ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B = ι x ∈ ℂ | B ⁢ x = A
11 10 3impb ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B = ι x ∈ ℂ | B ⁢ x = A