Theorem zriotaneg

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

	Ref	Expression
Hypothesis	zriotaneg.1	⊢ ( 𝑥 = - 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion	zriotaneg	⊢ ( ∃! 𝑥 ∈ ℤ 𝜑 → ( ℩ 𝑥 ∈ ℤ 𝜑 ) = - ( ℩ 𝑦 ∈ ℤ 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		zriotaneg.1	⊢ ( 𝑥 = - 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2		tru	⊢ ⊤
3		nfriota1	⊢ Ⅎ 𝑦 ( ℩ 𝑦 ∈ ℤ 𝜓 )
4	3	nfneg	⊢ Ⅎ 𝑦 - ( ℩ 𝑦 ∈ ℤ 𝜓 )
5		znegcl	⊢ ( 𝑦 ∈ ℤ → - 𝑦 ∈ ℤ )
6	5	adantl	⊢ ( ( ⊤ ∧ 𝑦 ∈ ℤ ) → - 𝑦 ∈ ℤ )
7		simpr	⊢ ( ( ⊤ ∧ ( ℩ 𝑦 ∈ ℤ 𝜓 ) ∈ ℤ ) → ( ℩ 𝑦 ∈ ℤ 𝜓 ) ∈ ℤ )
8	7	znegcld	⊢ ( ( ⊤ ∧ ( ℩ 𝑦 ∈ ℤ 𝜓 ) ∈ ℤ ) → - ( ℩ 𝑦 ∈ ℤ 𝜓 ) ∈ ℤ )
9		negeq	⊢ ( 𝑦 = ( ℩ 𝑦 ∈ ℤ 𝜓 ) → - 𝑦 = - ( ℩ 𝑦 ∈ ℤ 𝜓 ) )
10		znegcl	⊢ ( 𝑥 ∈ ℤ → - 𝑥 ∈ ℤ )
11		zcn	⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
12		zcn	⊢ ( 𝑦 ∈ ℤ → 𝑦 ∈ ℂ )
13		negcon2	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 = - 𝑦 ↔ 𝑦 = - 𝑥 ) )
14	11 12 13	syl2an	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑥 = - 𝑦 ↔ 𝑦 = - 𝑥 ) )
15	10 14	reuhyp	⊢ ( 𝑥 ∈ ℤ → ∃! 𝑦 ∈ ℤ 𝑥 = - 𝑦 )
16	15	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℤ ) → ∃! 𝑦 ∈ ℤ 𝑥 = - 𝑦 )
17	4 6 8 1 9 16	riotaxfrd	⊢ ( ( ⊤ ∧ ∃! 𝑥 ∈ ℤ 𝜑 ) → ( ℩ 𝑥 ∈ ℤ 𝜑 ) = - ( ℩ 𝑦 ∈ ℤ 𝜓 ) )
18	2 17	mpan	⊢ ( ∃! 𝑥 ∈ ℤ 𝜑 → ( ℩ 𝑥 ∈ ℤ 𝜑 ) = - ( ℩ 𝑦 ∈ ℤ 𝜓 ) )