Metamath Proof Explorer


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 )