Metamath Proof Explorer

Theorem qmulcl

Description: Closure of multiplication of rationals. (Contributed by NM, 1-Aug-2004)

Ref Expression
Assertion qmulcl 
|- ( ( A e. QQ /\ B e. QQ ) -> ( A x. B ) e. QQ )

Proof

Step Hyp Ref Expression
1 elq 
 |-  ( A e. QQ <-> E. x e. ZZ E. y e. NN A = ( x / y ) )
2 elq 
 |-  ( B e. QQ <-> E. z e. ZZ E. w e. NN B = ( z / w ) )
3 zmulcl 
 |-  ( ( x e. ZZ /\ z e. ZZ ) -> ( x x. z ) e. ZZ )
4 nnmulcl 
 |-  ( ( y e. NN /\ w e. NN ) -> ( y x. w ) e. NN )
5 3 4 anim12i 
 |-  ( ( ( x e. ZZ /\ z e. ZZ ) /\ ( y e. NN /\ w e. NN ) ) -> ( ( x x. z ) e. ZZ /\ ( y x. w ) e. NN ) )
6 5 an4s 
 |-  ( ( ( x e. ZZ /\ y e. NN ) /\ ( z e. ZZ /\ w e. NN ) ) -> ( ( x x. z ) e. ZZ /\ ( y x. w ) e. NN ) )
7 oveq12 
 |-  ( ( A = ( x / y ) /\ B = ( z / w ) ) -> ( A x. B ) = ( ( x / y ) x. ( z / w ) ) )
8 zcn 
 |-  ( x e. ZZ -> x e. CC )
9 zcn 
 |-  ( z e. ZZ -> z e. CC )
10 8 9 anim12i 
 |-  ( ( x e. ZZ /\ z e. ZZ ) -> ( x e. CC /\ z e. CC ) )
11 10 ad2ant2r 
 |-  ( ( ( x e. ZZ /\ y e. NN ) /\ ( z e. ZZ /\ w e. NN ) ) -> ( x e. CC /\ z e. CC ) )
12 nncn 
 |-  ( y e. NN -> y e. CC )
13 nnne0 
 |-  ( y e. NN -> y =/= 0 )
14 12 13 jca 
 |-  ( y e. NN -> ( y e. CC /\ y =/= 0 ) )
15 nncn 
 |-  ( w e. NN -> w e. CC )
16 nnne0 
 |-  ( w e. NN -> w =/= 0 )
17 15 16 jca 
 |-  ( w e. NN -> ( w e. CC /\ w =/= 0 ) )
18 14 17 anim12i 
 |-  ( ( y e. NN /\ w e. NN ) -> ( ( y e. CC /\ y =/= 0 ) /\ ( w e. CC /\ w =/= 0 ) ) )
19 18 ad2ant2l 
 |-  ( ( ( x e. ZZ /\ y e. NN ) /\ ( z e. ZZ /\ w e. NN ) ) -> ( ( y e. CC /\ y =/= 0 ) /\ ( w e. CC /\ w =/= 0 ) ) )
20 divmuldiv 
 |-  ( ( ( x e. CC /\ z e. CC ) /\ ( ( y e. CC /\ y =/= 0 ) /\ ( w e. CC /\ w =/= 0 ) ) ) -> ( ( x / y ) x. ( z / w ) ) = ( ( x x. z ) / ( y x. w ) ) )
21 11 19 20 syl2anc 
 |-  ( ( ( x e. ZZ /\ y e. NN ) /\ ( z e. ZZ /\ w e. NN ) ) -> ( ( x / y ) x. ( z / w ) ) = ( ( x x. z ) / ( y x. w ) ) )
22 7 21 sylan9eqr 
 |-  ( ( ( ( x e. ZZ /\ y e. NN ) /\ ( z e. ZZ /\ w e. NN ) ) /\ ( A = ( x / y ) /\ B = ( z / w ) ) ) -> ( A x. B ) = ( ( x x. z ) / ( y x. w ) ) )
23 rspceov 
 |-  ( ( ( x x. z ) e. ZZ /\ ( y x. w ) e. NN /\ ( A x. B ) = ( ( x x. z ) / ( y x. w ) ) ) -> E. v e. ZZ E. u e. NN ( A x. B ) = ( v / u ) )
24 23 3expa 
 |-  ( ( ( ( x x. z ) e. ZZ /\ ( y x. w ) e. NN ) /\ ( A x. B ) = ( ( x x. z ) / ( y x. w ) ) ) -> E. v e. ZZ E. u e. NN ( A x. B ) = ( v / u ) )
25 elq 
 |-  ( ( A x. B ) e. QQ <-> E. v e. ZZ E. u e. NN ( A x. B ) = ( v / u ) )
26 24 25 sylibr 
 |-  ( ( ( ( x x. z ) e. ZZ /\ ( y x. w ) e. NN ) /\ ( A x. B ) = ( ( x x. z ) / ( y x. w ) ) ) -> ( A x. B ) e. QQ )
27 6 22 26 syl2an2r 
 |-  ( ( ( ( x e. ZZ /\ y e. NN ) /\ ( z e. ZZ /\ w e. NN ) ) /\ ( A = ( x / y ) /\ B = ( z / w ) ) ) -> ( A x. B ) e. QQ )
28 27 an4s 
 |-  ( ( ( ( x e. ZZ /\ y e. NN ) /\ A = ( x / y ) ) /\ ( ( z e. ZZ /\ w e. NN ) /\ B = ( z / w ) ) ) -> ( A x. B ) e. QQ )
29 28 exp43 
 |-  ( ( x e. ZZ /\ y e. NN ) -> ( A = ( x / y ) -> ( ( z e. ZZ /\ w e. NN ) -> ( B = ( z / w ) -> ( A x. B ) e. QQ ) ) ) )
30 29 rexlimivv 
 |-  ( E. x e. ZZ E. y e. NN A = ( x / y ) -> ( ( z e. ZZ /\ w e. NN ) -> ( B = ( z / w ) -> ( A x. B ) e. QQ ) ) )
31 30 rexlimdvv 
 |-  ( E. x e. ZZ E. y e. NN A = ( x / y ) -> ( E. z e. ZZ E. w e. NN B = ( z / w ) -> ( A x. B ) e. QQ ) )
32 31 imp 
 |-  ( ( E. x e. ZZ E. y e. NN A = ( x / y ) /\ E. z e. ZZ E. w e. NN B = ( z / w ) ) -> ( A x. B ) e. QQ )
33 1 2 32 syl2anb 
 |-  ( ( A e. QQ /\ B e. QQ ) -> ( A x. B ) e. QQ )