# Metamath Proof Explorer

## 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 {x}{y}\in {F}$
expcllem.3 ${⊢}1\in {F}$
Assertion expcllem ${⊢}\left({A}\in {F}\wedge {B}\in {ℕ}_{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 {x}{y}\in {F}$
3 expcllem.3 ${⊢}1\in {F}$
4 elnn0 ${⊢}{B}\in {ℕ}_{0}↔\left({B}\in ℕ\vee {B}=0\right)$
5 oveq2 ${⊢}{z}=1\to {{A}}^{{z}}={{A}}^{1}$
6 5 eleq1d ${⊢}{z}=1\to \left({{A}}^{{z}}\in {F}↔{{A}}^{1}\in {F}\right)$
7 6 imbi2d ${⊢}{z}=1\to \left(\left({A}\in {F}\to {{A}}^{{z}}\in {F}\right)↔\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}↔{{A}}^{{w}}\in {F}\right)$
10 9 imbi2d ${⊢}{z}={w}\to \left(\left({A}\in {F}\to {{A}}^{{z}}\in {F}\right)↔\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}↔{{A}}^{{w}+1}\in {F}\right)$
13 12 imbi2d ${⊢}{z}={w}+1\to \left(\left({A}\in {F}\to {{A}}^{{z}}\in {F}\right)↔\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}↔{{A}}^{{B}}\in {F}\right)$
16 15 imbi2d ${⊢}{z}={B}\to \left(\left({A}\in {F}\to {{A}}^{{z}}\in {F}\right)↔\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}↔{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 ℕ\right)\wedge {{A}}^{{w}}\in {F}\right)\to {{A}}^{{w}}{A}\in {F}$
25 nnnn0 ${⊢}{w}\in ℕ\to {w}\in {ℕ}_{0}$
26 expp1 ${⊢}\left({A}\in ℂ\wedge {w}\in {ℕ}_{0}\right)\to {{A}}^{{w}+1}={{A}}^{{w}}{A}$
27 17 25 26 syl2an ${⊢}\left({A}\in {F}\wedge {w}\in ℕ\right)\to {{A}}^{{w}+1}={{A}}^{{w}}{A}$
28 27 eleq1d ${⊢}\left({A}\in {F}\wedge {w}\in ℕ\right)\to \left({{A}}^{{w}+1}\in {F}↔{{A}}^{{w}}{A}\in {F}\right)$
29 28 adantr ${⊢}\left(\left({A}\in {F}\wedge {w}\in ℕ\right)\wedge {{A}}^{{w}}\in {F}\right)\to \left({{A}}^{{w}+1}\in {F}↔{{A}}^{{w}}{A}\in {F}\right)$
30 24 29 mpbird ${⊢}\left(\left({A}\in {F}\wedge {w}\in ℕ\right)\wedge {{A}}^{{w}}\in {F}\right)\to {{A}}^{{w}+1}\in {F}$
31 30 exp31 ${⊢}{A}\in {F}\to \left({w}\in ℕ\to \left({{A}}^{{w}}\in {F}\to {{A}}^{{w}+1}\in {F}\right)\right)$
32 31 com12 ${⊢}{w}\in ℕ\to \left({A}\in {F}\to \left({{A}}^{{w}}\in {F}\to {{A}}^{{w}+1}\in {F}\right)\right)$
33 32 a2d ${⊢}{w}\in ℕ\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 ℕ\to \left({A}\in {F}\to {{A}}^{{B}}\in {F}\right)$
35 34 impcom ${⊢}\left({A}\in {F}\wedge {B}\in ℕ\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 syl6eqel ${⊢}\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 ℕ\vee {B}=0\right)\right)\to {{A}}^{{B}}\in {F}$
42 4 41 sylan2b ${⊢}\left({A}\in {F}\wedge {B}\in {ℕ}_{0}\right)\to {{A}}^{{B}}\in {F}$