Theorem 1neg1t1neg1

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

	Ref	Expression
Assertion	1neg1t1neg1	⊢ ( 𝑁 ∈ { - 1 , 1 } → ( 𝑁 · 𝑁 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		elpri	⊢ ( 𝑁 ∈ { - 1 , 1 } → ( 𝑁 = - 1 ∨ 𝑁 = 1 ) )
2		id	⊢ ( 𝑁 = - 1 → 𝑁 = - 1 )
3	2 2	oveq12d	⊢ ( 𝑁 = - 1 → ( 𝑁 · 𝑁 ) = ( - 1 · - 1 ) )
4		neg1mulneg1e1	⊢ ( - 1 · - 1 ) = 1
5	3 4	eqtrdi	⊢ ( 𝑁 = - 1 → ( 𝑁 · 𝑁 ) = 1 )
6		id	⊢ ( 𝑁 = 1 → 𝑁 = 1 )
7	6 6	oveq12d	⊢ ( 𝑁 = 1 → ( 𝑁 · 𝑁 ) = ( 1 · 1 ) )
8		1t1e1	⊢ ( 1 · 1 ) = 1
9	7 8	eqtrdi	⊢ ( 𝑁 = 1 → ( 𝑁 · 𝑁 ) = 1 )
10	5 9	jaoi	⊢ ( ( 𝑁 = - 1 ∨ 𝑁 = 1 ) → ( 𝑁 · 𝑁 ) = 1 )
11	1 10	syl	⊢ ( 𝑁 ∈ { - 1 , 1 } → ( 𝑁 · 𝑁 ) = 1 )