Metamath Proof Explorer

Theorem expcl2lem

Description: Lemma for proving integer exponentiation closure laws. (Contributed by Mario Carneiro, 4-Jun-2014) (Revised by Mario Carneiro, 9-Sep-2014)

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

Proof

Step Hyp Ref Expression
1 expcllem.1 ⊢ 𝐹 ⊆ ℂ
2 expcllem.2 ⊢ ( ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) → ( 𝑥 · 𝑦 ) ∈ 𝐹 )
3 expcllem.3 ⊢ 1 ∈ 𝐹
4 expcl2lem.4 ⊢ ( ( 𝑥 ∈ 𝐹 ∧ 𝑥 ≠ 0 ) → ( 1 / 𝑥 ) ∈ 𝐹 )
5 elznn0nn ⊢ ( 𝐵 ∈ ℤ ↔ ( 𝐵 ∈ ℕ0 ∨ ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) ) )
6 1 2 3 expcllem ⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 ↑ 𝐵 ) ∈ 𝐹 )
7 6 ex ⊢ ( 𝐴 ∈ 𝐹 → ( 𝐵 ∈ ℕ0 → ( 𝐴 ↑ 𝐵 ) ∈ 𝐹 ) )
8 7 adantr ⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) → ( 𝐵 ∈ ℕ0 → ( 𝐴 ↑ 𝐵 ) ∈ 𝐹 ) )
9 simpll ⊢ ( ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) ) → 𝐴 ∈ 𝐹 )
10 1 9 sselid ⊢ ( ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) ) → 𝐴 ∈ ℂ )
11 simprl ⊢ ( ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) ) → 𝐵 ∈ ℝ )
12 11 recnd ⊢ ( ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) ) → 𝐵 ∈ ℂ )
13 nnnn0 ⊢ ( - 𝐵 ∈ ℕ → - 𝐵 ∈ ℕ0 )
14 13 ad2antll ⊢ ( ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) ) → - 𝐵 ∈ ℕ0 )
15 expneg2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ - 𝐵 ∈ ℕ0 ) → ( 𝐴 ↑ 𝐵 ) = ( 1 / ( 𝐴 ↑ - 𝐵 ) ) )
16 10 12 14 15 syl3anc ⊢ ( ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) ) → ( 𝐴 ↑ 𝐵 ) = ( 1 / ( 𝐴 ↑ - 𝐵 ) ) )
17 difss ⊢ ( 𝐹 ∖ { 0 } ) ⊆ 𝐹
18 simpl ⊢ ( ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) ) → ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) )
19 eldifsn ⊢ ( 𝐴 ∈ ( 𝐹 ∖ { 0 } ) ↔ ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) )
20 18 19 sylibr ⊢ ( ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) ) → 𝐴 ∈ ( 𝐹 ∖ { 0 } ) )
21 17 1 sstri ⊢ ( 𝐹 ∖ { 0 } ) ⊆ ℂ
22 17 sseli ⊢ ( 𝑥 ∈ ( 𝐹 ∖ { 0 } ) → 𝑥 ∈ 𝐹 )
23 17 sseli ⊢ ( 𝑦 ∈ ( 𝐹 ∖ { 0 } ) → 𝑦 ∈ 𝐹 )
24 22 23 2 syl2an ⊢ ( ( 𝑥 ∈ ( 𝐹 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝐹 ∖ { 0 } ) ) → ( 𝑥 · 𝑦 ) ∈ 𝐹 )
25 eldifsn ⊢ ( 𝑥 ∈ ( 𝐹 ∖ { 0 } ) ↔ ( 𝑥 ∈ 𝐹 ∧ 𝑥 ≠ 0 ) )
26 1 sseli ⊢ ( 𝑥 ∈ 𝐹 → 𝑥 ∈ ℂ )
27 26 anim1i ⊢ ( ( 𝑥 ∈ 𝐹 ∧ 𝑥 ≠ 0 ) → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
28 25 27 sylbi ⊢ ( 𝑥 ∈ ( 𝐹 ∖ { 0 } ) → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
29 eldifsn ⊢ ( 𝑦 ∈ ( 𝐹 ∖ { 0 } ) ↔ ( 𝑦 ∈ 𝐹 ∧ 𝑦 ≠ 0 ) )
30 1 sseli ⊢ ( 𝑦 ∈ 𝐹 → 𝑦 ∈ ℂ )
31 30 anim1i ⊢ ( ( 𝑦 ∈ 𝐹 ∧ 𝑦 ≠ 0 ) → ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) )
32 29 31 sylbi ⊢ ( 𝑦 ∈ ( 𝐹 ∖ { 0 } ) → ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) )
33 mulne0 ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ) → ( 𝑥 · 𝑦 ) ≠ 0 )
34 28 32 33 syl2an ⊢ ( ( 𝑥 ∈ ( 𝐹 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝐹 ∖ { 0 } ) ) → ( 𝑥 · 𝑦 ) ≠ 0 )
35 eldifsn ⊢ ( ( 𝑥 · 𝑦 ) ∈ ( 𝐹 ∖ { 0 } ) ↔ ( ( 𝑥 · 𝑦 ) ∈ 𝐹 ∧ ( 𝑥 · 𝑦 ) ≠ 0 ) )
36 24 34 35 sylanbrc ⊢ ( ( 𝑥 ∈ ( 𝐹 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝐹 ∖ { 0 } ) ) → ( 𝑥 · 𝑦 ) ∈ ( 𝐹 ∖ { 0 } ) )
37 ax-1ne0 ⊢ 1 ≠ 0
38 eldifsn ⊢ ( 1 ∈ ( 𝐹 ∖ { 0 } ) ↔ ( 1 ∈ 𝐹 ∧ 1 ≠ 0 ) )
39 3 37 38 mpbir2an ⊢ 1 ∈ ( 𝐹 ∖ { 0 } )
40 21 36 39 expcllem ⊢ ( ( 𝐴 ∈ ( 𝐹 ∖ { 0 } ) ∧ - 𝐵 ∈ ℕ0 ) → ( 𝐴 ↑ - 𝐵 ) ∈ ( 𝐹 ∖ { 0 } ) )
41 20 14 40 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) ) → ( 𝐴 ↑ - 𝐵 ) ∈ ( 𝐹 ∖ { 0 } ) )
42 17 41 sselid ⊢ ( ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) ) → ( 𝐴 ↑ - 𝐵 ) ∈ 𝐹 )
43 eldifsn ⊢ ( ( 𝐴 ↑ - 𝐵 ) ∈ ( 𝐹 ∖ { 0 } ) ↔ ( ( 𝐴 ↑ - 𝐵 ) ∈ 𝐹 ∧ ( 𝐴 ↑ - 𝐵 ) ≠ 0 ) )
44 41 43 sylib ⊢ ( ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) ) → ( ( 𝐴 ↑ - 𝐵 ) ∈ 𝐹 ∧ ( 𝐴 ↑ - 𝐵 ) ≠ 0 ) )
45 44 simprd ⊢ ( ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) ) → ( 𝐴 ↑ - 𝐵 ) ≠ 0 )
46 neeq1 ⊢ ( 𝑥 = ( 𝐴 ↑ - 𝐵 ) → ( 𝑥 ≠ 0 ↔ ( 𝐴 ↑ - 𝐵 ) ≠ 0 ) )
47 oveq2 ⊢ ( 𝑥 = ( 𝐴 ↑ - 𝐵 ) → ( 1 / 𝑥 ) = ( 1 / ( 𝐴 ↑ - 𝐵 ) ) )
48 47 eleq1d ⊢ ( 𝑥 = ( 𝐴 ↑ - 𝐵 ) → ( ( 1 / 𝑥 ) ∈ 𝐹 ↔ ( 1 / ( 𝐴 ↑ - 𝐵 ) ) ∈ 𝐹 ) )
49 46 48 imbi12d ⊢ ( 𝑥 = ( 𝐴 ↑ - 𝐵 ) → ( ( 𝑥 ≠ 0 → ( 1 / 𝑥 ) ∈ 𝐹 ) ↔ ( ( 𝐴 ↑ - 𝐵 ) ≠ 0 → ( 1 / ( 𝐴 ↑ - 𝐵 ) ) ∈ 𝐹 ) ) )
50 4 ex ⊢ ( 𝑥 ∈ 𝐹 → ( 𝑥 ≠ 0 → ( 1 / 𝑥 ) ∈ 𝐹 ) )
51 49 50 vtoclga ⊢ ( ( 𝐴 ↑ - 𝐵 ) ∈ 𝐹 → ( ( 𝐴 ↑ - 𝐵 ) ≠ 0 → ( 1 / ( 𝐴 ↑ - 𝐵 ) ) ∈ 𝐹 ) )
52 42 45 51 sylc ⊢ ( ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) ) → ( 1 / ( 𝐴 ↑ - 𝐵 ) ) ∈ 𝐹 )
53 16 52 eqeltrd ⊢ ( ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) ) → ( 𝐴 ↑ 𝐵 ) ∈ 𝐹 )
54 53 ex ⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) → ( ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) → ( 𝐴 ↑ 𝐵 ) ∈ 𝐹 ) )
55 8 54 jaod ⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) → ( ( 𝐵 ∈ ℕ0 ∨ ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) ) → ( 𝐴 ↑ 𝐵 ) ∈ 𝐹 ) )
56 5 55 syl5bi ⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) → ( 𝐵 ∈ ℤ → ( 𝐴 ↑ 𝐵 ) ∈ 𝐹 ) )
57 56 3impia ⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℤ ) → ( 𝐴 ↑ 𝐵 ) ∈ 𝐹 )