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

Metamath Proof Explorer

Theorem zringinvg

Description: The additive inverse of an element of the ring of integers. (Contributed by AV, 24-May-2019) (Revised by AV, 10-Jun-2019)

Ref Expression
Assertion zringinvg ⊢ A ∈ ℤ → − A = inv g ⁡ ℤ ring ⁡ A

Proof

Step Hyp Ref Expression
1 zcn ⊢ A ∈ ℤ → A ∈ ℂ
2 1 negidd ⊢ A ∈ ℤ → A + − A = 0
3 zringgrp ⊢ ℤ ring ∈ Grp
4 id ⊢ A ∈ ℤ → A ∈ ℤ
5 znegcl ⊢ A ∈ ℤ → − A ∈ ℤ
6 zringbas ⊢ ℤ = Base ℤ ring
7 zringplusg ⊢ + = + ℤ ring
8 zring0 ⊢ 0 = 0 ℤ ring
9 eqid ⊢ inv g ⁡ ℤ ring = inv g ⁡ ℤ ring
10 6 7 8 9 grpinvid1 ⊢ ℤ ring ∈ Grp ∧ A ∈ ℤ ∧ − A ∈ ℤ → inv g ⁡ ℤ ring ⁡ A = − A ↔ A + − A = 0
11 3 4 5 10 mp3an2i ⊢ A ∈ ℤ → inv g ⁡ ℤ ring ⁡ A = − A ↔ A + − A = 0
12 2 11 mpbird ⊢ A ∈ ℤ → inv g ⁡ ℤ ring ⁡ A = − A
13 12 eqcomd ⊢ A ∈ ℤ → − A = inv g ⁡ ℤ ring ⁡ A