Theorem expcllem

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

	Ref	Expression
Hypotheses	expcllem.1	⊢ 𝐹 ⊆ ℂ
	expcllem.2	⊢ ( ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) → ( 𝑥 · 𝑦 ) ∈ 𝐹 )
	expcllem.3	⊢ 1 ∈ 𝐹
Assertion	expcllem	⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 ↑ 𝐵 ) ∈ 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		expcllem.1	⊢ 𝐹 ⊆ ℂ
2		expcllem.2	⊢ ( ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) → ( 𝑥 · 𝑦 ) ∈ 𝐹 )
3		expcllem.3	⊢ 1 ∈ 𝐹
4		elnn0	⊢ ( 𝐵 ∈ ℕ0 ↔ ( 𝐵 ∈ ℕ ∨ 𝐵 = 0 ) )
5		oveq2	⊢ ( 𝑧 = 1 → ( 𝐴 ↑ 𝑧 ) = ( 𝐴 ↑ 1 ) )
6	5	eleq1d	⊢ ( 𝑧 = 1 → ( ( 𝐴 ↑ 𝑧 ) ∈ 𝐹 ↔ ( 𝐴 ↑ 1 ) ∈ 𝐹 ) )
7	6	imbi2d	⊢ ( 𝑧 = 1 → ( ( 𝐴 ∈ 𝐹 → ( 𝐴 ↑ 𝑧 ) ∈ 𝐹 ) ↔ ( 𝐴 ∈ 𝐹 → ( 𝐴 ↑ 1 ) ∈ 𝐹 ) ) )
8		oveq2	⊢ ( 𝑧 = 𝑤 → ( 𝐴 ↑ 𝑧 ) = ( 𝐴 ↑ 𝑤 ) )
9	8	eleq1d	⊢ ( 𝑧 = 𝑤 → ( ( 𝐴 ↑ 𝑧 ) ∈ 𝐹 ↔ ( 𝐴 ↑ 𝑤 ) ∈ 𝐹 ) )
10	9	imbi2d	⊢ ( 𝑧 = 𝑤 → ( ( 𝐴 ∈ 𝐹 → ( 𝐴 ↑ 𝑧 ) ∈ 𝐹 ) ↔ ( 𝐴 ∈ 𝐹 → ( 𝐴 ↑ 𝑤 ) ∈ 𝐹 ) ) )
11		oveq2	⊢ ( 𝑧 = ( 𝑤 + 1 ) → ( 𝐴 ↑ 𝑧 ) = ( 𝐴 ↑ ( 𝑤 + 1 ) ) )
12	11	eleq1d	⊢ ( 𝑧 = ( 𝑤 + 1 ) → ( ( 𝐴 ↑ 𝑧 ) ∈ 𝐹 ↔ ( 𝐴 ↑ ( 𝑤 + 1 ) ) ∈ 𝐹 ) )
13	12	imbi2d	⊢ ( 𝑧 = ( 𝑤 + 1 ) → ( ( 𝐴 ∈ 𝐹 → ( 𝐴 ↑ 𝑧 ) ∈ 𝐹 ) ↔ ( 𝐴 ∈ 𝐹 → ( 𝐴 ↑ ( 𝑤 + 1 ) ) ∈ 𝐹 ) ) )
14		oveq2	⊢ ( 𝑧 = 𝐵 → ( 𝐴 ↑ 𝑧 ) = ( 𝐴 ↑ 𝐵 ) )
15	14	eleq1d	⊢ ( 𝑧 = 𝐵 → ( ( 𝐴 ↑ 𝑧 ) ∈ 𝐹 ↔ ( 𝐴 ↑ 𝐵 ) ∈ 𝐹 ) )
16	15	imbi2d	⊢ ( 𝑧 = 𝐵 → ( ( 𝐴 ∈ 𝐹 → ( 𝐴 ↑ 𝑧 ) ∈ 𝐹 ) ↔ ( 𝐴 ∈ 𝐹 → ( 𝐴 ↑ 𝐵 ) ∈ 𝐹 ) ) )
17	1	sseli	⊢ ( 𝐴 ∈ 𝐹 → 𝐴 ∈ ℂ )
18		exp1	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 1 ) = 𝐴 )
19	17 18	syl	⊢ ( 𝐴 ∈ 𝐹 → ( 𝐴 ↑ 1 ) = 𝐴 )
20	19	eleq1d	⊢ ( 𝐴 ∈ 𝐹 → ( ( 𝐴 ↑ 1 ) ∈ 𝐹 ↔ 𝐴 ∈ 𝐹 ) )
21	20	ibir	⊢ ( 𝐴 ∈ 𝐹 → ( 𝐴 ↑ 1 ) ∈ 𝐹 )
22	2	caovcl	⊢ ( ( ( 𝐴 ↑ 𝑤 ) ∈ 𝐹 ∧ 𝐴 ∈ 𝐹 ) → ( ( 𝐴 ↑ 𝑤 ) · 𝐴 ) ∈ 𝐹 )
23	22	ancoms	⊢ ( ( 𝐴 ∈ 𝐹 ∧ ( 𝐴 ↑ 𝑤 ) ∈ 𝐹 ) → ( ( 𝐴 ↑ 𝑤 ) · 𝐴 ) ∈ 𝐹 )
24	23	adantlr	⊢ ( ( ( 𝐴 ∈ 𝐹 ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 ↑ 𝑤 ) ∈ 𝐹 ) → ( ( 𝐴 ↑ 𝑤 ) · 𝐴 ) ∈ 𝐹 )
25		nnnn0	⊢ ( 𝑤 ∈ ℕ → 𝑤 ∈ ℕ0 )
26		expp1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑤 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑤 + 1 ) ) = ( ( 𝐴 ↑ 𝑤 ) · 𝐴 ) )
27	17 25 26	syl2an	⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝑤 ∈ ℕ ) → ( 𝐴 ↑ ( 𝑤 + 1 ) ) = ( ( 𝐴 ↑ 𝑤 ) · 𝐴 ) )
28	27	eleq1d	⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝑤 ∈ ℕ ) → ( ( 𝐴 ↑ ( 𝑤 + 1 ) ) ∈ 𝐹 ↔ ( ( 𝐴 ↑ 𝑤 ) · 𝐴 ) ∈ 𝐹 ) )
29	28	adantr	⊢ ( ( ( 𝐴 ∈ 𝐹 ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 ↑ 𝑤 ) ∈ 𝐹 ) → ( ( 𝐴 ↑ ( 𝑤 + 1 ) ) ∈ 𝐹 ↔ ( ( 𝐴 ↑ 𝑤 ) · 𝐴 ) ∈ 𝐹 ) )
30	24 29	mpbird	⊢ ( ( ( 𝐴 ∈ 𝐹 ∧ 𝑤 ∈ ℕ ) ∧ ( 𝐴 ↑ 𝑤 ) ∈ 𝐹 ) → ( 𝐴 ↑ ( 𝑤 + 1 ) ) ∈ 𝐹 )
31	30	exp31	⊢ ( 𝐴 ∈ 𝐹 → ( 𝑤 ∈ ℕ → ( ( 𝐴 ↑ 𝑤 ) ∈ 𝐹 → ( 𝐴 ↑ ( 𝑤 + 1 ) ) ∈ 𝐹 ) ) )
32	31	com12	⊢ ( 𝑤 ∈ ℕ → ( 𝐴 ∈ 𝐹 → ( ( 𝐴 ↑ 𝑤 ) ∈ 𝐹 → ( 𝐴 ↑ ( 𝑤 + 1 ) ) ∈ 𝐹 ) ) )
33	32	a2d	⊢ ( 𝑤 ∈ ℕ → ( ( 𝐴 ∈ 𝐹 → ( 𝐴 ↑ 𝑤 ) ∈ 𝐹 ) → ( 𝐴 ∈ 𝐹 → ( 𝐴 ↑ ( 𝑤 + 1 ) ) ∈ 𝐹 ) ) )
34	7 10 13 16 21 33	nnind	⊢ ( 𝐵 ∈ ℕ → ( 𝐴 ∈ 𝐹 → ( 𝐴 ↑ 𝐵 ) ∈ 𝐹 ) )
35	34	impcom	⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ ℕ ) → ( 𝐴 ↑ 𝐵 ) ∈ 𝐹 )
36		oveq2	⊢ ( 𝐵 = 0 → ( 𝐴 ↑ 𝐵 ) = ( 𝐴 ↑ 0 ) )
37		exp0	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 0 ) = 1 )
38	17 37	syl	⊢ ( 𝐴 ∈ 𝐹 → ( 𝐴 ↑ 0 ) = 1 )
39	36 38	sylan9eqr	⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝐵 = 0 ) → ( 𝐴 ↑ 𝐵 ) = 1 )
40	39 3	eqeltrdi	⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝐵 = 0 ) → ( 𝐴 ↑ 𝐵 ) ∈ 𝐹 )
41	35 40	jaodan	⊢ ( ( 𝐴 ∈ 𝐹 ∧ ( 𝐵 ∈ ℕ ∨ 𝐵 = 0 ) ) → ( 𝐴 ↑ 𝐵 ) ∈ 𝐹 )
42	4 41	sylan2b	⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 ↑ 𝐵 ) ∈ 𝐹 )