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

Metamath Proof Explorer

Theorem znq

Description: The ratio of an integer and a positive integer is a rational number. (Contributed by NM, 12-Jan-2002)

Ref Expression
Assertion znq ⊢ A ∈ ℤ ∧ B ∈ ℕ → A B ∈ ℚ

Proof

Step Hyp Ref Expression
1 eqid ⊢ A B = A B
2 rspceov ⊢ A ∈ ℤ ∧ B ∈ ℕ ∧ A B = A B → ∃ x ∈ ℤ ∃ y ∈ ℕ A B = x y
3 1 2 mp3an3 ⊢ A ∈ ℤ ∧ B ∈ ℕ → ∃ x ∈ ℤ ∃ y ∈ ℕ A B = x y
4 elq ⊢ A B ∈ ℚ ↔ ∃ x ∈ ℤ ∃ y ∈ ℕ A B = x y
5 3 4 sylibr ⊢ A ∈ ℤ ∧ B ∈ ℕ → A B ∈ ℚ