Theorem 1exp

Description: Value of one raised to a nonnegative 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 )