Metamath Proof Explorer

Theorem sq1

Description: The square of 1 is 1. (Contributed by NM, 22-Aug-1999)

Ref Expression
Assertion sq1 
|- ( 1 ^ 2 ) = 1

Proof

Step Hyp Ref Expression
1 2z 
 |-  2 e. ZZ
2 1exp 
 |-  ( 2 e. ZZ -> ( 1 ^ 2 ) = 1 )
3 1 2 ax-mp 
 |-  ( 1 ^ 2 ) = 1