etransclem38

Description: P divides the I -th derivative of F applied to J . if it is not the case that I = P - 1 and J = 0 . This is case 1 and the second part of case 2 proven in in Juillerat p. 13 . (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	etransclem38.p	$⊢ φ \to P \in ℕ$
	etransclem38.m	$⊢ φ \to M \in ℕ_{0}$
	etransclem38.f	$⊢ F = (x \in ℝ ⟼ x^{P - 1} \prod_{j = 1}^{M} {(x - j)}^{P})$
	etransclem38.i	$⊢ φ \to I \in ℕ_{0}$
	etransclem38.j	$⊢ φ \to J \in (0 \dots M)$
	etransclem38.ij	$⊢ φ \to \neg (I = P - 1 \land J = 0)$
	etransclem38.c	$⊢ C = (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = n\})$
Assertion	etransclem38	$⊢ φ \to P ∥ (\frac{(ℝ D^{n} F) (I) (J)}{(P - 1)!})$

Proof

Step	Hyp	Ref	Expression
1		etransclem38.p	$⊢ φ \to P \in ℕ$
2		etransclem38.m	$⊢ φ \to M \in ℕ_{0}$
3		etransclem38.f	$⊢ F = (x \in ℝ ⟼ x^{P - 1} \prod_{j = 1}^{M} {(x - j)}^{P})$
4		etransclem38.i	$⊢ φ \to I \in ℕ_{0}$
5		etransclem38.j	$⊢ φ \to J \in (0 \dots M)$
6		etransclem38.ij	$⊢ φ \to \neg (I = P - 1 \land J = 0)$
7		etransclem38.c	$⊢ C = (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = n\})$
8	7 4	etransclem16	$⊢ φ \to C (I) \in Fin$
9	1	nnzd	$⊢ φ \to P \in ℤ$
10	1	adantr	$⊢ (φ \land c \in C (I)) \to P \in ℕ$
11	2	adantr	$⊢ (φ \land c \in C (I)) \to M \in ℕ_{0}$
12	4	adantr	$⊢ (φ \land c \in C (I)) \to I \in ℕ_{0}$
13		etransclem11	$⊢ (n \in ℕ_{0} ⟼ \{c \in ({(0 \dots n)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = n\}) = (m \in ℕ_{0} ⟼ \{e \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} e (k) = m\})$
14		etransclem11	$⊢ (m \in ℕ_{0} ⟼ \{e \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} e (k) = m\}) = (n \in ℕ_{0} ⟼ \{d \in ({(0 \dots n)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} d (j) = n\})$
15	7 13 14	3eqtri	$⊢ C = (n \in ℕ_{0} ⟼ \{d \in ({(0 \dots n)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} d (j) = n\})$
16		simpr	$⊢ (φ \land c \in C (I)) \to c \in C (I)$
17	5	adantr	$⊢ (φ \land c \in C (I)) \to J \in (0 \dots M)$
18		eqid	$⊢ (\frac{I!}{\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{I!}{\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)})$
19	10 11 12 15 16 17 18	etransclem28	$⊢ (φ \land c \in C (I)) \to (P - 1)! ∥ (\frac{I!}{\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)})$
20		nnm1nn0	$⊢ P \in ℕ \to P - 1 \in ℕ_{0}$
21	1 20	syl	$⊢ φ \to P - 1 \in ℕ_{0}$
22	21	faccld	$⊢ φ \to (P - 1)! \in ℕ$
23	22	nnzd	$⊢ φ \to (P - 1)! \in ℤ$
24	23	adantr	$⊢ (φ \land c \in C (I)) \to (P - 1)! \in ℤ$
25	22	nnne0d	$⊢ φ \to (P - 1)! \neq 0$
26	25	adantr	$⊢ (φ \land c \in C (I)) \to (P - 1)! \neq 0$
27	5	elfzelzd	$⊢ φ \to J \in ℤ$
28	27	adantr	$⊢ (φ \land c \in C (I)) \to J \in ℤ$
29	10 11 12 28 15 16	etransclem26	$⊢ (φ \land c \in C (I)) \to (\frac{I!}{\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 ℤ$
30		dvdsval2	$⊢ ((P - 1)! \in ℤ \land (P - 1)! \neq 0 \land (\frac{I!}{\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 ℤ) \to ((P - 1)! ∥ (\frac{I!}{\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)}) \leftrightarrow \frac{(\frac{I!}{\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)})}{(P - 1)!} \in ℤ)$
31	24 26 29 30	syl3anc	$⊢ (φ \land c \in C (I)) \to ((P - 1)! ∥ (\frac{I!}{\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)}) \leftrightarrow \frac{(\frac{I!}{\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)})}{(P - 1)!} \in ℤ)$
32	19 31	mpbid	$⊢ (φ \land c \in C (I)) \to \frac{(\frac{I!}{\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)})}{(P - 1)!} \in ℤ$
33		pm3.22	$⊢ (J = 0 \land I = P - 1) \to (I = P - 1 \land J = 0)$
34	33	adantll	$⊢ (((φ \land c \in C (I)) \land J = 0) \land I = P - 1) \to (I = P - 1 \land J = 0)$
35	6	ad3antrrr	$⊢ (((φ \land c \in C (I)) \land J = 0) \land I = P - 1) \to \neg (I = P - 1 \land J = 0)$
36	34 35	pm2.65da	$⊢ ((φ \land c \in C (I)) \land J = 0) \to \neg I = P - 1$
37	36	neqned	$⊢ ((φ \land c \in C (I)) \land J = 0) \to I \neq P - 1$
38	1	ad3antrrr	$⊢ (((φ \land c \in C (I)) \land J = 0) \land I \neq P - 1) \to P \in ℕ$
39	2	ad3antrrr	$⊢ (((φ \land c \in C (I)) \land J = 0) \land I \neq P - 1) \to M \in ℕ_{0}$
40	4	ad3antrrr	$⊢ (((φ \land c \in C (I)) \land J = 0) \land I \neq P - 1) \to I \in ℕ_{0}$
41		simpr	$⊢ (((φ \land c \in C (I)) \land J = 0) \land I \neq P - 1) \to I \neq P - 1$
42		simplr	$⊢ (((φ \land c \in C (I)) \land J = 0) \land I \neq P - 1) \to J = 0$
43	16	ad2antrr	$⊢ (((φ \land c \in C (I)) \land J = 0) \land I \neq P - 1) \to c \in C (I)$
44	38 39 40 41 42 15 43	etransclem24	$⊢ (((φ \land c \in C (I)) \land J = 0) \land I \neq P - 1) \to P ∥ (\frac{(\frac{I!}{\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)})}{(P - 1)!})$
45	37 44	mpdan	$⊢ ((φ \land c \in C (I)) \land J = 0) \to P ∥ (\frac{(\frac{I!}{\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)})}{(P - 1)!})$
46	1	ad2antrr	$⊢ ((φ \land c \in C (I)) \land \neg J = 0) \to P \in ℕ$
47	2	ad2antrr	$⊢ ((φ \land c \in C (I)) \land \neg J = 0) \to M \in ℕ_{0}$
48	4	ad2antrr	$⊢ ((φ \land c \in C (I)) \land \neg J = 0) \to I \in ℕ_{0}$
49	7 4	etransclem12	$⊢ φ \to C (I) = \{c \in ({(0 \dots I)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = I\}$
50	49	adantr	$⊢ (φ \land c \in C (I)) \to C (I) = \{c \in ({(0 \dots I)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = I\}$
51	16 50	eleqtrd	$⊢ (φ \land c \in C (I)) \to c \in \{c \in ({(0 \dots I)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = I\}$
52		rabid	$⊢ c \in \{c \in ({(0 \dots I)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = I\} \leftrightarrow (c \in ({(0 \dots I)}^{(0 \dots M)}) \land \sum_{j = 0}^{M} c (j) = I)$
53	51 52	sylib	$⊢ (φ \land c \in C (I)) \to (c \in ({(0 \dots I)}^{(0 \dots M)}) \land \sum_{j = 0}^{M} c (j) = I)$
54	53	simpld	$⊢ (φ \land c \in C (I)) \to c \in ({(0 \dots I)}^{(0 \dots M)})$
55		elmapi	$⊢ c \in ({(0 \dots I)}^{(0 \dots M)}) \to c : (0 \dots M) ⟶ (0 \dots I)$
56	54 55	syl	$⊢ (φ \land c \in C (I)) \to c : (0 \dots M) ⟶ (0 \dots I)$
57	56	adantr	$⊢ ((φ \land c \in C (I)) \land \neg J = 0) \to c : (0 \dots M) ⟶ (0 \dots I)$
58	53	simprd	$⊢ (φ \land c \in C (I)) \to \sum_{j = 0}^{M} c (j) = I$
59	58	adantr	$⊢ ((φ \land c \in C (I)) \land \neg J = 0) \to \sum_{j = 0}^{M} c (j) = I$
60		1zzd	$⊢ (φ \land \neg J = 0) \to 1 \in ℤ$
61	2	nn0zd	$⊢ φ \to M \in ℤ$
62	61	adantr	$⊢ (φ \land \neg J = 0) \to M \in ℤ$
63	27	adantr	$⊢ (φ \land \neg J = 0) \to J \in ℤ$
64		elfznn0	$⊢ J \in (0 \dots M) \to J \in ℕ_{0}$
65	5 64	syl	$⊢ φ \to J \in ℕ_{0}$
66		neqne	$⊢ \neg J = 0 \to J \neq 0$
67	65 66	anim12i	$⊢ (φ \land \neg J = 0) \to (J \in ℕ_{0} \land J \neq 0)$
68		elnnne0	$⊢ J \in ℕ \leftrightarrow (J \in ℕ_{0} \land J \neq 0)$
69	67 68	sylibr	$⊢ (φ \land \neg J = 0) \to J \in ℕ$
70	69	nnge1d	$⊢ (φ \land \neg J = 0) \to 1 \leq J$
71		elfzle2	$⊢ J \in (0 \dots M) \to J \leq M$
72	5 71	syl	$⊢ φ \to J \leq M$
73	72	adantr	$⊢ (φ \land \neg J = 0) \to J \leq M$
74	60 62 63 70 73	elfzd	$⊢ (φ \land \neg J = 0) \to J \in (1 \dots M)$
75	74	adantlr	$⊢ ((φ \land c \in C (I)) \land \neg J = 0) \to J \in (1 \dots M)$
76	46 47 48 57 59 18 75	etransclem25	$⊢ ((φ \land c \in C (I)) \land \neg J = 0) \to P! ∥ (\frac{I!}{\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)})$
77	1	nncnd	$⊢ φ \to P \in ℂ$
78		1cnd	$⊢ φ \to 1 \in ℂ$
79	77 78	npcand	$⊢ φ \to P - 1 + 1 = P$
80	79	eqcomd	$⊢ φ \to P = P - 1 + 1$
81	80	fveq2d	$⊢ φ \to P! = (P - 1 + 1)!$
82		facp1	$⊢ P - 1 \in ℕ_{0} \to (P - 1 + 1)! = (P - 1)! (P - 1 + 1)$
83	21 82	syl	$⊢ φ \to (P - 1 + 1)! = (P - 1)! (P - 1 + 1)$
84	79	oveq2d	$⊢ φ \to (P - 1)! (P - 1 + 1) = (P - 1)! P$
85	22	nncnd	$⊢ φ \to (P - 1)! \in ℂ$
86	85 77	mulcomd	$⊢ φ \to (P - 1)! P = P (P - 1)!$
87	84 86	eqtrd	$⊢ φ \to (P - 1)! (P - 1 + 1) = P (P - 1)!$
88	81 83 87	3eqtrrd	$⊢ φ \to P (P - 1)! = P!$
89	88	ad2antrr	$⊢ ((φ \land c \in C (I)) \land \neg J = 0) \to P (P - 1)! = P!$
90	29	zcnd	$⊢ (φ \land c \in C (I)) \to (\frac{I!}{\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 ℂ$
91	85	adantr	$⊢ (φ \land c \in C (I)) \to (P - 1)! \in ℂ$
92	90 91 26	divcan1d	$⊢ (φ \land c \in C (I)) \to (\frac{(\frac{I!}{\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)})}{(P - 1)!}) (P - 1)! = (\frac{I!}{\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)})$
93	92	adantr	$⊢ ((φ \land c \in C (I)) \land \neg J = 0) \to (\frac{(\frac{I!}{\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)})}{(P - 1)!}) (P - 1)! = (\frac{I!}{\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)})$
94	76 89 93	3brtr4d	$⊢ ((φ \land c \in C (I)) \land \neg J = 0) \to P (P - 1)! ∥ (\frac{(\frac{I!}{\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)})}{(P - 1)!}) (P - 1)!$
95	9	ad2antrr	$⊢ ((φ \land c \in C (I)) \land \neg J = 0) \to P \in ℤ$
96	32	adantr	$⊢ ((φ \land c \in C (I)) \land \neg J = 0) \to \frac{(\frac{I!}{\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)})}{(P - 1)!} \in ℤ$
97	23	ad2antrr	$⊢ ((φ \land c \in C (I)) \land \neg J = 0) \to (P - 1)! \in ℤ$
98	25	ad2antrr	$⊢ ((φ \land c \in C (I)) \land \neg J = 0) \to (P - 1)! \neq 0$
99		dvdsmulcr	$⊢ (P \in ℤ \land \frac{(\frac{I!}{\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)})}{(P - 1)!} \in ℤ \land ((P - 1)! \in ℤ \land (P - 1)! \neq 0)) \to (P (P - 1)! ∥ (\frac{(\frac{I!}{\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)})}{(P - 1)!}) (P - 1)! \leftrightarrow P ∥ (\frac{(\frac{I!}{\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)})}{(P - 1)!}))$
100	95 96 97 98 99	syl112anc	$⊢ ((φ \land c \in C (I)) \land \neg J = 0) \to (P (P - 1)! ∥ (\frac{(\frac{I!}{\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)})}{(P - 1)!}) (P - 1)! \leftrightarrow P ∥ (\frac{(\frac{I!}{\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)})}{(P - 1)!}))$
101	94 100	mpbid	$⊢ ((φ \land c \in C (I)) \land \neg J = 0) \to P ∥ (\frac{(\frac{I!}{\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)})}{(P - 1)!})$
102	45 101	pm2.61dan	$⊢ (φ \land c \in C (I)) \to P ∥ (\frac{(\frac{I!}{\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)})}{(P - 1)!})$
103	8 9 32 102	fsumdvds	$⊢ φ \to P ∥ \sum_{c \in C (I)} (\frac{(\frac{I!}{\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)})}{(P - 1)!})$
104		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
105	104	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
106		reopn	$⊢ ℝ \in topGen (ran (.))$
107		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
108	107	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
109	106 108	eleqtri	$⊢ ℝ \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
110	109	a1i	$⊢ φ \to ℝ \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
111		etransclem5	$⊢ (k \in (0 \dots M) ⟼ (y \in ℝ ⟼ {(y - k)}^{if (k = 0, P - 1, P)})) = (j \in (0 \dots M) ⟼ (x \in ℝ ⟼ {(x - j)}^{if (j = 0, P - 1, P)}))$
112		fzssre	$⊢ (0 \dots M) \subseteq ℝ$
113	112 5	sselid	$⊢ φ \to J \in ℝ$
114	105 110 1 2 3 4 111 7 113	etransclem31	$⊢ φ \to (ℝ D^{n} F) (I) (J) = \sum_{c \in C (I)} (\frac{I!}{\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)})$
115	114	oveq1d	$⊢ φ \to \frac{(ℝ D^{n} F) (I) (J)}{(P - 1)!} = \frac{\sum_{c \in C (I)} (\frac{I!}{\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)})}{(P - 1)!}$
116	8 85 90 25	fsumdivc	$⊢ φ \to \frac{\sum_{c \in C (I)} (\frac{I!}{\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)})}{(P - 1)!} = \sum_{c \in C (I)} (\frac{(\frac{I!}{\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)})}{(P - 1)!})$
117	115 116	eqtrd	$⊢ φ \to \frac{(ℝ D^{n} F) (I) (J)}{(P - 1)!} = \sum_{c \in C (I)} (\frac{(\frac{I!}{\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)})}{(P - 1)!})$
118	103 117	breqtrrd	$⊢ φ \to P ∥ (\frac{(ℝ D^{n} F) (I) (J)}{(P - 1)!})$

Metamath Proof Explorer

Theorem etransclem38

Proof