Step | Hyp | Ref
| Expression |
1 | | etransclem1.x |
. . . . . 6
⊢ (𝜑 → 𝑋 ⊆ ℂ) |
2 | 1 | sselda 3568 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ ℂ) |
3 | | etransclem1.j |
. . . . . . . 8
⊢ (𝜑 → 𝐽 ∈ (0...𝑀)) |
4 | 3 | elfzelzd 38471 |
. . . . . . 7
⊢ (𝜑 → 𝐽 ∈ ℤ) |
5 | 4 | zcnd 11359 |
. . . . . 6
⊢ (𝜑 → 𝐽 ∈ ℂ) |
6 | 5 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐽 ∈ ℂ) |
7 | 2, 6 | subcld 10271 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑥 − 𝐽) ∈ ℂ) |
8 | | etransclem1.p |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ ℕ) |
9 | | nnm1nn0 11211 |
. . . . . . 7
⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈
ℕ0) |
10 | 8, 9 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑃 − 1) ∈
ℕ0) |
11 | 8 | nnnn0d 11228 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈
ℕ0) |
12 | 10, 11 | ifcld 4081 |
. . . . 5
⊢ (𝜑 → if(𝐽 = 0, (𝑃 − 1), 𝑃) ∈
ℕ0) |
13 | 12 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → if(𝐽 = 0, (𝑃 − 1), 𝑃) ∈
ℕ0) |
14 | 7, 13 | expcld 12870 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑥 − 𝐽)↑if(𝐽 = 0, (𝑃 − 1), 𝑃)) ∈ ℂ) |
15 | | eqid 2610 |
. . 3
⊢ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝐽)↑if(𝐽 = 0, (𝑃 − 1), 𝑃))) = (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝐽)↑if(𝐽 = 0, (𝑃 − 1), 𝑃))) |
16 | 14, 15 | fmptd 6292 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝐽)↑if(𝐽 = 0, (𝑃 − 1), 𝑃))):𝑋⟶ℂ) |
17 | | etransclem1.h |
. . . . . 6
⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) |
18 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑗 = 𝑛 → (𝑥 − 𝑗) = (𝑥 − 𝑛)) |
19 | | eqeq1 2614 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑛 → (𝑗 = 0 ↔ 𝑛 = 0)) |
20 | 19 | ifbid 4058 |
. . . . . . . . 9
⊢ (𝑗 = 𝑛 → if(𝑗 = 0, (𝑃 − 1), 𝑃) = if(𝑛 = 0, (𝑃 − 1), 𝑃)) |
21 | 18, 20 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝑗 = 𝑛 → ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)) = ((𝑥 − 𝑛)↑if(𝑛 = 0, (𝑃 − 1), 𝑃))) |
22 | 21 | mpteq2dv 4673 |
. . . . . . 7
⊢ (𝑗 = 𝑛 → (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃))) = (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑛)↑if(𝑛 = 0, (𝑃 − 1), 𝑃)))) |
23 | 22 | cbvmptv 4678 |
. . . . . 6
⊢ (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) = (𝑛 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑛)↑if(𝑛 = 0, (𝑃 − 1), 𝑃)))) |
24 | 17, 23 | eqtri 2632 |
. . . . 5
⊢ 𝐻 = (𝑛 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑛)↑if(𝑛 = 0, (𝑃 − 1), 𝑃)))) |
25 | 24 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐻 = (𝑛 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑛)↑if(𝑛 = 0, (𝑃 − 1), 𝑃))))) |
26 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑛 = 𝐽 → (𝑥 − 𝑛) = (𝑥 − 𝐽)) |
27 | | eqeq1 2614 |
. . . . . . . 8
⊢ (𝑛 = 𝐽 → (𝑛 = 0 ↔ 𝐽 = 0)) |
28 | 27 | ifbid 4058 |
. . . . . . 7
⊢ (𝑛 = 𝐽 → if(𝑛 = 0, (𝑃 − 1), 𝑃) = if(𝐽 = 0, (𝑃 − 1), 𝑃)) |
29 | 26, 28 | oveq12d 6567 |
. . . . . 6
⊢ (𝑛 = 𝐽 → ((𝑥 − 𝑛)↑if(𝑛 = 0, (𝑃 − 1), 𝑃)) = ((𝑥 − 𝐽)↑if(𝐽 = 0, (𝑃 − 1), 𝑃))) |
30 | 29 | mpteq2dv 4673 |
. . . . 5
⊢ (𝑛 = 𝐽 → (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑛)↑if(𝑛 = 0, (𝑃 − 1), 𝑃))) = (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝐽)↑if(𝐽 = 0, (𝑃 − 1), 𝑃)))) |
31 | 30 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 = 𝐽) → (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑛)↑if(𝑛 = 0, (𝑃 − 1), 𝑃))) = (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝐽)↑if(𝐽 = 0, (𝑃 − 1), 𝑃)))) |
32 | | cnex 9896 |
. . . . . 6
⊢ ℂ
∈ V |
33 | 32 | ssex 4730 |
. . . . 5
⊢ (𝑋 ⊆ ℂ → 𝑋 ∈ V) |
34 | | mptexg 6389 |
. . . . 5
⊢ (𝑋 ∈ V → (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝐽)↑if(𝐽 = 0, (𝑃 − 1), 𝑃))) ∈ V) |
35 | 1, 33, 34 | 3syl 18 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝐽)↑if(𝐽 = 0, (𝑃 − 1), 𝑃))) ∈ V) |
36 | 25, 31, 3, 35 | fvmptd 6197 |
. . 3
⊢ (𝜑 → (𝐻‘𝐽) = (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝐽)↑if(𝐽 = 0, (𝑃 − 1), 𝑃)))) |
37 | 36 | feq1d 5943 |
. 2
⊢ (𝜑 → ((𝐻‘𝐽):𝑋⟶ℂ ↔ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝐽)↑if(𝐽 = 0, (𝑃 − 1), 𝑃))):𝑋⟶ℂ)) |
38 | 16, 37 | mpbird 246 |
1
⊢ (𝜑 → (𝐻‘𝐽):𝑋⟶ℂ) |