Step | Hyp | Ref
| Expression |
1 | | elznn0nn 9226 |
. . 3
⊢ (𝐵 ∈ ℤ ↔ (𝐵 ∈ ℕ0 ∨
(𝐵 ∈ ℝ ∧
-𝐵 ∈
ℕ))) |
2 | | expcllem.1 |
. . . . . . 7
⊢ 𝐹 ⊆
ℂ |
3 | | expcllem.2 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹) → (𝑥 · 𝑦) ∈ 𝐹) |
4 | | expcllem.3 |
. . . . . . 7
⊢ 1 ∈
𝐹 |
5 | 2, 3, 4 | expcllem 10487 |
. . . . . 6
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐵 ∈ ℕ0) → (𝐴↑𝐵) ∈ 𝐹) |
6 | 5 | ex 114 |
. . . . 5
⊢ (𝐴 ∈ 𝐹 → (𝐵 ∈ ℕ0 → (𝐴↑𝐵) ∈ 𝐹)) |
7 | 6 | adantr 274 |
. . . 4
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐴 # 0) → (𝐵 ∈ ℕ0 → (𝐴↑𝐵) ∈ 𝐹)) |
8 | | simpll 524 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → 𝐴 ∈ 𝐹) |
9 | 2, 8 | sselid 3145 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → 𝐴 ∈ ℂ) |
10 | | simplr 525 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → 𝐴 # 0) |
11 | | simprl 526 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → 𝐵 ∈ ℝ) |
12 | 11 | recnd 7948 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → 𝐵 ∈ ℂ) |
13 | | nnnn0 9142 |
. . . . . . . 8
⊢ (-𝐵 ∈ ℕ → -𝐵 ∈
ℕ0) |
14 | 13 | ad2antll 488 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → -𝐵 ∈
ℕ0) |
15 | | expineg2 10485 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℂ ∧ -𝐵 ∈ ℕ0)) → (𝐴↑𝐵) = (1 / (𝐴↑-𝐵))) |
16 | 9, 10, 12, 14, 15 | syl22anc 1234 |
. . . . . 6
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → (𝐴↑𝐵) = (1 / (𝐴↑-𝐵))) |
17 | | ssrab2 3232 |
. . . . . . . 8
⊢ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0} ⊆ 𝐹 |
18 | | simpl 108 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → (𝐴 ∈ 𝐹 ∧ 𝐴 # 0)) |
19 | | breq1 3992 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝐴 → (𝑧 # 0 ↔ 𝐴 # 0)) |
20 | 19 | elrab 2886 |
. . . . . . . . . 10
⊢ (𝐴 ∈ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0} ↔ (𝐴 ∈ 𝐹 ∧ 𝐴 # 0)) |
21 | 18, 20 | sylibr 133 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → 𝐴 ∈ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0}) |
22 | 17, 2 | sstri 3156 |
. . . . . . . . . 10
⊢ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0} ⊆ ℂ |
23 | 17 | sseli 3143 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0} → 𝑥 ∈ 𝐹) |
24 | 17 | sseli 3143 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0} → 𝑦 ∈ 𝐹) |
25 | 23, 24, 3 | syl2an 287 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0} ∧ 𝑦 ∈ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0}) → (𝑥 · 𝑦) ∈ 𝐹) |
26 | | breq1 3992 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑥 → (𝑧 # 0 ↔ 𝑥 # 0)) |
27 | 26 | elrab 2886 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0} ↔ (𝑥 ∈ 𝐹 ∧ 𝑥 # 0)) |
28 | 2 | sseli 3143 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐹 → 𝑥 ∈ ℂ) |
29 | 28 | anim1i 338 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐹 ∧ 𝑥 # 0) → (𝑥 ∈ ℂ ∧ 𝑥 # 0)) |
30 | 27, 29 | sylbi 120 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0} → (𝑥 ∈ ℂ ∧ 𝑥 # 0)) |
31 | | breq1 3992 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑦 → (𝑧 # 0 ↔ 𝑦 # 0)) |
32 | 31 | elrab 2886 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0} ↔ (𝑦 ∈ 𝐹 ∧ 𝑦 # 0)) |
33 | 2 | sseli 3143 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝐹 → 𝑦 ∈ ℂ) |
34 | 33 | anim1i 338 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ 𝐹 ∧ 𝑦 # 0) → (𝑦 ∈ ℂ ∧ 𝑦 # 0)) |
35 | 32, 34 | sylbi 120 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0} → (𝑦 ∈ ℂ ∧ 𝑦 # 0)) |
36 | | mulap0 8572 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℂ ∧ 𝑥 # 0) ∧ (𝑦 ∈ ℂ ∧ 𝑦 # 0)) → (𝑥 · 𝑦) # 0) |
37 | 30, 35, 36 | syl2an 287 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0} ∧ 𝑦 ∈ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0}) → (𝑥 · 𝑦) # 0) |
38 | | breq1 3992 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝑥 · 𝑦) → (𝑧 # 0 ↔ (𝑥 · 𝑦) # 0)) |
39 | 38 | elrab 2886 |
. . . . . . . . . . 11
⊢ ((𝑥 · 𝑦) ∈ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0} ↔ ((𝑥 · 𝑦) ∈ 𝐹 ∧ (𝑥 · 𝑦) # 0)) |
40 | 25, 37, 39 | sylanbrc 415 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0} ∧ 𝑦 ∈ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0}) → (𝑥 · 𝑦) ∈ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0}) |
41 | | 1ap0 8509 |
. . . . . . . . . . 11
⊢ 1 #
0 |
42 | | breq1 3992 |
. . . . . . . . . . . 12
⊢ (𝑧 = 1 → (𝑧 # 0 ↔ 1 # 0)) |
43 | 42 | elrab 2886 |
. . . . . . . . . . 11
⊢ (1 ∈
{𝑧 ∈ 𝐹 ∣ 𝑧 # 0} ↔ (1 ∈ 𝐹 ∧ 1 # 0)) |
44 | 4, 41, 43 | mpbir2an 937 |
. . . . . . . . . 10
⊢ 1 ∈
{𝑧 ∈ 𝐹 ∣ 𝑧 # 0} |
45 | 22, 40, 44 | expcllem 10487 |
. . . . . . . . 9
⊢ ((𝐴 ∈ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0} ∧ -𝐵 ∈ ℕ0) → (𝐴↑-𝐵) ∈ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0}) |
46 | 21, 14, 45 | syl2anc 409 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → (𝐴↑-𝐵) ∈ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0}) |
47 | 17, 46 | sselid 3145 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → (𝐴↑-𝐵) ∈ 𝐹) |
48 | | breq1 3992 |
. . . . . . . . . 10
⊢ (𝑧 = (𝐴↑-𝐵) → (𝑧 # 0 ↔ (𝐴↑-𝐵) # 0)) |
49 | 48 | elrab 2886 |
. . . . . . . . 9
⊢ ((𝐴↑-𝐵) ∈ {𝑧 ∈ 𝐹 ∣ 𝑧 # 0} ↔ ((𝐴↑-𝐵) ∈ 𝐹 ∧ (𝐴↑-𝐵) # 0)) |
50 | 46, 49 | sylib 121 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → ((𝐴↑-𝐵) ∈ 𝐹 ∧ (𝐴↑-𝐵) # 0)) |
51 | 50 | simprd 113 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → (𝐴↑-𝐵) # 0) |
52 | | breq1 3992 |
. . . . . . . . 9
⊢ (𝑥 = (𝐴↑-𝐵) → (𝑥 # 0 ↔ (𝐴↑-𝐵) # 0)) |
53 | | oveq2 5861 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐴↑-𝐵) → (1 / 𝑥) = (1 / (𝐴↑-𝐵))) |
54 | 53 | eleq1d 2239 |
. . . . . . . . 9
⊢ (𝑥 = (𝐴↑-𝐵) → ((1 / 𝑥) ∈ 𝐹 ↔ (1 / (𝐴↑-𝐵)) ∈ 𝐹)) |
55 | 52, 54 | imbi12d 233 |
. . . . . . . 8
⊢ (𝑥 = (𝐴↑-𝐵) → ((𝑥 # 0 → (1 / 𝑥) ∈ 𝐹) ↔ ((𝐴↑-𝐵) # 0 → (1 / (𝐴↑-𝐵)) ∈ 𝐹))) |
56 | | expcl2lemap.4 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐹 ∧ 𝑥 # 0) → (1 / 𝑥) ∈ 𝐹) |
57 | 56 | ex 114 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐹 → (𝑥 # 0 → (1 / 𝑥) ∈ 𝐹)) |
58 | 55, 57 | vtoclga 2796 |
. . . . . . 7
⊢ ((𝐴↑-𝐵) ∈ 𝐹 → ((𝐴↑-𝐵) # 0 → (1 / (𝐴↑-𝐵)) ∈ 𝐹)) |
59 | 47, 51, 58 | sylc 62 |
. . . . . 6
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → (1 / (𝐴↑-𝐵)) ∈ 𝐹) |
60 | 16, 59 | eqeltrd 2247 |
. . . . 5
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → (𝐴↑𝐵) ∈ 𝐹) |
61 | 60 | ex 114 |
. . . 4
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐴 # 0) → ((𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ) → (𝐴↑𝐵) ∈ 𝐹)) |
62 | 7, 61 | jaod 712 |
. . 3
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐴 # 0) → ((𝐵 ∈ ℕ0 ∨ (𝐵 ∈ ℝ ∧ -𝐵 ∈ ℕ)) → (𝐴↑𝐵) ∈ 𝐹)) |
63 | 1, 62 | syl5bi 151 |
. 2
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐴 # 0) → (𝐵 ∈ ℤ → (𝐴↑𝐵) ∈ 𝐹)) |
64 | 63 | 3impia 1195 |
1
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐴 # 0 ∧ 𝐵 ∈ ℤ) → (𝐴↑𝐵) ∈ 𝐹) |