expcl2lem

Description: Lemma for proving integer exponentiation closure laws. (Contributed by Mario Carneiro, 4-Jun-2014) (Revised by Mario Carneiro, 9-Sep-2014)

	Ref	Expression
Hypotheses	expcllem.1	$⊢ F \subseteq ℂ$
	expcllem.2	$⊢ (x \in F \land y \in F) \to x y \in F$
	expcllem.3	$⊢ 1 \in F$
	expcl2lem.4	$⊢ (x \in F \land x \neq 0) \to \frac{1}{x} \in F$
Assertion	expcl2lem	$⊢ (A \in F \land A \neq 0 \land B \in ℤ) \to A^{B} \in F$

Proof

Step	Hyp	Ref	Expression
1		expcllem.1	$⊢ F \subseteq ℂ$
2		expcllem.2	$⊢ (x \in F \land y \in F) \to x y \in F$
3		expcllem.3	$⊢ 1 \in F$
4		expcl2lem.4	$⊢ (x \in F \land x \neq 0) \to \frac{1}{x} \in F$
5		elznn0nn	$⊢ B \in ℤ \leftrightarrow (B \in ℕ_{0} \lor (B \in ℝ \land - B \in ℕ))$
6	1 2 3	expcllem	$⊢ (A \in F \land B \in ℕ_{0}) \to A^{B} \in F$
7	6	ex	$⊢ A \in F \to (B \in ℕ_{0} \to A^{B} \in F)$
8	7	adantr	$⊢ (A \in F \land A \neq 0) \to (B \in ℕ_{0} \to A^{B} \in F)$
9		simpll	$⊢ ((A \in F \land A \neq 0) \land (B \in ℝ \land - B \in ℕ)) \to A \in F$
10	1 9	sselid	$⊢ ((A \in F \land A \neq 0) \land (B \in ℝ \land - B \in ℕ)) \to A \in ℂ$
11		simprl	$⊢ ((A \in F \land A \neq 0) \land (B \in ℝ \land - B \in ℕ)) \to B \in ℝ$
12	11	recnd	$⊢ ((A \in F \land A \neq 0) \land (B \in ℝ \land - B \in ℕ)) \to B \in ℂ$
13		nnnn0	$⊢ - B \in ℕ \to - B \in ℕ_{0}$
14	13	ad2antll	$⊢ ((A \in F \land A \neq 0) \land (B \in ℝ \land - B \in ℕ)) \to - B \in ℕ_{0}$
15		expneg2	$⊢ (A \in ℂ \land B \in ℂ \land - B \in ℕ_{0}) \to A^{B} = \frac{1}{A^{- B}}$
16	10 12 14 15	syl3anc	$⊢ ((A \in F \land A \neq 0) \land (B \in ℝ \land - B \in ℕ)) \to A^{B} = \frac{1}{A^{- B}}$
17		difss	$⊢ F ∖ \{0\} \subseteq F$
18		simpl	$⊢ ((A \in F \land A \neq 0) \land (B \in ℝ \land - B \in ℕ)) \to (A \in F \land A \neq 0)$
19		eldifsn	$⊢ A \in (F ∖ \{0\}) \leftrightarrow (A \in F \land A \neq 0)$
20	18 19	sylibr	$⊢ ((A \in F \land A \neq 0) \land (B \in ℝ \land - B \in ℕ)) \to A \in (F ∖ \{0\})$
21	17 1	sstri	$⊢ F ∖ \{0\} \subseteq ℂ$
22	17	sseli	$⊢ x \in (F ∖ \{0\}) \to x \in F$
23	17	sseli	$⊢ y \in (F ∖ \{0\}) \to y \in F$
24	22 23 2	syl2an	$⊢ (x \in (F ∖ \{0\}) \land y \in (F ∖ \{0\})) \to x y \in F$
25		eldifsn	$⊢ x \in (F ∖ \{0\}) \leftrightarrow (x \in F \land x \neq 0)$
26	1	sseli	$⊢ x \in F \to x \in ℂ$
27	26	anim1i	$⊢ (x \in F \land x \neq 0) \to (x \in ℂ \land x \neq 0)$
28	25 27	sylbi	$⊢ x \in (F ∖ \{0\}) \to (x \in ℂ \land x \neq 0)$
29		eldifsn	$⊢ y \in (F ∖ \{0\}) \leftrightarrow (y \in F \land y \neq 0)$
30	1	sseli	$⊢ y \in F \to y \in ℂ$
31	30	anim1i	$⊢ (y \in F \land y \neq 0) \to (y \in ℂ \land y \neq 0)$
32	29 31	sylbi	$⊢ y \in (F ∖ \{0\}) \to (y \in ℂ \land y \neq 0)$
33		mulne0	$⊢ ((x \in ℂ \land x \neq 0) \land (y \in ℂ \land y \neq 0)) \to x y \neq 0$
34	28 32 33	syl2an	$⊢ (x \in (F ∖ \{0\}) \land y \in (F ∖ \{0\})) \to x y \neq 0$
35		eldifsn	$⊢ x y \in (F ∖ \{0\}) \leftrightarrow (x y \in F \land x y \neq 0)$
36	24 34 35	sylanbrc	$⊢ (x \in (F ∖ \{0\}) \land y \in (F ∖ \{0\})) \to x y \in (F ∖ \{0\})$
37		ax-1ne0	$⊢ 1 \neq 0$
38		eldifsn	$⊢ 1 \in (F ∖ \{0\}) \leftrightarrow (1 \in F \land 1 \neq 0)$
39	3 37 38	mpbir2an	$⊢ 1 \in (F ∖ \{0\})$
40	21 36 39	expcllem	$⊢ (A \in (F ∖ \{0\}) \land - B \in ℕ_{0}) \to A^{- B} \in (F ∖ \{0\})$
41	20 14 40	syl2anc	$⊢ ((A \in F \land A \neq 0) \land (B \in ℝ \land - B \in ℕ)) \to A^{- B} \in (F ∖ \{0\})$
42	17 41	sselid	$⊢ ((A \in F \land A \neq 0) \land (B \in ℝ \land - B \in ℕ)) \to A^{- B} \in F$
43		eldifsn	$⊢ A^{- B} \in (F ∖ \{0\}) \leftrightarrow (A^{- B} \in F \land A^{- B} \neq 0)$
44	41 43	sylib	$⊢ ((A \in F \land A \neq 0) \land (B \in ℝ \land - B \in ℕ)) \to (A^{- B} \in F \land A^{- B} \neq 0)$
45	44	simprd	$⊢ ((A \in F \land A \neq 0) \land (B \in ℝ \land - B \in ℕ)) \to A^{- B} \neq 0$
46		neeq1	$⊢ x = A^{- B} \to (x \neq 0 \leftrightarrow A^{- B} \neq 0)$
47		oveq2	$⊢ x = A^{- B} \to \frac{1}{x} = \frac{1}{A^{- B}}$
48	47	eleq1d	$⊢ x = A^{- B} \to (\frac{1}{x} \in F \leftrightarrow \frac{1}{A^{- B}} \in F)$
49	46 48	imbi12d	$⊢ x = A^{- B} \to ((x \neq 0 \to \frac{1}{x} \in F) \leftrightarrow (A^{- B} \neq 0 \to \frac{1}{A^{- B}} \in F))$
50	4	ex	$⊢ x \in F \to (x \neq 0 \to \frac{1}{x} \in F)$
51	49 50	vtoclga	$⊢ A^{- B} \in F \to (A^{- B} \neq 0 \to \frac{1}{A^{- B}} \in F)$
52	42 45 51	sylc	$⊢ ((A \in F \land A \neq 0) \land (B \in ℝ \land - B \in ℕ)) \to \frac{1}{A^{- B}} \in F$
53	16 52	eqeltrd	$⊢ ((A \in F \land A \neq 0) \land (B \in ℝ \land - B \in ℕ)) \to A^{B} \in F$
54	53	ex	$⊢ (A \in F \land A \neq 0) \to ((B \in ℝ \land - B \in ℕ) \to A^{B} \in F)$
55	8 54	jaod	$⊢ (A \in F \land A \neq 0) \to ((B \in ℕ_{0} \lor (B \in ℝ \land - B \in ℕ)) \to A^{B} \in F)$
56	5 55	biimtrid	$⊢ (A \in F \land A \neq 0) \to (B \in ℤ \to A^{B} \in F)$
57	56	3impia	$⊢ (A \in F \land A \neq 0 \land B \in ℤ) \to A^{B} \in F$

Metamath Proof Explorer

Theorem expcl2lem

Proof