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

Metamath Proof Explorer

Theorem zring0

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

Ref Expression
Assertion zring0 ⊢ 0 = 0 ℤ ring

Proof

Step Hyp Ref Expression
1 cncrng ⊢ ℂ fld ∈ CRing
2 crngring ⊢ ℂ fld ∈ CRing → ℂ fld ∈ Ring
3 ringmnd ⊢ ℂ fld ∈ Ring → ℂ fld ∈ Mnd
4 1 2 3 mp2b ⊢ ℂ fld ∈ Mnd
5 0z ⊢ 0 ∈ ℤ
6 zsscn ⊢ ℤ ⊆ ℂ
7 df-zring ⊢ ℤ ring = ℂ fld ↾ 𝑠 ℤ
8 cnfldbas ⊢ ℂ = Base ℂ fld
9 cnfld0 ⊢ 0 = 0 ℂ fld
10 7 8 9 ress0g ⊢ ℂ fld ∈ Mnd ∧ 0 ∈ ℤ ∧ ℤ ⊆ ℂ → 0 = 0 ℤ ring
11 4 5 6 10 mp3an ⊢ 0 = 0 ℤ ring