Definition df-xdiv

Description: Define division over extended real numbers. (Contributed by Thierry Arnoux, 17-Dec-2016)

	Ref	Expression
Assertion	df-xdiv	|- /e = ( x e. RR* , y e. ( RR \ { 0 } ) |-> ( iota_ z e. RR* ( y *e z ) = x ) )

Detailed syntax breakdown

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