Metamath Proof Explorer

Theorem xdivcl

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

Ref Expression
Assertion xdivcl 
|- ( ( A e. RR* /\ B e. RR /\ B =/= 0 ) -> ( A /e B ) e. RR* )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A e. RR* /\ B e. RR /\ B =/= 0 ) -> A e. RR* )
2 simp2 
 |-  ( ( A e. RR* /\ B e. RR /\ B =/= 0 ) -> B e. RR )
3 simp3 
 |-  ( ( A e. RR* /\ B e. RR /\ B =/= 0 ) -> B =/= 0 )
4 1 2 3 xdivcld 
 |-  ( ( A e. RR* /\ B e. RR /\ B =/= 0 ) -> ( A /e B ) e. RR* )