expclzlem

Description: Closure law for integer exponentiation. (Contributed by Mario Carneiro, 4-Jun-2014)

		Ref	Expression
	Assertion	expclzlem	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to A^{N} \in (ℂ ∖ \{0\})$

Proof

Step	Hyp	Ref	Expression
1		eldifsn	$⊢ A \in (ℂ ∖ \{0\}) \leftrightarrow (A \in ℂ \land A \neq 0)$
2		difss	$⊢ ℂ ∖ \{0\} \subseteq ℂ$
3		eldifsn	$⊢ x \in (ℂ ∖ \{0\}) \leftrightarrow (x \in ℂ \land x \neq 0)$
4		eldifsn	$⊢ y \in (ℂ ∖ \{0\}) \leftrightarrow (y \in ℂ \land y \neq 0)$
5		mulcl	$⊢ (x \in ℂ \land y \in ℂ) \to x y \in ℂ$
6	5	ad2ant2r	$⊢ ((x \in ℂ \land x \neq 0) \land (y \in ℂ \land y \neq 0)) \to x y \in ℂ$
7		mulne0	$⊢ ((x \in ℂ \land x \neq 0) \land (y \in ℂ \land y \neq 0)) \to x y \neq 0$
8		eldifsn	$⊢ x y \in (ℂ ∖ \{0\}) \leftrightarrow (x y \in ℂ \land x y \neq 0)$
9	6 7 8	sylanbrc	$⊢ ((x \in ℂ \land x \neq 0) \land (y \in ℂ \land y \neq 0)) \to x y \in (ℂ ∖ \{0\})$
10	3 4 9	syl2anb	$⊢ (x \in (ℂ ∖ \{0\}) \land y \in (ℂ ∖ \{0\})) \to x y \in (ℂ ∖ \{0\})$
11		ax-1cn	$⊢ 1 \in ℂ$
12		ax-1ne0	$⊢ 1 \neq 0$
13		eldifsn	$⊢ 1 \in (ℂ ∖ \{0\}) \leftrightarrow (1 \in ℂ \land 1 \neq 0)$
14	11 12 13	mpbir2an	$⊢ 1 \in (ℂ ∖ \{0\})$
15		reccl	$⊢ (x \in ℂ \land x \neq 0) \to \frac{1}{x} \in ℂ$
16		recne0	$⊢ (x \in ℂ \land x \neq 0) \to \frac{1}{x} \neq 0$
17	15 16	jca	$⊢ (x \in ℂ \land x \neq 0) \to (\frac{1}{x} \in ℂ \land \frac{1}{x} \neq 0)$
18		eldifsn	$⊢ \frac{1}{x} \in (ℂ ∖ \{0\}) \leftrightarrow (\frac{1}{x} \in ℂ \land \frac{1}{x} \neq 0)$
19	17 3 18	3imtr4i	$⊢ x \in (ℂ ∖ \{0\}) \to \frac{1}{x} \in (ℂ ∖ \{0\})$
20	19	adantr	$⊢ (x \in (ℂ ∖ \{0\}) \land x \neq 0) \to \frac{1}{x} \in (ℂ ∖ \{0\})$
21	2 10 14 20	expcl2lem	$⊢ (A \in (ℂ ∖ \{0\}) \land A \neq 0 \land N \in ℤ) \to A^{N} \in (ℂ ∖ \{0\})$
22	21	3expia	$⊢ (A \in (ℂ ∖ \{0\}) \land A \neq 0) \to (N \in ℤ \to A^{N} \in (ℂ ∖ \{0\}))$
23	1 22	sylanbr	$⊢ ((A \in ℂ \land A \neq 0) \land A \neq 0) \to (N \in ℤ \to A^{N} \in (ℂ ∖ \{0\}))$
24	23	anabss3	$⊢ (A \in ℂ \land A \neq 0) \to (N \in ℤ \to A^{N} \in (ℂ ∖ \{0\}))$
25	24	3impia	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to A^{N} \in (ℂ ∖ \{0\})$

Metamath Proof Explorer

Theorem expclzlem

Proof