Theorem expcllem

Description: Lemma for proving nonnegative integer exponentiation closure laws. (Contributed by NM, 14-Dec-2005)

	Ref	Expression
Hypotheses	expcllem.1	$$⊢F\subseteq ℂ$$
	expcllem.2	$$⊢\left(x\in F\wedge y\in F\right)\to xy\in F$$
	expcllem.3	$$⊢1\in F$$
Assertion	expcllem	$$⊢\left(A\in F\wedge B\in {\mathbb{N}}_0\right)\to A^B\in F$$

Proof

Step	Hyp	Ref	Expression
1		expcllem.1	$$⊢F\subseteq ℂ$$
2		expcllem.2	$$⊢\left(x\in F\wedge y\in F\right)\to xy\in F$$
3		expcllem.3	$$⊢1\in F$$
4		elnn0	$$⊢B\in {\mathbb{N}}_0\leftrightarrow \left(B\in \mathbb{N}\vee B=0\right)$$
5		oveq2	$$⊢z=1\to A^z=A^1$$
6	5	eleq1d	$$⊢z=1\to \left(A^z\in F\leftrightarrow A^1\in F\right)$$
7	6	imbi2d	$$⊢z=1\to \left(\left(A\in F\to A^z\in F\right)\leftrightarrow \left(A\in F\to A^1\in F\right)\right)$$
8		oveq2	$$⊢z=w\to A^z=A^w$$
9	8	eleq1d	$$⊢z=w\to \left(A^z\in F\leftrightarrow A^w\in F\right)$$
10	9	imbi2d	$$⊢z=w\to \left(\left(A\in F\to A^z\in F\right)\leftrightarrow \left(A\in F\to A^w\in F\right)\right)$$
11		oveq2	$$⊢z=w+1\to A^z=A^{w+1}$$
12	11	eleq1d	$$⊢z=w+1\to \left(A^z\in F\leftrightarrow A^{w+1}\in F\right)$$
13	12	imbi2d	$$⊢z=w+1\to \left(\left(A\in F\to A^z\in F\right)\leftrightarrow \left(A\in F\to A^{w+1}\in F\right)\right)$$
14		oveq2	$$⊢z=B\to A^z=A^B$$
15	14	eleq1d	$$⊢z=B\to \left(A^z\in F\leftrightarrow A^B\in F\right)$$
16	15	imbi2d	$$⊢z=B\to \left(\left(A\in F\to A^z\in F\right)\leftrightarrow \left(A\in F\to A^B\in F\right)\right)$$
17	1	sseli	$$⊢A\in F\to A\in ℂ$$
18		exp1	$$⊢A\in ℂ\to A^1=A$$
19	17 18	syl	$$⊢A\in F\to A^1=A$$
20	19	eleq1d	$$⊢A\in F\to \left(A^1\in F\leftrightarrow A\in F\right)$$
21	20	ibir	$$⊢A\in F\to A^1\in F$$
22	2	caovcl	$$⊢\left(A^w\in F\wedge A\in F\right)\to A^{w}A\in F$$
23	22	ancoms	$$⊢\left(A\in F\wedge A^w\in F\right)\to A^{w}A\in F$$
24	23	adantlr	$$⊢\left(\left(A\in F\wedge w\in \mathbb{N}\right)\wedge A^w\in F\right)\to A^{w}A\in F$$
25		nnnn0	$$⊢w\in \mathbb{N}\to w\in {\mathbb{N}}_0$$
26		expp1	$$⊢\left(A\in ℂ\wedge w\in {\mathbb{N}}_0\right)\to A^{w+1}=A^{w}A$$
27	17 25 26	syl2an	$$⊢\left(A\in F\wedge w\in \mathbb{N}\right)\to A^{w+1}=A^{w}A$$
28	27	eleq1d	$$⊢\left(A\in F\wedge w\in \mathbb{N}\right)\to \left(A^{w+1}\in F\leftrightarrow A^{w}A\in F\right)$$
29	28	adantr	$$⊢\left(\left(A\in F\wedge w\in \mathbb{N}\right)\wedge A^w\in F\right)\to \left(A^{w+1}\in F\leftrightarrow A^{w}A\in F\right)$$
30	24 29	mpbird	$$⊢\left(\left(A\in F\wedge w\in \mathbb{N}\right)\wedge A^w\in F\right)\to A^{w+1}\in F$$
31	30	exp31	$$⊢A\in F\to \left(w\in \mathbb{N}\to \left(A^w\in F\to A^{w+1}\in F\right)\right)$$
32	31	com12	$$⊢w\in \mathbb{N}\to \left(A\in F\to \left(A^w\in F\to A^{w+1}\in F\right)\right)$$
33	32	a2d	$$⊢w\in \mathbb{N}\to \left(\left(A\in F\to A^w\in F\right)\to \left(A\in F\to A^{w+1}\in F\right)\right)$$
34	7 10 13 16 21 33	nnind	$$⊢B\in \mathbb{N}\to \left(A\in F\to A^B\in F\right)$$
35	34	impcom	$$⊢\left(A\in F\wedge B\in \mathbb{N}\right)\to A^B\in F$$
36		oveq2	$$⊢B=0\to A^B=A^0$$
37		exp0	$$⊢A\in ℂ\to A^0=1$$
38	17 37	syl	$$⊢A\in F\to A^0=1$$
39	36 38	sylan9eqr	$$⊢\left(A\in F\wedge B=0\right)\to A^B=1$$
40	39 3	eqeltrdi	$$⊢\left(A\in F\wedge B=0\right)\to A^B\in F$$
41	35 40	jaodan	$$⊢\left(A\in F\wedge \left(B\in \mathbb{N}\vee B=0\right)\right)\to A^B\in F$$
42	4 41	sylan2b	$$⊢\left(A\in F\wedge B\in {\mathbb{N}}_0\right)\to A^B\in F$$