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 e. ZZ -> A e. QQ )

Proof

Step Hyp Ref Expression
1 zcn 
 |-  ( A e. ZZ -> A e. CC )
2 1 div1d 
 |-  ( A e. ZZ -> ( A / 1 ) = A )
3 1nn 
 |-  1 e. NN
4 znq 
 |-  ( ( A e. ZZ /\ 1 e. NN ) -> ( A / 1 ) e. QQ )
5 3 4 mpan2 
 |-  ( A e. ZZ -> ( A / 1 ) e. QQ )
6 2 5 eqeltrrd 
 |-  ( A e. ZZ -> A e. QQ )