Theorem qaddcl

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

	Ref	Expression
Assertion	qaddcl	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ) → ( 𝐴 + 𝐵 ) ∈ ℚ )

Proof

Step	Hyp	Ref	Expression
1		elq	⊢ ( 𝐴 ∈ ℚ ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) )
2		elq	⊢ ( 𝐵 ∈ ℚ ↔ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℕ 𝐵 = ( 𝑧 / 𝑤 ) )
3		nnz	⊢ ( 𝑤 ∈ ℕ → 𝑤 ∈ ℤ )
4		zmulcl	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑤 ∈ ℤ ) → ( 𝑥 · 𝑤 ) ∈ ℤ )
5	3 4	sylan2	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑤 ∈ ℕ ) → ( 𝑥 · 𝑤 ) ∈ ℤ )
6	5	ad2ant2rl	⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ ) ) → ( 𝑥 · 𝑤 ) ∈ ℤ )
7		simpl	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ ) → 𝑧 ∈ ℤ )
8		nnz	⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℤ )
9	8	adantl	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) → 𝑦 ∈ ℤ )
10		zmulcl	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑧 · 𝑦 ) ∈ ℤ )
11	7 9 10	syl2anr	⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ ) ) → ( 𝑧 · 𝑦 ) ∈ ℤ )
12	6 11	zaddcld	⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ ) ) → ( ( 𝑥 · 𝑤 ) + ( 𝑧 · 𝑦 ) ) ∈ ℤ )
13	12	adantr	⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ ) ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) → ( ( 𝑥 · 𝑤 ) + ( 𝑧 · 𝑦 ) ) ∈ ℤ )
14		nnmulcl	⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) → ( 𝑦 · 𝑤 ) ∈ ℕ )
15	14	ad2ant2l	⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ ) ) → ( 𝑦 · 𝑤 ) ∈ ℕ )
16	15	adantr	⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ ) ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) → ( 𝑦 · 𝑤 ) ∈ ℕ )
17		oveq12	⊢ ( ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) → ( 𝐴 + 𝐵 ) = ( ( 𝑥 / 𝑦 ) + ( 𝑧 / 𝑤 ) ) )
18		zcn	⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
19		zcn	⊢ ( 𝑧 ∈ ℤ → 𝑧 ∈ ℂ )
20	18 19	anim12i	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) → ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ) )
21		nncn	⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℂ )
22		nnne0	⊢ ( 𝑦 ∈ ℕ → 𝑦 ≠ 0 )
23	21 22	jca	⊢ ( 𝑦 ∈ ℕ → ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) )
24		nncn	⊢ ( 𝑤 ∈ ℕ → 𝑤 ∈ ℂ )
25		nnne0	⊢ ( 𝑤 ∈ ℕ → 𝑤 ≠ 0 )
26	24 25	jca	⊢ ( 𝑤 ∈ ℕ → ( 𝑤 ∈ ℂ ∧ 𝑤 ≠ 0 ) )
27	23 26	anim12i	⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) → ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑤 ∈ ℂ ∧ 𝑤 ≠ 0 ) ) )
28		divadddiv	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ) ∧ ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑤 ∈ ℂ ∧ 𝑤 ≠ 0 ) ) ) → ( ( 𝑥 / 𝑦 ) + ( 𝑧 / 𝑤 ) ) = ( ( ( 𝑥 · 𝑤 ) + ( 𝑧 · 𝑦 ) ) / ( 𝑦 · 𝑤 ) ) )
29	20 27 28	syl2an	⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ) → ( ( 𝑥 / 𝑦 ) + ( 𝑧 / 𝑤 ) ) = ( ( ( 𝑥 · 𝑤 ) + ( 𝑧 · 𝑦 ) ) / ( 𝑦 · 𝑤 ) ) )
30	29	an4s	⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ ) ) → ( ( 𝑥 / 𝑦 ) + ( 𝑧 / 𝑤 ) ) = ( ( ( 𝑥 · 𝑤 ) + ( 𝑧 · 𝑦 ) ) / ( 𝑦 · 𝑤 ) ) )
31	17 30	sylan9eqr	⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ ) ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) → ( 𝐴 + 𝐵 ) = ( ( ( 𝑥 · 𝑤 ) + ( 𝑧 · 𝑦 ) ) / ( 𝑦 · 𝑤 ) ) )
32		rspceov	⊢ ( ( ( ( 𝑥 · 𝑤 ) + ( 𝑧 · 𝑦 ) ) ∈ ℤ ∧ ( 𝑦 · 𝑤 ) ∈ ℕ ∧ ( 𝐴 + 𝐵 ) = ( ( ( 𝑥 · 𝑤 ) + ( 𝑧 · 𝑦 ) ) / ( 𝑦 · 𝑤 ) ) ) → ∃ 𝑢 ∈ ℤ ∃ 𝑣 ∈ ℕ ( 𝐴 + 𝐵 ) = ( 𝑢 / 𝑣 ) )
33		elq	⊢ ( ( 𝐴 + 𝐵 ) ∈ ℚ ↔ ∃ 𝑢 ∈ ℤ ∃ 𝑣 ∈ ℕ ( 𝐴 + 𝐵 ) = ( 𝑢 / 𝑣 ) )
34	32 33	sylibr	⊢ ( ( ( ( 𝑥 · 𝑤 ) + ( 𝑧 · 𝑦 ) ) ∈ ℤ ∧ ( 𝑦 · 𝑤 ) ∈ ℕ ∧ ( 𝐴 + 𝐵 ) = ( ( ( 𝑥 · 𝑤 ) + ( 𝑧 · 𝑦 ) ) / ( 𝑦 · 𝑤 ) ) ) → ( 𝐴 + 𝐵 ) ∈ ℚ )
35	13 16 31 34	syl3anc	⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ ) ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) → ( 𝐴 + 𝐵 ) ∈ ℚ )
36	35	an4s	⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ 𝐴 = ( 𝑥 / 𝑦 ) ) ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) → ( 𝐴 + 𝐵 ) ∈ ℚ )
37	36	exp43	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) → ( 𝐴 = ( 𝑥 / 𝑦 ) → ( ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ ) → ( 𝐵 = ( 𝑧 / 𝑤 ) → ( 𝐴 + 𝐵 ) ∈ ℚ ) ) ) )
38	37	rexlimivv	⊢ ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) → ( ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ ) → ( 𝐵 = ( 𝑧 / 𝑤 ) → ( 𝐴 + 𝐵 ) ∈ ℚ ) ) )
39	38	rexlimdvv	⊢ ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) → ( ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℕ 𝐵 = ( 𝑧 / 𝑤 ) → ( 𝐴 + 𝐵 ) ∈ ℚ ) )
40	39	imp	⊢ ( ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) ∧ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℕ 𝐵 = ( 𝑧 / 𝑤 ) ) → ( 𝐴 + 𝐵 ) ∈ ℚ )
41	1 2 40	syl2anb	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ) → ( 𝐴 + 𝐵 ) ∈ ℚ )