Theorem ex-pr

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

	Ref	Expression
Assertion	ex-pr	$$⊢A\in \left\{1,-1\right\}\to A^2=1$$

Proof

Step	Hyp	Ref	Expression
1		elpri	$$⊢A\in \left\{1,-1\right\}\to \left(A=1\vee A=-1\right)$$
2		oveq1	$$⊢A=1\to A^2=1^2$$
3		sq1	$$⊢1^2=1$$
4	2 3	eqtrdi	$$⊢A=1\to A^2=1$$
5		oveq1	$$⊢A=-1\to A^2={\left(-1\right)}^2$$
6		neg1sqe1	$$⊢{\left(-1\right)}^2=1$$
7	5 6	eqtrdi	$$⊢A=-1\to A^2=1$$
8	4 7	jaoi	$$⊢\left(A=1\vee A=-1\right)\to A^2=1$$
9	1 8	syl	$$⊢A\in \left\{1,-1\right\}\to A^2=1$$