Metamath Proof Explorer

Theorem qmulcl

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

Ref Expression
Assertion qmulcl ${⊢}\left({A}\in ℚ\wedge {B}\in ℚ\right)\to {A}{B}\in ℚ$

Proof

Step Hyp Ref Expression
1 elq ${⊢}{A}\in ℚ↔\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}{A}=\frac{{x}}{{y}}$
2 elq ${⊢}{B}\in ℚ↔\exists {z}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {w}\in ℕ\phantom{\rule{.4em}{0ex}}{B}=\frac{{z}}{{w}}$
3 zmulcl ${⊢}\left({x}\in ℤ\wedge {z}\in ℤ\right)\to {x}{z}\in ℤ$
4 nnmulcl ${⊢}\left({y}\in ℕ\wedge {w}\in ℕ\right)\to {y}{w}\in ℕ$
5 3 4 anim12i ${⊢}\left(\left({x}\in ℤ\wedge {z}\in ℤ\right)\wedge \left({y}\in ℕ\wedge {w}\in ℕ\right)\right)\to \left({x}{z}\in ℤ\wedge {y}{w}\in ℕ\right)$
6 5 an4s ${⊢}\left(\left({x}\in ℤ\wedge {y}\in ℕ\right)\wedge \left({z}\in ℤ\wedge {w}\in ℕ\right)\right)\to \left({x}{z}\in ℤ\wedge {y}{w}\in ℕ\right)$
7 oveq12 ${⊢}\left({A}=\frac{{x}}{{y}}\wedge {B}=\frac{{z}}{{w}}\right)\to {A}{B}=\left(\frac{{x}}{{y}}\right)\left(\frac{{z}}{{w}}\right)$
8 zcn ${⊢}{x}\in ℤ\to {x}\in ℂ$
9 zcn ${⊢}{z}\in ℤ\to {z}\in ℂ$
10 8 9 anim12i ${⊢}\left({x}\in ℤ\wedge {z}\in ℤ\right)\to \left({x}\in ℂ\wedge {z}\in ℂ\right)$
11 10 ad2ant2r ${⊢}\left(\left({x}\in ℤ\wedge {y}\in ℕ\right)\wedge \left({z}\in ℤ\wedge {w}\in ℕ\right)\right)\to \left({x}\in ℂ\wedge {z}\in ℂ\right)$
12 nncn ${⊢}{y}\in ℕ\to {y}\in ℂ$
13 nnne0 ${⊢}{y}\in ℕ\to {y}\ne 0$
14 12 13 jca ${⊢}{y}\in ℕ\to \left({y}\in ℂ\wedge {y}\ne 0\right)$
15 nncn ${⊢}{w}\in ℕ\to {w}\in ℂ$
16 nnne0 ${⊢}{w}\in ℕ\to {w}\ne 0$
17 15 16 jca ${⊢}{w}\in ℕ\to \left({w}\in ℂ\wedge {w}\ne 0\right)$
18 14 17 anim12i ${⊢}\left({y}\in ℕ\wedge {w}\in ℕ\right)\to \left(\left({y}\in ℂ\wedge {y}\ne 0\right)\wedge \left({w}\in ℂ\wedge {w}\ne 0\right)\right)$
19 18 ad2ant2l ${⊢}\left(\left({x}\in ℤ\wedge {y}\in ℕ\right)\wedge \left({z}\in ℤ\wedge {w}\in ℕ\right)\right)\to \left(\left({y}\in ℂ\wedge {y}\ne 0\right)\wedge \left({w}\in ℂ\wedge {w}\ne 0\right)\right)$
20 divmuldiv ${⊢}\left(\left({x}\in ℂ\wedge {z}\in ℂ\right)\wedge \left(\left({y}\in ℂ\wedge {y}\ne 0\right)\wedge \left({w}\in ℂ\wedge {w}\ne 0\right)\right)\right)\to \left(\frac{{x}}{{y}}\right)\left(\frac{{z}}{{w}}\right)=\frac{{x}{z}}{{y}{w}}$
21 11 19 20 syl2anc ${⊢}\left(\left({x}\in ℤ\wedge {y}\in ℕ\right)\wedge \left({z}\in ℤ\wedge {w}\in ℕ\right)\right)\to \left(\frac{{x}}{{y}}\right)\left(\frac{{z}}{{w}}\right)=\frac{{x}{z}}{{y}{w}}$
22 7 21 sylan9eqr ${⊢}\left(\left(\left({x}\in ℤ\wedge {y}\in ℕ\right)\wedge \left({z}\in ℤ\wedge {w}\in ℕ\right)\right)\wedge \left({A}=\frac{{x}}{{y}}\wedge {B}=\frac{{z}}{{w}}\right)\right)\to {A}{B}=\frac{{x}{z}}{{y}{w}}$
23 rspceov ${⊢}\left({x}{z}\in ℤ\wedge {y}{w}\in ℕ\wedge {A}{B}=\frac{{x}{z}}{{y}{w}}\right)\to \exists {v}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {u}\in ℕ\phantom{\rule{.4em}{0ex}}{A}{B}=\frac{{v}}{{u}}$
24 23 3expa ${⊢}\left(\left({x}{z}\in ℤ\wedge {y}{w}\in ℕ\right)\wedge {A}{B}=\frac{{x}{z}}{{y}{w}}\right)\to \exists {v}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {u}\in ℕ\phantom{\rule{.4em}{0ex}}{A}{B}=\frac{{v}}{{u}}$
25 elq ${⊢}{A}{B}\in ℚ↔\exists {v}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {u}\in ℕ\phantom{\rule{.4em}{0ex}}{A}{B}=\frac{{v}}{{u}}$
26 24 25 sylibr ${⊢}\left(\left({x}{z}\in ℤ\wedge {y}{w}\in ℕ\right)\wedge {A}{B}=\frac{{x}{z}}{{y}{w}}\right)\to {A}{B}\in ℚ$
27 6 22 26 syl2an2r ${⊢}\left(\left(\left({x}\in ℤ\wedge {y}\in ℕ\right)\wedge \left({z}\in ℤ\wedge {w}\in ℕ\right)\right)\wedge \left({A}=\frac{{x}}{{y}}\wedge {B}=\frac{{z}}{{w}}\right)\right)\to {A}{B}\in ℚ$
28 27 an4s ${⊢}\left(\left(\left({x}\in ℤ\wedge {y}\in ℕ\right)\wedge {A}=\frac{{x}}{{y}}\right)\wedge \left(\left({z}\in ℤ\wedge {w}\in ℕ\right)\wedge {B}=\frac{{z}}{{w}}\right)\right)\to {A}{B}\in ℚ$
29 28 exp43 ${⊢}\left({x}\in ℤ\wedge {y}\in ℕ\right)\to \left({A}=\frac{{x}}{{y}}\to \left(\left({z}\in ℤ\wedge {w}\in ℕ\right)\to \left({B}=\frac{{z}}{{w}}\to {A}{B}\in ℚ\right)\right)\right)$
30 29 rexlimivv ${⊢}\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}{A}=\frac{{x}}{{y}}\to \left(\left({z}\in ℤ\wedge {w}\in ℕ\right)\to \left({B}=\frac{{z}}{{w}}\to {A}{B}\in ℚ\right)\right)$
31 30 rexlimdvv ${⊢}\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}{A}=\frac{{x}}{{y}}\to \left(\exists {z}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {w}\in ℕ\phantom{\rule{.4em}{0ex}}{B}=\frac{{z}}{{w}}\to {A}{B}\in ℚ\right)$
32 31 imp ${⊢}\left(\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {y}\in ℕ\phantom{\rule{.4em}{0ex}}{A}=\frac{{x}}{{y}}\wedge \exists {z}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {w}\in ℕ\phantom{\rule{.4em}{0ex}}{B}=\frac{{z}}{{w}}\right)\to {A}{B}\in ℚ$
33 1 2 32 syl2anb ${⊢}\left({A}\in ℚ\wedge {B}\in ℚ\right)\to {A}{B}\in ℚ$