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 syl6eq 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 syl6eq 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