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 )