Metamath Proof Explorer


Theorem qmulcl

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

Ref Expression
Assertion qmulcl ( ( 𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ) → ( 𝐴 · 𝐵 ) ∈ ℚ )

Proof

Step Hyp Ref Expression
1 elq ( 𝐴 ∈ ℚ ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) )
2 elq ( 𝐵 ∈ ℚ ↔ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℕ 𝐵 = ( 𝑧 / 𝑤 ) )
3 zmulcl ( ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) → ( 𝑥 · 𝑧 ) ∈ ℤ )
4 nnmulcl ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) → ( 𝑦 · 𝑤 ) ∈ ℕ )
5 3 4 anim12i ( ( ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ) → ( ( 𝑥 · 𝑧 ) ∈ ℤ ∧ ( 𝑦 · 𝑤 ) ∈ ℕ ) )
6 5 an4s ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ ) ) → ( ( 𝑥 · 𝑧 ) ∈ ℤ ∧ ( 𝑦 · 𝑤 ) ∈ ℕ ) )
7 oveq12 ( ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) → ( 𝐴 · 𝐵 ) = ( ( 𝑥 / 𝑦 ) · ( 𝑧 / 𝑤 ) ) )
8 zcn ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
9 zcn ( 𝑧 ∈ ℤ → 𝑧 ∈ ℂ )
10 8 9 anim12i ( ( 𝑥 ∈ ℤ ∧ 𝑧 ∈ ℤ ) → ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ) )
11 10 ad2ant2r ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ ) ) → ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ) )
12 nncn ( 𝑦 ∈ ℕ → 𝑦 ∈ ℂ )
13 nnne0 ( 𝑦 ∈ ℕ → 𝑦 ≠ 0 )
14 12 13 jca ( 𝑦 ∈ ℕ → ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) )
15 nncn ( 𝑤 ∈ ℕ → 𝑤 ∈ ℂ )
16 nnne0 ( 𝑤 ∈ ℕ → 𝑤 ≠ 0 )
17 15 16 jca ( 𝑤 ∈ ℕ → ( 𝑤 ∈ ℂ ∧ 𝑤 ≠ 0 ) )
18 14 17 anim12i ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) → ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑤 ∈ ℂ ∧ 𝑤 ≠ 0 ) ) )
19 18 ad2ant2l ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ ) ) → ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑤 ∈ ℂ ∧ 𝑤 ≠ 0 ) ) )
20 divmuldiv ( ( ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ) ∧ ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ∧ ( 𝑤 ∈ ℂ ∧ 𝑤 ≠ 0 ) ) ) → ( ( 𝑥 / 𝑦 ) · ( 𝑧 / 𝑤 ) ) = ( ( 𝑥 · 𝑧 ) / ( 𝑦 · 𝑤 ) ) )
21 11 19 20 syl2anc ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ ) ) → ( ( 𝑥 / 𝑦 ) · ( 𝑧 / 𝑤 ) ) = ( ( 𝑥 · 𝑧 ) / ( 𝑦 · 𝑤 ) ) )
22 7 21 sylan9eqr ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ ) ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) → ( 𝐴 · 𝐵 ) = ( ( 𝑥 · 𝑧 ) / ( 𝑦 · 𝑤 ) ) )
23 rspceov ( ( ( 𝑥 · 𝑧 ) ∈ ℤ ∧ ( 𝑦 · 𝑤 ) ∈ ℕ ∧ ( 𝐴 · 𝐵 ) = ( ( 𝑥 · 𝑧 ) / ( 𝑦 · 𝑤 ) ) ) → ∃ 𝑣 ∈ ℤ ∃ 𝑢 ∈ ℕ ( 𝐴 · 𝐵 ) = ( 𝑣 / 𝑢 ) )
24 23 3expa ( ( ( ( 𝑥 · 𝑧 ) ∈ ℤ ∧ ( 𝑦 · 𝑤 ) ∈ ℕ ) ∧ ( 𝐴 · 𝐵 ) = ( ( 𝑥 · 𝑧 ) / ( 𝑦 · 𝑤 ) ) ) → ∃ 𝑣 ∈ ℤ ∃ 𝑢 ∈ ℕ ( 𝐴 · 𝐵 ) = ( 𝑣 / 𝑢 ) )
25 elq ( ( 𝐴 · 𝐵 ) ∈ ℚ ↔ ∃ 𝑣 ∈ ℤ ∃ 𝑢 ∈ ℕ ( 𝐴 · 𝐵 ) = ( 𝑣 / 𝑢 ) )
26 24 25 sylibr ( ( ( ( 𝑥 · 𝑧 ) ∈ ℤ ∧ ( 𝑦 · 𝑤 ) ∈ ℕ ) ∧ ( 𝐴 · 𝐵 ) = ( ( 𝑥 · 𝑧 ) / ( 𝑦 · 𝑤 ) ) ) → ( 𝐴 · 𝐵 ) ∈ ℚ )
27 6 22 26 syl2an2r ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ ) ) ∧ ( 𝐴 = ( 𝑥 / 𝑦 ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) → ( 𝐴 · 𝐵 ) ∈ ℚ )
28 27 an4s ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) ∧ 𝐴 = ( 𝑥 / 𝑦 ) ) ∧ ( ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ ) ∧ 𝐵 = ( 𝑧 / 𝑤 ) ) ) → ( 𝐴 · 𝐵 ) ∈ ℚ )
29 28 exp43 ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) → ( 𝐴 = ( 𝑥 / 𝑦 ) → ( ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ ) → ( 𝐵 = ( 𝑧 / 𝑤 ) → ( 𝐴 · 𝐵 ) ∈ ℚ ) ) ) )
30 29 rexlimivv ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) → ( ( 𝑧 ∈ ℤ ∧ 𝑤 ∈ ℕ ) → ( 𝐵 = ( 𝑧 / 𝑤 ) → ( 𝐴 · 𝐵 ) ∈ ℚ ) ) )
31 30 rexlimdvv ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) → ( ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℕ 𝐵 = ( 𝑧 / 𝑤 ) → ( 𝐴 · 𝐵 ) ∈ ℚ ) )
32 31 imp ( ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) ∧ ∃ 𝑧 ∈ ℤ ∃ 𝑤 ∈ ℕ 𝐵 = ( 𝑧 / 𝑤 ) ) → ( 𝐴 · 𝐵 ) ∈ ℚ )
33 1 2 32 syl2anb ( ( 𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ ) → ( 𝐴 · 𝐵 ) ∈ ℚ )