This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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