Metamath Proof Explorer


Theorem zringbas

Description: The integers are the base of the ring of integers. (Contributed by Thierry Arnoux, 31-Oct-2017) (Revised by AV, 9-Jun-2019)

Ref Expression
Assertion zringbas =Basering

Proof

Step Hyp Ref Expression
1 zsscn
2 df-zring ring=fld𝑠
3 cnfldbas =Basefld
4 2 3 ressbas2 =Basering
5 1 4 ax-mp =Basering