# 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 ${⊢}{N}\in ℤ\to {1}^{{N}}=1$

### Proof

Step Hyp Ref Expression
1 1ex ${⊢}1\in \mathrm{V}$
2 1 snid ${⊢}1\in \left\{1\right\}$
3 ax-1ne0 ${⊢}1\ne 0$
4 ax-1cn ${⊢}1\in ℂ$
5 snssi ${⊢}1\in ℂ\to \left\{1\right\}\subseteq ℂ$
6 4 5 ax-mp ${⊢}\left\{1\right\}\subseteq ℂ$
7 elsni ${⊢}{x}\in \left\{1\right\}\to {x}=1$
8 elsni ${⊢}{y}\in \left\{1\right\}\to {y}=1$
9 oveq12 ${⊢}\left({x}=1\wedge {y}=1\right)\to {x}{y}=1\cdot 1$
10 1t1e1 ${⊢}1\cdot 1=1$
11 9 10 eqtrdi ${⊢}\left({x}=1\wedge {y}=1\right)\to {x}{y}=1$
12 7 8 11 syl2an ${⊢}\left({x}\in \left\{1\right\}\wedge {y}\in \left\{1\right\}\right)\to {x}{y}=1$
13 ovex ${⊢}{x}{y}\in \mathrm{V}$
14 13 elsn ${⊢}{x}{y}\in \left\{1\right\}↔{x}{y}=1$
15 12 14 sylibr ${⊢}\left({x}\in \left\{1\right\}\wedge {y}\in \left\{1\right\}\right)\to {x}{y}\in \left\{1\right\}$
16 7 oveq2d ${⊢}{x}\in \left\{1\right\}\to \frac{1}{{x}}=\frac{1}{1}$
17 1div1e1 ${⊢}\frac{1}{1}=1$
18 16 17 eqtrdi ${⊢}{x}\in \left\{1\right\}\to \frac{1}{{x}}=1$
19 ovex ${⊢}\frac{1}{{x}}\in \mathrm{V}$
20 19 elsn ${⊢}\frac{1}{{x}}\in \left\{1\right\}↔\frac{1}{{x}}=1$
21 18 20 sylibr ${⊢}{x}\in \left\{1\right\}\to \frac{1}{{x}}\in \left\{1\right\}$
22 21 adantr ${⊢}\left({x}\in \left\{1\right\}\wedge {x}\ne 0\right)\to \frac{1}{{x}}\in \left\{1\right\}$
23 6 15 2 22 expcl2lem ${⊢}\left(1\in \left\{1\right\}\wedge 1\ne 0\wedge {N}\in ℤ\right)\to {1}^{{N}}\in \left\{1\right\}$
24 2 3 23 mp3an12 ${⊢}{N}\in ℤ\to {1}^{{N}}\in \left\{1\right\}$
25 elsni ${⊢}{1}^{{N}}\in \left\{1\right\}\to {1}^{{N}}=1$
26 24 25 syl ${⊢}{N}\in ℤ\to {1}^{{N}}=1$