Theorem riotaneg

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

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

Proof

Step	Hyp	Ref	Expression
1		riotaneg.1	⊢ ( 𝑥 = - 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2		tru	⊢ ⊤
3		nfriota1	⊢ Ⅎ 𝑦 ( ℩ 𝑦 ∈ ℝ 𝜓 )
4	3	nfneg	⊢ Ⅎ 𝑦 - ( ℩ 𝑦 ∈ ℝ 𝜓 )
5		renegcl	⊢ ( 𝑦 ∈ ℝ → - 𝑦 ∈ ℝ )
6	5	adantl	⊢ ( ( ⊤ ∧ 𝑦 ∈ ℝ ) → - 𝑦 ∈ ℝ )
7		simpr	⊢ ( ( ⊤ ∧ ( ℩ 𝑦 ∈ ℝ 𝜓 ) ∈ ℝ ) → ( ℩ 𝑦 ∈ ℝ 𝜓 ) ∈ ℝ )
8	7	renegcld	⊢ ( ( ⊤ ∧ ( ℩ 𝑦 ∈ ℝ 𝜓 ) ∈ ℝ ) → - ( ℩ 𝑦 ∈ ℝ 𝜓 ) ∈ ℝ )
9		negeq	⊢ ( 𝑦 = ( ℩ 𝑦 ∈ ℝ 𝜓 ) → - 𝑦 = - ( ℩ 𝑦 ∈ ℝ 𝜓 ) )
10		renegcl	⊢ ( 𝑥 ∈ ℝ → - 𝑥 ∈ ℝ )
11		recn	⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ )
12		recn	⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℂ )
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	⊢ ( ∃! 𝑥 ∈ ℝ 𝜑 → ( ℩ 𝑥 ∈ ℝ 𝜑 ) = - ( ℩ 𝑦 ∈ ℝ 𝜓 ) )