Theorem expcllem

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

	Ref	Expression
Hypotheses	expcllem.1	|- F C_ CC
	expcllem.2	|- ( ( x e. F /\ y e. F ) -> ( x x. y ) e. F )
	expcllem.3	|- 1 e. F
Assertion	expcllem	|- ( ( A e. F /\ B e. NN0 ) -> ( A ^ B ) e. F )

Proof

Step	Hyp	Ref	Expression
1		expcllem.1	|- F C_ CC
2		expcllem.2	|- ( ( x e. F /\ y e. F ) -> ( x x. y ) e. F )
3		expcllem.3	|- 1 e. F
4		elnn0	|- ( B e. NN0 <-> ( B e. NN \/ B = 0 ) )
5		oveq2	|- ( z = 1 -> ( A ^ z ) = ( A ^ 1 ) )
6	5	eleq1d	|- ( z = 1 -> ( ( A ^ z ) e. F <-> ( A ^ 1 ) e. F ) )
7	6	imbi2d	|- ( z = 1 -> ( ( A e. F -> ( A ^ z ) e. F ) <-> ( A e. F -> ( A ^ 1 ) e. F ) ) )
8		oveq2	|- ( z = w -> ( A ^ z ) = ( A ^ w ) )
9	8	eleq1d	|- ( z = w -> ( ( A ^ z ) e. F <-> ( A ^ w ) e. F ) )
10	9	imbi2d	|- ( z = w -> ( ( A e. F -> ( A ^ z ) e. F ) <-> ( A e. F -> ( A ^ w ) e. F ) ) )
11		oveq2	|- ( z = ( w + 1 ) -> ( A ^ z ) = ( A ^ ( w + 1 ) ) )
12	11	eleq1d	|- ( z = ( w + 1 ) -> ( ( A ^ z ) e. F <-> ( A ^ ( w + 1 ) ) e. F ) )
13	12	imbi2d	|- ( z = ( w + 1 ) -> ( ( A e. F -> ( A ^ z ) e. F ) <-> ( A e. F -> ( A ^ ( w + 1 ) ) e. F ) ) )
14		oveq2	|- ( z = B -> ( A ^ z ) = ( A ^ B ) )
15	14	eleq1d	|- ( z = B -> ( ( A ^ z ) e. F <-> ( A ^ B ) e. F ) )
16	15	imbi2d	|- ( z = B -> ( ( A e. F -> ( A ^ z ) e. F ) <-> ( A e. F -> ( A ^ B ) e. F ) ) )
17	1	sseli	|- ( A e. F -> A e. CC )
18		exp1	|- ( A e. CC -> ( A ^ 1 ) = A )
19	17 18	syl	|- ( A e. F -> ( A ^ 1 ) = A )
20	19	eleq1d	|- ( A e. F -> ( ( A ^ 1 ) e. F <-> A e. F ) )
21	20	ibir	|- ( A e. F -> ( A ^ 1 ) e. F )
22	2	caovcl	|- ( ( ( A ^ w ) e. F /\ A e. F ) -> ( ( A ^ w ) x. A ) e. F )
23	22	ancoms	|- ( ( A e. F /\ ( A ^ w ) e. F ) -> ( ( A ^ w ) x. A ) e. F )
24	23	adantlr	|- ( ( ( A e. F /\ w e. NN ) /\ ( A ^ w ) e. F ) -> ( ( A ^ w ) x. A ) e. F )
25		nnnn0	|- ( w e. NN -> w e. NN0 )
26		expp1	|- ( ( A e. CC /\ w e. NN0 ) -> ( A ^ ( w + 1 ) ) = ( ( A ^ w ) x. A ) )
27	17 25 26	syl2an	|- ( ( A e. F /\ w e. NN ) -> ( A ^ ( w + 1 ) ) = ( ( A ^ w ) x. A ) )
28	27	eleq1d	|- ( ( A e. F /\ w e. NN ) -> ( ( A ^ ( w + 1 ) ) e. F <-> ( ( A ^ w ) x. A ) e. F ) )
29	28	adantr	|- ( ( ( A e. F /\ w e. NN ) /\ ( A ^ w ) e. F ) -> ( ( A ^ ( w + 1 ) ) e. F <-> ( ( A ^ w ) x. A ) e. F ) )
30	24 29	mpbird	|- ( ( ( A e. F /\ w e. NN ) /\ ( A ^ w ) e. F ) -> ( A ^ ( w + 1 ) ) e. F )
31	30	exp31	|- ( A e. F -> ( w e. NN -> ( ( A ^ w ) e. F -> ( A ^ ( w + 1 ) ) e. F ) ) )
32	31	com12	|- ( w e. NN -> ( A e. F -> ( ( A ^ w ) e. F -> ( A ^ ( w + 1 ) ) e. F ) ) )
33	32	a2d	|- ( w e. NN -> ( ( A e. F -> ( A ^ w ) e. F ) -> ( A e. F -> ( A ^ ( w + 1 ) ) e. F ) ) )
34	7 10 13 16 21 33	nnind	|- ( B e. NN -> ( A e. F -> ( A ^ B ) e. F ) )
35	34	impcom	|- ( ( A e. F /\ B e. NN ) -> ( A ^ B ) e. F )
36		oveq2	|- ( B = 0 -> ( A ^ B ) = ( A ^ 0 ) )
37		exp0	|- ( A e. CC -> ( A ^ 0 ) = 1 )
38	17 37	syl	|- ( A e. F -> ( A ^ 0 ) = 1 )
39	36 38	sylan9eqr	|- ( ( A e. F /\ B = 0 ) -> ( A ^ B ) = 1 )
40	39 3	eqeltrdi	|- ( ( A e. F /\ B = 0 ) -> ( A ^ B ) e. F )
41	35 40	jaodan	|- ( ( A e. F /\ ( B e. NN \/ B = 0 ) ) -> ( A ^ B ) e. F )
42	4 41	sylan2b	|- ( ( A e. F /\ B e. NN0 ) -> ( A ^ B ) e. F )