qdivcl

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

		Ref	Expression
	Assertion	qdivcl	$⊢ (A \in ℚ \land B \in ℚ \land B \neq 0) \to \frac{A}{B} \in ℚ$

Step	Hyp	Ref	Expression
1		qcn	$⊢ A \in ℚ \to A \in ℂ$
2		qcn	$⊢ B \in ℚ \to B \in ℂ$
3		id	$⊢ B \neq 0 \to B \neq 0$
4		divrec	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to \frac{A}{B} = A (\frac{1}{B})$
5	1 2 3 4	syl3an	$⊢ (A \in ℚ \land B \in ℚ \land B \neq 0) \to \frac{A}{B} = A (\frac{1}{B})$
6		qreccl	$⊢ (B \in ℚ \land B \neq 0) \to \frac{1}{B} \in ℚ$
7		qmulcl	$⊢ (A \in ℚ \land \frac{1}{B} \in ℚ) \to A (\frac{1}{B}) \in ℚ$
8	6 7	sylan2	$⊢ (A \in ℚ \land (B \in ℚ \land B \neq 0)) \to A (\frac{1}{B}) \in ℚ$
9	8	3impb	$⊢ (A \in ℚ \land B \in ℚ \land B \neq 0) \to A (\frac{1}{B}) \in ℚ$
10	5 9	eqeltrd	$⊢ (A \in ℚ \land B \in ℚ \land B \neq 0) \to \frac{A}{B} \in ℚ$

Metamath Proof Explorer