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 \mathbb{Z}\to A\in \mathbb{Q}$$

Proof

Step	Hyp	Ref	Expression
1		zcn	$$⊢A\in \mathbb{Z}\to A\in ℂ$$
2	1	div1d	$$⊢A\in \mathbb{Z}\to \frac{A}{1}=A$$
3		1nn	$$⊢1\in \mathbb{N}$$
4		znq	$$⊢\left(A\in \mathbb{Z}\wedge 1\in \mathbb{N}\right)\to \frac{A}{1}\in \mathbb{Q}$$
5	3 4	mpan2	$$⊢A\in \mathbb{Z}\to \frac{A}{1}\in \mathbb{Q}$$
6	2 5	eqeltrrd	$$⊢A\in \mathbb{Z}\to A\in \mathbb{Q}$$