Metamath Proof Explorer


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 ( ∃! 𝑥 ∈ ℝ 𝜑 → ( 𝑥 ∈ ℝ 𝜑 ) = - ( 𝑦 ∈ ℝ 𝜓 ) )