Theorem addclnq

Description: Closure of addition on positive fractions. (Contributed by NM, 29-Aug-1995) (Revised by Mario Carneiro, 8-May-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	addclnq	$$⊢\left(A\in 𝑸\wedge B\in 𝑸\right)\to A{+}_{𝑸}B\in 𝑸$$

Proof

Step	Hyp	Ref	Expression
1		addpqnq	$$⊢\left(A\in 𝑸\wedge B\in 𝑸\right)\to A{+}_{𝑸}B={/}_{𝑸}\left(A{+}_{\mathrm{𝑝𝑸}}B\right)$$
2		elpqn	$$⊢A\in 𝑸\to A\in \left(𝑵\times 𝑵\right)$$
3		elpqn	$$⊢B\in 𝑸\to B\in \left(𝑵\times 𝑵\right)$$
4		addpqf	$$⊢{+}_{\mathrm{𝑝𝑸}}:\left(𝑵\times 𝑵\right)\times \left(𝑵\times 𝑵\right)⟶𝑵\times 𝑵$$
5	4	fovcl	$$⊢\left(A\in \left(𝑵\times 𝑵\right)\wedge B\in \left(𝑵\times 𝑵\right)\right)\to A{+}_{\mathrm{𝑝𝑸}}B\in \left(𝑵\times 𝑵\right)$$
6	2 3 5	syl2an	$$⊢\left(A\in 𝑸\wedge B\in 𝑸\right)\to A{+}_{\mathrm{𝑝𝑸}}B\in \left(𝑵\times 𝑵\right)$$
7		nqercl	$$⊢A{+}_{\mathrm{𝑝𝑸}}B\in \left(𝑵\times 𝑵\right)\to {/}_{𝑸}\left(A{+}_{\mathrm{𝑝𝑸}}B\right)\in 𝑸$$
8	6 7	syl	$$⊢\left(A\in 𝑸\wedge B\in 𝑸\right)\to {/}_{𝑸}\left(A{+}_{\mathrm{𝑝𝑸}}B\right)\in 𝑸$$
9	1 8	eqeltrd	$$⊢\left(A\in 𝑸\wedge B\in 𝑸\right)\to A{+}_{𝑸}B\in 𝑸$$