This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 1exp

Description: Value of 1 raised to an integer power. (Contributed by NM, 15-Dec-2005) (Revised by Mario Carneiro, 4-Jun-2014)

Ref Expression
Assertion 1exp 
|- ( N e. ZZ -> ( 1 ^ N ) = 1 )

Proof

Step Hyp Ref Expression
1 1ex 
 |-  1 e. _V
2 1 snid 
 |-  1 e. { 1 }
3 ax-1ne0 
 |-  1 =/= 0
4 ax-1cn 
 |-  1 e. CC
5 snssi 
 |-  ( 1 e. CC -> { 1 } C_ CC )
6 4 5 ax-mp 
 |-  { 1 } C_ CC
7 elsni 
 |-  ( x e. { 1 } -> x = 1 )
8 elsni 
 |-  ( y e. { 1 } -> y = 1 )
9 oveq12 
 |-  ( ( x = 1 /\ y = 1 ) -> ( x x. y ) = ( 1 x. 1 ) )
10 1t1e1 
 |-  ( 1 x. 1 ) = 1
11 9 10 eqtrdi 
 |-  ( ( x = 1 /\ y = 1 ) -> ( x x. y ) = 1 )
12 7 8 11 syl2an 
 |-  ( ( x e. { 1 } /\ y e. { 1 } ) -> ( x x. y ) = 1 )
13 ovex 
 |-  ( x x. y ) e. _V
14 13 elsn 
 |-  ( ( x x. y ) e. { 1 } <-> ( x x. y ) = 1 )
15 12 14 sylibr 
 |-  ( ( x e. { 1 } /\ y e. { 1 } ) -> ( x x. y ) e. { 1 } )
16 7 oveq2d 
 |-  ( x e. { 1 } -> ( 1 / x ) = ( 1 / 1 ) )
17 1div1e1 
 |-  ( 1 / 1 ) = 1
18 16 17 eqtrdi 
 |-  ( x e. { 1 } -> ( 1 / x ) = 1 )
19 ovex 
 |-  ( 1 / x ) e. _V
20 19 elsn 
 |-  ( ( 1 / x ) e. { 1 } <-> ( 1 / x ) = 1 )
21 18 20 sylibr 
 |-  ( x e. { 1 } -> ( 1 / x ) e. { 1 } )
22 21 adantr 
 |-  ( ( x e. { 1 } /\ x =/= 0 ) -> ( 1 / x ) e. { 1 } )
23 6 15 2 22 expcl2lem 
 |-  ( ( 1 e. { 1 } /\ 1 =/= 0 /\ N e. ZZ ) -> ( 1 ^ N ) e. { 1 } )
24 2 3 23 mp3an12 
 |-  ( N e. ZZ -> ( 1 ^ N ) e. { 1 } )
25 elsni 
 |-  ( ( 1 ^ N ) e. { 1 } -> ( 1 ^ N ) = 1 )
26 24 25 syl 
 |-  ( N e. ZZ -> ( 1 ^ N ) = 1 )