This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem divcl

Description: Closure law for division. (Contributed by NM, 21-Jul-2001) (Proof shortened by Mario Carneiro, 17-Feb-2014)

Ref Expression
Assertion divcl ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B ∈ ℂ

Proof

Step Hyp Ref Expression
1 divval ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B = ι x ∈ ℂ | B ⁢ x = A
2 receu ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → ∃! x ∈ ℂ B ⁢ x = A
3 riotacl ⊢ ∃! x ∈ ℂ B ⁢ x = A → ι x ∈ ℂ | B ⁢ x = A ∈ ℂ
4 2 3 syl ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → ι x ∈ ℂ | B ⁢ x = A ∈ ℂ
5 1 4 eqeltrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B ∈ ℂ