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