Metamath Proof Explorer

Theorem elq

Description: Membership in the set of rationals. (Contributed by NM, 8-Jan-2002) (Revised by Mario Carneiro, 28-Jan-2014)

Ref Expression
Assertion elq ⊢ A ∈ ℚ ↔ ∃ x ∈ ℤ ∃ y ∈ ℕ A = x y

Proof

Step Hyp Ref Expression
1 df-q ⊢ ℚ = ÷ ℤ × ℕ
2 1 eleq2i ⊢ A ∈ ℚ ↔ A ∈ ÷ ℤ × ℕ
3 df-div ⊢ ÷ = x ∈ ℂ , y ∈ ℂ ∖ 0 ⟼ ι z ∈ ℂ | y ⁢ z = x
4 riotaex ⊢ ι z ∈ ℂ | y ⁢ z = x ∈ V
5 3 4 fnmpoi ⊢ ÷ Fn ℂ × ℂ ∖ 0
6 zsscn ⊢ ℤ ⊆ ℂ
7 nncn ⊢ x ∈ ℕ → x ∈ ℂ
8 nnne0 ⊢ x ∈ ℕ → x ≠ 0
9 eldifsn ⊢ x ∈ ℂ ∖ 0 ↔ x ∈ ℂ ∧ x ≠ 0
10 7 8 9 sylanbrc ⊢ x ∈ ℕ → x ∈ ℂ ∖ 0
11 10 ssriv ⊢ ℕ ⊆ ℂ ∖ 0
12 xpss12 ⊢ ℤ ⊆ ℂ ∧ ℕ ⊆ ℂ ∖ 0 → ℤ × ℕ ⊆ ℂ × ℂ ∖ 0
13 6 11 12 mp2an ⊢ ℤ × ℕ ⊆ ℂ × ℂ ∖ 0
14 ovelimab ⊢ ÷ Fn ℂ × ℂ ∖ 0 ∧ ℤ × ℕ ⊆ ℂ × ℂ ∖ 0 → A ∈ ÷ ℤ × ℕ ↔ ∃ x ∈ ℤ ∃ y ∈ ℕ A = x y
15 5 13 14 mp2an ⊢ A ∈ ÷ ℤ × ℕ ↔ ∃ x ∈ ℤ ∃ y ∈ ℕ A = x y
16 2 15 bitri ⊢ A ∈ ℚ ↔ ∃ x ∈ ℤ ∃ y ∈ ℕ A = x y