This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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