Theorem riotaneg

Description: The negative of the unique real such that ph . (Contributed by NM, 13-Jun-2005)

	Ref	Expression
Hypothesis	riotaneg.1	$$⊢x=-y\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	riotaneg	$$⊢\exists !x\in ℝ\phi \to \left(\iota x\in ℝ|\phi \right)=-\left(\iota y\in ℝ|\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		riotaneg.1	$$⊢x=-y\to \left(\phi \leftrightarrow \psi \right)$$
2		tru	$$⊢\top$$
3		nfriota1	$$⊢\underset{\_}{Ⅎ}y\left(\iota y\in ℝ|\psi \right)$$
4	3	nfneg	$$⊢\underset{\_}{Ⅎ}y\left(-\left(\iota y\in ℝ|\psi \right)\right)$$
5		renegcl	$$⊢y\in ℝ\to -y\in ℝ$$
6	5	adantl	$$⊢\left(\top \wedge y\in ℝ\right)\to -y\in ℝ$$
7		simpr	$$⊢\left(\top \wedge \left(\iota y\in ℝ|\psi \right)\in ℝ\right)\to \left(\iota y\in ℝ|\psi \right)\in ℝ$$
8	7	renegcld	$$⊢\left(\top \wedge \left(\iota y\in ℝ|\psi \right)\in ℝ\right)\to -\left(\iota y\in ℝ|\psi \right)\in ℝ$$
9		negeq	$$⊢y=\left(\iota y\in ℝ|\psi \right)\to -y=-\left(\iota y\in ℝ|\psi \right)$$
10		renegcl	$$⊢x\in ℝ\to -x\in ℝ$$
11		recn	$$⊢x\in ℝ\to x\in ℂ$$
12		recn	$$⊢y\in ℝ\to y\in ℂ$$
13		negcon2	$$⊢\left(x\in ℂ\wedge y\in ℂ\right)\to \left(x=-y\leftrightarrow y=-x\right)$$
14	11 12 13	syl2an	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \left(x=-y\leftrightarrow y=-x\right)$$
15	10 14	reuhyp	$$⊢x\in ℝ\to \exists !y\in ℝx=-y$$
16	15	adantl	$$⊢\left(\top \wedge x\in ℝ\right)\to \exists !y\in ℝx=-y$$
17	4 6 8 1 9 16	riotaxfrd	$$⊢\left(\top \wedge \exists !x\in ℝ\phi \right)\to \left(\iota x\in ℝ|\phi \right)=-\left(\iota y\in ℝ|\psi \right)$$
18	2 17	mpan	$$⊢\exists !x\in ℝ\phi \to \left(\iota x\in ℝ|\phi \right)=-\left(\iota y\in ℝ|\psi \right)$$