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