etransclem33

	Ref	Expression
Hypotheses	etransclem33.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
	etransclem33.x	$⊢ φ \to X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
	etransclem33.p	$⊢ φ \to P \in ℕ$
	etransclem33.m	$⊢ φ \to M \in ℕ_{0}$
	etransclem33.f	$⊢ F = (x \in X ⟼ x^{P - 1} \prod_{j = 1}^{M} {(x - j)}^{P})$
	etransclem33.n	$⊢ φ \to N \in ℕ_{0}$
Assertion	etransclem33	$⊢ φ \to (S D^{n} F) (N) : X ⟶ ℂ$

Proof

Step	Hyp	Ref	Expression
1		etransclem33.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
2		etransclem33.x	$⊢ φ \to X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
3		etransclem33.p	$⊢ φ \to P \in ℕ$
4		etransclem33.m	$⊢ φ \to M \in ℕ_{0}$
5		etransclem33.f	$⊢ F = (x \in X ⟼ x^{P - 1} \prod_{j = 1}^{M} {(x - j)}^{P})$
6		etransclem33.n	$⊢ φ \to N \in ℕ_{0}$
7		eqidd	$⊢ φ \to (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) = (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\})$
8		oveq2	$⊢ m = N \to (0 \dots m) = (0 \dots N)$
9	8	oveq1d	$⊢ m = N \to {(0 \dots m)}^{(0 \dots M)} = {(0 \dots N)}^{(0 \dots M)}$
10		eqeq2	$⊢ m = N \to (\sum_{k = 0}^{M} d (k) = m \leftrightarrow \sum_{k = 0}^{M} d (k) = N)$
11	9 10	rabeqbidv	$⊢ m = N \to \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\} = \{d \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = N\}$
12	11	adantl	$⊢ (φ \land m = N) \to \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\} = \{d \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = N\}$
13		ovex	$⊢ {(0 \dots N)}^{(0 \dots M)} \in V$
14	13	rabex	$⊢ \{d \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = N\} \in V$
15	14	a1i	$⊢ φ \to \{d \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = N\} \in V$
16	7 12 6 15	fvmptd	$⊢ φ \to (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N) = \{d \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = N\}$
17		fzfi	$⊢ (0 \dots N) \in Fin$
18		fzfi	$⊢ (0 \dots M) \in Fin$
19		mapfi	$⊢ ((0 \dots N) \in Fin \land (0 \dots M) \in Fin) \to {(0 \dots N)}^{(0 \dots M)} \in Fin$
20	17 18 19	mp2an	$⊢ {(0 \dots N)}^{(0 \dots M)} \in Fin$
21		ssrab2	$⊢ \{d \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = N\} \subseteq {(0 \dots N)}^{(0 \dots M)}$
22		ssfi	$⊢ ({(0 \dots N)}^{(0 \dots M)} \in Fin \land \{d \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = N\} \subseteq {(0 \dots N)}^{(0 \dots M)}) \to \{d \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = N\} \in Fin$
23	20 21 22	mp2an	$⊢ \{d \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = N\} \in Fin$
24	16 23	eqeltrdi	$⊢ φ \to (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N) \in Fin$
25	24	adantr	$⊢ (φ \land x \in X) \to (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N) \in Fin$
26	6	faccld	$⊢ φ \to N! \in ℕ$
27	26	nncnd	$⊢ φ \to N! \in ℂ$
28	27	ad2antrr	$⊢ ((φ \land x \in X) \land c \in (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N)) \to N! \in ℂ$
29	18	a1i	$⊢ ((φ \land x \in X) \land c \in (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N)) \to (0 \dots M) \in Fin$
30		simpr	$⊢ (φ \land c \in (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N)) \to c \in (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N)$
31	16	adantr	$⊢ (φ \land c \in (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N)) \to (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N) = \{d \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = N\}$
32	30 31	eleqtrd	$⊢ (φ \land c \in (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N)) \to c \in \{d \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = N\}$
33	21 32	sseldi	$⊢ (φ \land c \in (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N)) \to c \in ({(0 \dots N)}^{(0 \dots M)})$
34		elmapi	$⊢ c \in ({(0 \dots N)}^{(0 \dots M)}) \to c : (0 \dots M) ⟶ (0 \dots N)$
35	33 34	syl	$⊢ (φ \land c \in (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N)) \to c : (0 \dots M) ⟶ (0 \dots N)$
36	35	ffvelrnda	$⊢ ((φ \land c \in (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N)) \land j \in (0 \dots M)) \to c (j) \in (0 \dots N)$
37	36	adantllr	$⊢ (((φ \land x \in X) \land c \in (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N)) \land j \in (0 \dots M)) \to c (j) \in (0 \dots N)$
38		elfznn0	$⊢ c (j) \in (0 \dots N) \to c (j) \in ℕ_{0}$
39	37 38	syl	$⊢ (((φ \land x \in X) \land c \in (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N)) \land j \in (0 \dots M)) \to c (j) \in ℕ_{0}$
40	39	faccld	$⊢ (((φ \land x \in X) \land c \in (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N)) \land j \in (0 \dots M)) \to c (j)! \in ℕ$
41	40	nncnd	$⊢ (((φ \land x \in X) \land c \in (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N)) \land j \in (0 \dots M)) \to c (j)! \in ℂ$
42	29 41	fprodcl	$⊢ ((φ \land x \in X) \land c \in (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N)) \to \prod_{j = 0}^{M} c (j)! \in ℂ$
43	40	nnne0d	$⊢ (((φ \land x \in X) \land c \in (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N)) \land j \in (0 \dots M)) \to c (j)! \neq 0$
44	29 41 43	fprodn0	$⊢ ((φ \land x \in X) \land c \in (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N)) \to \prod_{j = 0}^{M} c (j)! \neq 0$
45	28 42 44	divcld	$⊢ ((φ \land x \in X) \land c \in (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N)) \to \frac{N!}{\prod_{j = 0}^{M} c (j)!} \in ℂ$
46	1	ad3antrrr	$⊢ (((φ \land x \in X) \land c \in (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N)) \land j \in (0 \dots M)) \to S \in \{ℝ, ℂ\}$
47	2	ad3antrrr	$⊢ (((φ \land x \in X) \land c \in (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N)) \land j \in (0 \dots M)) \to X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
48	3	ad3antrrr	$⊢ (((φ \land x \in X) \land c \in (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N)) \land j \in (0 \dots M)) \to P \in ℕ$
49		etransclem5	$⊢ (k \in (0 \dots M) ⟼ (y \in X ⟼ {(y - k)}^{if (k = 0, P - 1, P)})) = (w \in (0 \dots M) ⟼ (z \in X ⟼ {(z - w)}^{if (w = 0, P - 1, P)}))$
50		simpr	$⊢ (((φ \land x \in X) \land c \in (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N)) \land j \in (0 \dots M)) \to j \in (0 \dots M)$
51	46 47 48 49 50 39	etransclem20	$⊢ (((φ \land x \in X) \land c \in (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N)) \land j \in (0 \dots M)) \to (S D^{n} (k \in (0 \dots M) ⟼ (y \in X ⟼ {(y - k)}^{if (k = 0, P - 1, P)})) (j)) (c (j)) : X ⟶ ℂ$
52		simpllr	$⊢ (((φ \land x \in X) \land c \in (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N)) \land j \in (0 \dots M)) \to x \in X$
53	51 52	ffvelrnd	$⊢ (((φ \land x \in X) \land c \in (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N)) \land j \in (0 \dots M)) \to (S D^{n} (k \in (0 \dots M) ⟼ (y \in X ⟼ {(y - k)}^{if (k = 0, P - 1, P)})) (j)) (c (j)) (x) \in ℂ$
54	29 53	fprodcl	$⊢ ((φ \land x \in X) \land c \in (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N)) \to \prod_{j = 0}^{M} (S D^{n} (k \in (0 \dots M) ⟼ (y \in X ⟼ {(y - k)}^{if (k = 0, P - 1, P)})) (j)) (c (j)) (x) \in ℂ$
55	45 54	mulcld	$⊢ ((φ \land x \in X) \land c \in (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N)) \to (\frac{N!}{\prod_{j = 0}^{M} c (j)!}) \prod_{j = 0}^{M} (S D^{n} (k \in (0 \dots M) ⟼ (y \in X ⟼ {(y - k)}^{if (k = 0, P - 1, P)})) (j)) (c (j)) (x) \in ℂ$
56	25 55	fsumcl	$⊢ (φ \land x \in X) \to \sum_{c \in (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N)} (\frac{N!}{\prod_{j = 0}^{M} c (j)!}) \prod_{j = 0}^{M} (S D^{n} (k \in (0 \dots M) ⟼ (y \in X ⟼ {(y - k)}^{if (k = 0, P - 1, P)})) (j)) (c (j)) (x) \in ℂ$
57		eqid	$⊢ (x \in X ⟼ \sum_{c \in (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N)} (\frac{N!}{\prod_{j = 0}^{M} c (j)!}) \prod_{j = 0}^{M} (S D^{n} (k \in (0 \dots M) ⟼ (y \in X ⟼ {(y - k)}^{if (k = 0, P - 1, P)})) (j)) (c (j)) (x)) = (x \in X ⟼ \sum_{c \in (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N)} (\frac{N!}{\prod_{j = 0}^{M} c (j)!}) \prod_{j = 0}^{M} (S D^{n} (k \in (0 \dots M) ⟼ (y \in X ⟼ {(y - k)}^{if (k = 0, P - 1, P)})) (j)) (c (j)) (x))$
58	56 57	fmptd	$⊢ φ \to (x \in X ⟼ \sum_{c \in (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N)} (\frac{N!}{\prod_{j = 0}^{M} c (j)!}) \prod_{j = 0}^{M} (S D^{n} (k \in (0 \dots M) ⟼ (y \in X ⟼ {(y - k)}^{if (k = 0, P - 1, P)})) (j)) (c (j)) (x)) : X ⟶ ℂ$
59		etransclem5	$⊢ (k \in (0 \dots M) ⟼ (y \in X ⟼ {(y - k)}^{if (k = 0, P - 1, P)})) = (j \in (0 \dots M) ⟼ (x \in X ⟼ {(x - j)}^{if (j = 0, P - 1, P)}))$
60		etransclem11	$⊢ (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) = (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = n\})$
61	1 2 3 4 5 6 59 60	etransclem30	$⊢ φ \to (S D^{n} F) (N) = (x \in X ⟼ \sum_{c \in (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N)} (\frac{N!}{\prod_{j = 0}^{M} c (j)!}) \prod_{j = 0}^{M} (S D^{n} (k \in (0 \dots M) ⟼ (y \in X ⟼ {(y - k)}^{if (k = 0, P - 1, P)})) (j)) (c (j)) (x))$
62	61	feq1d	$⊢ φ \to ((S D^{n} F) (N) : X ⟶ ℂ \leftrightarrow (x \in X ⟼ \sum_{c \in (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N)} (\frac{N!}{\prod_{j = 0}^{M} c (j)!}) \prod_{j = 0}^{M} (S D^{n} (k \in (0 \dots M) ⟼ (y \in X ⟼ {(y - k)}^{if (k = 0, P - 1, P)})) (j)) (c (j)) (x)) : X ⟶ ℂ)$
63	58 62	mpbird	$⊢ φ \to (S D^{n} F) (N) : X ⟶ ℂ$

Metamath Proof Explorer

Theorem etransclem33

Proof