etransclem37

Description: ( P - 1 ) factorial divides the N -th derivative of F applied to J . (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	etransclem37.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
	etransclem37.x	$⊢ φ \to X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
	etransclem37.p	$⊢ φ \to P \in ℕ$
	etransclem37.m	$⊢ φ \to M \in ℕ_{0}$
	etransclem37.f	$⊢ F = (x \in X ⟼ x^{P - 1} \prod_{j = 1}^{M} {(x - j)}^{P})$
	etransclem37.n	$⊢ φ \to N \in ℕ_{0}$
	etransclem37.h	$⊢ H = (j \in (0 \dots M) ⟼ (x \in X ⟼ {(x - j)}^{if (j = 0, P - 1, P)}))$
	etransclem37.c	$⊢ C = (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = n\})$
	etransclem37.9	$⊢ φ \to J \in (0 \dots M)$
	etransclem37.j	$⊢ φ \to J \in X$
Assertion	etransclem37	$⊢ φ \to (P - 1)! ∥ (S D^{n} F) (N) (J)$

Proof

Step	Hyp	Ref	Expression
1		etransclem37.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
2		etransclem37.x	$⊢ φ \to X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
3		etransclem37.p	$⊢ φ \to P \in ℕ$
4		etransclem37.m	$⊢ φ \to M \in ℕ_{0}$
5		etransclem37.f	$⊢ F = (x \in X ⟼ x^{P - 1} \prod_{j = 1}^{M} {(x - j)}^{P})$
6		etransclem37.n	$⊢ φ \to N \in ℕ_{0}$
7		etransclem37.h	$⊢ H = (j \in (0 \dots M) ⟼ (x \in X ⟼ {(x - j)}^{if (j = 0, P - 1, P)}))$
8		etransclem37.c	$⊢ C = (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = n\})$
9		etransclem37.9	$⊢ φ \to J \in (0 \dots M)$
10		etransclem37.j	$⊢ φ \to J \in X$
11	8 6	etransclem16	$⊢ φ \to C (N) \in Fin$
12		nnm1nn0	$⊢ P \in ℕ \to P - 1 \in ℕ_{0}$
13	3 12	syl	$⊢ φ \to P - 1 \in ℕ_{0}$
14	13	faccld	$⊢ φ \to (P - 1)! \in ℕ$
15	14	nnzd	$⊢ φ \to (P - 1)! \in ℤ$
16	8 6	etransclem12	$⊢ φ \to C (N) = \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}$
17	16	eleq2d	$⊢ φ \to (c \in C (N) \leftrightarrow c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\})$
18	17	biimpa	$⊢ (φ \land c \in C (N)) \to c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}$
19		rabid	$⊢ c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\} \leftrightarrow (c \in ({(0 \dots N)}^{(0 \dots M)}) \land \sum_{j = 0}^{M} c (j) = N)$
20	19	biimpi	$⊢ c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\} \to (c \in ({(0 \dots N)}^{(0 \dots M)}) \land \sum_{j = 0}^{M} c (j) = N)$
21	20	simprd	$⊢ c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\} \to \sum_{j = 0}^{M} c (j) = N$
22	18 21	syl	$⊢ (φ \land c \in C (N)) \to \sum_{j = 0}^{M} c (j) = N$
23	22	eqcomd	$⊢ (φ \land c \in C (N)) \to N = \sum_{j = 0}^{M} c (j)$
24	23	fveq2d	$⊢ (φ \land c \in C (N)) \to N! = \sum_{j = 0}^{M} c (j)!$
25	24	oveq1d	$⊢ (φ \land c \in C (N)) \to \frac{N!}{\prod_{j = 0}^{M} c (j)!} = \frac{\sum_{j = 0}^{M} c (j)!}{\prod_{j = 0}^{M} c (j)!}$
26		nfcv	$⊢ \underline{Ⅎ} j c$
27		fzfid	$⊢ (φ \land c \in C (N)) \to (0 \dots M) \in Fin$
28		nn0ex	$⊢ ℕ_{0} \in V$
29	28	a1i	$⊢ c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\} \to ℕ_{0} \in V$
30		fzssnn0	$⊢ (0 \dots N) \subseteq ℕ_{0}$
31		mapss	$⊢ (ℕ_{0} \in V \land (0 \dots N) \subseteq ℕ_{0}) \to {(0 \dots N)}^{(0 \dots M)} \subseteq {ℕ_{0}}^{(0 \dots M)}$
32	29 30 31	sylancl	$⊢ c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\} \to {(0 \dots N)}^{(0 \dots M)} \subseteq {ℕ_{0}}^{(0 \dots M)}$
33	20	simpld	$⊢ c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\} \to c \in ({(0 \dots N)}^{(0 \dots M)})$
34	32 33	sseldd	$⊢ c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\} \to c \in ({ℕ_{0}}^{(0 \dots M)})$
35	18 34	syl	$⊢ (φ \land c \in C (N)) \to c \in ({ℕ_{0}}^{(0 \dots M)})$
36	26 27 35	mccl	$⊢ (φ \land c \in C (N)) \to \frac{\sum_{j = 0}^{M} c (j)!}{\prod_{j = 0}^{M} c (j)!} \in ℕ$
37	25 36	eqeltrd	$⊢ (φ \land c \in C (N)) \to \frac{N!}{\prod_{j = 0}^{M} c (j)!} \in ℕ$
38	37	nnzd	$⊢ (φ \land c \in C (N)) \to \frac{N!}{\prod_{j = 0}^{M} c (j)!} \in ℤ$
39	3	adantr	$⊢ (φ \land c \in C (N)) \to P \in ℕ$
40	4	adantr	$⊢ (φ \land c \in C (N)) \to M \in ℕ_{0}$
41		elmapi	$⊢ c \in ({(0 \dots N)}^{(0 \dots M)}) \to c : (0 \dots M) ⟶ (0 \dots N)$
42	18 33 41	3syl	$⊢ (φ \land c \in C (N)) \to c : (0 \dots M) ⟶ (0 \dots N)$
43	9	elfzelzd	$⊢ φ \to J \in ℤ$
44	43	adantr	$⊢ (φ \land c \in C (N)) \to J \in ℤ$
45	39 40 42 44	etransclem10	$⊢ (φ \land c \in C (N)) \to if (P - 1 < c (0), 0, (\frac{(P - 1)!}{(P - 1 - c (0))!}) J^{P - 1 - c (0)}) \in ℤ$
46		fzfid	$⊢ (φ \land c \in C (N)) \to (1 \dots M) \in Fin$
47	39	adantr	$⊢ ((φ \land c \in C (N)) \land j \in (1 \dots M)) \to P \in ℕ$
48	42	adantr	$⊢ ((φ \land c \in C (N)) \land j \in (1 \dots M)) \to c : (0 \dots M) ⟶ (0 \dots N)$
49		0z	$⊢ 0 \in ℤ$
50		fzp1ss	$⊢ 0 \in ℤ \to (0 + 1 \dots M) \subseteq (0 \dots M)$
51	49 50	ax-mp	$⊢ (0 + 1 \dots M) \subseteq (0 \dots M)$
52	51	sseli	$⊢ j \in (0 + 1 \dots M) \to j \in (0 \dots M)$
53		1e0p1	$⊢ 1 = 0 + 1$
54	53	oveq1i	$⊢ (1 \dots M) = (0 + 1 \dots M)$
55	52 54	eleq2s	$⊢ j \in (1 \dots M) \to j \in (0 \dots M)$
56	55	adantl	$⊢ ((φ \land c \in C (N)) \land j \in (1 \dots M)) \to j \in (0 \dots M)$
57	44	adantr	$⊢ ((φ \land c \in C (N)) \land j \in (1 \dots M)) \to J \in ℤ$
58	47 48 56 57	etransclem3	$⊢ ((φ \land c \in C (N)) \land j \in (1 \dots M)) \to if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(J - j)}^{P - c (j)}) \in ℤ$
59	46 58	fprodzcl	$⊢ (φ \land c \in C (N)) \to \prod_{j = 1}^{M} if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(J - j)}^{P - c (j)}) \in ℤ$
60	45 59	zmulcld	$⊢ (φ \land c \in C (N)) \to if (P - 1 < c (0), 0, (\frac{(P - 1)!}{(P - 1 - c (0))!}) J^{P - 1 - c (0)}) \prod_{j = 1}^{M} if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(J - j)}^{P - c (j)}) \in ℤ$
61	38 60	zmulcld	$⊢ (φ \land c \in C (N)) \to (\frac{N!}{\prod_{j = 0}^{M} c (j)!}) if (P - 1 < c (0), 0, (\frac{(P - 1)!}{(P - 1 - c (0))!}) J^{P - 1 - c (0)}) \prod_{j = 1}^{M} if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(J - j)}^{P - c (j)}) \in ℤ$
62	6	adantr	$⊢ (φ \land c \in C (N)) \to N \in ℕ_{0}$
63		etransclem11	$⊢ (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = n\}) = (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\})$
64	8 63	eqtri	$⊢ C = (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\})$
65		simpr	$⊢ (φ \land c \in C (N)) \to c \in C (N)$
66	9	adantr	$⊢ (φ \land c \in C (N)) \to J \in (0 \dots M)$
67		fveq2	$⊢ j = k \to c (j) = c (k)$
68	67	fveq2d	$⊢ j = k \to c (j)! = c (k)!$
69	68	cbvprodv	$⊢ \prod_{j = 0}^{M} c (j)! = \prod_{k = 0}^{M} c (k)!$
70	69	oveq2i	$⊢ \frac{N!}{\prod_{j = 0}^{M} c (j)!} = \frac{N!}{\prod_{k = 0}^{M} c (k)!}$
71	67	breq2d	$⊢ j = k \to (P < c (j) \leftrightarrow P < c (k))$
72	67	oveq2d	$⊢ j = k \to P - c (j) = P - c (k)$
73	72	fveq2d	$⊢ j = k \to (P - c (j))! = (P - c (k))!$
74	73	oveq2d	$⊢ j = k \to \frac{P!}{(P - c (j))!} = \frac{P!}{(P - c (k))!}$
75		oveq2	$⊢ j = k \to J - j = J - k$
76	75 72	oveq12d	$⊢ j = k \to {(J - j)}^{P - c (j)} = {(J - k)}^{P - c (k)}$
77	74 76	oveq12d	$⊢ j = k \to (\frac{P!}{(P - c (j))!}) {(J - j)}^{P - c (j)} = (\frac{P!}{(P - c (k))!}) {(J - k)}^{P - c (k)}$
78	71 77	ifbieq2d	$⊢ j = k \to if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(J - j)}^{P - c (j)}) = if (P < c (k), 0, (\frac{P!}{(P - c (k))!}) {(J - k)}^{P - c (k)})$
79	78	cbvprodv	$⊢ \prod_{j = 1}^{M} if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(J - j)}^{P - c (j)}) = \prod_{k = 1}^{M} if (P < c (k), 0, (\frac{P!}{(P - c (k))!}) {(J - k)}^{P - c (k)})$
80	79	oveq2i	$⊢ if (P - 1 < c (0), 0, (\frac{(P - 1)!}{(P - 1 - c (0))!}) J^{P - 1 - c (0)}) \prod_{j = 1}^{M} if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(J - j)}^{P - c (j)}) = if (P - 1 < c (0), 0, (\frac{(P - 1)!}{(P - 1 - c (0))!}) J^{P - 1 - c (0)}) \prod_{k = 1}^{M} if (P < c (k), 0, (\frac{P!}{(P - c (k))!}) {(J - k)}^{P - c (k)})$
81	70 80	oveq12i	$⊢ (\frac{N!}{\prod_{j = 0}^{M} c (j)!}) if (P - 1 < c (0), 0, (\frac{(P - 1)!}{(P - 1 - c (0))!}) J^{P - 1 - c (0)}) \prod_{j = 1}^{M} if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(J - j)}^{P - c (j)}) = (\frac{N!}{\prod_{k = 0}^{M} c (k)!}) if (P - 1 < c (0), 0, (\frac{(P - 1)!}{(P - 1 - c (0))!}) J^{P - 1 - c (0)}) \prod_{k = 1}^{M} if (P < c (k), 0, (\frac{P!}{(P - c (k))!}) {(J - k)}^{P - c (k)})$
82	39 40 62 64 65 66 81	etransclem28	$⊢ (φ \land c \in C (N)) \to (P - 1)! ∥ (\frac{N!}{\prod_{j = 0}^{M} c (j)!}) if (P - 1 < c (0), 0, (\frac{(P - 1)!}{(P - 1 - c (0))!}) J^{P - 1 - c (0)}) \prod_{j = 1}^{M} if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(J - j)}^{P - c (j)})$
83	11 15 61 82	fsumdvds	$⊢ φ \to (P - 1)! ∥ \sum_{c \in C (N)} (\frac{N!}{\prod_{j = 0}^{M} c (j)!}) if (P - 1 < c (0), 0, (\frac{(P - 1)!}{(P - 1 - c (0))!}) J^{P - 1 - c (0)}) \prod_{j = 1}^{M} if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(J - j)}^{P - c (j)})$
84	1 2 3 4 5 6 7 8 10	etransclem31	$⊢ φ \to (S D^{n} F) (N) (J) = \sum_{c \in C (N)} (\frac{N!}{\prod_{j = 0}^{M} c (j)!}) if (P - 1 < c (0), 0, (\frac{(P - 1)!}{(P - 1 - c (0))!}) J^{P - 1 - c (0)}) \prod_{j = 1}^{M} if (P < c (j), 0, (\frac{P!}{(P - c (j))!}) {(J - j)}^{P - c (j)})$
85	83 84	breqtrrd	$⊢ φ \to (P - 1)! ∥ (S D^{n} F) (N) (J)$

Metamath Proof Explorer

Theorem etransclem37

Proof