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

Metamath Proof Explorer

Theorem zriotaneg

Description: The negative of the unique integer such that ph . (Contributed by AV, 1-Dec-2018)

Ref Expression
Hypothesis zriotaneg.1 ⊢ x = − y → φ ↔ ψ
Assertion zriotaneg ⊢ ∃! x ∈ ℤ φ → ι x ∈ ℤ | φ = − ι y ∈ ℤ | ψ

Proof

Step Hyp Ref Expression
1 zriotaneg.1 ⊢ x = − y → φ ↔ ψ
2 tru ⊢ ⊤
3 nfriota1 ⊢ Ⅎ _ y ι y ∈ ℤ | ψ
4 3 nfneg ⊢ Ⅎ _ y − ι y ∈ ℤ | ψ
5 znegcl ⊢ y ∈ ℤ → − y ∈ ℤ
6 5 adantl ⊢ ⊤ ∧ y ∈ ℤ → − y ∈ ℤ
7 simpr ⊢ ⊤ ∧ ι y ∈ ℤ | ψ ∈ ℤ → ι y ∈ ℤ | ψ ∈ ℤ
8 7 znegcld ⊢ ⊤ ∧ ι y ∈ ℤ | ψ ∈ ℤ → − ι y ∈ ℤ | ψ ∈ ℤ
9 negeq ⊢ y = ι y ∈ ℤ | ψ → − y = − ι y ∈ ℤ | ψ
10 znegcl ⊢ x ∈ ℤ → − x ∈ ℤ
11 zcn ⊢ x ∈ ℤ → x ∈ ℂ
12 zcn ⊢ y ∈ ℤ → y ∈ ℂ
13 negcon2 ⊢ x ∈ ℂ ∧ y ∈ ℂ → x = − y ↔ y = − x
14 11 12 13 syl2an ⊢ x ∈ ℤ ∧ y ∈ ℤ → x = − y ↔ y = − x
15 10 14 reuhyp ⊢ x ∈ ℤ → ∃! y ∈ ℤ x = − y
16 15 adantl ⊢ ⊤ ∧ x ∈ ℤ → ∃! y ∈ ℤ x = − y
17 4 6 8 1 9 16 riotaxfrd ⊢ ⊤ ∧ ∃! x ∈ ℤ φ → ι x ∈ ℤ | φ = − ι y ∈ ℤ | ψ
18 2 17 mpan ⊢ ∃! x ∈ ℤ φ → ι x ∈ ℤ | φ = − ι y ∈ ℤ | ψ