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 𝐹 ⊆ ℂ
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 ) → ( 𝐴𝐵 ) ∈ 𝐹 )