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

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

Metamath Proof Explorer