Metamath Proof Explorer

Theorem neg1sqe1

Description: The square of -u 1 is 1. (Contributed by David A. Wheeler, 8-Dec-2018)

Ref Expression
Assertion neg1sqe1 
|- ( -u 1 ^ 2 ) = 1

Proof

Step Hyp Ref Expression
1 ax-1cn 
 |-  1 e. CC
2 sqneg 
 |-  ( 1 e. CC -> ( -u 1 ^ 2 ) = ( 1 ^ 2 ) )
3 1 2 ax-mp 
 |-  ( -u 1 ^ 2 ) = ( 1 ^ 2 )
4 sq1 
 |-  ( 1 ^ 2 ) = 1
5 3 4 eqtri 
 |-  ( -u 1 ^ 2 ) = 1