Metamath Proof Explorer

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 
|- x. = ( .r ` ZZring )

Proof

Step Hyp Ref Expression
1 zex 
 |-  ZZ e. _V
2 df-zring 
 |-  ZZring = ( CCfld |`s ZZ )
3 cnfldmul 
 |-  x. = ( .r ` CCfld )
4 2 3 ressmulr 
 |-  ( ZZ e. _V -> x. = ( .r ` ZZring ) )
5 1 4 ax-mp 
 |-  x. = ( .r ` ZZring )