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 ‘ ℤring )

Proof

Step	Hyp	Ref	Expression
1		zsubrg	⊢ ℤ ∈ ( SubRing ‘ ℂfld )
2		df-zring	⊢ ℤring = ( ℂfld ↾s ℤ )
3		cnfld1	⊢ 1 = ( 1r ‘ ℂfld )
4	2 3	subrg1	⊢ ( ℤ ∈ ( SubRing ‘ ℂfld ) → 1 = ( 1r ‘ ℤring ) )
5	1 4	ax-mp	⊢ 1 = ( 1r ‘ ℤring )