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 = -u y -> ( ph <-> ps ) )
Assertion riotaneg
|- ( E! x e. RR ph -> ( iota_ x e. RR ph ) = -u ( iota_ y e. RR ps ) )

Proof

Step Hyp Ref Expression
1 riotaneg.1
 |-  ( x = -u y -> ( ph <-> ps ) )
2 tru
 |-  T.
3 nfriota1
 |-  F/_ y ( iota_ y e. RR ps )
4 3 nfneg
 |-  F/_ y -u ( iota_ y e. RR ps )
5 renegcl
 |-  ( y e. RR -> -u y e. RR )
6 5 adantl
 |-  ( ( T. /\ y e. RR ) -> -u y e. RR )
7 simpr
 |-  ( ( T. /\ ( iota_ y e. RR ps ) e. RR ) -> ( iota_ y e. RR ps ) e. RR )
8 7 renegcld
 |-  ( ( T. /\ ( iota_ y e. RR ps ) e. RR ) -> -u ( iota_ y e. RR ps ) e. RR )
9 negeq
 |-  ( y = ( iota_ y e. RR ps ) -> -u y = -u ( iota_ y e. RR ps ) )
10 renegcl
 |-  ( x e. RR -> -u x e. RR )
11 recn
 |-  ( x e. RR -> x e. CC )
12 recn
 |-  ( y e. RR -> y e. CC )
13 negcon2
 |-  ( ( x e. CC /\ y e. CC ) -> ( x = -u y <-> y = -u x ) )
14 11 12 13 syl2an
 |-  ( ( x e. RR /\ y e. RR ) -> ( x = -u y <-> y = -u x ) )
15 10 14 reuhyp
 |-  ( x e. RR -> E! y e. RR x = -u y )
16 15 adantl
 |-  ( ( T. /\ x e. RR ) -> E! y e. RR x = -u y )
17 4 6 8 1 9 16 riotaxfrd
 |-  ( ( T. /\ E! x e. RR ph ) -> ( iota_ x e. RR ph ) = -u ( iota_ y e. RR ps ) )
18 2 17 mpan
 |-  ( E! x e. RR ph -> ( iota_ x e. RR ph ) = -u ( iota_ y e. RR ps ) )