Proof of Theorem expcl2lem
Step | Hyp | Ref
| Expression |
1 | | elznn0nn 12190 |
. . 3
⊢ (𝐵 ∈ ℤ ↔ (𝐵 ∈ ℕ0 ∨
(𝐵 ∈ ℝ ∧
-𝐵 ∈
ℕ))) |
2 | | expcllem.1 |
. . . . . . 7
⊢ 𝐹 ⊆
ℂ |
3 | | expcllem.2 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹) → (𝑥 · 𝑦) ∈ 𝐹) |
4 | | expcllem.3 |
. . . . . . 7
⊢ 1 ∈
𝐹 |
5 | 2, 3, 4 | expcllem 13646 |
. . . . . 6
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐵 ∈ ℕ0) → (𝐴↑𝐵) ∈ 𝐹) |
6 | 5 | ex 416 |
. . . . 5
⊢ (𝐴 ∈ 𝐹 → (𝐵 ∈ ℕ0 → (𝐴↑𝐵) ∈ 𝐹)) |
7 | 6 | adantr 484 |
. . . 4
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0) → (𝐵 ∈ ℕ0 → (𝐴↑𝐵) ∈ 𝐹)) |
8 | | simpll 767 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → 𝐴 ∈ 𝐹) |
9 | 2, 8 | sselid 3898 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → 𝐴 ∈ ℂ) |
10 | | simprl 771 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → 𝐵 ∈ ℝ) |
11 | 10 | recnd 10861 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → 𝐵 ∈ ℂ) |
12 | | nnnn0 12097 |
. . . . . . . 8
⊢ (-𝐵 ∈ ℕ → -𝐵 ∈
ℕ0) |
13 | 12 | ad2antll 729 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → -𝐵 ∈
ℕ0) |
14 | | expneg2 13644 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ -𝐵 ∈ ℕ0)
→ (𝐴↑𝐵) = (1 / (𝐴↑-𝐵))) |
15 | 9, 11, 13, 14 | syl3anc 1373 |
. . . . . 6
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → (𝐴↑𝐵) = (1 / (𝐴↑-𝐵))) |
16 | | difss 4046 |
. . . . . . . 8
⊢ (𝐹 ∖ {0}) ⊆ 𝐹 |
17 | | simpl 486 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → (𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0)) |
18 | | eldifsn 4700 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (𝐹 ∖ {0}) ↔ (𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0)) |
19 | 17, 18 | sylibr 237 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → 𝐴 ∈ (𝐹 ∖ {0})) |
20 | 16, 2 | sstri 3910 |
. . . . . . . . . 10
⊢ (𝐹 ∖ {0}) ⊆
ℂ |
21 | 16 | sseli 3896 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝐹 ∖ {0}) → 𝑥 ∈ 𝐹) |
22 | 16 | sseli 3896 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (𝐹 ∖ {0}) → 𝑦 ∈ 𝐹) |
23 | 21, 22, 3 | syl2an 599 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (𝐹 ∖ {0}) ∧ 𝑦 ∈ (𝐹 ∖ {0})) → (𝑥 · 𝑦) ∈ 𝐹) |
24 | | eldifsn 4700 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝐹 ∖ {0}) ↔ (𝑥 ∈ 𝐹 ∧ 𝑥 ≠ 0)) |
25 | 2 | sseli 3896 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐹 → 𝑥 ∈ ℂ) |
26 | 25 | anim1i 618 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐹 ∧ 𝑥 ≠ 0) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) |
27 | 24, 26 | sylbi 220 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝐹 ∖ {0}) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) |
28 | | eldifsn 4700 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (𝐹 ∖ {0}) ↔ (𝑦 ∈ 𝐹 ∧ 𝑦 ≠ 0)) |
29 | 2 | sseli 3896 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝐹 → 𝑦 ∈ ℂ) |
30 | 29 | anim1i 618 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ 𝐹 ∧ 𝑦 ≠ 0) → (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0)) |
31 | 28, 30 | sylbi 220 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (𝐹 ∖ {0}) → (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0)) |
32 | | mulne0 11474 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0)) → (𝑥 · 𝑦) ≠ 0) |
33 | 27, 31, 32 | syl2an 599 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (𝐹 ∖ {0}) ∧ 𝑦 ∈ (𝐹 ∖ {0})) → (𝑥 · 𝑦) ≠ 0) |
34 | | eldifsn 4700 |
. . . . . . . . . . 11
⊢ ((𝑥 · 𝑦) ∈ (𝐹 ∖ {0}) ↔ ((𝑥 · 𝑦) ∈ 𝐹 ∧ (𝑥 · 𝑦) ≠ 0)) |
35 | 23, 33, 34 | sylanbrc 586 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (𝐹 ∖ {0}) ∧ 𝑦 ∈ (𝐹 ∖ {0})) → (𝑥 · 𝑦) ∈ (𝐹 ∖ {0})) |
36 | | ax-1ne0 10798 |
. . . . . . . . . . 11
⊢ 1 ≠
0 |
37 | | eldifsn 4700 |
. . . . . . . . . . 11
⊢ (1 ∈
(𝐹 ∖ {0}) ↔ (1
∈ 𝐹 ∧ 1 ≠
0)) |
38 | 4, 36, 37 | mpbir2an 711 |
. . . . . . . . . 10
⊢ 1 ∈
(𝐹 ∖
{0}) |
39 | 20, 35, 38 | expcllem 13646 |
. . . . . . . . 9
⊢ ((𝐴 ∈ (𝐹 ∖ {0}) ∧ -𝐵 ∈ ℕ0) → (𝐴↑-𝐵) ∈ (𝐹 ∖ {0})) |
40 | 19, 13, 39 | syl2anc 587 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → (𝐴↑-𝐵) ∈ (𝐹 ∖ {0})) |
41 | 16, 40 | sselid 3898 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → (𝐴↑-𝐵) ∈ 𝐹) |
42 | | eldifsn 4700 |
. . . . . . . . 9
⊢ ((𝐴↑-𝐵) ∈ (𝐹 ∖ {0}) ↔ ((𝐴↑-𝐵) ∈ 𝐹 ∧ (𝐴↑-𝐵) ≠ 0)) |
43 | 40, 42 | sylib 221 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → ((𝐴↑-𝐵) ∈ 𝐹 ∧ (𝐴↑-𝐵) ≠ 0)) |
44 | 43 | simprd 499 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → (𝐴↑-𝐵) ≠ 0) |
45 | | neeq1 3003 |
. . . . . . . . 9
⊢ (𝑥 = (𝐴↑-𝐵) → (𝑥 ≠ 0 ↔ (𝐴↑-𝐵) ≠ 0)) |
46 | | oveq2 7221 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐴↑-𝐵) → (1 / 𝑥) = (1 / (𝐴↑-𝐵))) |
47 | 46 | eleq1d 2822 |
. . . . . . . . 9
⊢ (𝑥 = (𝐴↑-𝐵) → ((1 / 𝑥) ∈ 𝐹 ↔ (1 / (𝐴↑-𝐵)) ∈ 𝐹)) |
48 | 45, 47 | imbi12d 348 |
. . . . . . . 8
⊢ (𝑥 = (𝐴↑-𝐵) → ((𝑥 ≠ 0 → (1 / 𝑥) ∈ 𝐹) ↔ ((𝐴↑-𝐵) ≠ 0 → (1 / (𝐴↑-𝐵)) ∈ 𝐹))) |
49 | | expcl2lem.4 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐹 ∧ 𝑥 ≠ 0) → (1 / 𝑥) ∈ 𝐹) |
50 | 49 | ex 416 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐹 → (𝑥 ≠ 0 → (1 / 𝑥) ∈ 𝐹)) |
51 | 48, 50 | vtoclga 3489 |
. . . . . . 7
⊢ ((𝐴↑-𝐵) ∈ 𝐹 → ((𝐴↑-𝐵) ≠ 0 → (1 / (𝐴↑-𝐵)) ∈ 𝐹)) |
52 | 41, 44, 51 | sylc 65 |
. . . . . 6
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → (1 / (𝐴↑-𝐵)) ∈ 𝐹) |
53 | 15, 52 | eqeltrd 2838 |
. . . . 5
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → (𝐴↑𝐵) ∈ 𝐹) |
54 | 53 | ex 416 |
. . . 4
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0) → ((𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ) → (𝐴↑𝐵) ∈ 𝐹)) |
55 | 7, 54 | jaod 859 |
. . 3
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0) → ((𝐵 ∈ ℕ0 ∨ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → (𝐴↑𝐵) ∈ 𝐹)) |
56 | 1, 55 | syl5bi 245 |
. 2
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0) → (𝐵 ∈ ℤ → (𝐴↑𝐵) ∈ 𝐹)) |
57 | 56 | 3impia 1119 |
1
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℤ) → (𝐴↑𝐵) ∈ 𝐹) |