Metamath Proof Explorer

Theorem 1neg1t1neg1

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

Ref Expression
Assertion 1neg1t1neg1 ⊢ N ∈ − 1 1 → N ⋅ N = 1

Proof

Step Hyp Ref Expression
1 elpri ⊢ N ∈ − 1 1 → N = − 1 ∨ N = 1
2 id ⊢ N = − 1 → N = − 1
3 2 2 oveq12d ⊢ N = − 1 → N ⋅ N = -1 ⁢ -1
4 neg1mulneg1e1 ⊢ -1 ⁢ -1 = 1
5 3 4 eqtrdi ⊢ N = − 1 → N ⋅ N = 1
6 id ⊢ N = 1 → N = 1
7 6 6 oveq12d ⊢ N = 1 → N ⋅ N = 1 ⋅ 1
8 1t1e1 ⊢ 1 ⋅ 1 = 1
9 7 8 eqtrdi ⊢ N = 1 → N ⋅ N = 1
10 5 9 jaoi ⊢ N = − 1 ∨ N = 1 → N ⋅ N = 1
11 1 10 syl ⊢ N ∈ − 1 1 → N ⋅ N = 1