Theorem zzsnm

Description: The norm of the ring of the integers. (Contributed by Thierry Arnoux, 8-Nov-2017) (Revised by AV, 13-Jun-2019)

	Ref	Expression
Assertion	zzsnm	|- ( M e. ZZ -> ( abs ` M ) = ( ( norm ` ZZring ) ` M ) )

Proof

Step	Hyp	Ref	Expression
1		fvres	|- ( M e. ZZ -> ( ( abs |` ZZ ) ` M ) = ( abs ` M ) )
2		zringnm	|- ( norm ` ZZring ) = ( abs |` ZZ )
3	2	eqcomi	|- ( abs |` ZZ ) = ( norm ` ZZring )
4	3	fveq1i	|- ( ( abs |` ZZ ) ` M ) = ( ( norm ` ZZring ) ` M )
5	1 4	eqtr3di	|- ( M e. ZZ -> ( abs ` M ) = ( ( norm ` ZZring ) ` M ) )