Metamath Proof Explorer

Theorem 1neg1t1neg1

Description: An integer unit times itself. (Contributed by Thierry Arnoux, 23-Aug-2020)

Ref Expression
Assertion 1neg1t1neg1 
|- ( N e. { -u 1 , 1 } -> ( N x. N ) = 1 )

Proof

Step Hyp Ref Expression
1 elpri 
 |-  ( N e. { -u 1 , 1 } -> ( N = -u 1 \/ N = 1 ) )
2 id 
 |-  ( N = -u 1 -> N = -u 1 )
3 2 2 oveq12d 
 |-  ( N = -u 1 -> ( N x. N ) = ( -u 1 x. -u 1 ) )
4 neg1mulneg1e1 
 |-  ( -u 1 x. -u 1 ) = 1
5 3 4 eqtrdi 
 |-  ( N = -u 1 -> ( N x. N ) = 1 )
6 id 
 |-  ( N = 1 -> N = 1 )
7 6 6 oveq12d 
 |-  ( N = 1 -> ( N x. N ) = ( 1 x. 1 ) )
8 1t1e1 
 |-  ( 1 x. 1 ) = 1
9 7 8 eqtrdi 
 |-  ( N = 1 -> ( N x. N ) = 1 )
10 5 9 jaoi 
 |-  ( ( N = -u 1 \/ N = 1 ) -> ( N x. N ) = 1 )
11 1 10 syl 
 |-  ( N e. { -u 1 , 1 } -> ( N x. N ) = 1 )