etransclem32

Description: This is the proof for the last equation in the proof of the derivative calculated in Juillerat p. 12, just after equation *(6) . (Contributed by Glauco Siliprandi, 5-Apr-2020)

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

Proof

Step	Hyp	Ref	Expression
1		etransclem32.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
2		etransclem32.x	$⊢ φ \to X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
3		etransclem32.p	$⊢ φ \to P \in ℕ$
4		etransclem32.m	$⊢ φ \to M \in ℕ_{0}$
5		etransclem32.f	$⊢ F = (x \in X ⟼ x^{P - 1} \prod_{j = 1}^{M} {(x - j)}^{P})$
6		etransclem32.n	$⊢ φ \to N \in ℕ_{0}$
7		etransclem32.ngt	$⊢ φ \to M P + P - 1 < N$
8		etransclem32.h	$⊢ H = (j \in (0 \dots M) ⟼ (x \in X ⟼ {(x - j)}^{if (j = 0, P - 1, P)}))$
9		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\})$
10	1 2 3 4 5 6 8 9	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} H (j)) (c (j)) (x))$
11		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)$
12	9 6	etransclem12	$⊢ φ \to (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N) = \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}$
13	12	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) = \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}$
14	11 13	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 \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}$
15	14	adantlr	$⊢ ((φ \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 c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}$
16		nfv	$⊢ Ⅎ k (φ \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\})$
17		nfre1	$⊢ Ⅎ k \exists k \in (0 \dots M) if (k = 0, P - 1, P) < c (k)$
18	17	nfn	$⊢ Ⅎ k \neg \exists k \in (0 \dots M) if (k = 0, P - 1, P) < c (k)$
19	16 18	nfan	$⊢ Ⅎ k ((φ \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land \neg \exists k \in (0 \dots M) if (k = 0, P - 1, P) < c (k))$
20		fzssre	$⊢ (0 \dots N) \subseteq ℝ$
21		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)$
22	21	simplbi	$⊢ 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)})$
23		elmapi	$⊢ c \in ({(0 \dots N)}^{(0 \dots M)}) \to c : (0 \dots M) ⟶ (0 \dots N)$
24	22 23	syl	$⊢ c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\} \to c : (0 \dots M) ⟶ (0 \dots N)$
25	24	adantl	$⊢ (φ \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \to c : (0 \dots M) ⟶ (0 \dots N)$
26	25	ffvelcdmda	$⊢ ((φ \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land k \in (0 \dots M)) \to c (k) \in (0 \dots N)$
27	20 26	sselid	$⊢ ((φ \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land k \in (0 \dots M)) \to c (k) \in ℝ$
28	27	adantlr	$⊢ (((φ \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land \neg \exists k \in (0 \dots M) if (k = 0, P - 1, P) < c (k)) \land k \in (0 \dots M)) \to c (k) \in ℝ$
29		nnm1nn0	$⊢ P \in ℕ \to P - 1 \in ℕ_{0}$
30	3 29	syl	$⊢ φ \to P - 1 \in ℕ_{0}$
31	30	nn0red	$⊢ φ \to P - 1 \in ℝ$
32	3	nnred	$⊢ φ \to P \in ℝ$
33	31 32	ifcld	$⊢ φ \to if (k = 0, P - 1, P) \in ℝ$
34	33	ad3antrrr	$⊢ (((φ \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land \neg \exists k \in (0 \dots M) if (k = 0, P - 1, P) < c (k)) \land k \in (0 \dots M)) \to if (k = 0, P - 1, P) \in ℝ$
35		ralnex	$⊢ \forall k \in (0 \dots M) \neg if (k = 0, P - 1, P) < c (k) \leftrightarrow \neg \exists k \in (0 \dots M) if (k = 0, P - 1, P) < c (k)$
36	35	biimpri	$⊢ \neg \exists k \in (0 \dots M) if (k = 0, P - 1, P) < c (k) \to \forall k \in (0 \dots M) \neg if (k = 0, P - 1, P) < c (k)$
37	36	r19.21bi	$⊢ (\neg \exists k \in (0 \dots M) if (k = 0, P - 1, P) < c (k) \land k \in (0 \dots M)) \to \neg if (k = 0, P - 1, P) < c (k)$
38	37	adantll	$⊢ (((φ \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land \neg \exists k \in (0 \dots M) if (k = 0, P - 1, P) < c (k)) \land k \in (0 \dots M)) \to \neg if (k = 0, P - 1, P) < c (k)$
39	28 34 38	nltled	$⊢ (((φ \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land \neg \exists k \in (0 \dots M) if (k = 0, P - 1, P) < c (k)) \land k \in (0 \dots M)) \to c (k) \leq if (k = 0, P - 1, P)$
40	39	ex	$⊢ ((φ \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land \neg \exists k \in (0 \dots M) if (k = 0, P - 1, P) < c (k)) \to (k \in (0 \dots M) \to c (k) \leq if (k = 0, P - 1, P))$
41	19 40	ralrimi	$⊢ ((φ \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land \neg \exists k \in (0 \dots M) if (k = 0, P - 1, P) < c (k)) \to \forall k \in (0 \dots M) c (k) \leq if (k = 0, P - 1, P)$
42	21	simprbi	$⊢ 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$
43		fveq2	$⊢ j = k \to c (j) = c (k)$
44	43	cbvsumv	$⊢ \sum_{j = 0}^{M} c (j) = \sum_{k = 0}^{M} c (k)$
45	42 44	eqtr3di	$⊢ c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\} \to N = \sum_{k = 0}^{M} c (k)$
46	45	ad2antlr	$⊢ ((φ \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land \forall k \in (0 \dots M) c (k) \leq if (k = 0, P - 1, P)) \to N = \sum_{k = 0}^{M} c (k)$
47		fveq2	$⊢ k = h \to c (k) = c (h)$
48	47	cbvsumv	$⊢ \sum_{k = 0}^{M} c (k) = \sum_{h = 0}^{M} c (h)$
49		fzfid	$⊢ ((φ \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land \forall k \in (0 \dots M) c (k) \leq if (k = 0, P - 1, P)) \to (0 \dots M) \in Fin$
50	25	ffvelcdmda	$⊢ ((φ \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land h \in (0 \dots M)) \to c (h) \in (0 \dots N)$
51	20 50	sselid	$⊢ ((φ \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land h \in (0 \dots M)) \to c (h) \in ℝ$
52	51	adantlr	$⊢ (((φ \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land \forall k \in (0 \dots M) c (k) \leq if (k = 0, P - 1, P)) \land h \in (0 \dots M)) \to c (h) \in ℝ$
53	31 32	ifcld	$⊢ φ \to if (h = 0, P - 1, P) \in ℝ$
54	53	ad3antrrr	$⊢ (((φ \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land \forall k \in (0 \dots M) c (k) \leq if (k = 0, P - 1, P)) \land h \in (0 \dots M)) \to if (h = 0, P - 1, P) \in ℝ$
55		eqeq1	$⊢ k = h \to (k = 0 \leftrightarrow h = 0)$
56	55	ifbid	$⊢ k = h \to if (k = 0, P - 1, P) = if (h = 0, P - 1, P)$
57	47 56	breq12d	$⊢ k = h \to (c (k) \leq if (k = 0, P - 1, P) \leftrightarrow c (h) \leq if (h = 0, P - 1, P))$
58	57	rspccva	$⊢ (\forall k \in (0 \dots M) c (k) \leq if (k = 0, P - 1, P) \land h \in (0 \dots M)) \to c (h) \leq if (h = 0, P - 1, P)$
59	58	adantll	$⊢ (((φ \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land \forall k \in (0 \dots M) c (k) \leq if (k = 0, P - 1, P)) \land h \in (0 \dots M)) \to c (h) \leq if (h = 0, P - 1, P)$
60	49 52 54 59	fsumle	$⊢ ((φ \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land \forall k \in (0 \dots M) c (k) \leq if (k = 0, P - 1, P)) \to \sum_{h = 0}^{M} c (h) \leq \sum_{h = 0}^{M} if (h = 0, P - 1, P)$
61		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
62	4 61	eleqtrdi	$⊢ φ \to M \in ℤ_{\geq 0}$
63	3	nnnn0d	$⊢ φ \to P \in ℕ_{0}$
64	30 63	ifcld	$⊢ φ \to if (h = 0, P - 1, P) \in ℕ_{0}$
65	64	adantr	$⊢ (φ \land h \in (0 \dots M)) \to if (h = 0, P - 1, P) \in ℕ_{0}$
66	65	nn0cnd	$⊢ (φ \land h \in (0 \dots M)) \to if (h = 0, P - 1, P) \in ℂ$
67		iftrue	$⊢ h = 0 \to if (h = 0, P - 1, P) = P - 1$
68	62 66 67	fsum1p	$⊢ φ \to \sum_{h = 0}^{M} if (h = 0, P - 1, P) = P - 1 + \sum_{h = 0 + 1}^{M} if (h = 0, P - 1, P)$
69		0p1e1	$⊢ 0 + 1 = 1$
70	69	oveq1i	$⊢ (0 + 1 \dots M) = (1 \dots M)$
71	70	a1i	$⊢ φ \to (0 + 1 \dots M) = (1 \dots M)$
72	71	sumeq1d	$⊢ φ \to \sum_{h = 0 + 1}^{M} if (h = 0, P - 1, P) = \sum_{h = 1}^{M} if (h = 0, P - 1, P)$
73		0red	$⊢ h \in (1 \dots M) \to 0 \in ℝ$
74		1red	$⊢ h \in (1 \dots M) \to 1 \in ℝ$
75		elfzelz	$⊢ h \in (1 \dots M) \to h \in ℤ$
76	75	zred	$⊢ h \in (1 \dots M) \to h \in ℝ$
77		0lt1	$⊢ 0 < 1$
78	77	a1i	$⊢ h \in (1 \dots M) \to 0 < 1$
79		elfzle1	$⊢ h \in (1 \dots M) \to 1 \leq h$
80	73 74 76 78 79	ltletrd	$⊢ h \in (1 \dots M) \to 0 < h$
81	80	gt0ne0d	$⊢ h \in (1 \dots M) \to h \neq 0$
82	81	neneqd	$⊢ h \in (1 \dots M) \to \neg h = 0$
83	82	iffalsed	$⊢ h \in (1 \dots M) \to if (h = 0, P - 1, P) = P$
84	83	adantl	$⊢ (φ \land h \in (1 \dots M)) \to if (h = 0, P - 1, P) = P$
85	84	sumeq2dv	$⊢ φ \to \sum_{h = 1}^{M} if (h = 0, P - 1, P) = \sum_{h = 1}^{M} P$
86		fzfid	$⊢ φ \to (1 \dots M) \in Fin$
87	3	nncnd	$⊢ φ \to P \in ℂ$
88		fsumconst	$⊢ ((1 \dots M) \in Fin \land P \in ℂ) \to \sum_{h = 1}^{M} P = \|(1 \dots M)\| P$
89	86 87 88	syl2anc	$⊢ φ \to \sum_{h = 1}^{M} P = \|(1 \dots M)\| P$
90		hashfz1	$⊢ M \in ℕ_{0} \to \|(1 \dots M)\| = M$
91	4 90	syl	$⊢ φ \to \|(1 \dots M)\| = M$
92	91	oveq1d	$⊢ φ \to \|(1 \dots M)\| P = M P$
93	89 92	eqtrd	$⊢ φ \to \sum_{h = 1}^{M} P = M P$
94	72 85 93	3eqtrd	$⊢ φ \to \sum_{h = 0 + 1}^{M} if (h = 0, P - 1, P) = M P$
95	94	oveq2d	$⊢ φ \to P - 1 + \sum_{h = 0 + 1}^{M} if (h = 0, P - 1, P) = P - 1 + M P$
96	30	nn0cnd	$⊢ φ \to P - 1 \in ℂ$
97	4 63	nn0mulcld	$⊢ φ \to M P \in ℕ_{0}$
98	97	nn0cnd	$⊢ φ \to M P \in ℂ$
99	96 98	addcomd	$⊢ φ \to P - 1 + M P = M P + P - 1$
100	68 95 99	3eqtrd	$⊢ φ \to \sum_{h = 0}^{M} if (h = 0, P - 1, P) = M P + P - 1$
101	100	ad2antrr	$⊢ ((φ \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land \forall k \in (0 \dots M) c (k) \leq if (k = 0, P - 1, P)) \to \sum_{h = 0}^{M} if (h = 0, P - 1, P) = M P + P - 1$
102	60 101	breqtrd	$⊢ ((φ \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land \forall k \in (0 \dots M) c (k) \leq if (k = 0, P - 1, P)) \to \sum_{h = 0}^{M} c (h) \leq M P + P - 1$
103	48 102	eqbrtrid	$⊢ ((φ \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land \forall k \in (0 \dots M) c (k) \leq if (k = 0, P - 1, P)) \to \sum_{k = 0}^{M} c (k) \leq M P + P - 1$
104	46 103	eqbrtrd	$⊢ ((φ \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land \forall k \in (0 \dots M) c (k) \leq if (k = 0, P - 1, P)) \to N \leq M P + P - 1$
105	41 104	syldan	$⊢ ((φ \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land \neg \exists k \in (0 \dots M) if (k = 0, P - 1, P) < c (k)) \to N \leq M P + P - 1$
106	97 30	nn0addcld	$⊢ φ \to M P + P - 1 \in ℕ_{0}$
107	106	nn0red	$⊢ φ \to M P + P - 1 \in ℝ$
108	6	nn0red	$⊢ φ \to N \in ℝ$
109	107 108	ltnled	$⊢ φ \to (M P + P - 1 < N \leftrightarrow \neg N \leq M P + P - 1)$
110	7 109	mpbid	$⊢ φ \to \neg N \leq M P + P - 1$
111	110	ad2antrr	$⊢ ((φ \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land \neg \exists k \in (0 \dots M) if (k = 0, P - 1, P) < c (k)) \to \neg N \leq M P + P - 1$
112	105 111	condan	$⊢ (φ \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \to \exists k \in (0 \dots M) if (k = 0, P - 1, P) < c (k)$
113	112	adantlr	$⊢ ((φ \land x \in X) \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \to \exists k \in (0 \dots M) if (k = 0, P - 1, P) < c (k)$
114		nfv	$⊢ Ⅎ j (φ \land x \in X)$
115		nfcv	$⊢ \underline{Ⅎ} j (0 \dots M)$
116	115	nfsum1	$⊢ \underline{Ⅎ} j \sum_{j = 0}^{M} c (j)$
117	116	nfeq1	$⊢ Ⅎ j \sum_{j = 0}^{M} c (j) = N$
118		nfcv	$⊢ \underline{Ⅎ} j ({(0 \dots N)}^{(0 \dots M)})$
119	117 118	nfrabw	$⊢ \underline{Ⅎ} j \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}$
120	119	nfcri	$⊢ Ⅎ j c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}$
121	114 120	nfan	$⊢ Ⅎ j ((φ \land x \in X) \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\})$
122		nfv	$⊢ Ⅎ j k \in (0 \dots M)$
123		nfv	$⊢ Ⅎ j if (k = 0, P - 1, P) < c (k)$
124	121 122 123	nf3an	$⊢ Ⅎ j (((φ \land x \in X) \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land k \in (0 \dots M) \land if (k = 0, P - 1, P) < c (k))$
125		nfcv	$⊢ \underline{Ⅎ} j (S D^{n} H (k)) (c (k)) (x)$
126		fzfid	$⊢ (((φ \land x \in X) \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land k \in (0 \dots M) \land if (k = 0, P - 1, P) < c (k)) \to (0 \dots M) \in Fin$
127	1	ad3antrrr	$⊢ (((φ \land x \in X) \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land j \in (0 \dots M)) \to S \in \{ℝ, ℂ\}$
128	2	ad3antrrr	$⊢ (((φ \land x \in X) \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land j \in (0 \dots M)) \to X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
129	3	ad3antrrr	$⊢ (((φ \land x \in X) \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land j \in (0 \dots M)) \to P \in ℕ$
130		etransclem5	$⊢ (j \in (0 \dots M) ⟼ (x \in X ⟼ {(x - j)}^{if (j = 0, P - 1, P)})) = (k \in (0 \dots M) ⟼ (y \in X ⟼ {(y - k)}^{if (k = 0, P - 1, P)}))$
131	8 130	eqtri	$⊢ H = (k \in (0 \dots M) ⟼ (y \in X ⟼ {(y - k)}^{if (k = 0, P - 1, P)}))$
132		simpr	$⊢ (((φ \land x \in X) \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land j \in (0 \dots M)) \to j \in (0 \dots M)$
133	24	ad2antlr	$⊢ ((φ \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land j \in (0 \dots M)) \to c : (0 \dots M) ⟶ (0 \dots N)$
134		simpr	$⊢ ((φ \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land j \in (0 \dots M)) \to j \in (0 \dots M)$
135	133 134	ffvelcdmd	$⊢ ((φ \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land j \in (0 \dots M)) \to c (j) \in (0 \dots N)$
136	135	adantllr	$⊢ (((φ \land x \in X) \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land j \in (0 \dots M)) \to c (j) \in (0 \dots N)$
137		elfznn0	$⊢ c (j) \in (0 \dots N) \to c (j) \in ℕ_{0}$
138	136 137	syl	$⊢ (((φ \land x \in X) \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land j \in (0 \dots M)) \to c (j) \in ℕ_{0}$
139	127 128 129 131 132 138	etransclem20	$⊢ (((φ \land x \in X) \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land j \in (0 \dots M)) \to (S D^{n} H (j)) (c (j)) : X ⟶ ℂ$
140		simpllr	$⊢ (((φ \land x \in X) \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land j \in (0 \dots M)) \to x \in X$
141	139 140	ffvelcdmd	$⊢ (((φ \land x \in X) \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land j \in (0 \dots M)) \to (S D^{n} H (j)) (c (j)) (x) \in ℂ$
142	141	3ad2antl1	$⊢ ((((φ \land x \in X) \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land k \in (0 \dots M) \land if (k = 0, P - 1, P) < c (k)) \land j \in (0 \dots M)) \to (S D^{n} H (j)) (c (j)) (x) \in ℂ$
143		fveq2	$⊢ j = k \to H (j) = H (k)$
144	143	oveq2d	$⊢ j = k \to S D^{n} H (j) = S D^{n} H (k)$
145	144 43	fveq12d	$⊢ j = k \to (S D^{n} H (j)) (c (j)) = (S D^{n} H (k)) (c (k))$
146	145	fveq1d	$⊢ j = k \to (S D^{n} H (j)) (c (j)) (x) = (S D^{n} H (k)) (c (k)) (x)$
147		simp2	$⊢ (((φ \land x \in X) \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land k \in (0 \dots M) \land if (k = 0, P - 1, P) < c (k)) \to k \in (0 \dots M)$
148	1	ad2antrr	$⊢ ((φ \land x \in X) \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \to S \in \{ℝ, ℂ\}$
149	148	3ad2ant1	$⊢ (((φ \land x \in X) \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land k \in (0 \dots M) \land if (k = 0, P - 1, P) < c (k)) \to S \in \{ℝ, ℂ\}$
150	2	ad2antrr	$⊢ ((φ \land x \in X) \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \to X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
151	150	3ad2ant1	$⊢ (((φ \land x \in X) \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land k \in (0 \dots M) \land if (k = 0, P - 1, P) < c (k)) \to X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
152	3	ad2antrr	$⊢ ((φ \land x \in X) \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \to P \in ℕ$
153	152	3ad2ant1	$⊢ (((φ \land x \in X) \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land k \in (0 \dots M) \land if (k = 0, P - 1, P) < c (k)) \to P \in ℕ$
154		etransclem5	$⊢ (j \in (0 \dots M) ⟼ (x \in X ⟼ {(x - j)}^{if (j = 0, P - 1, P)})) = (h \in (0 \dots M) ⟼ (y \in X ⟼ {(y - h)}^{if (h = 0, P - 1, P)}))$
155	8 154	eqtri	$⊢ H = (h \in (0 \dots M) ⟼ (y \in X ⟼ {(y - h)}^{if (h = 0, P - 1, P)}))$
156	26	elfzelzd	$⊢ ((φ \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land k \in (0 \dots M)) \to c (k) \in ℤ$
157	156	adantllr	$⊢ (((φ \land x \in X) \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land k \in (0 \dots M)) \to c (k) \in ℤ$
158	157	3adant3	$⊢ (((φ \land x \in X) \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land k \in (0 \dots M) \land if (k = 0, P - 1, P) < c (k)) \to c (k) \in ℤ$
159		simp3	$⊢ (((φ \land x \in X) \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land k \in (0 \dots M) \land if (k = 0, P - 1, P) < c (k)) \to if (k = 0, P - 1, P) < c (k)$
160	149 151 153 155 147 158 159	etransclem19	$⊢ (((φ \land x \in X) \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land k \in (0 \dots M) \land if (k = 0, P - 1, P) < c (k)) \to (S D^{n} H (k)) (c (k)) = (y \in X ⟼ 0)$
161		eqidd	$⊢ ((((φ \land x \in X) \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land k \in (0 \dots M) \land if (k = 0, P - 1, P) < c (k)) \land y = x) \to 0 = 0$
162		simp1lr	$⊢ (((φ \land x \in X) \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land k \in (0 \dots M) \land if (k = 0, P - 1, P) < c (k)) \to x \in X$
163		0red	$⊢ (((φ \land x \in X) \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land k \in (0 \dots M) \land if (k = 0, P - 1, P) < c (k)) \to 0 \in ℝ$
164	160 161 162 163	fvmptd	$⊢ (((φ \land x \in X) \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land k \in (0 \dots M) \land if (k = 0, P - 1, P) < c (k)) \to (S D^{n} H (k)) (c (k)) (x) = 0$
165	124 125 126 142 146 147 164	fprod0	$⊢ (((φ \land x \in X) \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \land k \in (0 \dots M) \land if (k = 0, P - 1, P) < c (k)) \to \prod_{j = 0}^{M} (S D^{n} H (j)) (c (j)) (x) = 0$
166	165	rexlimdv3a	$⊢ ((φ \land x \in X) \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \to (\exists k \in (0 \dots M) if (k = 0, P - 1, P) < c (k) \to \prod_{j = 0}^{M} (S D^{n} H (j)) (c (j)) (x) = 0)$
167	113 166	mpd	$⊢ ((φ \land x \in X) \land c \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}) \to \prod_{j = 0}^{M} (S D^{n} H (j)) (c (j)) (x) = 0$
168	15 167	syldan	$⊢ ((φ \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} H (j)) (c (j)) (x) = 0$
169	168	oveq2d	$⊢ ((φ \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} H (j)) (c (j)) (x) = (\frac{N!}{\prod_{j = 0}^{M} c (j)!}) \cdot 0$
170	6	faccld	$⊢ φ \to N! \in ℕ$
171	170	nncnd	$⊢ φ \to N! \in ℂ$
172	171	adantr	$⊢ (φ \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 ℂ$
173		fzfid	$⊢ (φ \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$
174		simpll	$⊢ ((φ \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 φ$
175	14	adantr	$⊢ ((φ \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 \in \{c \in ({(0 \dots N)}^{(0 \dots M)}) \| \sum_{j = 0}^{M} c (j) = N\}$
176		simpr	$⊢ ((φ \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)$
177	174 175 176 135	syl21anc	$⊢ ((φ \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)$
178	177 137	syl	$⊢ ((φ \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}$
179	178	faccld	$⊢ ((φ \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 ℕ$
180	179	nncnd	$⊢ ((φ \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 ℂ$
181	173 180	fprodcl	$⊢ (φ \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 ℂ$
182	179	nnne0d	$⊢ ((φ \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$
183	173 180 182	fprodn0	$⊢ (φ \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$
184	172 181 183	divcld	$⊢ (φ \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 ℂ$
185	184	mul01d	$⊢ (φ \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)!}) \cdot 0 = 0$
186	185	adantlr	$⊢ ((φ \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)!}) \cdot 0 = 0$
187	169 186	eqtrd	$⊢ ((φ \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} H (j)) (c (j)) (x) = 0$
188	187	sumeq2dv	$⊢ (φ \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} H (j)) (c (j)) (x) = \sum_{c \in (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N)} 0$
189		eqid	$⊢ (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\})$
190	189 6	etransclem16	$⊢ φ \to (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N) \in Fin$
191	190	olcd	$⊢ φ \to ((m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N) \subseteq ℤ_{\geq A} \lor (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N) \in Fin)$
192	191	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) \subseteq ℤ_{\geq A} \lor (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N) \in Fin)$
193		sumz	$⊢ ((m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N) \subseteq ℤ_{\geq A} \lor (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N) \in Fin) \to \sum_{c \in (m \in ℕ_{0} ⟼ \{d \in ({(0 \dots m)}^{(0 \dots M)}) \| \sum_{k = 0}^{M} d (k) = m\}) (N)} 0 = 0$
194	192 193	syl	$⊢ (φ \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)} 0 = 0$
195	188 194	eqtrd	$⊢ (φ \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} H (j)) (c (j)) (x) = 0$
196	195	mpteq2dva	$⊢ φ \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} H (j)) (c (j)) (x)) = (x \in X ⟼ 0)$
197	10 196	eqtrd	$⊢ φ \to (S D^{n} F) (N) = (x \in X ⟼ 0)$

Metamath Proof Explorer

Theorem etransclem32

Proof