This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem zring1

Description: The unity element of the ring of integers. (Contributed by Thierry Arnoux, 1-Nov-2017) (Revised by AV, 9-Jun-2019)

Ref Expression
Assertion zring1 ⊢ 1 = 1 ℤ ring

Proof

Step Hyp Ref Expression
1 zsubrg ⊢ ℤ ∈ SubRing ⁡ ℂ fld
2 df-zring ⊢ ℤ ring = ℂ fld ↾ 𝑠 ℤ
3 cnfld1 ⊢ 1 = 1 ℂ fld
4 2 3 subrg1 ⊢ ℤ ∈ SubRing ⁡ ℂ fld → 1 = 1 ℤ ring
5 1 4 ax-mp ⊢ 1 = 1 ℤ ring