Theorem zringmulr

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

	Ref	Expression
Assertion	zringmulr	⊢ · = ( .r ‘ ℤring )

Proof

Step	Hyp	Ref	Expression
1		zex	⊢ ℤ ∈ V
2		df-zring	⊢ ℤring = ( ℂfld ↾s ℤ )
3		cnfldmul	⊢ · = ( .r ‘ ℂfld )
4	2 3	ressmulr	⊢ ( ℤ ∈ V → · = ( .r ‘ ℤring ) )
5	1 4	ax-mp	⊢ · = ( .r ‘ ℤring )