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

Metamath Proof Explorer

Definition df-div

Description: Define division. Theorem divmuli relates it to multiplication, and divcli and redivcli prove its closure laws. (Contributed by NM, 2-Feb-1995) Use divval instead. (Revised by Mario Carneiro, 1-Apr-2014) (New usage is discouraged.)

Ref Expression
Assertion df-div ⊢ ÷ = x ∈ ℂ , y ∈ ℂ ∖ 0 ⟼ ι z ∈ ℂ | y ⁢ z = x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdiv class ÷
1 vx setvar x
2 cc class ℂ
3 vy setvar y
4 cc0 class 0
5 4 csn class 0
6 2 5 cdif class ℂ ∖ 0
7 vz setvar z
8 3 cv setvar y
9 cmul class ×
10 7 cv setvar z
11 8 10 9 co class y ⁢ z
12 1 cv setvar x
13 11 12 wceq wff y ⁢ z = x
14 13 7 2 crio class ι z ∈ ℂ | y ⁢ z = x
15 1 3 2 6 14 cmpo class x ∈ ℂ , y ∈ ℂ ∖ 0 ⟼ ι z ∈ ℂ | y ⁢ z = x
16 0 15 wceq wff ÷ = x ∈ ℂ , y ∈ ℂ ∖ 0 ⟼ ι z ∈ ℂ | y ⁢ z = x