Step |
Hyp |
Ref |
Expression |
1 |
|
df-q |
⊢ ℚ = ( / “ ( ℤ × ℕ ) ) |
2 |
1
|
eleq2i |
⊢ ( 𝐴 ∈ ℚ ↔ 𝐴 ∈ ( / “ ( ℤ × ℕ ) ) ) |
3 |
|
df-div |
⊢ / = ( 𝑥 ∈ ℂ , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℩ 𝑧 ∈ ℂ ( 𝑦 · 𝑧 ) = 𝑥 ) ) |
4 |
|
riotaex |
⊢ ( ℩ 𝑧 ∈ ℂ ( 𝑦 · 𝑧 ) = 𝑥 ) ∈ V |
5 |
3 4
|
fnmpoi |
⊢ / Fn ( ℂ × ( ℂ ∖ { 0 } ) ) |
6 |
|
zsscn |
⊢ ℤ ⊆ ℂ |
7 |
|
nncn |
⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ℂ ) |
8 |
|
nnne0 |
⊢ ( 𝑥 ∈ ℕ → 𝑥 ≠ 0 ) |
9 |
|
eldifsn |
⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ) |
10 |
7 8 9
|
sylanbrc |
⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ( ℂ ∖ { 0 } ) ) |
11 |
10
|
ssriv |
⊢ ℕ ⊆ ( ℂ ∖ { 0 } ) |
12 |
|
xpss12 |
⊢ ( ( ℤ ⊆ ℂ ∧ ℕ ⊆ ( ℂ ∖ { 0 } ) ) → ( ℤ × ℕ ) ⊆ ( ℂ × ( ℂ ∖ { 0 } ) ) ) |
13 |
6 11 12
|
mp2an |
⊢ ( ℤ × ℕ ) ⊆ ( ℂ × ( ℂ ∖ { 0 } ) ) |
14 |
|
ovelimab |
⊢ ( ( / Fn ( ℂ × ( ℂ ∖ { 0 } ) ) ∧ ( ℤ × ℕ ) ⊆ ( ℂ × ( ℂ ∖ { 0 } ) ) ) → ( 𝐴 ∈ ( / “ ( ℤ × ℕ ) ) ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) ) ) |
15 |
5 13 14
|
mp2an |
⊢ ( 𝐴 ∈ ( / “ ( ℤ × ℕ ) ) ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) ) |
16 |
2 15
|
bitri |
⊢ ( 𝐴 ∈ ℚ ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) ) |