Step |
Hyp |
Ref |
Expression |
1 |
|
elq |
⊢ ( 𝐴 ∈ ℚ ↔ ∃ 𝑦 ∈ ℤ ∃ 𝑥 ∈ ℕ 𝐴 = ( 𝑦 / 𝑥 ) ) |
2 |
|
rexcom |
⊢ ( ∃ 𝑦 ∈ ℤ ∃ 𝑥 ∈ ℕ 𝐴 = ( 𝑦 / 𝑥 ) ↔ ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℤ 𝐴 = ( 𝑦 / 𝑥 ) ) |
3 |
|
zcn |
⊢ ( 𝑦 ∈ ℤ → 𝑦 ∈ ℂ ) |
4 |
3
|
adantl |
⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℤ ) → 𝑦 ∈ ℂ ) |
5 |
|
nncn |
⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ℂ ) |
6 |
5
|
adantr |
⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℤ ) → 𝑥 ∈ ℂ ) |
7 |
|
nnne0 |
⊢ ( 𝑥 ∈ ℕ → 𝑥 ≠ 0 ) |
8 |
7
|
adantr |
⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℤ ) → 𝑥 ≠ 0 ) |
9 |
4 6 8
|
divcan1d |
⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℤ ) → ( ( 𝑦 / 𝑥 ) · 𝑥 ) = 𝑦 ) |
10 |
|
simpr |
⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℤ ) → 𝑦 ∈ ℤ ) |
11 |
9 10
|
eqeltrd |
⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℤ ) → ( ( 𝑦 / 𝑥 ) · 𝑥 ) ∈ ℤ ) |
12 |
|
oveq1 |
⊢ ( 𝐴 = ( 𝑦 / 𝑥 ) → ( 𝐴 · 𝑥 ) = ( ( 𝑦 / 𝑥 ) · 𝑥 ) ) |
13 |
12
|
eleq1d |
⊢ ( 𝐴 = ( 𝑦 / 𝑥 ) → ( ( 𝐴 · 𝑥 ) ∈ ℤ ↔ ( ( 𝑦 / 𝑥 ) · 𝑥 ) ∈ ℤ ) ) |
14 |
11 13
|
syl5ibrcom |
⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℤ ) → ( 𝐴 = ( 𝑦 / 𝑥 ) → ( 𝐴 · 𝑥 ) ∈ ℤ ) ) |
15 |
14
|
rexlimdva |
⊢ ( 𝑥 ∈ ℕ → ( ∃ 𝑦 ∈ ℤ 𝐴 = ( 𝑦 / 𝑥 ) → ( 𝐴 · 𝑥 ) ∈ ℤ ) ) |
16 |
15
|
reximia |
⊢ ( ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℤ 𝐴 = ( 𝑦 / 𝑥 ) → ∃ 𝑥 ∈ ℕ ( 𝐴 · 𝑥 ) ∈ ℤ ) |
17 |
2 16
|
sylbi |
⊢ ( ∃ 𝑦 ∈ ℤ ∃ 𝑥 ∈ ℕ 𝐴 = ( 𝑦 / 𝑥 ) → ∃ 𝑥 ∈ ℕ ( 𝐴 · 𝑥 ) ∈ ℤ ) |
18 |
1 17
|
sylbi |
⊢ ( 𝐴 ∈ ℚ → ∃ 𝑥 ∈ ℕ ( 𝐴 · 𝑥 ) ∈ ℤ ) |