Metamath Proof Explorer

Theorem zringeuf

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

Ref Expression
Assertion zringeuf 
|- abs = ( EuclF ` ZZring )

Proof

Step Hyp Ref Expression
1 zex 
 |-  ZZ e. _V
2 df-zring 
 |-  ZZring = ( CCfld |`s ZZ )
3 cnfldeuf 
 |-  abs = ( EuclF ` CCfld )
4 2 3 resseuf 
 |-  ( ZZ e. _V -> abs = ( EuclF ` ZZring ) )
5 1 4 ax-mp 
 |-  abs = ( EuclF ` ZZring )