Metamath Proof Explorer

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 ⊢ ( ( 𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ) → ( 𝐴 + 𝐵 ) ∈ ℚ )