Metamath Proof Explorer


Theorem ex-pr

Description: Example for df-pr . (Contributed by Mario Carneiro, 7-May-2015)

Ref Expression
Assertion ex-pr
|- ( A e. { 1 , -u 1 } -> ( A ^ 2 ) = 1 )

Proof

Step Hyp Ref Expression
1 elpri
 |-  ( A e. { 1 , -u 1 } -> ( A = 1 \/ A = -u 1 ) )
2 oveq1
 |-  ( A = 1 -> ( A ^ 2 ) = ( 1 ^ 2 ) )
3 sq1
 |-  ( 1 ^ 2 ) = 1
4 2 3 eqtrdi
 |-  ( A = 1 -> ( A ^ 2 ) = 1 )
5 oveq1
 |-  ( A = -u 1 -> ( A ^ 2 ) = ( -u 1 ^ 2 ) )
6 neg1sqe1
 |-  ( -u 1 ^ 2 ) = 1
7 5 6 eqtrdi
 |-  ( A = -u 1 -> ( A ^ 2 ) = 1 )
8 4 7 jaoi
 |-  ( ( A = 1 \/ A = -u 1 ) -> ( A ^ 2 ) = 1 )
9 1 8 syl
 |-  ( A e. { 1 , -u 1 } -> ( A ^ 2 ) = 1 )