| Step | Hyp | Ref
| Expression |
| 1 | | etransclem32.s |
. . 3
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) |
| 2 | | etransclem32.x |
. . 3
⊢ (𝜑 → 𝑋 ∈
((TopOpen‘ℂfld) ↾t 𝑆)) |
| 3 | | etransclem32.p |
. . 3
⊢ (𝜑 → 𝑃 ∈ ℕ) |
| 4 | | etransclem32.m |
. . 3
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
| 5 | | etransclem32.f |
. . 3
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥↑(𝑃 − 1)) · ∏𝑗 ∈ (1...𝑀)((𝑥 − 𝑗)↑𝑃))) |
| 6 | | etransclem32.n |
. . 3
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
| 7 | | etransclem32.h |
. . 3
⊢ 𝐻 = (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) |
| 8 | | etransclem11 46260 |
. . 3
⊢ (𝑚 ∈ ℕ0
↦ {𝑑 ∈
((0...𝑚) ↑m
(0...𝑀)) ∣
Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑛}) |
| 9 | 1, 2, 3, 4, 5, 6, 7, 8 | etransclem30 46279 |
. 2
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚})‘𝑁)(((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · ∏𝑗 ∈ (0...𝑀)(((𝑆 D𝑛 (𝐻‘𝑗))‘(𝑐‘𝑗))‘𝑥)))) |
| 10 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚})‘𝑁)) → 𝑐 ∈ ((𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚})‘𝑁)) |
| 11 | 8, 6 | etransclem12 46261 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚})‘𝑁) = {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) |
| 12 | 11 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚})‘𝑁)) → ((𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚})‘𝑁) = {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) |
| 13 | 10, 12 | eleqtrd 2843 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚})‘𝑁)) → 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) |
| 14 | 13 | adantlr 715 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ((𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚})‘𝑁)) → 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) |
| 15 | | nfv 1914 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘(𝜑 ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) |
| 16 | | nfre1 3285 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘∃𝑘 ∈ (0...𝑀)if(𝑘 = 0, (𝑃 − 1), 𝑃) < (𝑐‘𝑘) |
| 17 | 16 | nfn 1857 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘 ¬
∃𝑘 ∈ (0...𝑀)if(𝑘 = 0, (𝑃 − 1), 𝑃) < (𝑐‘𝑘) |
| 18 | 15, 17 | nfan 1899 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘((𝜑 ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ ¬ ∃𝑘 ∈ (0...𝑀)if(𝑘 = 0, (𝑃 − 1), 𝑃) < (𝑐‘𝑘)) |
| 19 | | fzssre 45326 |
. . . . . . . . . . . . . . . . 17
⊢
(0...𝑁) ⊆
ℝ |
| 20 | | rabid 3458 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁} ↔ (𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∧ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁)) |
| 21 | 20 | simplbi 497 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁} → 𝑐 ∈ ((0...𝑁) ↑m (0...𝑀))) |
| 22 | | elmapi 8889 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) → 𝑐:(0...𝑀)⟶(0...𝑁)) |
| 23 | 21, 22 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁} → 𝑐:(0...𝑀)⟶(0...𝑁)) |
| 24 | 23 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) → 𝑐:(0...𝑀)⟶(0...𝑁)) |
| 25 | 24 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ 𝑘 ∈ (0...𝑀)) → (𝑐‘𝑘) ∈ (0...𝑁)) |
| 26 | 19, 25 | sselid 3981 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ 𝑘 ∈ (0...𝑀)) → (𝑐‘𝑘) ∈ ℝ) |
| 27 | 26 | adantlr 715 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ ¬ ∃𝑘 ∈ (0...𝑀)if(𝑘 = 0, (𝑃 − 1), 𝑃) < (𝑐‘𝑘)) ∧ 𝑘 ∈ (0...𝑀)) → (𝑐‘𝑘) ∈ ℝ) |
| 28 | | nnm1nn0 12567 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈
ℕ0) |
| 29 | 3, 28 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑃 − 1) ∈
ℕ0) |
| 30 | 29 | nn0red 12588 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑃 − 1) ∈ ℝ) |
| 31 | 3 | nnred 12281 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑃 ∈ ℝ) |
| 32 | 30, 31 | ifcld 4572 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℝ) |
| 33 | 32 | ad3antrrr 730 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ ¬ ∃𝑘 ∈ (0...𝑀)if(𝑘 = 0, (𝑃 − 1), 𝑃) < (𝑐‘𝑘)) ∧ 𝑘 ∈ (0...𝑀)) → if(𝑘 = 0, (𝑃 − 1), 𝑃) ∈ ℝ) |
| 34 | | ralnex 3072 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑘 ∈
(0...𝑀) ¬ if(𝑘 = 0, (𝑃 − 1), 𝑃) < (𝑐‘𝑘) ↔ ¬ ∃𝑘 ∈ (0...𝑀)if(𝑘 = 0, (𝑃 − 1), 𝑃) < (𝑐‘𝑘)) |
| 35 | 34 | biimpri 228 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
∃𝑘 ∈ (0...𝑀)if(𝑘 = 0, (𝑃 − 1), 𝑃) < (𝑐‘𝑘) → ∀𝑘 ∈ (0...𝑀) ¬ if(𝑘 = 0, (𝑃 − 1), 𝑃) < (𝑐‘𝑘)) |
| 36 | 35 | r19.21bi 3251 |
. . . . . . . . . . . . . . . 16
⊢ ((¬
∃𝑘 ∈ (0...𝑀)if(𝑘 = 0, (𝑃 − 1), 𝑃) < (𝑐‘𝑘) ∧ 𝑘 ∈ (0...𝑀)) → ¬ if(𝑘 = 0, (𝑃 − 1), 𝑃) < (𝑐‘𝑘)) |
| 37 | 36 | adantll 714 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ ¬ ∃𝑘 ∈ (0...𝑀)if(𝑘 = 0, (𝑃 − 1), 𝑃) < (𝑐‘𝑘)) ∧ 𝑘 ∈ (0...𝑀)) → ¬ if(𝑘 = 0, (𝑃 − 1), 𝑃) < (𝑐‘𝑘)) |
| 38 | 27, 33, 37 | nltled 11411 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ ¬ ∃𝑘 ∈ (0...𝑀)if(𝑘 = 0, (𝑃 − 1), 𝑃) < (𝑐‘𝑘)) ∧ 𝑘 ∈ (0...𝑀)) → (𝑐‘𝑘) ≤ if(𝑘 = 0, (𝑃 − 1), 𝑃)) |
| 39 | 38 | ex 412 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ ¬ ∃𝑘 ∈ (0...𝑀)if(𝑘 = 0, (𝑃 − 1), 𝑃) < (𝑐‘𝑘)) → (𝑘 ∈ (0...𝑀) → (𝑐‘𝑘) ≤ if(𝑘 = 0, (𝑃 − 1), 𝑃))) |
| 40 | 18, 39 | ralrimi 3257 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ ¬ ∃𝑘 ∈ (0...𝑀)if(𝑘 = 0, (𝑃 − 1), 𝑃) < (𝑐‘𝑘)) → ∀𝑘 ∈ (0...𝑀)(𝑐‘𝑘) ≤ if(𝑘 = 0, (𝑃 − 1), 𝑃)) |
| 41 | 20 | simprbi 496 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁} → Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁) |
| 42 | | fveq2 6906 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑘 → (𝑐‘𝑗) = (𝑐‘𝑘)) |
| 43 | 42 | cbvsumv 15732 |
. . . . . . . . . . . . . . 15
⊢
Σ𝑗 ∈
(0...𝑀)(𝑐‘𝑗) = Σ𝑘 ∈ (0...𝑀)(𝑐‘𝑘) |
| 44 | 41, 43 | eqtr3di 2792 |
. . . . . . . . . . . . . 14
⊢ (𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁} → 𝑁 = Σ𝑘 ∈ (0...𝑀)(𝑐‘𝑘)) |
| 45 | 44 | ad2antlr 727 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ ∀𝑘 ∈ (0...𝑀)(𝑐‘𝑘) ≤ if(𝑘 = 0, (𝑃 − 1), 𝑃)) → 𝑁 = Σ𝑘 ∈ (0...𝑀)(𝑐‘𝑘)) |
| 46 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = ℎ → (𝑐‘𝑘) = (𝑐‘ℎ)) |
| 47 | 46 | cbvsumv 15732 |
. . . . . . . . . . . . . 14
⊢
Σ𝑘 ∈
(0...𝑀)(𝑐‘𝑘) = Σℎ ∈ (0...𝑀)(𝑐‘ℎ) |
| 48 | | fzfid 14014 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ ∀𝑘 ∈ (0...𝑀)(𝑐‘𝑘) ≤ if(𝑘 = 0, (𝑃 − 1), 𝑃)) → (0...𝑀) ∈ Fin) |
| 49 | 24 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ ℎ ∈ (0...𝑀)) → (𝑐‘ℎ) ∈ (0...𝑁)) |
| 50 | 19, 49 | sselid 3981 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ ℎ ∈ (0...𝑀)) → (𝑐‘ℎ) ∈ ℝ) |
| 51 | 50 | adantlr 715 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ ∀𝑘 ∈ (0...𝑀)(𝑐‘𝑘) ≤ if(𝑘 = 0, (𝑃 − 1), 𝑃)) ∧ ℎ ∈ (0...𝑀)) → (𝑐‘ℎ) ∈ ℝ) |
| 52 | 30, 31 | ifcld 4572 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → if(ℎ = 0, (𝑃 − 1), 𝑃) ∈ ℝ) |
| 53 | 52 | ad3antrrr 730 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ ∀𝑘 ∈ (0...𝑀)(𝑐‘𝑘) ≤ if(𝑘 = 0, (𝑃 − 1), 𝑃)) ∧ ℎ ∈ (0...𝑀)) → if(ℎ = 0, (𝑃 − 1), 𝑃) ∈ ℝ) |
| 54 | | eqeq1 2741 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = ℎ → (𝑘 = 0 ↔ ℎ = 0)) |
| 55 | 54 | ifbid 4549 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = ℎ → if(𝑘 = 0, (𝑃 − 1), 𝑃) = if(ℎ = 0, (𝑃 − 1), 𝑃)) |
| 56 | 46, 55 | breq12d 5156 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = ℎ → ((𝑐‘𝑘) ≤ if(𝑘 = 0, (𝑃 − 1), 𝑃) ↔ (𝑐‘ℎ) ≤ if(ℎ = 0, (𝑃 − 1), 𝑃))) |
| 57 | 56 | rspccva 3621 |
. . . . . . . . . . . . . . . . 17
⊢
((∀𝑘 ∈
(0...𝑀)(𝑐‘𝑘) ≤ if(𝑘 = 0, (𝑃 − 1), 𝑃) ∧ ℎ ∈ (0...𝑀)) → (𝑐‘ℎ) ≤ if(ℎ = 0, (𝑃 − 1), 𝑃)) |
| 58 | 57 | adantll 714 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ ∀𝑘 ∈ (0...𝑀)(𝑐‘𝑘) ≤ if(𝑘 = 0, (𝑃 − 1), 𝑃)) ∧ ℎ ∈ (0...𝑀)) → (𝑐‘ℎ) ≤ if(ℎ = 0, (𝑃 − 1), 𝑃)) |
| 59 | 48, 51, 53, 58 | fsumle 15835 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ ∀𝑘 ∈ (0...𝑀)(𝑐‘𝑘) ≤ if(𝑘 = 0, (𝑃 − 1), 𝑃)) → Σℎ ∈ (0...𝑀)(𝑐‘ℎ) ≤ Σℎ ∈ (0...𝑀)if(ℎ = 0, (𝑃 − 1), 𝑃)) |
| 60 | | nn0uz 12920 |
. . . . . . . . . . . . . . . . . . 19
⊢
ℕ0 = (ℤ≥‘0) |
| 61 | 4, 60 | eleqtrdi 2851 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘0)) |
| 62 | 3 | nnnn0d 12587 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑃 ∈
ℕ0) |
| 63 | 29, 62 | ifcld 4572 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → if(ℎ = 0, (𝑃 − 1), 𝑃) ∈
ℕ0) |
| 64 | 63 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ ℎ ∈ (0...𝑀)) → if(ℎ = 0, (𝑃 − 1), 𝑃) ∈
ℕ0) |
| 65 | 64 | nn0cnd 12589 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ℎ ∈ (0...𝑀)) → if(ℎ = 0, (𝑃 − 1), 𝑃) ∈ ℂ) |
| 66 | | iftrue 4531 |
. . . . . . . . . . . . . . . . . 18
⊢ (ℎ = 0 → if(ℎ = 0, (𝑃 − 1), 𝑃) = (𝑃 − 1)) |
| 67 | 61, 65, 66 | fsum1p 15789 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → Σℎ ∈ (0...𝑀)if(ℎ = 0, (𝑃 − 1), 𝑃) = ((𝑃 − 1) + Σℎ ∈ ((0 + 1)...𝑀)if(ℎ = 0, (𝑃 − 1), 𝑃))) |
| 68 | | 0p1e1 12388 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (0 + 1) =
1 |
| 69 | 68 | oveq1i 7441 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((0 +
1)...𝑀) = (1...𝑀) |
| 70 | 69 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((0 + 1)...𝑀) = (1...𝑀)) |
| 71 | 70 | sumeq1d 15736 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → Σℎ ∈ ((0 + 1)...𝑀)if(ℎ = 0, (𝑃 − 1), 𝑃) = Σℎ ∈ (1...𝑀)if(ℎ = 0, (𝑃 − 1), 𝑃)) |
| 72 | | 0red 11264 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (ℎ ∈ (1...𝑀) → 0 ∈ ℝ) |
| 73 | | 1red 11262 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (ℎ ∈ (1...𝑀) → 1 ∈ ℝ) |
| 74 | | elfzelz 13564 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (ℎ ∈ (1...𝑀) → ℎ ∈ ℤ) |
| 75 | 74 | zred 12722 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (ℎ ∈ (1...𝑀) → ℎ ∈ ℝ) |
| 76 | | 0lt1 11785 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 0 <
1 |
| 77 | 76 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (ℎ ∈ (1...𝑀) → 0 < 1) |
| 78 | | elfzle1 13567 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (ℎ ∈ (1...𝑀) → 1 ≤ ℎ) |
| 79 | 72, 73, 75, 77, 78 | ltletrd 11421 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (ℎ ∈ (1...𝑀) → 0 < ℎ) |
| 80 | 79 | gt0ne0d 11827 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ℎ ∈ (1...𝑀) → ℎ ≠ 0) |
| 81 | 80 | neneqd 2945 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (ℎ ∈ (1...𝑀) → ¬ ℎ = 0) |
| 82 | 81 | iffalsed 4536 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℎ ∈ (1...𝑀) → if(ℎ = 0, (𝑃 − 1), 𝑃) = 𝑃) |
| 83 | 82 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ ℎ ∈ (1...𝑀)) → if(ℎ = 0, (𝑃 − 1), 𝑃) = 𝑃) |
| 84 | 83 | sumeq2dv 15738 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → Σℎ ∈ (1...𝑀)if(ℎ = 0, (𝑃 − 1), 𝑃) = Σℎ ∈ (1...𝑀)𝑃) |
| 85 | | fzfid 14014 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (1...𝑀) ∈ Fin) |
| 86 | 3 | nncnd 12282 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑃 ∈ ℂ) |
| 87 | | fsumconst 15826 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((1...𝑀) ∈ Fin
∧ 𝑃 ∈ ℂ)
→ Σℎ ∈
(1...𝑀)𝑃 = ((♯‘(1...𝑀)) · 𝑃)) |
| 88 | 85, 86, 87 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → Σℎ ∈ (1...𝑀)𝑃 = ((♯‘(1...𝑀)) · 𝑃)) |
| 89 | | hashfz1 14385 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑀 ∈ ℕ0
→ (♯‘(1...𝑀)) = 𝑀) |
| 90 | 4, 89 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (♯‘(1...𝑀)) = 𝑀) |
| 91 | 90 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((♯‘(1...𝑀)) · 𝑃) = (𝑀 · 𝑃)) |
| 92 | 88, 91 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → Σℎ ∈ (1...𝑀)𝑃 = (𝑀 · 𝑃)) |
| 93 | 71, 84, 92 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → Σℎ ∈ ((0 + 1)...𝑀)if(ℎ = 0, (𝑃 − 1), 𝑃) = (𝑀 · 𝑃)) |
| 94 | 93 | oveq2d 7447 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑃 − 1) + Σℎ ∈ ((0 + 1)...𝑀)if(ℎ = 0, (𝑃 − 1), 𝑃)) = ((𝑃 − 1) + (𝑀 · 𝑃))) |
| 95 | 29 | nn0cnd 12589 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑃 − 1) ∈ ℂ) |
| 96 | 4, 62 | nn0mulcld 12592 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑀 · 𝑃) ∈
ℕ0) |
| 97 | 96 | nn0cnd 12589 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑀 · 𝑃) ∈ ℂ) |
| 98 | 95, 97 | addcomd 11463 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑃 − 1) + (𝑀 · 𝑃)) = ((𝑀 · 𝑃) + (𝑃 − 1))) |
| 99 | 67, 94, 98 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → Σℎ ∈ (0...𝑀)if(ℎ = 0, (𝑃 − 1), 𝑃) = ((𝑀 · 𝑃) + (𝑃 − 1))) |
| 100 | 99 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ ∀𝑘 ∈ (0...𝑀)(𝑐‘𝑘) ≤ if(𝑘 = 0, (𝑃 − 1), 𝑃)) → Σℎ ∈ (0...𝑀)if(ℎ = 0, (𝑃 − 1), 𝑃) = ((𝑀 · 𝑃) + (𝑃 − 1))) |
| 101 | 59, 100 | breqtrd 5169 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ ∀𝑘 ∈ (0...𝑀)(𝑐‘𝑘) ≤ if(𝑘 = 0, (𝑃 − 1), 𝑃)) → Σℎ ∈ (0...𝑀)(𝑐‘ℎ) ≤ ((𝑀 · 𝑃) + (𝑃 − 1))) |
| 102 | 47, 101 | eqbrtrid 5178 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ ∀𝑘 ∈ (0...𝑀)(𝑐‘𝑘) ≤ if(𝑘 = 0, (𝑃 − 1), 𝑃)) → Σ𝑘 ∈ (0...𝑀)(𝑐‘𝑘) ≤ ((𝑀 · 𝑃) + (𝑃 − 1))) |
| 103 | 45, 102 | eqbrtrd 5165 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ ∀𝑘 ∈ (0...𝑀)(𝑐‘𝑘) ≤ if(𝑘 = 0, (𝑃 − 1), 𝑃)) → 𝑁 ≤ ((𝑀 · 𝑃) + (𝑃 − 1))) |
| 104 | 40, 103 | syldan 591 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ ¬ ∃𝑘 ∈ (0...𝑀)if(𝑘 = 0, (𝑃 − 1), 𝑃) < (𝑐‘𝑘)) → 𝑁 ≤ ((𝑀 · 𝑃) + (𝑃 − 1))) |
| 105 | | etransclem32.ngt |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑀 · 𝑃) + (𝑃 − 1)) < 𝑁) |
| 106 | 96, 29 | nn0addcld 12591 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑀 · 𝑃) + (𝑃 − 1)) ∈
ℕ0) |
| 107 | 106 | nn0red 12588 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑀 · 𝑃) + (𝑃 − 1)) ∈
ℝ) |
| 108 | 6 | nn0red 12588 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℝ) |
| 109 | 107, 108 | ltnled 11408 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑀 · 𝑃) + (𝑃 − 1)) < 𝑁 ↔ ¬ 𝑁 ≤ ((𝑀 · 𝑃) + (𝑃 − 1)))) |
| 110 | 105, 109 | mpbid 232 |
. . . . . . . . . . . 12
⊢ (𝜑 → ¬ 𝑁 ≤ ((𝑀 · 𝑃) + (𝑃 − 1))) |
| 111 | 110 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ ¬ ∃𝑘 ∈ (0...𝑀)if(𝑘 = 0, (𝑃 − 1), 𝑃) < (𝑐‘𝑘)) → ¬ 𝑁 ≤ ((𝑀 · 𝑃) + (𝑃 − 1))) |
| 112 | 104, 111 | condan 818 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) → ∃𝑘 ∈ (0...𝑀)if(𝑘 = 0, (𝑃 − 1), 𝑃) < (𝑐‘𝑘)) |
| 113 | 112 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) → ∃𝑘 ∈ (0...𝑀)if(𝑘 = 0, (𝑃 − 1), 𝑃) < (𝑐‘𝑘)) |
| 114 | | nfv 1914 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑗(𝜑 ∧ 𝑥 ∈ 𝑋) |
| 115 | | nfcv 2905 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑗(0...𝑀) |
| 116 | 115 | nfsum1 15726 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑗Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) |
| 117 | 116 | nfeq1 2921 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑗Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁 |
| 118 | | nfcv 2905 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑗((0...𝑁) ↑m (0...𝑀)) |
| 119 | 117, 118 | nfrabw 3475 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑗{𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁} |
| 120 | 119 | nfcri 2897 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑗 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁} |
| 121 | 114, 120 | nfan 1899 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑗((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) |
| 122 | | nfv 1914 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑗 𝑘 ∈ (0...𝑀) |
| 123 | | nfv 1914 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑗if(𝑘 = 0, (𝑃 − 1), 𝑃) < (𝑐‘𝑘) |
| 124 | 121, 122,
123 | nf3an 1901 |
. . . . . . . . . . 11
⊢
Ⅎ𝑗(((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ 𝑘 ∈ (0...𝑀) ∧ if(𝑘 = 0, (𝑃 − 1), 𝑃) < (𝑐‘𝑘)) |
| 125 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑗(((𝑆 D𝑛 (𝐻‘𝑘))‘(𝑐‘𝑘))‘𝑥) |
| 126 | | fzfid 14014 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ 𝑘 ∈ (0...𝑀) ∧ if(𝑘 = 0, (𝑃 − 1), 𝑃) < (𝑐‘𝑘)) → (0...𝑀) ∈ Fin) |
| 127 | 1 | ad3antrrr 730 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ 𝑗 ∈ (0...𝑀)) → 𝑆 ∈ {ℝ, ℂ}) |
| 128 | 2 | ad3antrrr 730 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ 𝑗 ∈ (0...𝑀)) → 𝑋 ∈
((TopOpen‘ℂfld) ↾t 𝑆)) |
| 129 | 3 | ad3antrrr 730 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ 𝑗 ∈ (0...𝑀)) → 𝑃 ∈ ℕ) |
| 130 | | etransclem5 46254 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) = (𝑘 ∈ (0...𝑀) ↦ (𝑦 ∈ 𝑋 ↦ ((𝑦 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))) |
| 131 | 7, 130 | eqtri 2765 |
. . . . . . . . . . . . . 14
⊢ 𝐻 = (𝑘 ∈ (0...𝑀) ↦ (𝑦 ∈ 𝑋 ↦ ((𝑦 − 𝑘)↑if(𝑘 = 0, (𝑃 − 1), 𝑃)))) |
| 132 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ (0...𝑀)) |
| 133 | 23 | ad2antlr 727 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ 𝑗 ∈ (0...𝑀)) → 𝑐:(0...𝑀)⟶(0...𝑁)) |
| 134 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ (0...𝑀)) |
| 135 | 133, 134 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ 𝑗 ∈ (0...𝑀)) → (𝑐‘𝑗) ∈ (0...𝑁)) |
| 136 | 135 | adantllr 719 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ 𝑗 ∈ (0...𝑀)) → (𝑐‘𝑗) ∈ (0...𝑁)) |
| 137 | | elfznn0 13660 |
. . . . . . . . . . . . . . 15
⊢ ((𝑐‘𝑗) ∈ (0...𝑁) → (𝑐‘𝑗) ∈
ℕ0) |
| 138 | 136, 137 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ 𝑗 ∈ (0...𝑀)) → (𝑐‘𝑗) ∈
ℕ0) |
| 139 | 127, 128,
129, 131, 132, 138 | etransclem20 46269 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ 𝑗 ∈ (0...𝑀)) → ((𝑆 D𝑛 (𝐻‘𝑗))‘(𝑐‘𝑗)):𝑋⟶ℂ) |
| 140 | | simpllr 776 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ 𝑗 ∈ (0...𝑀)) → 𝑥 ∈ 𝑋) |
| 141 | 139, 140 | ffvelcdmd 7105 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ 𝑗 ∈ (0...𝑀)) → (((𝑆 D𝑛 (𝐻‘𝑗))‘(𝑐‘𝑗))‘𝑥) ∈ ℂ) |
| 142 | 141 | 3ad2antl1 1186 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ 𝑘 ∈ (0...𝑀) ∧ if(𝑘 = 0, (𝑃 − 1), 𝑃) < (𝑐‘𝑘)) ∧ 𝑗 ∈ (0...𝑀)) → (((𝑆 D𝑛 (𝐻‘𝑗))‘(𝑐‘𝑗))‘𝑥) ∈ ℂ) |
| 143 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑘 → (𝐻‘𝑗) = (𝐻‘𝑘)) |
| 144 | 143 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑘 → (𝑆 D𝑛 (𝐻‘𝑗)) = (𝑆 D𝑛 (𝐻‘𝑘))) |
| 145 | 144, 42 | fveq12d 6913 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑘 → ((𝑆 D𝑛 (𝐻‘𝑗))‘(𝑐‘𝑗)) = ((𝑆 D𝑛 (𝐻‘𝑘))‘(𝑐‘𝑘))) |
| 146 | 145 | fveq1d 6908 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑘 → (((𝑆 D𝑛 (𝐻‘𝑗))‘(𝑐‘𝑗))‘𝑥) = (((𝑆 D𝑛 (𝐻‘𝑘))‘(𝑐‘𝑘))‘𝑥)) |
| 147 | | simp2 1138 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ 𝑘 ∈ (0...𝑀) ∧ if(𝑘 = 0, (𝑃 − 1), 𝑃) < (𝑐‘𝑘)) → 𝑘 ∈ (0...𝑀)) |
| 148 | 1 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) → 𝑆 ∈ {ℝ, ℂ}) |
| 149 | 148 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ 𝑘 ∈ (0...𝑀) ∧ if(𝑘 = 0, (𝑃 − 1), 𝑃) < (𝑐‘𝑘)) → 𝑆 ∈ {ℝ, ℂ}) |
| 150 | 2 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) → 𝑋 ∈
((TopOpen‘ℂfld) ↾t 𝑆)) |
| 151 | 150 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ 𝑘 ∈ (0...𝑀) ∧ if(𝑘 = 0, (𝑃 − 1), 𝑃) < (𝑐‘𝑘)) → 𝑋 ∈
((TopOpen‘ℂfld) ↾t 𝑆)) |
| 152 | 3 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) → 𝑃 ∈ ℕ) |
| 153 | 152 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ 𝑘 ∈ (0...𝑀) ∧ if(𝑘 = 0, (𝑃 − 1), 𝑃) < (𝑐‘𝑘)) → 𝑃 ∈ ℕ) |
| 154 | | etransclem5 46254 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (0...𝑀) ↦ (𝑥 ∈ 𝑋 ↦ ((𝑥 − 𝑗)↑if(𝑗 = 0, (𝑃 − 1), 𝑃)))) = (ℎ ∈ (0...𝑀) ↦ (𝑦 ∈ 𝑋 ↦ ((𝑦 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃)))) |
| 155 | 7, 154 | eqtri 2765 |
. . . . . . . . . . . . 13
⊢ 𝐻 = (ℎ ∈ (0...𝑀) ↦ (𝑦 ∈ 𝑋 ↦ ((𝑦 − ℎ)↑if(ℎ = 0, (𝑃 − 1), 𝑃)))) |
| 156 | 25 | elfzelzd 13565 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ 𝑘 ∈ (0...𝑀)) → (𝑐‘𝑘) ∈ ℤ) |
| 157 | 156 | adantllr 719 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ 𝑘 ∈ (0...𝑀)) → (𝑐‘𝑘) ∈ ℤ) |
| 158 | 157 | 3adant3 1133 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ 𝑘 ∈ (0...𝑀) ∧ if(𝑘 = 0, (𝑃 − 1), 𝑃) < (𝑐‘𝑘)) → (𝑐‘𝑘) ∈ ℤ) |
| 159 | | simp3 1139 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ 𝑘 ∈ (0...𝑀) ∧ if(𝑘 = 0, (𝑃 − 1), 𝑃) < (𝑐‘𝑘)) → if(𝑘 = 0, (𝑃 − 1), 𝑃) < (𝑐‘𝑘)) |
| 160 | 149, 151,
153, 155, 147, 158, 159 | etransclem19 46268 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ 𝑘 ∈ (0...𝑀) ∧ if(𝑘 = 0, (𝑃 − 1), 𝑃) < (𝑐‘𝑘)) → ((𝑆 D𝑛 (𝐻‘𝑘))‘(𝑐‘𝑘)) = (𝑦 ∈ 𝑋 ↦ 0)) |
| 161 | | eqidd 2738 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ 𝑘 ∈ (0...𝑀) ∧ if(𝑘 = 0, (𝑃 − 1), 𝑃) < (𝑐‘𝑘)) ∧ 𝑦 = 𝑥) → 0 = 0) |
| 162 | | simp1lr 1238 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ 𝑘 ∈ (0...𝑀) ∧ if(𝑘 = 0, (𝑃 − 1), 𝑃) < (𝑐‘𝑘)) → 𝑥 ∈ 𝑋) |
| 163 | | 0red 11264 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ 𝑘 ∈ (0...𝑀) ∧ if(𝑘 = 0, (𝑃 − 1), 𝑃) < (𝑐‘𝑘)) → 0 ∈ ℝ) |
| 164 | 160, 161,
162, 163 | fvmptd 7023 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ 𝑘 ∈ (0...𝑀) ∧ if(𝑘 = 0, (𝑃 − 1), 𝑃) < (𝑐‘𝑘)) → (((𝑆 D𝑛 (𝐻‘𝑘))‘(𝑐‘𝑘))‘𝑥) = 0) |
| 165 | 124, 125,
126, 142, 146, 147, 164 | fprod0 45611 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) ∧ 𝑘 ∈ (0...𝑀) ∧ if(𝑘 = 0, (𝑃 − 1), 𝑃) < (𝑐‘𝑘)) → ∏𝑗 ∈ (0...𝑀)(((𝑆 D𝑛 (𝐻‘𝑗))‘(𝑐‘𝑗))‘𝑥) = 0) |
| 166 | 165 | rexlimdv3a 3159 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) → (∃𝑘 ∈ (0...𝑀)if(𝑘 = 0, (𝑃 − 1), 𝑃) < (𝑐‘𝑘) → ∏𝑗 ∈ (0...𝑀)(((𝑆 D𝑛 (𝐻‘𝑗))‘(𝑐‘𝑗))‘𝑥) = 0)) |
| 167 | 113, 166 | mpd 15 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) → ∏𝑗 ∈ (0...𝑀)(((𝑆 D𝑛 (𝐻‘𝑗))‘(𝑐‘𝑗))‘𝑥) = 0) |
| 168 | 14, 167 | syldan 591 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ((𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚})‘𝑁)) → ∏𝑗 ∈ (0...𝑀)(((𝑆 D𝑛 (𝐻‘𝑗))‘(𝑐‘𝑗))‘𝑥) = 0) |
| 169 | 168 | oveq2d 7447 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ((𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚})‘𝑁)) → (((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · ∏𝑗 ∈ (0...𝑀)(((𝑆 D𝑛 (𝐻‘𝑗))‘(𝑐‘𝑗))‘𝑥)) = (((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · 0)) |
| 170 | 6 | faccld 14323 |
. . . . . . . . . . 11
⊢ (𝜑 → (!‘𝑁) ∈ ℕ) |
| 171 | 170 | nncnd 12282 |
. . . . . . . . . 10
⊢ (𝜑 → (!‘𝑁) ∈ ℂ) |
| 172 | 171 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚})‘𝑁)) → (!‘𝑁) ∈ ℂ) |
| 173 | | fzfid 14014 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚})‘𝑁)) → (0...𝑀) ∈ Fin) |
| 174 | | simpll 767 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚})‘𝑁)) ∧ 𝑗 ∈ (0...𝑀)) → 𝜑) |
| 175 | 13 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚})‘𝑁)) ∧ 𝑗 ∈ (0...𝑀)) → 𝑐 ∈ {𝑐 ∈ ((0...𝑁) ↑m (0...𝑀)) ∣ Σ𝑗 ∈ (0...𝑀)(𝑐‘𝑗) = 𝑁}) |
| 176 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚})‘𝑁)) ∧ 𝑗 ∈ (0...𝑀)) → 𝑗 ∈ (0...𝑀)) |
| 177 | 174, 175,
176, 135 | syl21anc 838 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚})‘𝑁)) ∧ 𝑗 ∈ (0...𝑀)) → (𝑐‘𝑗) ∈ (0...𝑁)) |
| 178 | 177, 137 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚})‘𝑁)) ∧ 𝑗 ∈ (0...𝑀)) → (𝑐‘𝑗) ∈
ℕ0) |
| 179 | 178 | faccld 14323 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚})‘𝑁)) ∧ 𝑗 ∈ (0...𝑀)) → (!‘(𝑐‘𝑗)) ∈ ℕ) |
| 180 | 179 | nncnd 12282 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚})‘𝑁)) ∧ 𝑗 ∈ (0...𝑀)) → (!‘(𝑐‘𝑗)) ∈ ℂ) |
| 181 | 173, 180 | fprodcl 15988 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚})‘𝑁)) → ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗)) ∈ ℂ) |
| 182 | 179 | nnne0d 12316 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ ((𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚})‘𝑁)) ∧ 𝑗 ∈ (0...𝑀)) → (!‘(𝑐‘𝑗)) ≠ 0) |
| 183 | 173, 180,
182 | fprodn0 16015 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚})‘𝑁)) → ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗)) ≠ 0) |
| 184 | 172, 181,
183 | divcld 12043 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚})‘𝑁)) → ((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) ∈ ℂ) |
| 185 | 184 | mul01d 11460 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ ((𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚})‘𝑁)) → (((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · 0) = 0) |
| 186 | 185 | adantlr 715 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ((𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚})‘𝑁)) → (((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · 0) = 0) |
| 187 | 169, 186 | eqtrd 2777 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ((𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚})‘𝑁)) → (((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · ∏𝑗 ∈ (0...𝑀)(((𝑆 D𝑛 (𝐻‘𝑗))‘(𝑐‘𝑗))‘𝑥)) = 0) |
| 188 | 187 | sumeq2dv 15738 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → Σ𝑐 ∈ ((𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚})‘𝑁)(((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · ∏𝑗 ∈ (0...𝑀)(((𝑆 D𝑛 (𝐻‘𝑗))‘(𝑐‘𝑗))‘𝑥)) = Σ𝑐 ∈ ((𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚})‘𝑁)0) |
| 189 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ0
↦ {𝑑 ∈
((0...𝑚) ↑m
(0...𝑀)) ∣
Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚}) = (𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚}) |
| 190 | 189, 6 | etransclem16 46265 |
. . . . . . 7
⊢ (𝜑 → ((𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚})‘𝑁) ∈ Fin) |
| 191 | 190 | olcd 875 |
. . . . . 6
⊢ (𝜑 → (((𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚})‘𝑁) ⊆
(ℤ≥‘𝐴) ∨ ((𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚})‘𝑁) ∈ Fin)) |
| 192 | 191 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (((𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚})‘𝑁) ⊆
(ℤ≥‘𝐴) ∨ ((𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚})‘𝑁) ∈ Fin)) |
| 193 | | sumz 15758 |
. . . . 5
⊢ ((((𝑚 ∈ ℕ0
↦ {𝑑 ∈
((0...𝑚) ↑m
(0...𝑀)) ∣
Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚})‘𝑁) ⊆
(ℤ≥‘𝐴) ∨ ((𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚})‘𝑁) ∈ Fin) → Σ𝑐 ∈ ((𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚})‘𝑁)0 = 0) |
| 194 | 192, 193 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → Σ𝑐 ∈ ((𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚})‘𝑁)0 = 0) |
| 195 | 188, 194 | eqtrd 2777 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → Σ𝑐 ∈ ((𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚})‘𝑁)(((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · ∏𝑗 ∈ (0...𝑀)(((𝑆 D𝑛 (𝐻‘𝑗))‘(𝑐‘𝑗))‘𝑥)) = 0) |
| 196 | 195 | mpteq2dva 5242 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ Σ𝑐 ∈ ((𝑚 ∈ ℕ0 ↦ {𝑑 ∈ ((0...𝑚) ↑m (0...𝑀)) ∣ Σ𝑘 ∈ (0...𝑀)(𝑑‘𝑘) = 𝑚})‘𝑁)(((!‘𝑁) / ∏𝑗 ∈ (0...𝑀)(!‘(𝑐‘𝑗))) · ∏𝑗 ∈ (0...𝑀)(((𝑆 D𝑛 (𝐻‘𝑗))‘(𝑐‘𝑗))‘𝑥))) = (𝑥 ∈ 𝑋 ↦ 0)) |
| 197 | 9, 196 | eqtrd 2777 |
1
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑥 ∈ 𝑋 ↦ 0)) |