Database
REAL AND COMPLEX NUMBERS
Integer sets
Integers (as a subset of complex numbers)
zriotaneg
Next ⟩
suprfinzcl
Metamath Proof Explorer
Ascii
Unicode
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
∈
ℤ
|
ψ