Theorem zringeuf

Description: The Euclidean function of the ring of integers. (Contributed by Thierry Arnoux, 9-Nov-2026)

	Ref	Expression
Assertion	zringeuf	⊢ abs = ( EuclF ‘ ℤring )

Proof

Step	Hyp	Ref	Expression
1		zex	⊢ ℤ ∈ V
2		df-zring	⊢ ℤring = ( ℂfld ↾s ℤ )
3		cnfldeuf	⊢ abs = ( EuclF ‘ ℂfld )
4	2 3	resseuf	⊢ ( ℤ ∈ V → abs = ( EuclF ‘ ℤring ) )
5	1 4	ax-mp	⊢ abs = ( EuclF ‘ ℤring )