Theorem elpqb

Description: A class is a positive rational iff it is the quotient of two positive integers. (Contributed by AV, 30-Dec-2022)

	Ref	Expression
Assertion	elpqb	⊢ ( ( 𝐴 ∈ ℚ ∧ 0 < 𝐴 ) ↔ ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		elpq	⊢ ( ( 𝐴 ∈ ℚ ∧ 0 < 𝐴 ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) )
2		nnz	⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ℤ )
3		znq	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ ) → ( 𝑥 / 𝑦 ) ∈ ℚ )
4	2 3	sylan	⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) → ( 𝑥 / 𝑦 ) ∈ ℚ )
5		nnre	⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ℝ )
6		nngt0	⊢ ( 𝑥 ∈ ℕ → 0 < 𝑥 )
7	5 6	jca	⊢ ( 𝑥 ∈ ℕ → ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) )
8		nnre	⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℝ )
9		nngt0	⊢ ( 𝑦 ∈ ℕ → 0 < 𝑦 )
10	8 9	jca	⊢ ( 𝑦 ∈ ℕ → ( 𝑦 ∈ ℝ ∧ 0 < 𝑦 ) )
11		divgt0	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) ∧ ( 𝑦 ∈ ℝ ∧ 0 < 𝑦 ) ) → 0 < ( 𝑥 / 𝑦 ) )
12	7 10 11	syl2an	⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) → 0 < ( 𝑥 / 𝑦 ) )
13	4 12	jca	⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) → ( ( 𝑥 / 𝑦 ) ∈ ℚ ∧ 0 < ( 𝑥 / 𝑦 ) ) )
14		eleq1	⊢ ( 𝐴 = ( 𝑥 / 𝑦 ) → ( 𝐴 ∈ ℚ ↔ ( 𝑥 / 𝑦 ) ∈ ℚ ) )
15		breq2	⊢ ( 𝐴 = ( 𝑥 / 𝑦 ) → ( 0 < 𝐴 ↔ 0 < ( 𝑥 / 𝑦 ) ) )
16	14 15	anbi12d	⊢ ( 𝐴 = ( 𝑥 / 𝑦 ) → ( ( 𝐴 ∈ ℚ ∧ 0 < 𝐴 ) ↔ ( ( 𝑥 / 𝑦 ) ∈ ℚ ∧ 0 < ( 𝑥 / 𝑦 ) ) ) )
17	13 16	syl5ibrcom	⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) → ( 𝐴 = ( 𝑥 / 𝑦 ) → ( 𝐴 ∈ ℚ ∧ 0 < 𝐴 ) ) )
18	17	rexlimivv	⊢ ( ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) → ( 𝐴 ∈ ℚ ∧ 0 < 𝐴 ) )
19	1 18	impbii	⊢ ( ( 𝐴 ∈ ℚ ∧ 0 < 𝐴 ) ↔ ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝐴 = ( 𝑥 / 𝑦 ) )