Metamath Proof Explorer


Theorem neg1sqe1

Description: -u 1 squared 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