This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ex-pr

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

Ref Expression
Assertion ex-pr ⊢ A ∈ 1 − 1 → A 2 = 1

Proof

Step Hyp Ref Expression
1 elpri ⊢ A ∈ 1 − 1 → A = 1 ∨ A = − 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 = − 1 → A 2 = − 1 2
6 neg1sqe1 ⊢ − 1 2 = 1
7 5 6 eqtrdi ⊢ A = − 1 → A 2 = 1
8 4 7 jaoi ⊢ A = 1 ∨ A = − 1 → A 2 = 1
9 1 8 syl ⊢ A ∈ 1 − 1 → A 2 = 1