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