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 ( 𝐴 ∈ ℚ ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) )

Proof

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 ( 𝐴 ∈ ℚ ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) )