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 / = ( 𝑥 ∈ ℂ , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℩ 𝑧 ∈ ℂ ( 𝑦 · 𝑧 ) = 𝑥 ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdiv ⊢ /
1 vx ⊢ 𝑥
2 cc ⊢ ℂ
3 vy ⊢ 𝑦
4 cc0 ⊢ 0
5 4 csn ⊢ { 0 }
6 2 5 cdif ⊢ ( ℂ ∖ { 0 } )
7 vz ⊢ 𝑧
8 3 cv ⊢ 𝑦
9 cmul ⊢ ·
10 7 cv ⊢ 𝑧
11 8 10 9 co ⊢ ( 𝑦 · 𝑧 )
12 1 cv ⊢ 𝑥
13 11 12 wceq ⊢ ( 𝑦 · 𝑧 ) = 𝑥
14 13 7 2 crio ⊢ ( ℩ 𝑧 ∈ ℂ ( 𝑦 · 𝑧 ) = 𝑥 )
15 1 3 2 6 14 cmpo ⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℩ 𝑧 ∈ ℂ ( 𝑦 · 𝑧 ) = 𝑥 ) )
16 0 15 wceq ⊢ / = ( 𝑥 ∈ ℂ , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℩ 𝑧 ∈ ℂ ( 𝑦 · 𝑧 ) = 𝑥 ) )