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

Step	Hyp	Ref	Expression
1		zcn	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
2	1	div1d	⊢ ( 𝐴 ∈ ℤ → ( 𝐴 / 1 ) = 𝐴 )
3		1nn	⊢ 1 ∈ ℕ
4		znq	⊢ ( ( 𝐴 ∈ ℤ ∧ 1 ∈ ℕ ) → ( 𝐴 / 1 ) ∈ ℚ )
5	3 4	mpan2	⊢ ( 𝐴 ∈ ℤ → ( 𝐴 / 1 ) ∈ ℚ )
6	2 5	eqeltrrd	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℚ )