Theorem 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	⊢ 𝐹 ⊆ ℂ
	expcllem.2	⊢ ( ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) → ( 𝑥 · 𝑦 ) ∈ 𝐹 )
	expcllem.3	⊢ 1 ∈ 𝐹
	expcl2lem.4	⊢ ( ( 𝑥 ∈ 𝐹 ∧ 𝑥 ≠ 0 ) → ( 1 / 𝑥 ) ∈ 𝐹 )
Assertion	expcl2lem	⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℤ ) → ( 𝐴 ↑ 𝐵 ) ∈ 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		expcllem.1	⊢ 𝐹 ⊆ ℂ
2		expcllem.2	⊢ ( ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) → ( 𝑥 · 𝑦 ) ∈ 𝐹 )
3		expcllem.3	⊢ 1 ∈ 𝐹
4		expcl2lem.4	⊢ ( ( 𝑥 ∈ 𝐹 ∧ 𝑥 ≠ 0 ) → ( 1 / 𝑥 ) ∈ 𝐹 )
5		elznn0nn	⊢ ( 𝐵 ∈ ℤ ↔ ( 𝐵 ∈ ℕ0 ∨ ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) ) )
6	1 2 3	expcllem	⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 ↑ 𝐵 ) ∈ 𝐹 )
7	6	ex	⊢ ( 𝐴 ∈ 𝐹 → ( 𝐵 ∈ ℕ0 → ( 𝐴 ↑ 𝐵 ) ∈ 𝐹 ) )
8	7	adantr	⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) → ( 𝐵 ∈ ℕ0 → ( 𝐴 ↑ 𝐵 ) ∈ 𝐹 ) )
9		simpll	⊢ ( ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) ) → 𝐴 ∈ 𝐹 )
10	1 9	sselid	⊢ ( ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) ) → 𝐴 ∈ ℂ )
11		simprl	⊢ ( ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) ) → 𝐵 ∈ ℝ )
12	11	recnd	⊢ ( ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) ) → 𝐵 ∈ ℂ )
13		nnnn0	⊢ ( - 𝐵 ∈ ℕ → - 𝐵 ∈ ℕ0 )
14	13	ad2antll	⊢ ( ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) ) → - 𝐵 ∈ ℕ0 )
15		expneg2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ - 𝐵 ∈ ℕ0 ) → ( 𝐴 ↑ 𝐵 ) = ( 1 / ( 𝐴 ↑ - 𝐵 ) ) )
16	10 12 14 15	syl3anc	⊢ ( ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) ) → ( 𝐴 ↑ 𝐵 ) = ( 1 / ( 𝐴 ↑ - 𝐵 ) ) )
17		difss	⊢ ( 𝐹 ∖ { 0 } ) ⊆ 𝐹
18		simpl	⊢ ( ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) ) → ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) )
19		eldifsn	⊢ ( 𝐴 ∈ ( 𝐹 ∖ { 0 } ) ↔ ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) )
20	18 19	sylibr	⊢ ( ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) ) → 𝐴 ∈ ( 𝐹 ∖ { 0 } ) )
21	17 1	sstri	⊢ ( 𝐹 ∖ { 0 } ) ⊆ ℂ
22	17	sseli	⊢ ( 𝑥 ∈ ( 𝐹 ∖ { 0 } ) → 𝑥 ∈ 𝐹 )
23	17	sseli	⊢ ( 𝑦 ∈ ( 𝐹 ∖ { 0 } ) → 𝑦 ∈ 𝐹 )
24	22 23 2	syl2an	⊢ ( ( 𝑥 ∈ ( 𝐹 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝐹 ∖ { 0 } ) ) → ( 𝑥 · 𝑦 ) ∈ 𝐹 )
25		eldifsn	⊢ ( 𝑥 ∈ ( 𝐹 ∖ { 0 } ) ↔ ( 𝑥 ∈ 𝐹 ∧ 𝑥 ≠ 0 ) )
26	1	sseli	⊢ ( 𝑥 ∈ 𝐹 → 𝑥 ∈ ℂ )
27	26	anim1i	⊢ ( ( 𝑥 ∈ 𝐹 ∧ 𝑥 ≠ 0 ) → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
28	25 27	sylbi	⊢ ( 𝑥 ∈ ( 𝐹 ∖ { 0 } ) → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
29		eldifsn	⊢ ( 𝑦 ∈ ( 𝐹 ∖ { 0 } ) ↔ ( 𝑦 ∈ 𝐹 ∧ 𝑦 ≠ 0 ) )
30	1	sseli	⊢ ( 𝑦 ∈ 𝐹 → 𝑦 ∈ ℂ )
31	30	anim1i	⊢ ( ( 𝑦 ∈ 𝐹 ∧ 𝑦 ≠ 0 ) → ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) )
32	29 31	sylbi	⊢ ( 𝑦 ∈ ( 𝐹 ∖ { 0 } ) → ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) )
33		mulne0	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ) → ( 𝑥 · 𝑦 ) ≠ 0 )
34	28 32 33	syl2an	⊢ ( ( 𝑥 ∈ ( 𝐹 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝐹 ∖ { 0 } ) ) → ( 𝑥 · 𝑦 ) ≠ 0 )
35		eldifsn	⊢ ( ( 𝑥 · 𝑦 ) ∈ ( 𝐹 ∖ { 0 } ) ↔ ( ( 𝑥 · 𝑦 ) ∈ 𝐹 ∧ ( 𝑥 · 𝑦 ) ≠ 0 ) )
36	24 34 35	sylanbrc	⊢ ( ( 𝑥 ∈ ( 𝐹 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝐹 ∖ { 0 } ) ) → ( 𝑥 · 𝑦 ) ∈ ( 𝐹 ∖ { 0 } ) )
37		ax-1ne0	⊢ 1 ≠ 0
38		eldifsn	⊢ ( 1 ∈ ( 𝐹 ∖ { 0 } ) ↔ ( 1 ∈ 𝐹 ∧ 1 ≠ 0 ) )
39	3 37 38	mpbir2an	⊢ 1 ∈ ( 𝐹 ∖ { 0 } )
40	21 36 39	expcllem	⊢ ( ( 𝐴 ∈ ( 𝐹 ∖ { 0 } ) ∧ - 𝐵 ∈ ℕ0 ) → ( 𝐴 ↑ - 𝐵 ) ∈ ( 𝐹 ∖ { 0 } ) )
41	20 14 40	syl2anc	⊢ ( ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) ) → ( 𝐴 ↑ - 𝐵 ) ∈ ( 𝐹 ∖ { 0 } ) )
42	17 41	sselid	⊢ ( ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) ) → ( 𝐴 ↑ - 𝐵 ) ∈ 𝐹 )
43		eldifsn	⊢ ( ( 𝐴 ↑ - 𝐵 ) ∈ ( 𝐹 ∖ { 0 } ) ↔ ( ( 𝐴 ↑ - 𝐵 ) ∈ 𝐹 ∧ ( 𝐴 ↑ - 𝐵 ) ≠ 0 ) )
44	41 43	sylib	⊢ ( ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) ) → ( ( 𝐴 ↑ - 𝐵 ) ∈ 𝐹 ∧ ( 𝐴 ↑ - 𝐵 ) ≠ 0 ) )
45	44	simprd	⊢ ( ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) ) → ( 𝐴 ↑ - 𝐵 ) ≠ 0 )
46		neeq1	⊢ ( 𝑥 = ( 𝐴 ↑ - 𝐵 ) → ( 𝑥 ≠ 0 ↔ ( 𝐴 ↑ - 𝐵 ) ≠ 0 ) )
47		oveq2	⊢ ( 𝑥 = ( 𝐴 ↑ - 𝐵 ) → ( 1 / 𝑥 ) = ( 1 / ( 𝐴 ↑ - 𝐵 ) ) )
48	47	eleq1d	⊢ ( 𝑥 = ( 𝐴 ↑ - 𝐵 ) → ( ( 1 / 𝑥 ) ∈ 𝐹 ↔ ( 1 / ( 𝐴 ↑ - 𝐵 ) ) ∈ 𝐹 ) )
49	46 48	imbi12d	⊢ ( 𝑥 = ( 𝐴 ↑ - 𝐵 ) → ( ( 𝑥 ≠ 0 → ( 1 / 𝑥 ) ∈ 𝐹 ) ↔ ( ( 𝐴 ↑ - 𝐵 ) ≠ 0 → ( 1 / ( 𝐴 ↑ - 𝐵 ) ) ∈ 𝐹 ) ) )
50	4	ex	⊢ ( 𝑥 ∈ 𝐹 → ( 𝑥 ≠ 0 → ( 1 / 𝑥 ) ∈ 𝐹 ) )
51	49 50	vtoclga	⊢ ( ( 𝐴 ↑ - 𝐵 ) ∈ 𝐹 → ( ( 𝐴 ↑ - 𝐵 ) ≠ 0 → ( 1 / ( 𝐴 ↑ - 𝐵 ) ) ∈ 𝐹 ) )
52	42 45 51	sylc	⊢ ( ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) ) → ( 1 / ( 𝐴 ↑ - 𝐵 ) ) ∈ 𝐹 )
53	16 52	eqeltrd	⊢ ( ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) ) → ( 𝐴 ↑ 𝐵 ) ∈ 𝐹 )
54	53	ex	⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) → ( ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) → ( 𝐴 ↑ 𝐵 ) ∈ 𝐹 ) )
55	8 54	jaod	⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) → ( ( 𝐵 ∈ ℕ0 ∨ ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) ) → ( 𝐴 ↑ 𝐵 ) ∈ 𝐹 ) )
56	5 55	biimtrid	⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) → ( 𝐵 ∈ ℤ → ( 𝐴 ↑ 𝐵 ) ∈ 𝐹 ) )
57	56	3impia	⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℤ ) → ( 𝐴 ↑ 𝐵 ) ∈ 𝐹 )