dvnxpaek

Description: The n -th derivative of the polynomial (x+A)^K. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	dvnxpaek.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
	dvnxpaek.x	$⊢ φ \to X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
	dvnxpaek.a	$⊢ φ \to A \in ℂ$
	dvnxpaek.k	$⊢ φ \to K \in ℕ_{0}$
	dvnxpaek.f	$⊢ F = (x \in X ⟼ {(x + A)}^{K})$
Assertion	dvnxpaek	$⊢ (φ \land N \in ℕ_{0}) \to (S D^{n} F) (N) = (x \in X ⟼ if (K < N, 0, (\frac{K!}{(K - N)!}) {(x + A)}^{K - N}))$

Proof

Step	Hyp	Ref	Expression
1		dvnxpaek.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
2		dvnxpaek.x	$⊢ φ \to X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
3		dvnxpaek.a	$⊢ φ \to A \in ℂ$
4		dvnxpaek.k	$⊢ φ \to K \in ℕ_{0}$
5		dvnxpaek.f	$⊢ F = (x \in X ⟼ {(x + A)}^{K})$
6		fveq2	$⊢ n = 0 \to (S D^{n} F) (n) = (S D^{n} F) (0)$
7		breq2	$⊢ n = 0 \to (K < n \leftrightarrow K < 0)$
8		eqidd	$⊢ n = 0 \to 0 = 0$
9		oveq2	$⊢ n = 0 \to K - n = K - 0$
10	9	fveq2d	$⊢ n = 0 \to (K - n)! = (K - 0)!$
11	10	oveq2d	$⊢ n = 0 \to \frac{K!}{(K - n)!} = \frac{K!}{(K - 0)!}$
12	9	oveq2d	$⊢ n = 0 \to {(x + A)}^{K - n} = {(x + A)}^{K - 0}$
13	11 12	oveq12d	$⊢ n = 0 \to (\frac{K!}{(K - n)!}) {(x + A)}^{K - n} = (\frac{K!}{(K - 0)!}) {(x + A)}^{K - 0}$
14	7 8 13	ifbieq12d	$⊢ n = 0 \to if (K < n, 0, (\frac{K!}{(K - n)!}) {(x + A)}^{K - n}) = if (K < 0, 0, (\frac{K!}{(K - 0)!}) {(x + A)}^{K - 0})$
15	14	mpteq2dv	$⊢ n = 0 \to (x \in X ⟼ if (K < n, 0, (\frac{K!}{(K - n)!}) {(x + A)}^{K - n})) = (x \in X ⟼ if (K < 0, 0, (\frac{K!}{(K - 0)!}) {(x + A)}^{K - 0}))$
16	6 15	eqeq12d	$⊢ n = 0 \to ((S D^{n} F) (n) = (x \in X ⟼ if (K < n, 0, (\frac{K!}{(K - n)!}) {(x + A)}^{K - n})) \leftrightarrow (S D^{n} F) (0) = (x \in X ⟼ if (K < 0, 0, (\frac{K!}{(K - 0)!}) {(x + A)}^{K - 0})))$
17		fveq2	$⊢ n = m \to (S D^{n} F) (n) = (S D^{n} F) (m)$
18		breq2	$⊢ n = m \to (K < n \leftrightarrow K < m)$
19		eqidd	$⊢ n = m \to 0 = 0$
20		oveq2	$⊢ n = m \to K - n = K - m$
21	20	fveq2d	$⊢ n = m \to (K - n)! = (K - m)!$
22	21	oveq2d	$⊢ n = m \to \frac{K!}{(K - n)!} = \frac{K!}{(K - m)!}$
23	20	oveq2d	$⊢ n = m \to {(x + A)}^{K - n} = {(x + A)}^{K - m}$
24	22 23	oveq12d	$⊢ n = m \to (\frac{K!}{(K - n)!}) {(x + A)}^{K - n} = (\frac{K!}{(K - m)!}) {(x + A)}^{K - m}$
25	18 19 24	ifbieq12d	$⊢ n = m \to if (K < n, 0, (\frac{K!}{(K - n)!}) {(x + A)}^{K - n}) = if (K < m, 0, (\frac{K!}{(K - m)!}) {(x + A)}^{K - m})$
26	25	mpteq2dv	$⊢ n = m \to (x \in X ⟼ if (K < n, 0, (\frac{K!}{(K - n)!}) {(x + A)}^{K - n})) = (x \in X ⟼ if (K < m, 0, (\frac{K!}{(K - m)!}) {(x + A)}^{K - m}))$
27	17 26	eqeq12d	$⊢ n = m \to ((S D^{n} F) (n) = (x \in X ⟼ if (K < n, 0, (\frac{K!}{(K - n)!}) {(x + A)}^{K - n})) \leftrightarrow (S D^{n} F) (m) = (x \in X ⟼ if (K < m, 0, (\frac{K!}{(K - m)!}) {(x + A)}^{K - m})))$
28		fveq2	$⊢ n = m + 1 \to (S D^{n} F) (n) = (S D^{n} F) (m + 1)$
29		breq2	$⊢ n = m + 1 \to (K < n \leftrightarrow K < m + 1)$
30		eqidd	$⊢ n = m + 1 \to 0 = 0$
31		oveq2	$⊢ n = m + 1 \to K - n = K - (m + 1)$
32	31	fveq2d	$⊢ n = m + 1 \to (K - n)! = (K - (m + 1))!$
33	32	oveq2d	$⊢ n = m + 1 \to \frac{K!}{(K - n)!} = \frac{K!}{(K - (m + 1))!}$
34	31	oveq2d	$⊢ n = m + 1 \to {(x + A)}^{K - n} = {(x + A)}^{K - (m + 1)}$
35	33 34	oveq12d	$⊢ n = m + 1 \to (\frac{K!}{(K - n)!}) {(x + A)}^{K - n} = (\frac{K!}{(K - (m + 1))!}) {(x + A)}^{K - (m + 1)}$
36	29 30 35	ifbieq12d	$⊢ n = m + 1 \to if (K < n, 0, (\frac{K!}{(K - n)!}) {(x + A)}^{K - n}) = if (K < m + 1, 0, (\frac{K!}{(K - (m + 1))!}) {(x + A)}^{K - (m + 1)})$
37	36	mpteq2dv	$⊢ n = m + 1 \to (x \in X ⟼ if (K < n, 0, (\frac{K!}{(K - n)!}) {(x + A)}^{K - n})) = (x \in X ⟼ if (K < m + 1, 0, (\frac{K!}{(K - (m + 1))!}) {(x + A)}^{K - (m + 1)}))$
38	28 37	eqeq12d	$⊢ n = m + 1 \to ((S D^{n} F) (n) = (x \in X ⟼ if (K < n, 0, (\frac{K!}{(K - n)!}) {(x + A)}^{K - n})) \leftrightarrow (S D^{n} F) (m + 1) = (x \in X ⟼ if (K < m + 1, 0, (\frac{K!}{(K - (m + 1))!}) {(x + A)}^{K - (m + 1)})))$
39		fveq2	$⊢ n = N \to (S D^{n} F) (n) = (S D^{n} F) (N)$
40		breq2	$⊢ n = N \to (K < n \leftrightarrow K < N)$
41		eqidd	$⊢ n = N \to 0 = 0$
42		oveq2	$⊢ n = N \to K - n = K - N$
43	42	fveq2d	$⊢ n = N \to (K - n)! = (K - N)!$
44	43	oveq2d	$⊢ n = N \to \frac{K!}{(K - n)!} = \frac{K!}{(K - N)!}$
45	42	oveq2d	$⊢ n = N \to {(x + A)}^{K - n} = {(x + A)}^{K - N}$
46	44 45	oveq12d	$⊢ n = N \to (\frac{K!}{(K - n)!}) {(x + A)}^{K - n} = (\frac{K!}{(K - N)!}) {(x + A)}^{K - N}$
47	40 41 46	ifbieq12d	$⊢ n = N \to if (K < n, 0, (\frac{K!}{(K - n)!}) {(x + A)}^{K - n}) = if (K < N, 0, (\frac{K!}{(K - N)!}) {(x + A)}^{K - N})$
48	47	mpteq2dv	$⊢ n = N \to (x \in X ⟼ if (K < n, 0, (\frac{K!}{(K - n)!}) {(x + A)}^{K - n})) = (x \in X ⟼ if (K < N, 0, (\frac{K!}{(K - N)!}) {(x + A)}^{K - N}))$
49	39 48	eqeq12d	$⊢ n = N \to ((S D^{n} F) (n) = (x \in X ⟼ if (K < n, 0, (\frac{K!}{(K - n)!}) {(x + A)}^{K - n})) \leftrightarrow (S D^{n} F) (N) = (x \in X ⟼ if (K < N, 0, (\frac{K!}{(K - N)!}) {(x + A)}^{K - N})))$
50		recnprss	$⊢ S \in \{ℝ, ℂ\} \to S \subseteq ℂ$
51	1 50	syl	$⊢ φ \to S \subseteq ℂ$
52		cnex	$⊢ ℂ \in V$
53	52	a1i	$⊢ φ \to ℂ \in V$
54		restsspw	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} S \subseteq 𝒫 S$
55		id	$⊢ X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S) \to X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
56	54 55	sseldi	$⊢ X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S) \to X \in 𝒫 S$
57		elpwi	$⊢ X \in 𝒫 S \to X \subseteq S$
58	56 57	syl	$⊢ X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S) \to X \subseteq S$
59	2 58	syl	$⊢ φ \to X \subseteq S$
60	59 51	sstrd	$⊢ φ \to X \subseteq ℂ$
61	60	adantr	$⊢ (φ \land x \in X) \to X \subseteq ℂ$
62		simpr	$⊢ (φ \land x \in X) \to x \in X$
63	61 62	sseldd	$⊢ (φ \land x \in X) \to x \in ℂ$
64	3	adantr	$⊢ (φ \land x \in X) \to A \in ℂ$
65	63 64	addcld	$⊢ (φ \land x \in X) \to x + A \in ℂ$
66	4	adantr	$⊢ (φ \land x \in X) \to K \in ℕ_{0}$
67	65 66	expcld	$⊢ (φ \land x \in X) \to {(x + A)}^{K} \in ℂ$
68	67 5	fmptd	$⊢ φ \to F : X ⟶ ℂ$
69		elpm2r	$⊢ ((ℂ \in V \land S \in \{ℝ, ℂ\}) \land (F : X ⟶ ℂ \land X \subseteq S)) \to F \in (ℂ ↑_{𝑝𝑚} S)$
70	53 1 68 59 69	syl22anc	$⊢ φ \to F \in (ℂ ↑_{𝑝𝑚} S)$
71		dvn0	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S)) \to (S D^{n} F) (0) = F$
72	51 70 71	syl2anc	$⊢ φ \to (S D^{n} F) (0) = F$
73	5	a1i	$⊢ φ \to F = (x \in X ⟼ {(x + A)}^{K})$
74	4	nn0ge0d	$⊢ φ \to 0 \leq K$
75		0red	$⊢ φ \to 0 \in ℝ$
76	4	nn0red	$⊢ φ \to K \in ℝ$
77	75 76	lenltd	$⊢ φ \to (0 \leq K \leftrightarrow \neg K < 0)$
78	74 77	mpbid	$⊢ φ \to \neg K < 0$
79	78	iffalsed	$⊢ φ \to if (K < 0, 0, (\frac{K!}{(K - 0)!}) {(x + A)}^{K - 0}) = (\frac{K!}{(K - 0)!}) {(x + A)}^{K - 0}$
80	79	adantr	$⊢ (φ \land x \in X) \to if (K < 0, 0, (\frac{K!}{(K - 0)!}) {(x + A)}^{K - 0}) = (\frac{K!}{(K - 0)!}) {(x + A)}^{K - 0}$
81	4	nn0cnd	$⊢ φ \to K \in ℂ$
82	81	subid1d	$⊢ φ \to K - 0 = K$
83	82	fveq2d	$⊢ φ \to (K - 0)! = K!$
84	83	oveq2d	$⊢ φ \to \frac{K!}{(K - 0)!} = \frac{K!}{K!}$
85		faccl	$⊢ K \in ℕ_{0} \to K! \in ℕ$
86	4 85	syl	$⊢ φ \to K! \in ℕ$
87	86	nncnd	$⊢ φ \to K! \in ℂ$
88	86	nnne0d	$⊢ φ \to K! \neq 0$
89	87 88	dividd	$⊢ φ \to \frac{K!}{K!} = 1$
90	84 89	eqtrd	$⊢ φ \to \frac{K!}{(K - 0)!} = 1$
91	82	oveq2d	$⊢ φ \to {(x + A)}^{K - 0} = {(x + A)}^{K}$
92	90 91	oveq12d	$⊢ φ \to (\frac{K!}{(K - 0)!}) {(x + A)}^{K - 0} = 1 {(x + A)}^{K}$
93	92	adantr	$⊢ (φ \land x \in X) \to (\frac{K!}{(K - 0)!}) {(x + A)}^{K - 0} = 1 {(x + A)}^{K}$
94	67	mulid2d	$⊢ (φ \land x \in X) \to 1 {(x + A)}^{K} = {(x + A)}^{K}$
95	80 93 94	3eqtrrd	$⊢ (φ \land x \in X) \to {(x + A)}^{K} = if (K < 0, 0, (\frac{K!}{(K - 0)!}) {(x + A)}^{K - 0})$
96	95	mpteq2dva	$⊢ φ \to (x \in X ⟼ {(x + A)}^{K}) = (x \in X ⟼ if (K < 0, 0, (\frac{K!}{(K - 0)!}) {(x + A)}^{K - 0}))$
97	72 73 96	3eqtrd	$⊢ φ \to (S D^{n} F) (0) = (x \in X ⟼ if (K < 0, 0, (\frac{K!}{(K - 0)!}) {(x + A)}^{K - 0}))$
98	51	adantr	$⊢ (φ \land m \in ℕ_{0}) \to S \subseteq ℂ$
99	70	adantr	$⊢ (φ \land m \in ℕ_{0}) \to F \in (ℂ ↑_{𝑝𝑚} S)$
100		simpr	$⊢ (φ \land m \in ℕ_{0}) \to m \in ℕ_{0}$
101		dvnp1	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S) \land m \in ℕ_{0}) \to (S D^{n} F) (m + 1) = S D (S D^{n} F) (m)$
102	98 99 100 101	syl3anc	$⊢ (φ \land m \in ℕ_{0}) \to (S D^{n} F) (m + 1) = S D (S D^{n} F) (m)$
103	102	adantr	$⊢ ((φ \land m \in ℕ_{0}) \land (S D^{n} F) (m) = (x \in X ⟼ if (K < m, 0, (\frac{K!}{(K - m)!}) {(x + A)}^{K - m}))) \to (S D^{n} F) (m + 1) = S D (S D^{n} F) (m)$
104		oveq2	$⊢ (S D^{n} F) (m) = (x \in X ⟼ if (K < m, 0, (\frac{K!}{(K - m)!}) {(x + A)}^{K - m})) \to S D (S D^{n} F) (m) = \frac{d (x \in X⟼ if (K < m, 0, (\frac{K!}{(K - m)!}) {(x + A)}^{K - m}))}{d_{S} x}$
105	104	adantl	$⊢ ((φ \land m \in ℕ_{0}) \land (S D^{n} F) (m) = (x \in X ⟼ if (K < m, 0, (\frac{K!}{(K - m)!}) {(x + A)}^{K - m}))) \to S D (S D^{n} F) (m) = \frac{d (x \in X⟼ if (K < m, 0, (\frac{K!}{(K - m)!}) {(x + A)}^{K - m}))}{d_{S} x}$
106		iftrue	$⊢ K < m \to if (K < m, 0, (\frac{K!}{(K - m)!}) {(x + A)}^{K - m}) = 0$
107	106	mpteq2dv	$⊢ K < m \to (x \in X ⟼ if (K < m, 0, (\frac{K!}{(K - m)!}) {(x + A)}^{K - m})) = (x \in X ⟼ 0)$
108	107	oveq2d	$⊢ K < m \to \frac{d (x \in X⟼ if (K < m, 0, (\frac{K!}{(K - m)!}) {(x + A)}^{K - m}))}{d_{S} x} = \frac{d (x \in X⟼ 0)}{d_{S} x}$
109	108	adantl	$⊢ ((φ \land m \in ℕ_{0}) \land K < m) \to \frac{d (x \in X⟼ if (K < m, 0, (\frac{K!}{(K - m)!}) {(x + A)}^{K - m}))}{d_{S} x} = \frac{d (x \in X⟼ 0)}{d_{S} x}$
110		0cnd	$⊢ φ \to 0 \in ℂ$
111	1 2 110	dvmptconst	$⊢ φ \to \frac{d (x \in X⟼ 0)}{d_{S} x} = (x \in X ⟼ 0)$
112	111	ad2antrr	$⊢ ((φ \land m \in ℕ_{0}) \land K < m) \to \frac{d (x \in X⟼ 0)}{d_{S} x} = (x \in X ⟼ 0)$
113	76	ad2antrr	$⊢ ((φ \land m \in ℕ_{0}) \land K < m) \to K \in ℝ$
114		nn0re	$⊢ m \in ℕ_{0} \to m \in ℝ$
115	114	ad2antlr	$⊢ ((φ \land m \in ℕ_{0}) \land K < m) \to m \in ℝ$
116		simpr	$⊢ ((φ \land m \in ℕ_{0}) \land K < m) \to K < m$
117	113 115 116	ltled	$⊢ ((φ \land m \in ℕ_{0}) \land K < m) \to K \leq m$
118	4	nn0zd	$⊢ φ \to K \in ℤ$
119	118	adantr	$⊢ (φ \land m \in ℕ_{0}) \to K \in ℤ$
120	100	nn0zd	$⊢ (φ \land m \in ℕ_{0}) \to m \in ℤ$
121		zleltp1	$⊢ (K \in ℤ \land m \in ℤ) \to (K \leq m \leftrightarrow K < m + 1)$
122	119 120 121	syl2anc	$⊢ (φ \land m \in ℕ_{0}) \to (K \leq m \leftrightarrow K < m + 1)$
123	122	adantr	$⊢ ((φ \land m \in ℕ_{0}) \land K < m) \to (K \leq m \leftrightarrow K < m + 1)$
124	117 123	mpbid	$⊢ ((φ \land m \in ℕ_{0}) \land K < m) \to K < m + 1$
125	124	iftrued	$⊢ ((φ \land m \in ℕ_{0}) \land K < m) \to if (K < m + 1, 0, (\frac{K!}{(K - (m + 1))!}) {(x + A)}^{K - (m + 1)}) = 0$
126	125	mpteq2dv	$⊢ ((φ \land m \in ℕ_{0}) \land K < m) \to (x \in X ⟼ if (K < m + 1, 0, (\frac{K!}{(K - (m + 1))!}) {(x + A)}^{K - (m + 1)})) = (x \in X ⟼ 0)$
127	126	eqcomd	$⊢ ((φ \land m \in ℕ_{0}) \land K < m) \to (x \in X ⟼ 0) = (x \in X ⟼ if (K < m + 1, 0, (\frac{K!}{(K - (m + 1))!}) {(x + A)}^{K - (m + 1)}))$
128	109 112 127	3eqtrd	$⊢ ((φ \land m \in ℕ_{0}) \land K < m) \to \frac{d (x \in X⟼ if (K < m, 0, (\frac{K!}{(K - m)!}) {(x + A)}^{K - m}))}{d_{S} x} = (x \in X ⟼ if (K < m + 1, 0, (\frac{K!}{(K - (m + 1))!}) {(x + A)}^{K - (m + 1)}))$
129		simpl	$⊢ ((φ \land m \in ℕ_{0}) \land \neg K < m) \to (φ \land m \in ℕ_{0})$
130		simpr	$⊢ ((φ \land m \in ℕ_{0}) \land \neg K < m) \to \neg K < m$
131	129 100 114	3syl	$⊢ ((φ \land m \in ℕ_{0}) \land \neg K < m) \to m \in ℝ$
132	76	ad2antrr	$⊢ ((φ \land m \in ℕ_{0}) \land \neg K < m) \to K \in ℝ$
133	131 132	lenltd	$⊢ ((φ \land m \in ℕ_{0}) \land \neg K < m) \to (m \leq K \leftrightarrow \neg K < m)$
134	130 133	mpbird	$⊢ ((φ \land m \in ℕ_{0}) \land \neg K < m) \to m \leq K$
135		simpr	$⊢ ((φ \land m \in ℕ_{0}) \land m = K) \to m = K$
136	114	ad2antlr	$⊢ ((φ \land m \in ℕ_{0}) \land m = K) \to m \in ℝ$
137	76	ad2antrr	$⊢ ((φ \land m \in ℕ_{0}) \land m = K) \to K \in ℝ$
138	136 137	lttri3d	$⊢ ((φ \land m \in ℕ_{0}) \land m = K) \to (m = K \leftrightarrow (\neg m < K \land \neg K < m))$
139	135 138	mpbid	$⊢ ((φ \land m \in ℕ_{0}) \land m = K) \to (\neg m < K \land \neg K < m)$
140		simpr	$⊢ (\neg m < K \land \neg K < m) \to \neg K < m$
141	139 140	syl	$⊢ ((φ \land m \in ℕ_{0}) \land m = K) \to \neg K < m$
142	141	iffalsed	$⊢ ((φ \land m \in ℕ_{0}) \land m = K) \to if (K < m, 0, (\frac{K!}{(K - m)!}) {(x + A)}^{K - m}) = (\frac{K!}{(K - m)!}) {(x + A)}^{K - m}$
143	142	mpteq2dv	$⊢ ((φ \land m \in ℕ_{0}) \land m = K) \to (x \in X ⟼ if (K < m, 0, (\frac{K!}{(K - m)!}) {(x + A)}^{K - m})) = (x \in X ⟼ (\frac{K!}{(K - m)!}) {(x + A)}^{K - m})$
144	143	oveq2d	$⊢ ((φ \land m \in ℕ_{0}) \land m = K) \to \frac{d (x \in X⟼ if (K < m, 0, (\frac{K!}{(K - m)!}) {(x + A)}^{K - m}))}{d_{S} x} = \frac{d (x \in X⟼ (\frac{K!}{(K - m)!}) {(x + A)}^{K - m})}{d_{S} x}$
145		oveq2	$⊢ m = K \to K - m = K - K$
146	145	fveq2d	$⊢ m = K \to (K - m)! = (K - K)!$
147	146	adantl	$⊢ (φ \land m = K) \to (K - m)! = (K - K)!$
148	81	subidd	$⊢ φ \to K - K = 0$
149	148	fveq2d	$⊢ φ \to (K - K)! = 0!$
150		fac0	$⊢ 0! = 1$
151	150	a1i	$⊢ φ \to 0! = 1$
152	149 151	eqtrd	$⊢ φ \to (K - K)! = 1$
153	152	adantr	$⊢ (φ \land m = K) \to (K - K)! = 1$
154	147 153	eqtrd	$⊢ (φ \land m = K) \to (K - m)! = 1$
155	154	oveq2d	$⊢ (φ \land m = K) \to \frac{K!}{(K - m)!} = \frac{K!}{1}$
156	87	div1d	$⊢ φ \to \frac{K!}{1} = K!$
157	156	adantr	$⊢ (φ \land m = K) \to \frac{K!}{1} = K!$
158	155 157	eqtrd	$⊢ (φ \land m = K) \to \frac{K!}{(K - m)!} = K!$
159	158	adantr	$⊢ ((φ \land m = K) \land x \in X) \to \frac{K!}{(K - m)!} = K!$
160	145	adantl	$⊢ (φ \land m = K) \to K - m = K - K$
161	148	adantr	$⊢ (φ \land m = K) \to K - K = 0$
162	160 161	eqtrd	$⊢ (φ \land m = K) \to K - m = 0$
163	162	oveq2d	$⊢ (φ \land m = K) \to {(x + A)}^{K - m} = {(x + A)}^{0}$
164	163	adantr	$⊢ ((φ \land m = K) \land x \in X) \to {(x + A)}^{K - m} = {(x + A)}^{0}$
165	65	exp0d	$⊢ (φ \land x \in X) \to {(x + A)}^{0} = 1$
166	165	adantlr	$⊢ ((φ \land m = K) \land x \in X) \to {(x + A)}^{0} = 1$
167	164 166	eqtrd	$⊢ ((φ \land m = K) \land x \in X) \to {(x + A)}^{K - m} = 1$
168	159 167	oveq12d	$⊢ ((φ \land m = K) \land x \in X) \to (\frac{K!}{(K - m)!}) {(x + A)}^{K - m} = K! \cdot 1$
169	87	mulid1d	$⊢ φ \to K! \cdot 1 = K!$
170	169	ad2antrr	$⊢ ((φ \land m = K) \land x \in X) \to K! \cdot 1 = K!$
171	168 170	eqtrd	$⊢ ((φ \land m = K) \land x \in X) \to (\frac{K!}{(K - m)!}) {(x + A)}^{K - m} = K!$
172	171	mpteq2dva	$⊢ (φ \land m = K) \to (x \in X ⟼ (\frac{K!}{(K - m)!}) {(x + A)}^{K - m}) = (x \in X ⟼ K!)$
173	172	oveq2d	$⊢ (φ \land m = K) \to \frac{d (x \in X⟼ (\frac{K!}{(K - m)!}) {(x + A)}^{K - m})}{d_{S} x} = \frac{d (x \in X⟼ K!)}{d_{S} x}$
174	1 2 87	dvmptconst	$⊢ φ \to \frac{d (x \in X⟼ K!)}{d_{S} x} = (x \in X ⟼ 0)$
175	174	adantr	$⊢ (φ \land m = K) \to \frac{d (x \in X⟼ K!)}{d_{S} x} = (x \in X ⟼ 0)$
176	173 175	eqtrd	$⊢ (φ \land m = K) \to \frac{d (x \in X⟼ (\frac{K!}{(K - m)!}) {(x + A)}^{K - m})}{d_{S} x} = (x \in X ⟼ 0)$
177	176	adantlr	$⊢ ((φ \land m \in ℕ_{0}) \land m = K) \to \frac{d (x \in X⟼ (\frac{K!}{(K - m)!}) {(x + A)}^{K - m})}{d_{S} x} = (x \in X ⟼ 0)$
178	137	ltp1d	$⊢ ((φ \land m \in ℕ_{0}) \land m = K) \to K < K + 1$
179		oveq1	$⊢ m = K \to m + 1 = K + 1$
180	179	eqcomd	$⊢ m = K \to K + 1 = m + 1$
181	180	adantl	$⊢ ((φ \land m \in ℕ_{0}) \land m = K) \to K + 1 = m + 1$
182	178 181	breqtrd	$⊢ ((φ \land m \in ℕ_{0}) \land m = K) \to K < m + 1$
183	182	iftrued	$⊢ ((φ \land m \in ℕ_{0}) \land m = K) \to if (K < m + 1, 0, (\frac{K!}{(K - (m + 1))!}) {(x + A)}^{K - (m + 1)}) = 0$
184	183	eqcomd	$⊢ ((φ \land m \in ℕ_{0}) \land m = K) \to 0 = if (K < m + 1, 0, (\frac{K!}{(K - (m + 1))!}) {(x + A)}^{K - (m + 1)})$
185	184	mpteq2dv	$⊢ ((φ \land m \in ℕ_{0}) \land m = K) \to (x \in X ⟼ 0) = (x \in X ⟼ if (K < m + 1, 0, (\frac{K!}{(K - (m + 1))!}) {(x + A)}^{K - (m + 1)}))$
186	144 177 185	3eqtrd	$⊢ ((φ \land m \in ℕ_{0}) \land m = K) \to \frac{d (x \in X⟼ if (K < m, 0, (\frac{K!}{(K - m)!}) {(x + A)}^{K - m}))}{d_{S} x} = (x \in X ⟼ if (K < m + 1, 0, (\frac{K!}{(K - (m + 1))!}) {(x + A)}^{K - (m + 1)}))$
187	186	adantlr	$⊢ (((φ \land m \in ℕ_{0}) \land m \leq K) \land m = K) \to \frac{d (x \in X⟼ if (K < m, 0, (\frac{K!}{(K - m)!}) {(x + A)}^{K - m}))}{d_{S} x} = (x \in X ⟼ if (K < m + 1, 0, (\frac{K!}{(K - (m + 1))!}) {(x + A)}^{K - (m + 1)}))$
188		simpll	$⊢ (((φ \land m \in ℕ_{0}) \land m \leq K) \land \neg m = K) \to (φ \land m \in ℕ_{0})$
189	188 100 114	3syl	$⊢ (((φ \land m \in ℕ_{0}) \land m \leq K) \land \neg m = K) \to m \in ℝ$
190	76	ad3antrrr	$⊢ (((φ \land m \in ℕ_{0}) \land m \leq K) \land \neg m = K) \to K \in ℝ$
191		simplr	$⊢ (((φ \land m \in ℕ_{0}) \land m \leq K) \land \neg m = K) \to m \leq K$
192		neqne	$⊢ \neg m = K \to m \neq K$
193	192	necomd	$⊢ \neg m = K \to K \neq m$
194	193	adantl	$⊢ (((φ \land m \in ℕ_{0}) \land m \leq K) \land \neg m = K) \to K \neq m$
195	189 190 191 194	leneltd	$⊢ (((φ \land m \in ℕ_{0}) \land m \leq K) \land \neg m = K) \to m < K$
196	114	ad2antlr	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to m \in ℝ$
197	76	ad2antrr	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to K \in ℝ$
198		simpr	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to m < K$
199	196 197 198	ltled	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to m \leq K$
200	196 197	lenltd	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to (m \leq K \leftrightarrow \neg K < m)$
201	199 200	mpbid	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to \neg K < m$
202	201	iffalsed	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to if (K < m, 0, (\frac{K!}{(K - m)!}) {(x + A)}^{K - m}) = (\frac{K!}{(K - m)!}) {(x + A)}^{K - m}$
203	202	mpteq2dv	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to (x \in X ⟼ if (K < m, 0, (\frac{K!}{(K - m)!}) {(x + A)}^{K - m})) = (x \in X ⟼ (\frac{K!}{(K - m)!}) {(x + A)}^{K - m})$
204	203	oveq2d	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to \frac{d (x \in X⟼ if (K < m, 0, (\frac{K!}{(K - m)!}) {(x + A)}^{K - m}))}{d_{S} x} = \frac{d (x \in X⟼ (\frac{K!}{(K - m)!}) {(x + A)}^{K - m})}{d_{S} x}$
205	1	adantr	$⊢ (φ \land m \in ℕ_{0}) \to S \in \{ℝ, ℂ\}$
206	205	adantr	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to S \in \{ℝ, ℂ\}$
207	87	ad2antrr	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to K! \in ℂ$
208	100	adantr	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to m \in ℕ_{0}$
209	4	ad2antrr	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to K \in ℕ_{0}$
210		nn0sub	$⊢ (m \in ℕ_{0} \land K \in ℕ_{0}) \to (m \leq K \leftrightarrow K - m \in ℕ_{0})$
211	208 209 210	syl2anc	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to (m \leq K \leftrightarrow K - m \in ℕ_{0})$
212	199 211	mpbid	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to K - m \in ℕ_{0}$
213		faccl	$⊢ K - m \in ℕ_{0} \to (K - m)! \in ℕ$
214	212 213	syl	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to (K - m)! \in ℕ$
215	214	nncnd	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to (K - m)! \in ℂ$
216	214	nnne0d	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to (K - m)! \neq 0$
217	207 215 216	divcld	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to \frac{K!}{(K - m)!} \in ℂ$
218	217	adantr	$⊢ (((φ \land m \in ℕ_{0}) \land m < K) \land x \in X) \to \frac{K!}{(K - m)!} \in ℂ$
219	75	ad3antrrr	$⊢ (((φ \land m \in ℕ_{0}) \land m < K) \land x \in X) \to 0 \in ℝ$
220	2	adantr	$⊢ (φ \land m \in ℕ_{0}) \to X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
221	220	adantr	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
222	206 221 217	dvmptconst	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to \frac{d (x \in X⟼ \frac{K!}{(K - m)!})}{d_{S} x} = (x \in X ⟼ 0)$
223	65	adantlr	$⊢ ((φ \land m \in ℕ_{0}) \land x \in X) \to x + A \in ℂ$
224	223	adantlr	$⊢ (((φ \land m \in ℕ_{0}) \land m < K) \land x \in X) \to x + A \in ℂ$
225	212	adantr	$⊢ (((φ \land m \in ℕ_{0}) \land m < K) \land x \in X) \to K - m \in ℕ_{0}$
226	224 225	expcld	$⊢ (((φ \land m \in ℕ_{0}) \land m < K) \land x \in X) \to {(x + A)}^{K - m} \in ℂ$
227	225	nn0cnd	$⊢ (((φ \land m \in ℕ_{0}) \land m < K) \land x \in X) \to K - m \in ℂ$
228	212	nn0zd	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to K - m \in ℤ$
229	196 197	posdifd	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to (m < K \leftrightarrow 0 < K - m)$
230	198 229	mpbid	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to 0 < K - m$
231	228 230	jca	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to (K - m \in ℤ \land 0 < K - m)$
232		elnnz	$⊢ K - m \in ℕ \leftrightarrow (K - m \in ℤ \land 0 < K - m)$
233	231 232	sylibr	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to K - m \in ℕ$
234		nnm1nn0	$⊢ K - m \in ℕ \to K - m - 1 \in ℕ_{0}$
235	233 234	syl	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to K - m - 1 \in ℕ_{0}$
236	235	adantr	$⊢ (((φ \land m \in ℕ_{0}) \land m < K) \land x \in X) \to K - m - 1 \in ℕ_{0}$
237	224 236	expcld	$⊢ (((φ \land m \in ℕ_{0}) \land m < K) \land x \in X) \to {(x + A)}^{K - m - 1} \in ℂ$
238	227 237	mulcld	$⊢ (((φ \land m \in ℕ_{0}) \land m < K) \land x \in X) \to (K - m) {(x + A)}^{K - m - 1} \in ℂ$
239	3	ad2antrr	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to A \in ℂ$
240	206 221 239 233	dvxpaek	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to \frac{d (x \in X⟼ {(x + A)}^{K - m})}{d_{S} x} = (x \in X ⟼ (K - m) {(x + A)}^{K - m - 1})$
241	206 218 219 222 226 238 240	dvmptmul	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to \frac{d (x \in X⟼ (\frac{K!}{(K - m)!}) {(x + A)}^{K - m})}{d_{S} x} = (x \in X ⟼ 0 \cdot {(x + A)}^{K - m} + (K - m) {(x + A)}^{K - m - 1} (\frac{K!}{(K - m)!}))$
242	226	mul02d	$⊢ (((φ \land m \in ℕ_{0}) \land m < K) \land x \in X) \to 0 \cdot {(x + A)}^{K - m} = 0$
243	242	oveq1d	$⊢ (((φ \land m \in ℕ_{0}) \land m < K) \land x \in X) \to 0 \cdot {(x + A)}^{K - m} + (K - m) {(x + A)}^{K - m - 1} (\frac{K!}{(K - m)!}) = 0 + (K - m) {(x + A)}^{K - m - 1} (\frac{K!}{(K - m)!})$
244	238 218	mulcld	$⊢ (((φ \land m \in ℕ_{0}) \land m < K) \land x \in X) \to (K - m) {(x + A)}^{K - m - 1} (\frac{K!}{(K - m)!}) \in ℂ$
245	244	addid2d	$⊢ (((φ \land m \in ℕ_{0}) \land m < K) \land x \in X) \to 0 + (K - m) {(x + A)}^{K - m - 1} (\frac{K!}{(K - m)!}) = (K - m) {(x + A)}^{K - m - 1} (\frac{K!}{(K - m)!})$
246	120	adantr	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to m \in ℤ$
247	119	adantr	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to K \in ℤ$
248		zltp1le	$⊢ (m \in ℤ \land K \in ℤ) \to (m < K \leftrightarrow m + 1 \leq K)$
249	246 247 248	syl2anc	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to (m < K \leftrightarrow m + 1 \leq K)$
250	198 249	mpbid	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to m + 1 \leq K$
251		peano2re	$⊢ m \in ℝ \to m + 1 \in ℝ$
252	196 251	syl	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to m + 1 \in ℝ$
253	252 197	lenltd	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to (m + 1 \leq K \leftrightarrow \neg K < m + 1)$
254	250 253	mpbid	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to \neg K < m + 1$
255	254	adantr	$⊢ (((φ \land m \in ℕ_{0}) \land m < K) \land x \in X) \to \neg K < m + 1$
256	255	iffalsed	$⊢ (((φ \land m \in ℕ_{0}) \land m < K) \land x \in X) \to if (K < m + 1, 0, (\frac{K!}{(K - (m + 1))!}) {(x + A)}^{K - (m + 1)}) = (\frac{K!}{(K - (m + 1))!}) {(x + A)}^{K - (m + 1)}$
257	218 227 237	mulassd	$⊢ (((φ \land m \in ℕ_{0}) \land m < K) \land x \in X) \to (\frac{K!}{(K - m)!}) (K - m) {(x + A)}^{K - m - 1} = (\frac{K!}{(K - m)!}) (K - m) {(x + A)}^{K - m - 1}$
258	257	eqcomd	$⊢ (((φ \land m \in ℕ_{0}) \land m < K) \land x \in X) \to (\frac{K!}{(K - m)!}) (K - m) {(x + A)}^{K - m - 1} = (\frac{K!}{(K - m)!}) (K - m) {(x + A)}^{K - m - 1}$
259	233	nncnd	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to K - m \in ℂ$
260	207 215 259 216	div32d	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to (\frac{K!}{(K - m)!}) (K - m) = K! (\frac{K - m}{(K - m)!})$
261		facnn2	$⊢ K - m \in ℕ \to (K - m)! = (K - m - 1)! (K - m)$
262	233 261	syl	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to (K - m)! = (K - m - 1)! (K - m)$
263	262	oveq2d	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to \frac{K - m}{(K - m)!} = \frac{K - m}{(K - m - 1)! (K - m)}$
264		faccl	$⊢ K - m - 1 \in ℕ_{0} \to (K - m - 1)! \in ℕ$
265	234 264	syl	$⊢ K - m \in ℕ \to (K - m - 1)! \in ℕ$
266	265	nncnd	$⊢ K - m \in ℕ \to (K - m - 1)! \in ℂ$
267	233 266	syl	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to (K - m - 1)! \in ℂ$
268	235 264	syl	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to (K - m - 1)! \in ℕ$
269		nnne0	$⊢ (K - m - 1)! \in ℕ \to (K - m - 1)! \neq 0$
270	268 269	syl	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to (K - m - 1)! \neq 0$
271		nnne0	$⊢ K - m \in ℕ \to K - m \neq 0$
272	233 271	syl	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to K - m \neq 0$
273	267 259 270 272	divcan8d	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to \frac{K - m}{(K - m - 1)! (K - m)} = \frac{1}{(K - m - 1)!}$
274	263 273	eqtrd	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to \frac{K - m}{(K - m)!} = \frac{1}{(K - m - 1)!}$
275	274	oveq2d	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to K! (\frac{K - m}{(K - m)!}) = K! (\frac{1}{(K - m - 1)!})$
276		eqidd	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to K! (\frac{1}{(K - m - 1)!}) = K! (\frac{1}{(K - m - 1)!})$
277	260 275 276	3eqtrd	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to (\frac{K!}{(K - m)!}) (K - m) = K! (\frac{1}{(K - m - 1)!})$
278	277	adantr	$⊢ (((φ \land m \in ℕ_{0}) \land m < K) \land x \in X) \to (\frac{K!}{(K - m)!}) (K - m) = K! (\frac{1}{(K - m - 1)!})$
279	81	adantr	$⊢ (φ \land m \in ℕ_{0}) \to K \in ℂ$
280	100	nn0cnd	$⊢ (φ \land m \in ℕ_{0}) \to m \in ℂ$
281		1cnd	$⊢ (φ \land m \in ℕ_{0}) \to 1 \in ℂ$
282	279 280 281	subsub4d	$⊢ (φ \land m \in ℕ_{0}) \to K - m - 1 = K - (m + 1)$
283	282	oveq2d	$⊢ (φ \land m \in ℕ_{0}) \to {(x + A)}^{K - m - 1} = {(x + A)}^{K - (m + 1)}$
284	283	ad2antrr	$⊢ (((φ \land m \in ℕ_{0}) \land m < K) \land x \in X) \to {(x + A)}^{K - m - 1} = {(x + A)}^{K - (m + 1)}$
285	278 284	oveq12d	$⊢ (((φ \land m \in ℕ_{0}) \land m < K) \land x \in X) \to (\frac{K!}{(K - m)!}) (K - m) {(x + A)}^{K - m - 1} = K! (\frac{1}{(K - m - 1)!}) {(x + A)}^{K - (m + 1)}$
286	282	adantr	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to K - m - 1 = K - (m + 1)$
287	286	eqcomd	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to K - (m + 1) = K - m - 1$
288	287	fveq2d	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to (K - (m + 1))! = (K - m - 1)!$
289	288	oveq2d	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to \frac{K!}{(K - (m + 1))!} = \frac{K!}{(K - m - 1)!}$
290	207 267 270	divrecd	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to \frac{K!}{(K - m - 1)!} = K! (\frac{1}{(K - m - 1)!})$
291	289 290	eqtr2d	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to K! (\frac{1}{(K - m - 1)!}) = \frac{K!}{(K - (m + 1))!}$
292	291	adantr	$⊢ (((φ \land m \in ℕ_{0}) \land m < K) \land x \in X) \to K! (\frac{1}{(K - m - 1)!}) = \frac{K!}{(K - (m + 1))!}$
293	292	oveq1d	$⊢ (((φ \land m \in ℕ_{0}) \land m < K) \land x \in X) \to K! (\frac{1}{(K - m - 1)!}) {(x + A)}^{K - (m + 1)} = (\frac{K!}{(K - (m + 1))!}) {(x + A)}^{K - (m + 1)}$
294	258 285 293	3eqtrrd	$⊢ (((φ \land m \in ℕ_{0}) \land m < K) \land x \in X) \to (\frac{K!}{(K - (m + 1))!}) {(x + A)}^{K - (m + 1)} = (\frac{K!}{(K - m)!}) (K - m) {(x + A)}^{K - m - 1}$
295	218 238	mulcomd	$⊢ (((φ \land m \in ℕ_{0}) \land m < K) \land x \in X) \to (\frac{K!}{(K - m)!}) (K - m) {(x + A)}^{K - m - 1} = (K - m) {(x + A)}^{K - m - 1} (\frac{K!}{(K - m)!})$
296	256 294 295	3eqtrrd	$⊢ (((φ \land m \in ℕ_{0}) \land m < K) \land x \in X) \to (K - m) {(x + A)}^{K - m - 1} (\frac{K!}{(K - m)!}) = if (K < m + 1, 0, (\frac{K!}{(K - (m + 1))!}) {(x + A)}^{K - (m + 1)})$
297	243 245 296	3eqtrd	$⊢ (((φ \land m \in ℕ_{0}) \land m < K) \land x \in X) \to 0 \cdot {(x + A)}^{K - m} + (K - m) {(x + A)}^{K - m - 1} (\frac{K!}{(K - m)!}) = if (K < m + 1, 0, (\frac{K!}{(K - (m + 1))!}) {(x + A)}^{K - (m + 1)})$
298	297	mpteq2dva	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to (x \in X ⟼ 0 \cdot {(x + A)}^{K - m} + (K - m) {(x + A)}^{K - m - 1} (\frac{K!}{(K - m)!})) = (x \in X ⟼ if (K < m + 1, 0, (\frac{K!}{(K - (m + 1))!}) {(x + A)}^{K - (m + 1)}))$
299	204 241 298	3eqtrd	$⊢ ((φ \land m \in ℕ_{0}) \land m < K) \to \frac{d (x \in X⟼ if (K < m, 0, (\frac{K!}{(K - m)!}) {(x + A)}^{K - m}))}{d_{S} x} = (x \in X ⟼ if (K < m + 1, 0, (\frac{K!}{(K - (m + 1))!}) {(x + A)}^{K - (m + 1)}))$
300	188 195 299	syl2anc	$⊢ (((φ \land m \in ℕ_{0}) \land m \leq K) \land \neg m = K) \to \frac{d (x \in X⟼ if (K < m, 0, (\frac{K!}{(K - m)!}) {(x + A)}^{K - m}))}{d_{S} x} = (x \in X ⟼ if (K < m + 1, 0, (\frac{K!}{(K - (m + 1))!}) {(x + A)}^{K - (m + 1)}))$
301	187 300	pm2.61dan	$⊢ ((φ \land m \in ℕ_{0}) \land m \leq K) \to \frac{d (x \in X⟼ if (K < m, 0, (\frac{K!}{(K - m)!}) {(x + A)}^{K - m}))}{d_{S} x} = (x \in X ⟼ if (K < m + 1, 0, (\frac{K!}{(K - (m + 1))!}) {(x + A)}^{K - (m + 1)}))$
302	129 134 301	syl2anc	$⊢ ((φ \land m \in ℕ_{0}) \land \neg K < m) \to \frac{d (x \in X⟼ if (K < m, 0, (\frac{K!}{(K - m)!}) {(x + A)}^{K - m}))}{d_{S} x} = (x \in X ⟼ if (K < m + 1, 0, (\frac{K!}{(K - (m + 1))!}) {(x + A)}^{K - (m + 1)}))$
303	128 302	pm2.61dan	$⊢ (φ \land m \in ℕ_{0}) \to \frac{d (x \in X⟼ if (K < m, 0, (\frac{K!}{(K - m)!}) {(x + A)}^{K - m}))}{d_{S} x} = (x \in X ⟼ if (K < m + 1, 0, (\frac{K!}{(K - (m + 1))!}) {(x + A)}^{K - (m + 1)}))$
304	303	adantr	$⊢ ((φ \land m \in ℕ_{0}) \land (S D^{n} F) (m) = (x \in X ⟼ if (K < m, 0, (\frac{K!}{(K - m)!}) {(x + A)}^{K - m}))) \to \frac{d (x \in X⟼ if (K < m, 0, (\frac{K!}{(K - m)!}) {(x + A)}^{K - m}))}{d_{S} x} = (x \in X ⟼ if (K < m + 1, 0, (\frac{K!}{(K - (m + 1))!}) {(x + A)}^{K - (m + 1)}))$
305	103 105 304	3eqtrd	$⊢ ((φ \land m \in ℕ_{0}) \land (S D^{n} F) (m) = (x \in X ⟼ if (K < m, 0, (\frac{K!}{(K - m)!}) {(x + A)}^{K - m}))) \to (S D^{n} F) (m + 1) = (x \in X ⟼ if (K < m + 1, 0, (\frac{K!}{(K - (m + 1))!}) {(x + A)}^{K - (m + 1)}))$
306	16 27 38 49 97 305	nn0indd	$⊢ (φ \land N \in ℕ_{0}) \to (S D^{n} F) (N) = (x \in X ⟼ if (K < N, 0, (\frac{K!}{(K - N)!}) {(x + A)}^{K - N}))$

Metamath Proof Explorer

Theorem dvnxpaek

Proof