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

Metamath Proof Explorer

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