Theorem divcl

Description: Closure law for division. (Contributed by NM, 21-Jul-2001) (Proof shortened by Mario Carneiro, 17-Feb-2014)

	Ref	Expression
Assertion	divcl	|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A / B ) e. CC )

Proof

Step	Hyp	Ref	Expression
1		divval	|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A / B ) = ( iota_ x e. CC ( B x. x ) = A ) )
2		receu	|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> E! x e. CC ( B x. x ) = A )
3		riotacl	|- ( E! x e. CC ( B x. x ) = A -> ( iota_ x e. CC ( B x. x ) = A ) e. CC )
4	2 3	syl	|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( iota_ x e. CC ( B x. x ) = A ) e. CC )
5	1 4	eqeltrd	|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A / B ) e. CC )