qaddcl

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

		Ref	Expression
	Assertion	qaddcl	$⊢ (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		nnz	$⊢ w \in ℕ \to w \in ℤ$
4		zmulcl	$⊢ (x \in ℤ \land w \in ℤ) \to x w \in ℤ$
5	3 4	sylan2	$⊢ (x \in ℤ \land w \in ℕ) \to x w \in ℤ$
6	5	ad2ant2rl	$⊢ ((x \in ℤ \land y \in ℕ) \land (z \in ℤ \land w \in ℕ)) \to x w \in ℤ$
7		simpl	$⊢ (z \in ℤ \land w \in ℕ) \to z \in ℤ$
8		nnz	$⊢ y \in ℕ \to y \in ℤ$
9	8	adantl	$⊢ (x \in ℤ \land y \in ℕ) \to y \in ℤ$
10		zmulcl	$⊢ (z \in ℤ \land y \in ℤ) \to z y \in ℤ$
11	7 9 10	syl2anr	$⊢ ((x \in ℤ \land y \in ℕ) \land (z \in ℤ \land w \in ℕ)) \to z y \in ℤ$
12	6 11	zaddcld	$⊢ ((x \in ℤ \land y \in ℕ) \land (z \in ℤ \land w \in ℕ)) \to x w + z y \in ℤ$
13	12	adantr	$⊢ (((x \in ℤ \land y \in ℕ) \land (z \in ℤ \land w \in ℕ)) \land (A = \frac{x}{y} \land B = \frac{z}{w})) \to x w + z y \in ℤ$
14		nnmulcl	$⊢ (y \in ℕ \land w \in ℕ) \to y w \in ℕ$
15	14	ad2ant2l	$⊢ ((x \in ℤ \land y \in ℕ) \land (z \in ℤ \land w \in ℕ)) \to y w \in ℕ$
16	15	adantr	$⊢ (((x \in ℤ \land y \in ℕ) \land (z \in ℤ \land w \in ℕ)) \land (A = \frac{x}{y} \land B = \frac{z}{w})) \to y w \in ℕ$
17		oveq12	$⊢ (A = \frac{x}{y} \land B = \frac{z}{w}) \to A + B = (\frac{x}{y}) + (\frac{z}{w})$
18		zcn	$⊢ x \in ℤ \to x \in ℂ$
19		zcn	$⊢ z \in ℤ \to z \in ℂ$
20	18 19	anim12i	$⊢ (x \in ℤ \land z \in ℤ) \to (x \in ℂ \land z \in ℂ)$
21		nncn	$⊢ y \in ℕ \to y \in ℂ$
22		nnne0	$⊢ y \in ℕ \to y \neq 0$
23	21 22	jca	$⊢ y \in ℕ \to (y \in ℂ \land y \neq 0)$
24		nncn	$⊢ w \in ℕ \to w \in ℂ$
25		nnne0	$⊢ w \in ℕ \to w \neq 0$
26	24 25	jca	$⊢ w \in ℕ \to (w \in ℂ \land w \neq 0)$
27	23 26	anim12i	$⊢ (y \in ℕ \land w \in ℕ) \to ((y \in ℂ \land y \neq 0) \land (w \in ℂ \land w \neq 0))$
28		divadddiv	$⊢ ((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 w + z y}{y w}$
29	20 27 28	syl2an	$⊢ ((x \in ℤ \land z \in ℤ) \land (y \in ℕ \land w \in ℕ)) \to (\frac{x}{y}) + (\frac{z}{w}) = \frac{x w + z y}{y w}$
30	29	an4s	$⊢ ((x \in ℤ \land y \in ℕ) \land (z \in ℤ \land w \in ℕ)) \to (\frac{x}{y}) + (\frac{z}{w}) = \frac{x w + z y}{y w}$
31	17 30	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 w + z y}{y w}$
32		rspceov	$⊢ (x w + z y \in ℤ \land y w \in ℕ \land A + B = \frac{x w + z y}{y w}) \to \exists u \in ℤ \exists v \in ℕ A + B = \frac{u}{v}$
33		elq	$⊢ A + B \in ℚ \leftrightarrow \exists u \in ℤ \exists v \in ℕ A + B = \frac{u}{v}$
34	32 33	sylibr	$⊢ (x w + z y \in ℤ \land y w \in ℕ \land A + B = \frac{x w + z y}{y w}) \to A + B \in ℚ$
35	13 16 31 34	syl3anc	$⊢ (((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 ℚ$
36	35	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 ℚ$
37	36	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 ℚ)))$
38	37	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 ℚ))$
39	38	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 ℚ)$
40	39	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 ℚ$
41	1 2 40	syl2anb	$⊢ (A \in ℚ \land B \in ℚ) \to A + B \in ℚ$

Metamath Proof Explorer

Theorem qaddcl

Proof