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 ⊢ A ∈ ℚ ∧ 0 < A ↔ ∃ x ∈ ℕ ∃ y ∈ ℕ A = x y

Proof

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