Metamath Proof Explorer


Theorem xdivcld

Description: Closure law for the extended division. (Contributed by Thierry Arnoux, 15-Mar-2017)

Ref Expression
Hypotheses xdivcld.1
|- ( ph -> A e. RR* )
xdivcld.2
|- ( ph -> B e. RR )
xdivcld.3
|- ( ph -> B =/= 0 )
Assertion xdivcld
|- ( ph -> ( A /e B ) e. RR* )

Proof

Step Hyp Ref Expression
1 xdivcld.1
 |-  ( ph -> A e. RR* )
2 xdivcld.2
 |-  ( ph -> B e. RR )
3 xdivcld.3
 |-  ( ph -> B =/= 0 )
4 xdivval
 |-  ( ( A e. RR* /\ B e. RR /\ B =/= 0 ) -> ( A /e B ) = ( iota_ x e. RR* ( B *e x ) = A ) )
5 1 2 3 4 syl3anc
 |-  ( ph -> ( A /e B ) = ( iota_ x e. RR* ( B *e x ) = A ) )
6 xreceu
 |-  ( ( A e. RR* /\ B e. RR /\ B =/= 0 ) -> E! x e. RR* ( B *e x ) = A )
7 1 2 3 6 syl3anc
 |-  ( ph -> E! x e. RR* ( B *e x ) = A )
8 riotacl
 |-  ( E! x e. RR* ( B *e x ) = A -> ( iota_ x e. RR* ( B *e x ) = A ) e. RR* )
9 7 8 syl
 |-  ( ph -> ( iota_ x e. RR* ( B *e x ) = A ) e. RR* )
10 5 9 eqeltrd
 |-  ( ph -> ( A /e B ) e. RR* )