Theorem qdivcl

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

	Ref	Expression
Assertion	qdivcl	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) → ( 𝐴 / 𝐵 ) ∈ ℚ )

Proof

Step	Hyp	Ref	Expression
1		qcn	⊢ ( 𝐴 ∈ ℚ → 𝐴 ∈ ℂ )
2		qcn	⊢ ( 𝐵 ∈ ℚ → 𝐵 ∈ ℂ )
3		id	⊢ ( 𝐵 ≠ 0 → 𝐵 ≠ 0 )
4		divrec	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( 𝐴 / 𝐵 ) = ( 𝐴 · ( 1 / 𝐵 ) ) )
5	1 2 3 4	syl3an	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) → ( 𝐴 / 𝐵 ) = ( 𝐴 · ( 1 / 𝐵 ) ) )
6		qreccl	⊢ ( ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) → ( 1 / 𝐵 ) ∈ ℚ )
7		qmulcl	⊢ ( ( 𝐴 ∈ ℚ ∧ ( 1 / 𝐵 ) ∈ ℚ ) → ( 𝐴 · ( 1 / 𝐵 ) ) ∈ ℚ )
8	6 7	sylan2	⊢ ( ( 𝐴 ∈ ℚ ∧ ( 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 · ( 1 / 𝐵 ) ) ∈ ℚ )
9	8	3impb	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) → ( 𝐴 · ( 1 / 𝐵 ) ) ∈ ℚ )
10	5 9	eqeltrd	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0 ) → ( 𝐴 / 𝐵 ) ∈ ℚ )