This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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