Metamath Proof Explorer

Theorem zring1

Description: The multiplicative neutral element of the ring of integers. (Contributed by Thierry Arnoux, 1-Nov-2017) (Revised by AV, 9-Jun-2019)

Ref Expression
Assertion zring1 
|- 1 = ( 1r ` ZZring )

Proof

Step Hyp Ref Expression
1 zsubrg 
 |-  ZZ e. ( SubRing ` CCfld )
2 df-zring 
 |-  ZZring = ( CCfld |`s ZZ )
3 cnfld1 
 |-  1 = ( 1r ` CCfld )
4 2 3 subrg1 
 |-  ( ZZ e. ( SubRing ` CCfld ) -> 1 = ( 1r ` ZZring ) )
5 1 4 ax-mp 
 |-  1 = ( 1r ` ZZring )