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 eldifsn ⊢ ( 𝐴 ∈ ( 𝐹 ∖ { 0 } ) ↔ ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) )
19 18 biranri ⊢ ( ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) ) → 𝐴 ∈ ( 𝐹 ∖ { 0 } ) )
20 17 1 sstri ⊢ ( 𝐹 ∖ { 0 } ) ⊆ ℂ
21 17 sseli ⊢ ( 𝑥 ∈ ( 𝐹 ∖ { 0 } ) → 𝑥 ∈ 𝐹 )
22 17 sseli ⊢ ( 𝑦 ∈ ( 𝐹 ∖ { 0 } ) → 𝑦 ∈ 𝐹 )
23 21 22 2 syl2an ⊢ ( ( 𝑥 ∈ ( 𝐹 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝐹 ∖ { 0 } ) ) → ( 𝑥 · 𝑦 ) ∈ 𝐹 )
24 eldifsn ⊢ ( 𝑥 ∈ ( 𝐹 ∖ { 0 } ) ↔ ( 𝑥 ∈ 𝐹 ∧ 𝑥 ≠ 0 ) )
25 1 sseli ⊢ ( 𝑥 ∈ 𝐹 → 𝑥 ∈ ℂ )
26 25 anim1i ⊢ ( ( 𝑥 ∈ 𝐹 ∧ 𝑥 ≠ 0 ) → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
27 24 26 sylbi ⊢ ( 𝑥 ∈ ( 𝐹 ∖ { 0 } ) → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
28 eldifsn ⊢ ( 𝑦 ∈ ( 𝐹 ∖ { 0 } ) ↔ ( 𝑦 ∈ 𝐹 ∧ 𝑦 ≠ 0 ) )
29 1 sseli ⊢ ( 𝑦 ∈ 𝐹 → 𝑦 ∈ ℂ )
30 29 anim1i ⊢ ( ( 𝑦 ∈ 𝐹 ∧ 𝑦 ≠ 0 ) → ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) )
31 28 30 sylbi ⊢ ( 𝑦 ∈ ( 𝐹 ∖ { 0 } ) → ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) )
32 mulne0 ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ) → ( 𝑥 · 𝑦 ) ≠ 0 )
33 27 31 32 syl2an ⊢ ( ( 𝑥 ∈ ( 𝐹 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝐹 ∖ { 0 } ) ) → ( 𝑥 · 𝑦 ) ≠ 0 )
34 eldifsn ⊢ ( ( 𝑥 · 𝑦 ) ∈ ( 𝐹 ∖ { 0 } ) ↔ ( ( 𝑥 · 𝑦 ) ∈ 𝐹 ∧ ( 𝑥 · 𝑦 ) ≠ 0 ) )
35 23 33 34 sylanbrc ⊢ ( ( 𝑥 ∈ ( 𝐹 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝐹 ∖ { 0 } ) ) → ( 𝑥 · 𝑦 ) ∈ ( 𝐹 ∖ { 0 } ) )
36 ax-1ne0 ⊢ 1 ≠ 0
37 eldifsn ⊢ ( 1 ∈ ( 𝐹 ∖ { 0 } ) ↔ ( 1 ∈ 𝐹 ∧ 1 ≠ 0 ) )
38 3 36 37 mpbir2an ⊢ 1 ∈ ( 𝐹 ∖ { 0 } )
39 20 35 38 expcllem ⊢ ( ( 𝐴 ∈ ( 𝐹 ∖ { 0 } ) ∧ - 𝐵 ∈ ℕ0 ) → ( 𝐴 ↑ - 𝐵 ) ∈ ( 𝐹 ∖ { 0 } ) )
40 19 14 39 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) ) → ( 𝐴 ↑ - 𝐵 ) ∈ ( 𝐹 ∖ { 0 } ) )
41 17 40 sselid ⊢ ( ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) ) → ( 𝐴 ↑ - 𝐵 ) ∈ 𝐹 )
42 eldifsn ⊢ ( ( 𝐴 ↑ - 𝐵 ) ∈ ( 𝐹 ∖ { 0 } ) ↔ ( ( 𝐴 ↑ - 𝐵 ) ∈ 𝐹 ∧ ( 𝐴 ↑ - 𝐵 ) ≠ 0 ) )
43 40 42 sylib ⊢ ( ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) ) → ( ( 𝐴 ↑ - 𝐵 ) ∈ 𝐹 ∧ ( 𝐴 ↑ - 𝐵 ) ≠ 0 ) )
44 43 simprd ⊢ ( ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) ) → ( 𝐴 ↑ - 𝐵 ) ≠ 0 )
45 neeq1 ⊢ ( 𝑥 = ( 𝐴 ↑ - 𝐵 ) → ( 𝑥 ≠ 0 ↔ ( 𝐴 ↑ - 𝐵 ) ≠ 0 ) )
46 oveq2 ⊢ ( 𝑥 = ( 𝐴 ↑ - 𝐵 ) → ( 1 / 𝑥 ) = ( 1 / ( 𝐴 ↑ - 𝐵 ) ) )
47 46 eleq1d ⊢ ( 𝑥 = ( 𝐴 ↑ - 𝐵 ) → ( ( 1 / 𝑥 ) ∈ 𝐹 ↔ ( 1 / ( 𝐴 ↑ - 𝐵 ) ) ∈ 𝐹 ) )
48 45 47 imbi12d ⊢ ( 𝑥 = ( 𝐴 ↑ - 𝐵 ) → ( ( 𝑥 ≠ 0 → ( 1 / 𝑥 ) ∈ 𝐹 ) ↔ ( ( 𝐴 ↑ - 𝐵 ) ≠ 0 → ( 1 / ( 𝐴 ↑ - 𝐵 ) ) ∈ 𝐹 ) ) )
49 4 ex ⊢ ( 𝑥 ∈ 𝐹 → ( 𝑥 ≠ 0 → ( 1 / 𝑥 ) ∈ 𝐹 ) )
50 48 49 vtoclga ⊢ ( ( 𝐴 ↑ - 𝐵 ) ∈ 𝐹 → ( ( 𝐴 ↑ - 𝐵 ) ≠ 0 → ( 1 / ( 𝐴 ↑ - 𝐵 ) ) ∈ 𝐹 ) )
51 41 44 50 sylc ⊢ ( ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) ) → ( 1 / ( 𝐴 ↑ - 𝐵 ) ) ∈ 𝐹 )
52 16 51 eqeltrd ⊢ ( ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) ) → ( 𝐴 ↑ 𝐵 ) ∈ 𝐹 )
53 52 ex ⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) → ( ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) → ( 𝐴 ↑ 𝐵 ) ∈ 𝐹 ) )
54 8 53 jaod ⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) → ( ( 𝐵 ∈ ℕ0 ∨ ( 𝐵 ∈ ℝ ∧ - 𝐵 ∈ ℕ ) ) → ( 𝐴 ↑ 𝐵 ) ∈ 𝐹 ) )
55 5 54 biimtrid ⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ) → ( 𝐵 ∈ ℤ → ( 𝐴 ↑ 𝐵 ) ∈ 𝐹 ) )
56 55 3impia ⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℤ ) → ( 𝐴 ↑ 𝐵 ) ∈ 𝐹 )