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 | ψ