Metamath Proof Explorer

Theorem zriotaneg

Description: The negative of the unique integer such that ph . (Contributed by AV, 1-Dec-2018)

Ref Expression
Hypothesis zriotaneg.1 
|- ( x = -u y -> ( ph <-> ps ) )
Assertion zriotaneg 
|- ( E! x e. ZZ ph -> ( iota_ x e. ZZ ph ) = -u ( iota_ y e. ZZ ps ) )

Proof

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