qmulcl

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

		Ref	Expression
	Assertion	qmulcl	$⊢ (A \in ℚ \land B \in ℚ) \to A B \in ℚ$

Proof

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

Metamath Proof Explorer

Theorem qmulcl

Proof