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		eldifsn	$⊢ A \in (F ∖ \{0\}) \leftrightarrow (A \in F \land A \neq 0)$
19	18	biranri	$⊢ ((A \in F \land A \neq 0) \land (B \in ℝ \land - B \in ℕ)) \to A \in (F ∖ \{0\})$
20	17 1	sstri	$⊢ F ∖ \{0\} \subseteq ℂ$
21	17	sseli	$⊢ x \in (F ∖ \{0\}) \to x \in F$
22	17	sseli	$⊢ y \in (F ∖ \{0\}) \to y \in F$
23	21 22 2	syl2an	$⊢ (x \in (F ∖ \{0\}) \land y \in (F ∖ \{0\})) \to x y \in F$
24		eldifsn	$⊢ x \in (F ∖ \{0\}) \leftrightarrow (x \in F \land x \neq 0)$
25	1	sseli	$⊢ x \in F \to x \in ℂ$
26	25	anim1i	$⊢ (x \in F \land x \neq 0) \to (x \in ℂ \land x \neq 0)$
27	24 26	sylbi	$⊢ x \in (F ∖ \{0\}) \to (x \in ℂ \land x \neq 0)$
28		eldifsn	$⊢ y \in (F ∖ \{0\}) \leftrightarrow (y \in F \land y \neq 0)$
29	1	sseli	$⊢ y \in F \to y \in ℂ$
30	29	anim1i	$⊢ (y \in F \land y \neq 0) \to (y \in ℂ \land y \neq 0)$
31	28 30	sylbi	$⊢ y \in (F ∖ \{0\}) \to (y \in ℂ \land y \neq 0)$
32		mulne0	$⊢ ((x \in ℂ \land x \neq 0) \land (y \in ℂ \land y \neq 0)) \to x y \neq 0$
33	27 31 32	syl2an	$⊢ (x \in (F ∖ \{0\}) \land y \in (F ∖ \{0\})) \to x y \neq 0$
34		eldifsn	$⊢ x y \in (F ∖ \{0\}) \leftrightarrow (x y \in F \land x y \neq 0)$
35	23 33 34	sylanbrc	$⊢ (x \in (F ∖ \{0\}) \land y \in (F ∖ \{0\})) \to x y \in (F ∖ \{0\})$
36		ax-1ne0	$⊢ 1 \neq 0$
37		eldifsn	$⊢ 1 \in (F ∖ \{0\}) \leftrightarrow (1 \in F \land 1 \neq 0)$
38	3 36 37	mpbir2an	$⊢ 1 \in (F ∖ \{0\})$
39	20 35 38	expcllem	$⊢ (A \in (F ∖ \{0\}) \land - B \in ℕ_{0}) \to A^{- B} \in (F ∖ \{0\})$
40	19 14 39	syl2anc	$⊢ ((A \in F \land A \neq 0) \land (B \in ℝ \land - B \in ℕ)) \to A^{- B} \in (F ∖ \{0\})$
41	17 40	sselid	$⊢ ((A \in F \land A \neq 0) \land (B \in ℝ \land - B \in ℕ)) \to A^{- B} \in F$
42		eldifsn	$⊢ A^{- B} \in (F ∖ \{0\}) \leftrightarrow (A^{- B} \in F \land A^{- B} \neq 0)$
43	40 42	sylib	$⊢ ((A \in F \land A \neq 0) \land (B \in ℝ \land - B \in ℕ)) \to (A^{- B} \in F \land A^{- B} \neq 0)$
44	43	simprd	$⊢ ((A \in F \land A \neq 0) \land (B \in ℝ \land - B \in ℕ)) \to A^{- B} \neq 0$
45		neeq1	$⊢ x = A^{- B} \to (x \neq 0 \leftrightarrow A^{- B} \neq 0)$
46		oveq2	$⊢ x = A^{- B} \to \frac{1}{x} = \frac{1}{A^{- B}}$
47	46	eleq1d	$⊢ x = A^{- B} \to (\frac{1}{x} \in F \leftrightarrow \frac{1}{A^{- B}} \in F)$
48	45 47	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))$
49	4	ex	$⊢ x \in F \to (x \neq 0 \to \frac{1}{x} \in F)$
50	48 49	vtoclga	$⊢ A^{- B} \in F \to (A^{- B} \neq 0 \to \frac{1}{A^{- B}} \in F)$
51	41 44 50	sylc	$⊢ ((A \in F \land A \neq 0) \land (B \in ℝ \land - B \in ℕ)) \to \frac{1}{A^{- B}} \in F$
52	16 51	eqeltrd	$⊢ ((A \in F \land A \neq 0) \land (B \in ℝ \land - B \in ℕ)) \to A^{B} \in F$
53	52	ex	$⊢ (A \in F \land A \neq 0) \to ((B \in ℝ \land - B \in ℕ) \to A^{B} \in F)$
54	8 53	jaod	$⊢ (A \in F \land A \neq 0) \to ((B \in ℕ_{0} \lor (B \in ℝ \land - B \in ℕ)) \to A^{B} \in F)$
55	5 54	biimtrid	$⊢ (A \in F \land A \neq 0) \to (B \in ℤ \to A^{B} \in F)$
56	55	3impia	$⊢ (A \in F \land A \neq 0 \land B \in ℤ) \to A^{B} \in F$

Metamath Proof Explorer

Theorem expcl2lem

Proof