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 ) )