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 e. CC , y e. ( CC \ { 0 } ) |-> ( iota_ z e. CC ( y x. z ) = x ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdiv	|- /
1		vx	|- x
2		cc	|- CC
3		vy	|- y
4		cc0	|- 0
5	4	csn	|- { 0 }
6	2 5	cdif	|- ( CC \ { 0 } )
7		vz	|- z
8	3	cv	|- y
9		cmul	|- x.
10	7	cv	|- z
11	8 10 9	co	|- ( y x. z )
12	1	cv	|- x
13	11 12	wceq	|- ( y x. z ) = x
14	13 7 2	crio	|- ( iota_ z e. CC ( y x. z ) = x )
15	1 3 2 6 14	cmpo	|- ( x e. CC , y e. ( CC \ { 0 } ) |-> ( iota_ z e. CC ( y x. z ) = x ) )
16	0 15	wceq	|- / = ( x e. CC , y e. ( CC \ { 0 } ) |-> ( iota_ z e. CC ( y x. z ) = x ) )