Theorem qmulcl 9631

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

Assertion

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

Proof of Theorem qmulcl

Dummy variables x y z w v u are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elq 9616	. 2 |- ( A e. QQ <-> E. x e. ZZ E. y e. NN A = ( x / y ) )
2		elq 9616	. 2 |- ( B e. QQ <-> E. z e. ZZ E. w e. NN B = ( z / w ) )
3		zmulcl 9300	. . . . . . . . . . 11 |- ( ( x e. ZZ /\ z e. ZZ ) -> ( x x. z ) e. ZZ )
4		nnmulcl 8934	. . . . . . . . . . 11 |- ( ( y e. NN /\ w e. NN ) -> ( y x. w ) e. NN )
5	3, 4	anim12i 338	. . . . . . . . . 10 |- ( ( ( 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 588	. . . . . . . . 9 |- ( ( ( x e. ZZ /\ y e. NN ) /\ ( z e. ZZ /\ w e. NN ) ) -> ( ( x x. z ) e. ZZ /\ ( y x. w ) e. NN ) )
7	6	adantr 276	. . . . . . . 8 |- ( ( ( ( x e. ZZ /\ y e. NN ) /\ ( z e. ZZ /\ w e. NN ) ) /\ ( A = ( x / y ) /\ B = ( z / w ) ) ) -> ( ( x x. z ) e. ZZ /\ ( y x. w ) e. NN ) )
8		oveq12 5879	. . . . . . . . 9 |- ( ( A = ( x / y ) /\ B = ( z / w ) ) -> ( A x. B ) = ( ( x / y ) x. ( z / w ) ) )
9		zcn 9252	. . . . . . . . . . . 12 |- ( x e. ZZ -> x e. CC )
10		zcn 9252	. . . . . . . . . . . 12 |- ( z e. ZZ -> z e. CC )
11	9, 10	anim12i 338	. . . . . . . . . . 11 |- ( ( x e. ZZ /\ z e. ZZ ) -> ( x e. CC /\ z e. CC ) )
12	11	ad2ant2r 509	. . . . . . . . . 10 |- ( ( ( x e. ZZ /\ y e. NN ) /\ ( z e. ZZ /\ w e. NN ) ) -> ( x e. CC /\ z e. CC ) )
13		nncn 8921	. . . . . . . . . . . . 13 |- ( y e. NN -> y e. CC )
14		nnap0 8942	. . . . . . . . . . . . 13 |- ( y e. NN -> y # 0 )
15	13, 14	jca 306	. . . . . . . . . . . 12 |- ( y e. NN -> ( y e. CC /\ y # 0 ) )
16		nncn 8921	. . . . . . . . . . . . 13 |- ( w e. NN -> w e. CC )
17		nnap0 8942	. . . . . . . . . . . . 13 |- ( w e. NN -> w # 0 )
18	16, 17	jca 306	. . . . . . . . . . . 12 |- ( w e. NN -> ( w e. CC /\ w # 0 ) )
19	15, 18	anim12i 338	. . . . . . . . . . 11 |- ( ( y e. NN /\ w e. NN ) -> ( ( y e. CC /\ y # 0 ) /\ ( w e. CC /\ w # 0 ) ) )
20	19	ad2ant2l 508	. . . . . . . . . 10 |- ( ( ( x e. ZZ /\ y e. NN ) /\ ( z e. ZZ /\ w e. NN ) ) -> ( ( y e. CC /\ y # 0 ) /\ ( w e. CC /\ w # 0 ) ) )
21		divmuldivap 8663	. . . . . . . . . 10 |- ( ( ( 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 ) ) )
22	12, 20, 21	syl2anc 411	. . . . . . . . 9 |- ( ( ( x e. ZZ /\ y e. NN ) /\ ( z e. ZZ /\ w e. NN ) ) -> ( ( x / y ) x. ( z / w ) ) = ( ( x x. z ) / ( y x. w ) ) )
23	8, 22	sylan9eqr 2232	. . . . . . . 8 |- ( ( ( ( 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 ) ) )
24		rspceov 5912	. . . . . . . . . 10 |- ( ( ( 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	24	3expa 1203	. . . . . . . . 9 |- ( ( ( ( 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 ) )
26		elq 9616	. . . . . . . . 9 |- ( ( A x. B ) e. QQ <-> E. v e. ZZ E. u e. NN ( A x. B ) = ( v / u ) )
27	25, 26	sylibr 134	. . . . . . . 8 |- ( ( ( ( x x. z ) e. ZZ /\ ( y x. w ) e. NN ) /\ ( A x. B ) = ( ( x x. z ) / ( y x. w ) ) ) -> ( A x. B ) e. QQ )
28	7, 23, 27	syl2anc 411	. . . . . . 7 |- ( ( ( ( x e. ZZ /\ y e. NN ) /\ ( z e. ZZ /\ w e. NN ) ) /\ ( A = ( x / y ) /\ B = ( z / w ) ) ) -> ( A x. B ) e. QQ )
29	28	an4s 588	. . . . . 6 |- ( ( ( ( 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	exp43 372	. . . . 5 |- ( ( x e. ZZ /\ y e. NN ) -> ( A = ( x / y ) -> ( ( z e. ZZ /\ w e. NN ) -> ( B = ( z / w ) -> ( A x. B ) e. QQ ) ) ) )
31	30	rexlimivv 2600	. . . 4 |- ( 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 ) ) )
32	31	rexlimdvv 2601	. . 3 |- ( 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	32	imp 124	. 2 |- ( ( 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 )
34	1, 2, 33	syl2anb 291	1 |- ( ( A e. QQ /\ B e. QQ ) -> ( A x. B ) e. QQ )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1353   e. wcel 2148   E.wrex 2456   class class class wbr 4001  (class class class)co 5870   CCcc 7804   0cc0 7806   x. cmul 7811   # cap 8532   / cdiv 8623   NNcn 8913   ZZcz 9247   QQcq 9613

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4119  ax-pow 4172  ax-pr 4207  ax-un 4431  ax-setind 4534  ax-cnex 7897  ax-resscn 7898  ax-1cn 7899  ax-1re 7900  ax-icn 7901  ax-addcl 7902  ax-addrcl 7903  ax-mulcl 7904  ax-mulrcl 7905  ax-addcom 7906  ax-mulcom 7907  ax-addass 7908  ax-mulass 7909  ax-distr 7910  ax-i2m1 7911  ax-0lt1 7912  ax-1rid 7913  ax-0id 7914  ax-rnegex 7915  ax-precex 7916  ax-cnre 7917  ax-pre-ltirr 7918  ax-pre-ltwlin 7919  ax-pre-lttrn 7920  ax-pre-apti 7921  ax-pre-ltadd 7922  ax-pre-mulgt0 7923  ax-pre-mulext 7924

This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rmo 2463  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3809  df-int 3844  df-iun 3887  df-br 4002  df-opab 4063  df-mpt 4064  df-id 4291  df-po 4294  df-iso 4295  df-xp 4630  df-rel 4631  df-cnv 4632  df-co 4633  df-dm 4634  df-rn 4635  df-res 4636  df-ima 4637  df-iota 5175  df-fun 5215  df-fn 5216  df-f 5217  df-fv 5221  df-riota 5826  df-ov 5873  df-oprab 5874  df-mpo 5875  df-1st 6136  df-2nd 6137  df-pnf 7988  df-mnf 7989  df-xr 7990  df-ltxr 7991  df-le 7992  df-sub 8124  df-neg 8125  df-reap 8526  df-ap 8533  df-div 8624  df-inn 8914  df-n0 9171  df-z 9248  df-q 9614

This theorem is referenced by:  qdivcl  9637  flqmulnn0  10292  modqcl  10319  mulqmod0  10323  modqmulnn  10335  modqcyc  10352  mulp1mod1  10358  modqmul1  10370  q2txmodxeq0  10377  modqaddmulmod  10384  modqdi  10385  modqsubdir  10386  qexpcl  10529  qexpclz  10534  qsqcl  10584  dvdslelemd  11839  crth  12214  pcaddlem  12328  apdifflemr  14566  apdiff  14567