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	⊢ ( 𝑁 ∈ ℤ → ( 1 ↑ 𝑁 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		1ex	⊢ 1 ∈ V
2	1	snid	⊢ 1 ∈ { 1 }
3		ax-1ne0	⊢ 1 ≠ 0
4		ax-1cn	⊢ 1 ∈ ℂ
5		snssi	⊢ ( 1 ∈ ℂ → { 1 } ⊆ ℂ )
6	4 5	ax-mp	⊢ { 1 } ⊆ ℂ
7		elsni	⊢ ( 𝑥 ∈ { 1 } → 𝑥 = 1 )
8		elsni	⊢ ( 𝑦 ∈ { 1 } → 𝑦 = 1 )
9		oveq12	⊢ ( ( 𝑥 = 1 ∧ 𝑦 = 1 ) → ( 𝑥 · 𝑦 ) = ( 1 · 1 ) )
10		1t1e1	⊢ ( 1 · 1 ) = 1
11	9 10	eqtrdi	⊢ ( ( 𝑥 = 1 ∧ 𝑦 = 1 ) → ( 𝑥 · 𝑦 ) = 1 )
12	7 8 11	syl2an	⊢ ( ( 𝑥 ∈ { 1 } ∧ 𝑦 ∈ { 1 } ) → ( 𝑥 · 𝑦 ) = 1 )
13		ovex	⊢ ( 𝑥 · 𝑦 ) ∈ V
14	13	elsn	⊢ ( ( 𝑥 · 𝑦 ) ∈ { 1 } ↔ ( 𝑥 · 𝑦 ) = 1 )
15	12 14	sylibr	⊢ ( ( 𝑥 ∈ { 1 } ∧ 𝑦 ∈ { 1 } ) → ( 𝑥 · 𝑦 ) ∈ { 1 } )
16	7	oveq2d	⊢ ( 𝑥 ∈ { 1 } → ( 1 / 𝑥 ) = ( 1 / 1 ) )
17		1div1e1	⊢ ( 1 / 1 ) = 1
18	16 17	eqtrdi	⊢ ( 𝑥 ∈ { 1 } → ( 1 / 𝑥 ) = 1 )
19		ovex	⊢ ( 1 / 𝑥 ) ∈ V
20	19	elsn	⊢ ( ( 1 / 𝑥 ) ∈ { 1 } ↔ ( 1 / 𝑥 ) = 1 )
21	18 20	sylibr	⊢ ( 𝑥 ∈ { 1 } → ( 1 / 𝑥 ) ∈ { 1 } )
22	21	adantr	⊢ ( ( 𝑥 ∈ { 1 } ∧ 𝑥 ≠ 0 ) → ( 1 / 𝑥 ) ∈ { 1 } )
23	6 15 2 22	expcl2lem	⊢ ( ( 1 ∈ { 1 } ∧ 1 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 1 ↑ 𝑁 ) ∈ { 1 } )
24	2 3 23	mp3an12	⊢ ( 𝑁 ∈ ℤ → ( 1 ↑ 𝑁 ) ∈ { 1 } )
25		elsni	⊢ ( ( 1 ↑ 𝑁 ) ∈ { 1 } → ( 1 ↑ 𝑁 ) = 1 )
26	24 25	syl	⊢ ( 𝑁 ∈ ℤ → ( 1 ↑ 𝑁 ) = 1 )