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 \mathbb{Z}\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 xy=1\cdot 1$$
10		1t1e1	$$⊢1\cdot 1=1$$
11	9 10	eqtrdi	$$⊢\left(x=1\wedge y=1\right)\to xy=1$$
12	7 8 11	syl2an	$$⊢\left(x\in \left\{1\right\}\wedge y\in \left\{1\right\}\right)\to xy=1$$
13		ovex	$$⊢xy\in \mathrm{V}$$
14	13	elsn	$$⊢xy\in \left\{1\right\}\leftrightarrow xy=1$$
15	12 14	sylibr	$$⊢\left(x\in \left\{1\right\}\wedge y\in \left\{1\right\}\right)\to xy\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\}\leftrightarrow \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 \mathbb{Z}\right)\to 1^N\in \left\{1\right\}$$
24	2 3 23	mp3an12	$$⊢N\in \mathbb{Z}\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 \mathbb{Z}\to 1^N=1$$