Definition df-div 6892

Description: Define division. Theorem divmuli 6894 relates it to multiplication, and divcli 6899 and redivcli 6976 prove its closure laws.

Assertion

Ref	Expression
df-div	|- / = {<.<.x, y>., z>. | ((x e. CC /\ y e. (CC \ {0})) /\ z = (iota_w e. CC(y x. w) = x))}

Distinct variable group:   x,y,z,w

Detailed syntax breakdown of Definition df-div

Step	Hyp	Ref	Expression
1		cdiv 6447	. 2 class /
2		vx	. . . . . . 7 set x
3	2	cv 1297	. . . . . 6 class x
4		cc 6384	. . . . . 6 class CC
5	3, 4	wcel 1300	. . . . 5 wff x e. CC
6		vy	. . . . . . 7 set y
7	6	cv 1297	. . . . . 6 class y
8		cc0 6386	. . . . . . . 8 class 0
9	8	csn 3044	. . . . . . 7 class {0}
10	4, 9	cdif 2590	. . . . . 6 class (CC \ {0})
11	7, 10	wcel 1300	. . . . 5 wff y e. (CC \ {0})
12	5, 11	wa 240	. . . 4 wff (x e. CC /\ y e. (CC \ {0}))
13		vz	. . . . . 6 set z
14	13	cv 1297	. . . . 5 class z
15		vw	. . . . . . . . 9 set w
16	15	cv 1297	. . . . . . . 8 class w
17		cmul 6391	. . . . . . . 8 class x.
18	7, 16, 17	co 4884	. . . . . . 7 class (y x. w)
19	18, 3	wceq 1298	. . . . . 6 wff (y x. w) = x
20	19, 15, 4	crio 5555	. . . . 5 class (iota_w e. CC(y x. w) = x)
21	14, 20	wceq 1298	. . . 4 wff z = (iota_w e. CC(y x. w) = x)
22	12, 21	wa 240	. . 3 wff ((x e. CC /\ y e. (CC \ {0})) /\ z = (iota_w e. CC(y x. w) = x))
23	22, 2, 6, 13	copab2 4885	. 2 class {<.<.x, y>., z>. | ((x e. CC /\ y e. (CC \ {0})) /\ z = (iota_w e. CC(y x. w) = x))}
24	1, 23	wceq 1298	1 wff / = {<.<.x, y>., z>. | ((x e. CC /\ y e. (CC \ {0})) /\ z = (iota_w e. CC(y x. w) = x))}

This definition is referenced by:  divvali 6893

Copyright terms: Public domain