Step | Hyp | Ref
| Expression |
1 | | ssrab2 3687 |
. . . . 5
⊢ {𝑥 ∈ ℝ ∣
(exp‘𝑥) ∈
ℕ} ⊆ ℝ |
2 | | ax-resscn 9993 |
. . . . 5
⊢ ℝ
⊆ ℂ |
3 | 1, 2 | sstri 3612 |
. . . 4
⊢ {𝑥 ∈ ℝ ∣
(exp‘𝑥) ∈
ℕ} ⊆ ℂ |
4 | 3 | a1i 11 |
. . 3
⊢ (𝜑 → {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈ ℕ} ⊆
ℂ) |
5 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (exp‘𝑥) = (exp‘𝑦)) |
6 | 5 | eleq1d 2686 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((exp‘𝑥) ∈ ℕ ↔ (exp‘𝑦) ∈
ℕ)) |
7 | 6 | elrab 3363 |
. . . . 5
⊢ (𝑦 ∈ {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈ ℕ} ↔ (𝑦 ∈ ℝ ∧
(exp‘𝑦) ∈
ℕ)) |
8 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (exp‘𝑥) = (exp‘𝑧)) |
9 | 8 | eleq1d 2686 |
. . . . . 6
⊢ (𝑥 = 𝑧 → ((exp‘𝑥) ∈ ℕ ↔ (exp‘𝑧) ∈
ℕ)) |
10 | 9 | elrab 3363 |
. . . . 5
⊢ (𝑧 ∈ {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈ ℕ} ↔ (𝑧 ∈ ℝ ∧
(exp‘𝑧) ∈
ℕ)) |
11 | | simpll 790 |
. . . . . . 7
⊢ (((𝑦 ∈ ℝ ∧
(exp‘𝑦) ∈
ℕ) ∧ (𝑧 ∈
ℝ ∧ (exp‘𝑧)
∈ ℕ)) → 𝑦
∈ ℝ) |
12 | | simprl 794 |
. . . . . . 7
⊢ (((𝑦 ∈ ℝ ∧
(exp‘𝑦) ∈
ℕ) ∧ (𝑧 ∈
ℝ ∧ (exp‘𝑧)
∈ ℕ)) → 𝑧
∈ ℝ) |
13 | 11, 12 | readdcld 10069 |
. . . . . 6
⊢ (((𝑦 ∈ ℝ ∧
(exp‘𝑦) ∈
ℕ) ∧ (𝑧 ∈
ℝ ∧ (exp‘𝑧)
∈ ℕ)) → (𝑦
+ 𝑧) ∈
ℝ) |
14 | 11 | recnd 10068 |
. . . . . . . 8
⊢ (((𝑦 ∈ ℝ ∧
(exp‘𝑦) ∈
ℕ) ∧ (𝑧 ∈
ℝ ∧ (exp‘𝑧)
∈ ℕ)) → 𝑦
∈ ℂ) |
15 | 12 | recnd 10068 |
. . . . . . . 8
⊢ (((𝑦 ∈ ℝ ∧
(exp‘𝑦) ∈
ℕ) ∧ (𝑧 ∈
ℝ ∧ (exp‘𝑧)
∈ ℕ)) → 𝑧
∈ ℂ) |
16 | | efadd 14824 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) →
(exp‘(𝑦 + 𝑧)) = ((exp‘𝑦) · (exp‘𝑧))) |
17 | 14, 15, 16 | syl2anc 693 |
. . . . . . 7
⊢ (((𝑦 ∈ ℝ ∧
(exp‘𝑦) ∈
ℕ) ∧ (𝑧 ∈
ℝ ∧ (exp‘𝑧)
∈ ℕ)) → (exp‘(𝑦 + 𝑧)) = ((exp‘𝑦) · (exp‘𝑧))) |
18 | | nnmulcl 11043 |
. . . . . . . 8
⊢
(((exp‘𝑦)
∈ ℕ ∧ (exp‘𝑧) ∈ ℕ) → ((exp‘𝑦) · (exp‘𝑧)) ∈
ℕ) |
19 | 18 | ad2ant2l 782 |
. . . . . . 7
⊢ (((𝑦 ∈ ℝ ∧
(exp‘𝑦) ∈
ℕ) ∧ (𝑧 ∈
ℝ ∧ (exp‘𝑧)
∈ ℕ)) → ((exp‘𝑦) · (exp‘𝑧)) ∈ ℕ) |
20 | 17, 19 | eqeltrd 2701 |
. . . . . 6
⊢ (((𝑦 ∈ ℝ ∧
(exp‘𝑦) ∈
ℕ) ∧ (𝑧 ∈
ℝ ∧ (exp‘𝑧)
∈ ℕ)) → (exp‘(𝑦 + 𝑧)) ∈ ℕ) |
21 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 + 𝑧) → (exp‘𝑥) = (exp‘(𝑦 + 𝑧))) |
22 | 21 | eleq1d 2686 |
. . . . . . 7
⊢ (𝑥 = (𝑦 + 𝑧) → ((exp‘𝑥) ∈ ℕ ↔ (exp‘(𝑦 + 𝑧)) ∈ ℕ)) |
23 | 22 | elrab 3363 |
. . . . . 6
⊢ ((𝑦 + 𝑧) ∈ {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈ ℕ} ↔ ((𝑦 + 𝑧) ∈ ℝ ∧ (exp‘(𝑦 + 𝑧)) ∈ ℕ)) |
24 | 13, 20, 23 | sylanbrc 698 |
. . . . 5
⊢ (((𝑦 ∈ ℝ ∧
(exp‘𝑦) ∈
ℕ) ∧ (𝑧 ∈
ℝ ∧ (exp‘𝑧)
∈ ℕ)) → (𝑦
+ 𝑧) ∈ {𝑥 ∈ ℝ ∣
(exp‘𝑥) ∈
ℕ}) |
25 | 7, 10, 24 | syl2anb 496 |
. . . 4
⊢ ((𝑦 ∈ {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈ ℕ} ∧ 𝑧 ∈ {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈ ℕ}) → (𝑦 + 𝑧) ∈ {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈
ℕ}) |
26 | 25 | adantl 482 |
. . 3
⊢ ((𝜑 ∧ (𝑦 ∈ {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈ ℕ} ∧ 𝑧 ∈ {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈ ℕ})) →
(𝑦 + 𝑧) ∈ {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈
ℕ}) |
27 | | efnnfsumcl.1 |
. . 3
⊢ (𝜑 → 𝐴 ∈ Fin) |
28 | | efnnfsumcl.2 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ) |
29 | | efnnfsumcl.3 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (exp‘𝐵) ∈ ℕ) |
30 | | fveq2 6191 |
. . . . . 6
⊢ (𝑥 = 𝐵 → (exp‘𝑥) = (exp‘𝐵)) |
31 | 30 | eleq1d 2686 |
. . . . 5
⊢ (𝑥 = 𝐵 → ((exp‘𝑥) ∈ ℕ ↔ (exp‘𝐵) ∈
ℕ)) |
32 | 31 | elrab 3363 |
. . . 4
⊢ (𝐵 ∈ {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈ ℕ} ↔ (𝐵 ∈ ℝ ∧
(exp‘𝐵) ∈
ℕ)) |
33 | 28, 29, 32 | sylanbrc 698 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈
ℕ}) |
34 | | 0re 10040 |
. . . . 5
⊢ 0 ∈
ℝ |
35 | | 1nn 11031 |
. . . . 5
⊢ 1 ∈
ℕ |
36 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑥 = 0 → (exp‘𝑥) =
(exp‘0)) |
37 | | ef0 14821 |
. . . . . . . 8
⊢
(exp‘0) = 1 |
38 | 36, 37 | syl6eq 2672 |
. . . . . . 7
⊢ (𝑥 = 0 → (exp‘𝑥) = 1) |
39 | 38 | eleq1d 2686 |
. . . . . 6
⊢ (𝑥 = 0 → ((exp‘𝑥) ∈ ℕ ↔ 1 ∈
ℕ)) |
40 | 39 | elrab 3363 |
. . . . 5
⊢ (0 ∈
{𝑥 ∈ ℝ ∣
(exp‘𝑥) ∈
ℕ} ↔ (0 ∈ ℝ ∧ 1 ∈ ℕ)) |
41 | 34, 35, 40 | mpbir2an 955 |
. . . 4
⊢ 0 ∈
{𝑥 ∈ ℝ ∣
(exp‘𝑥) ∈
ℕ} |
42 | 41 | a1i 11 |
. . 3
⊢ (𝜑 → 0 ∈ {𝑥 ∈ ℝ ∣
(exp‘𝑥) ∈
ℕ}) |
43 | 4, 26, 27, 33, 42 | fsumcllem 14463 |
. 2
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈
ℕ}) |
44 | | fveq2 6191 |
. . . . 5
⊢ (𝑥 = Σ𝑘 ∈ 𝐴 𝐵 → (exp‘𝑥) = (exp‘Σ𝑘 ∈ 𝐴 𝐵)) |
45 | 44 | eleq1d 2686 |
. . . 4
⊢ (𝑥 = Σ𝑘 ∈ 𝐴 𝐵 → ((exp‘𝑥) ∈ ℕ ↔
(exp‘Σ𝑘 ∈
𝐴 𝐵) ∈ ℕ)) |
46 | 45 | elrab 3363 |
. . 3
⊢
(Σ𝑘 ∈
𝐴 𝐵 ∈ {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈ ℕ} ↔
(Σ𝑘 ∈ 𝐴 𝐵 ∈ ℝ ∧
(exp‘Σ𝑘 ∈
𝐴 𝐵) ∈ ℕ)) |
47 | 46 | simprbi 480 |
. 2
⊢
(Σ𝑘 ∈
𝐴 𝐵 ∈ {𝑥 ∈ ℝ ∣ (exp‘𝑥) ∈ ℕ} →
(exp‘Σ𝑘 ∈
𝐴 𝐵) ∈ ℕ) |
48 | 43, 47 | syl 17 |
1
⊢ (𝜑 → (exp‘Σ𝑘 ∈ 𝐴 𝐵) ∈ ℕ) |