Step | Hyp | Ref
| Expression |
1 | | elznn0nn 8365 |
. . 3
⊢ (𝐵 ∈ ℤ ↔ (𝐵 ∈ ℕ0 ∨
(𝐵 ∈ ℝ ∧
-𝐵 ∈
ℕ))) |
2 | | expcllem.1 |
. . . . . . 7
⊢ 𝐹 ⊆
ℂ |
3 | | expcllem.2 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹) → (𝑥 · 𝑦) ∈ 𝐹) |
4 | | expcllem.3 |
. . . . . . 7
⊢ 1 ∈
𝐹 |
5 | 2, 3, 4 | expcllem 9487 |
. . . . . 6
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐵 ∈ ℕ0) → (𝐴↑𝐵) ∈ 𝐹) |
6 | 5 | ex 113 |
. . . . 5
⊢ (𝐴 ∈ 𝐹 → (𝐵 ∈ ℕ0 → (𝐴↑𝐵) ∈ 𝐹)) |
7 | 6 | adantr 270 |
. . . 4
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐴 # 0) → (𝐵 ∈ ℕ0 → (𝐴↑𝐵) ∈ 𝐹)) |
8 | | simpll 495 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → 𝐴 ∈ 𝐹) |
9 | 2, 8 | sseldi 2997 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → 𝐴 ∈ ℂ) |
10 | | simplr 496 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → 𝐴 # 0) |
11 | | simprl 497 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → 𝐵 ∈ ℝ) |
12 | 11 | recnd 7147 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → 𝐵 ∈ ℂ) |
13 | | nnnn0 8295 |
. . . . . . . 8
⊢ (-𝐵 ∈ ℕ → -𝐵 ∈
ℕ0) |
14 | 13 | ad2antll 474 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → -𝐵 ∈
ℕ0) |
15 | | expineg2 9485 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℂ ∧ -𝐵 ∈ ℕ0)) → (𝐴↑𝐵) = (1 / (𝐴↑-𝐵))) |
16 | 9, 10, 12, 14, 15 | syl22anc 1170 |
. . . . . 6
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → (𝐴↑𝐵) = (1 / (𝐴↑-𝐵))) |
17 | | ssrab2 3079 |
. . . . . . . 8
⊢ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0} ⊆ 𝐹 |
18 | | simpl 107 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → (𝐴 ∈ 𝐹 ∧ 𝐴 # 0)) |
19 | | breq1 3788 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝐴 → (𝑧 # 0 ↔ 𝐴 # 0)) |
20 | 19 | elrab 2749 |
. . . . . . . . . 10
⊢ (𝐴 ∈ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0} ↔ (𝐴 ∈ 𝐹 ∧ 𝐴 # 0)) |
21 | 18, 20 | sylibr 132 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → 𝐴 ∈ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0}) |
22 | 17, 2 | sstri 3008 |
. . . . . . . . . 10
⊢ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0} ⊆ ℂ |
23 | 17 | sseli 2995 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0} → 𝑥 ∈ 𝐹) |
24 | 17 | sseli 2995 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0} → 𝑦 ∈ 𝐹) |
25 | 23, 24, 3 | syl2an 283 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0} ∧ 𝑦 ∈ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0}) → (𝑥 · 𝑦) ∈ 𝐹) |
26 | | breq1 3788 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑥 → (𝑧 # 0 ↔ 𝑥 # 0)) |
27 | 26 | elrab 2749 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0} ↔ (𝑥 ∈ 𝐹 ∧ 𝑥 # 0)) |
28 | 2 | sseli 2995 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐹 → 𝑥 ∈ ℂ) |
29 | 28 | anim1i 333 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐹 ∧ 𝑥 # 0) → (𝑥 ∈ ℂ ∧ 𝑥 # 0)) |
30 | 27, 29 | sylbi 119 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0} → (𝑥 ∈ ℂ ∧ 𝑥 # 0)) |
31 | | breq1 3788 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑦 → (𝑧 # 0 ↔ 𝑦 # 0)) |
32 | 31 | elrab 2749 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0} ↔ (𝑦 ∈ 𝐹 ∧ 𝑦 # 0)) |
33 | 2 | sseli 2995 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝐹 → 𝑦 ∈ ℂ) |
34 | 33 | anim1i 333 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ 𝐹 ∧ 𝑦 # 0) → (𝑦 ∈ ℂ ∧ 𝑦 # 0)) |
35 | 32, 34 | sylbi 119 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0} → (𝑦 ∈ ℂ ∧ 𝑦 # 0)) |
36 | | mulap0 7744 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℂ ∧ 𝑥 # 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 # 0)) → (𝑥 · 𝑦) # 0) |
37 | 30, 35, 36 | syl2an 283 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0} ∧ 𝑦 ∈ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0}) → (𝑥 · 𝑦) # 0) |
38 | | breq1 3788 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝑥 · 𝑦) → (𝑧 # 0 ↔ (𝑥 · 𝑦) # 0)) |
39 | 38 | elrab 2749 |
. . . . . . . . . . 11
⊢ ((𝑥 · 𝑦) ∈ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0} ↔ ((𝑥 · 𝑦) ∈ 𝐹 ∧ (𝑥 · 𝑦) # 0)) |
40 | 25, 37, 39 | sylanbrc 408 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0} ∧ 𝑦 ∈ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0}) → (𝑥 · 𝑦) ∈ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0}) |
41 | | 1ap0 7690 |
. . . . . . . . . . 11
⊢ 1 #
0 |
42 | | breq1 3788 |
. . . . . . . . . . . 12
⊢ (𝑧 = 1 → (𝑧 # 0 ↔ 1 # 0)) |
43 | 42 | elrab 2749 |
. . . . . . . . . . 11
⊢ (1 ∈
{𝑧 ∈ 𝐹 ∣ 𝑧 # 0} ↔ (1 ∈ 𝐹 ∧ 1 # 0)) |
44 | 4, 41, 43 | mpbir2an 883 |
. . . . . . . . . 10
⊢ 1 ∈
{𝑧 ∈ 𝐹 ∣ 𝑧 # 0} |
45 | 22, 40, 44 | expcllem 9487 |
. . . . . . . . 9
⊢ ((𝐴 ∈ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0} ∧ -𝐵 ∈ ℕ0) → (𝐴↑-𝐵) ∈ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0}) |
46 | 21, 14, 45 | syl2anc 403 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → (𝐴↑-𝐵) ∈ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0}) |
47 | 17, 46 | sseldi 2997 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → (𝐴↑-𝐵) ∈ 𝐹) |
48 | | breq1 3788 |
. . . . . . . . . 10
⊢ (𝑧 = (𝐴↑-𝐵) → (𝑧 # 0 ↔ (𝐴↑-𝐵) # 0)) |
49 | 48 | elrab 2749 |
. . . . . . . . 9
⊢ ((𝐴↑-𝐵) ∈ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0} ↔ ((𝐴↑-𝐵) ∈ 𝐹 ∧ (𝐴↑-𝐵) # 0)) |
50 | 46, 49 | sylib 120 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → ((𝐴↑-𝐵) ∈ 𝐹 ∧ (𝐴↑-𝐵) # 0)) |
51 | 50 | simprd 112 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → (𝐴↑-𝐵) # 0) |
52 | | breq1 3788 |
. . . . . . . . 9
⊢ (𝑥 = (𝐴↑-𝐵) → (𝑥 # 0 ↔ (𝐴↑-𝐵) # 0)) |
53 | | oveq2 5540 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐴↑-𝐵) → (1 / 𝑥) = (1 / (𝐴↑-𝐵))) |
54 | 53 | eleq1d 2147 |
. . . . . . . . 9
⊢ (𝑥 = (𝐴↑-𝐵) → ((1 / 𝑥) ∈ 𝐹 ↔ (1 / (𝐴↑-𝐵)) ∈ 𝐹)) |
55 | 52, 54 | imbi12d 232 |
. . . . . . . 8
⊢ (𝑥 = (𝐴↑-𝐵) → ((𝑥 # 0 → (1 / 𝑥) ∈ 𝐹) ↔ ((𝐴↑-𝐵) # 0 → (1 / (𝐴↑-𝐵)) ∈ 𝐹))) |
56 | | expcl2lemap.4 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐹 ∧ 𝑥 # 0) → (1 / 𝑥) ∈ 𝐹) |
57 | 56 | ex 113 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐹 → (𝑥 # 0 → (1 / 𝑥) ∈ 𝐹)) |
58 | 55, 57 | vtoclga 2664 |
. . . . . . 7
⊢ ((𝐴↑-𝐵) ∈ 𝐹 → ((𝐴↑-𝐵) # 0 → (1 / (𝐴↑-𝐵)) ∈ 𝐹)) |
59 | 47, 51, 58 | sylc 61 |
. . . . . 6
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → (1 / (𝐴↑-𝐵)) ∈ 𝐹) |
60 | 16, 59 | eqeltrd 2155 |
. . . . 5
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → (𝐴↑𝐵) ∈ 𝐹) |
61 | 60 | ex 113 |
. . . 4
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐴 # 0) → ((𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ) → (𝐴↑𝐵) ∈ 𝐹)) |
62 | 7, 61 | jaod 669 |
. . 3
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐴 # 0) → ((𝐵 ∈ ℕ0 ∨ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → (𝐴↑𝐵) ∈ 𝐹)) |
63 | 1, 62 | syl5bi 150 |
. 2
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐴 # 0) → (𝐵 ∈ ℤ → (𝐴↑𝐵) ∈ 𝐹)) |
64 | 63 | 3impia 1135 |
1
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐴 # 0 ∧ 𝐵 ∈ ℤ) → (𝐴↑𝐵) ∈ 𝐹) |