Step |
Hyp |
Ref |
Expression |
1 |
|
elq |
⊢ ( 𝐴 ∈ ℚ ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) ) |
2 |
|
zcn |
⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ ) |
3 |
2
|
adantr |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) → 𝑥 ∈ ℂ ) |
4 |
|
nncn |
⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℂ ) |
5 |
4
|
adantl |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) → 𝑦 ∈ ℂ ) |
6 |
|
nnne0 |
⊢ ( 𝑦 ∈ ℕ → 𝑦 ≠ 0 ) |
7 |
6
|
adantl |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) → 𝑦 ≠ 0 ) |
8 |
3 5 7
|
divnegd |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) → - ( 𝑥 / 𝑦 ) = ( - 𝑥 / 𝑦 ) ) |
9 |
|
znegcl |
⊢ ( 𝑥 ∈ ℤ → - 𝑥 ∈ ℤ ) |
10 |
|
znq |
⊢ ( ( - 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) → ( - 𝑥 / 𝑦 ) ∈ ℚ ) |
11 |
9 10
|
sylan |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) → ( - 𝑥 / 𝑦 ) ∈ ℚ ) |
12 |
8 11
|
eqeltrd |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) → - ( 𝑥 / 𝑦 ) ∈ ℚ ) |
13 |
|
negeq |
⊢ ( 𝐴 = ( 𝑥 / 𝑦 ) → - 𝐴 = - ( 𝑥 / 𝑦 ) ) |
14 |
13
|
eleq1d |
⊢ ( 𝐴 = ( 𝑥 / 𝑦 ) → ( - 𝐴 ∈ ℚ ↔ - ( 𝑥 / 𝑦 ) ∈ ℚ ) ) |
15 |
12 14
|
syl5ibrcom |
⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) → ( 𝐴 = ( 𝑥 / 𝑦 ) → - 𝐴 ∈ ℚ ) ) |
16 |
15
|
rexlimivv |
⊢ ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) → - 𝐴 ∈ ℚ ) |
17 |
1 16
|
sylbi |
⊢ ( 𝐴 ∈ ℚ → - 𝐴 ∈ ℚ ) |