This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem qdivcl

Description: Closure of division of rationals. (Contributed by NM, 3-Aug-2004)

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

Proof

Step Hyp Ref Expression
1 qcn 
 |-  ( A e. QQ -> A e. CC )
2 qcn 
 |-  ( B e. QQ -> B e. CC )
3 id 
 |-  ( B =/= 0 -> B =/= 0 )
4 divrec 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A / B ) = ( A x. ( 1 / B ) ) )
5 1 2 3 4 syl3an 
 |-  ( ( A e. QQ /\ B e. QQ /\ B =/= 0 ) -> ( A / B ) = ( A x. ( 1 / B ) ) )
6 qreccl 
 |-  ( ( B e. QQ /\ B =/= 0 ) -> ( 1 / B ) e. QQ )
7 qmulcl 
 |-  ( ( A e. QQ /\ ( 1 / B ) e. QQ ) -> ( A x. ( 1 / B ) ) e. QQ )
8 6 7 sylan2 
 |-  ( ( A e. QQ /\ ( B e. QQ /\ B =/= 0 ) ) -> ( A x. ( 1 / B ) ) e. QQ )
9 8 3impb 
 |-  ( ( A e. QQ /\ B e. QQ /\ B =/= 0 ) -> ( A x. ( 1 / B ) ) e. QQ )
10 5 9 eqeltrd 
 |-  ( ( A e. QQ /\ B e. QQ /\ B =/= 0 ) -> ( A / B ) e. QQ )