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 ⊢ x = − y → φ ↔ ψ
Assertion riotaneg ⊢ ∃! x ∈ ℝ φ → ι x ∈ ℝ | φ = − ι y ∈ ℝ | ψ

Proof

Step Hyp Ref Expression
1 riotaneg.1 ⊢ x = − y → φ ↔ ψ
2 tru ⊢ ⊤
3 nfriota1 ⊢ Ⅎ _ y ι y ∈ ℝ | ψ
4 3 nfneg ⊢ Ⅎ _ y − ι y ∈ ℝ | ψ
5 renegcl ⊢ y ∈ ℝ → − y ∈ ℝ
6 5 adantl ⊢ ⊤ ∧ y ∈ ℝ → − y ∈ ℝ
7 simpr ⊢ ⊤ ∧ ι y ∈ ℝ | ψ ∈ ℝ → ι y ∈ ℝ | ψ ∈ ℝ
8 7 renegcld ⊢ ⊤ ∧ ι y ∈ ℝ | ψ ∈ ℝ → − ι y ∈ ℝ | ψ ∈ ℝ
9 negeq ⊢ y = ι y ∈ ℝ | ψ → − y = − ι y ∈ ℝ | ψ
10 renegcl ⊢ x ∈ ℝ → − x ∈ ℝ
11 recn ⊢ x ∈ ℝ → x ∈ ℂ
12 recn ⊢ y ∈ ℝ → y ∈ ℂ
13 negcon2 ⊢ x ∈ ℂ ∧ y ∈ ℂ → x = − y ↔ y = − x
14 11 12 13 syl2an ⊢ x ∈ ℝ ∧ y ∈ ℝ → x = − y ↔ y = − x
15 10 14 reuhyp ⊢ x ∈ ℝ → ∃! y ∈ ℝ x = − y
16 15 adantl ⊢ ⊤ ∧ x ∈ ℝ → ∃! y ∈ ℝ x = − y
17 4 6 8 1 9 16 riotaxfrd ⊢ ⊤ ∧ ∃! x ∈ ℝ φ → ι x ∈ ℝ | φ = − ι y ∈ ℝ | ψ
18 2 17 mpan ⊢ ∃! x ∈ ℝ φ → ι x ∈ ℝ | φ = − ι y ∈ ℝ | ψ