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 ( 𝑁 ∈ ℤ → ( 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 )