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	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 / 𝐵 ) ∈ ℚ )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝐴 / 𝐵 ) = ( 𝐴 / 𝐵 )
2		rspceov	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 / 𝐵 ) = ( 𝐴 / 𝐵 ) ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝐴 / 𝐵 ) = ( 𝑥 / 𝑦 ) )
3	1 2	mp3an3	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝐴 / 𝐵 ) = ( 𝑥 / 𝑦 ) )
4		elq	⊢ ( ( 𝐴 / 𝐵 ) ∈ ℚ ↔ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝐴 / 𝐵 ) = ( 𝑥 / 𝑦 ) )
5	3 4	sylibr	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 / 𝐵 ) ∈ ℚ )