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