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

Metamath Proof Explorer

Theorem zq

Description: An integer is a rational number. (Contributed by NM, 9-Jan-2002) (Proof shortened by Steven Nguyen, 23-Mar-2023)

		Ref	Expression
	Assertion	zq	$⊢ A \in ℤ \to A \in ℚ$

Step	Hyp	Ref	Expression
1		zcn	$⊢ A \in ℤ \to A \in ℂ$
2	1	div1d	$⊢ A \in ℤ \to \frac{A}{1} = A$
3		1nn	$⊢ 1 \in ℕ$
4		znq	$⊢ (A \in ℤ \land 1 \in ℕ) \to \frac{A}{1} \in ℚ$
5	3 4	mpan2	$⊢ A \in ℤ \to \frac{A}{1} \in ℚ$
6	2 5	eqeltrrd	$⊢ A \in ℤ \to A \in ℚ$