etransclem27

Description: The N -th derivative of F applied to J is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	etransclem27.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
	etransclem27.x	$⊢ φ \to X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
	etransclem27.p	$⊢ φ \to P \in ℕ$
	etransclem27.h	$⊢ H = (j \in (0 \dots M) ⟼ (x \in X ⟼ {(x - j)}^{if (j = 0, P - 1, P)}))$
	etransclem27.cfi	$⊢ φ \to C \in Fin$
	etransclem27.cf	$⊢ φ \to C : dom C ⟶ {ℕ_{0}}^{(0 \dots M)}$
	etransclem27.g	$⊢ G = (x \in X ⟼ \sum_{l \in dom C} \prod_{j = 0}^{M} (S D^{n} H (j)) (C (l) (j)) (x))$
	etransclem27.jx	$⊢ φ \to J \in X$
	etransclem27.jz	$⊢ φ \to J \in ℤ$
Assertion	etransclem27	$⊢ φ \to G (J) \in ℤ$

Proof

Step	Hyp	Ref	Expression
1		etransclem27.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
2		etransclem27.x	$⊢ φ \to X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
3		etransclem27.p	$⊢ φ \to P \in ℕ$
4		etransclem27.h	$⊢ H = (j \in (0 \dots M) ⟼ (x \in X ⟼ {(x - j)}^{if (j = 0, P - 1, P)}))$
5		etransclem27.cfi	$⊢ φ \to C \in Fin$
6		etransclem27.cf	$⊢ φ \to C : dom C ⟶ {ℕ_{0}}^{(0 \dots M)}$
7		etransclem27.g	$⊢ G = (x \in X ⟼ \sum_{l \in dom C} \prod_{j = 0}^{M} (S D^{n} H (j)) (C (l) (j)) (x))$
8		etransclem27.jx	$⊢ φ \to J \in X$
9		etransclem27.jz	$⊢ φ \to J \in ℤ$
10		fveq2	$⊢ x = J \to (S D^{n} H (j)) (C (l) (j)) (x) = (S D^{n} H (j)) (C (l) (j)) (J)$
11	10	prodeq2ad	$⊢ x = J \to \prod_{j = 0}^{M} (S D^{n} H (j)) (C (l) (j)) (x) = \prod_{j = 0}^{M} (S D^{n} H (j)) (C (l) (j)) (J)$
12	11	sumeq2sdv	$⊢ x = J \to \sum_{l \in dom C} \prod_{j = 0}^{M} (S D^{n} H (j)) (C (l) (j)) (x) = \sum_{l \in dom C} \prod_{j = 0}^{M} (S D^{n} H (j)) (C (l) (j)) (J)$
13		dmfi	$⊢ C \in Fin \to dom C \in Fin$
14	5 13	syl	$⊢ φ \to dom C \in Fin$
15		fzfid	$⊢ (φ \land l \in dom C) \to (0 \dots M) \in Fin$
16	1	ad2antrr	$⊢ ((φ \land l \in dom C) \land j \in (0 \dots M)) \to S \in \{ℝ, ℂ\}$
17	2	ad2antrr	$⊢ ((φ \land l \in dom C) \land j \in (0 \dots M)) \to X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
18	3	ad2antrr	$⊢ ((φ \land l \in dom C) \land j \in (0 \dots M)) \to P \in ℕ$
19		etransclem5	$⊢ (j \in (0 \dots M) ⟼ (x \in X ⟼ {(x - j)}^{if (j = 0, P - 1, P)})) = (z \in (0 \dots M) ⟼ (y \in X ⟼ {(y - z)}^{if (z = 0, P - 1, P)}))$
20	4 19	eqtri	$⊢ H = (z \in (0 \dots M) ⟼ (y \in X ⟼ {(y - z)}^{if (z = 0, P - 1, P)}))$
21		simpr	$⊢ ((φ \land l \in dom C) \land j \in (0 \dots M)) \to j \in (0 \dots M)$
22	6	ffvelcdmda	$⊢ (φ \land l \in dom C) \to C (l) \in ({ℕ_{0}}^{(0 \dots M)})$
23		elmapi	$⊢ C (l) \in ({ℕ_{0}}^{(0 \dots M)}) \to C (l) : (0 \dots M) ⟶ ℕ_{0}$
24	22 23	syl	$⊢ (φ \land l \in dom C) \to C (l) : (0 \dots M) ⟶ ℕ_{0}$
25	24	ffvelcdmda	$⊢ ((φ \land l \in dom C) \land j \in (0 \dots M)) \to C (l) (j) \in ℕ_{0}$
26	16 17 18 20 21 25	etransclem20	$⊢ ((φ \land l \in dom C) \land j \in (0 \dots M)) \to (S D^{n} H (j)) (C (l) (j)) : X ⟶ ℂ$
27	8	ad2antrr	$⊢ ((φ \land l \in dom C) \land j \in (0 \dots M)) \to J \in X$
28	26 27	ffvelcdmd	$⊢ ((φ \land l \in dom C) \land j \in (0 \dots M)) \to (S D^{n} H (j)) (C (l) (j)) (J) \in ℂ$
29	15 28	fprodcl	$⊢ (φ \land l \in dom C) \to \prod_{j = 0}^{M} (S D^{n} H (j)) (C (l) (j)) (J) \in ℂ$
30	14 29	fsumcl	$⊢ φ \to \sum_{l \in dom C} \prod_{j = 0}^{M} (S D^{n} H (j)) (C (l) (j)) (J) \in ℂ$
31	7 12 8 30	fvmptd3	$⊢ φ \to G (J) = \sum_{l \in dom C} \prod_{j = 0}^{M} (S D^{n} H (j)) (C (l) (j)) (J)$
32	16 17 18 20 21 25 27	etransclem21	$⊢ ((φ \land l \in dom C) \land j \in (0 \dots M)) \to (S D^{n} H (j)) (C (l) (j)) (J) = if (if (j = 0, P - 1, P) < C (l) (j), 0, (\frac{if (j = 0, P - 1, P)!}{(if (j = 0, P - 1, P) - C (l) (j))!}) {(J - j)}^{if (j = 0, P - 1, P) - C (l) (j)})$
33		iftrue	$⊢ if (j = 0, P - 1, P) < C (l) (j) \to if (if (j = 0, P - 1, P) < C (l) (j), 0, (\frac{if (j = 0, P - 1, P)!}{(if (j = 0, P - 1, P) - C (l) (j))!}) {(J - j)}^{if (j = 0, P - 1, P) - C (l) (j)}) = 0$
34		0zd	$⊢ if (j = 0, P - 1, P) < C (l) (j) \to 0 \in ℤ$
35	33 34	eqeltrd	$⊢ if (j = 0, P - 1, P) < C (l) (j) \to if (if (j = 0, P - 1, P) < C (l) (j), 0, (\frac{if (j = 0, P - 1, P)!}{(if (j = 0, P - 1, P) - C (l) (j))!}) {(J - j)}^{if (j = 0, P - 1, P) - C (l) (j)}) \in ℤ$
36	35	adantl	$⊢ (((φ \land l \in dom C) \land j \in (0 \dots M)) \land if (j = 0, P - 1, P) < C (l) (j)) \to if (if (j = 0, P - 1, P) < C (l) (j), 0, (\frac{if (j = 0, P - 1, P)!}{(if (j = 0, P - 1, P) - C (l) (j))!}) {(J - j)}^{if (j = 0, P - 1, P) - C (l) (j)}) \in ℤ$
37		0zd	$⊢ (((φ \land l \in dom C) \land j \in (0 \dots M)) \land \neg if (j = 0, P - 1, P) < C (l) (j)) \to 0 \in ℤ$
38		nnm1nn0	$⊢ P \in ℕ \to P - 1 \in ℕ_{0}$
39	3 38	syl	$⊢ φ \to P - 1 \in ℕ_{0}$
40	3	nnnn0d	$⊢ φ \to P \in ℕ_{0}$
41	39 40	ifcld	$⊢ φ \to if (j = 0, P - 1, P) \in ℕ_{0}$
42	41	nn0zd	$⊢ φ \to if (j = 0, P - 1, P) \in ℤ$
43	42	ad3antrrr	$⊢ (((φ \land l \in dom C) \land j \in (0 \dots M)) \land \neg if (j = 0, P - 1, P) < C (l) (j)) \to if (j = 0, P - 1, P) \in ℤ$
44	25	nn0zd	$⊢ ((φ \land l \in dom C) \land j \in (0 \dots M)) \to C (l) (j) \in ℤ$
45	44	adantr	$⊢ (((φ \land l \in dom C) \land j \in (0 \dots M)) \land \neg if (j = 0, P - 1, P) < C (l) (j)) \to C (l) (j) \in ℤ$
46	43 45	zsubcld	$⊢ (((φ \land l \in dom C) \land j \in (0 \dots M)) \land \neg if (j = 0, P - 1, P) < C (l) (j)) \to if (j = 0, P - 1, P) - C (l) (j) \in ℤ$
47	45	zred	$⊢ (((φ \land l \in dom C) \land j \in (0 \dots M)) \land \neg if (j = 0, P - 1, P) < C (l) (j)) \to C (l) (j) \in ℝ$
48	43	zred	$⊢ (((φ \land l \in dom C) \land j \in (0 \dots M)) \land \neg if (j = 0, P - 1, P) < C (l) (j)) \to if (j = 0, P - 1, P) \in ℝ$
49		simpr	$⊢ (((φ \land l \in dom C) \land j \in (0 \dots M)) \land \neg if (j = 0, P - 1, P) < C (l) (j)) \to \neg if (j = 0, P - 1, P) < C (l) (j)$
50	47 48 49	nltled	$⊢ (((φ \land l \in dom C) \land j \in (0 \dots M)) \land \neg if (j = 0, P - 1, P) < C (l) (j)) \to C (l) (j) \leq if (j = 0, P - 1, P)$
51	48 47	subge0d	$⊢ (((φ \land l \in dom C) \land j \in (0 \dots M)) \land \neg if (j = 0, P - 1, P) < C (l) (j)) \to (0 \leq if (j = 0, P - 1, P) - C (l) (j) \leftrightarrow C (l) (j) \leq if (j = 0, P - 1, P))$
52	50 51	mpbird	$⊢ (((φ \land l \in dom C) \land j \in (0 \dots M)) \land \neg if (j = 0, P - 1, P) < C (l) (j)) \to 0 \leq if (j = 0, P - 1, P) - C (l) (j)$
53		0red	$⊢ ((φ \land l \in dom C) \land j \in (0 \dots M)) \to 0 \in ℝ$
54	25	nn0red	$⊢ ((φ \land l \in dom C) \land j \in (0 \dots M)) \to C (l) (j) \in ℝ$
55	41	nn0red	$⊢ φ \to if (j = 0, P - 1, P) \in ℝ$
56	55	ad2antrr	$⊢ ((φ \land l \in dom C) \land j \in (0 \dots M)) \to if (j = 0, P - 1, P) \in ℝ$
57	25	nn0ge0d	$⊢ ((φ \land l \in dom C) \land j \in (0 \dots M)) \to 0 \leq C (l) (j)$
58	53 54 56 57	lesub2dd	$⊢ ((φ \land l \in dom C) \land j \in (0 \dots M)) \to if (j = 0, P - 1, P) - C (l) (j) \leq if (j = 0, P - 1, P) - 0$
59	56	recnd	$⊢ ((φ \land l \in dom C) \land j \in (0 \dots M)) \to if (j = 0, P - 1, P) \in ℂ$
60	59	subid1d	$⊢ ((φ \land l \in dom C) \land j \in (0 \dots M)) \to if (j = 0, P - 1, P) - 0 = if (j = 0, P - 1, P)$
61	58 60	breqtrd	$⊢ ((φ \land l \in dom C) \land j \in (0 \dots M)) \to if (j = 0, P - 1, P) - C (l) (j) \leq if (j = 0, P - 1, P)$
62	61	adantr	$⊢ (((φ \land l \in dom C) \land j \in (0 \dots M)) \land \neg if (j = 0, P - 1, P) < C (l) (j)) \to if (j = 0, P - 1, P) - C (l) (j) \leq if (j = 0, P - 1, P)$
63	37 43 46 52 62	elfzd	$⊢ (((φ \land l \in dom C) \land j \in (0 \dots M)) \land \neg if (j = 0, P - 1, P) < C (l) (j)) \to if (j = 0, P - 1, P) - C (l) (j) \in (0 \dots if (j = 0, P - 1, P))$
64		permnn	$⊢ if (j = 0, P - 1, P) - C (l) (j) \in (0 \dots if (j = 0, P - 1, P)) \to \frac{if (j = 0, P - 1, P)!}{(if (j = 0, P - 1, P) - C (l) (j))!} \in ℕ$
65	63 64	syl	$⊢ (((φ \land l \in dom C) \land j \in (0 \dots M)) \land \neg if (j = 0, P - 1, P) < C (l) (j)) \to \frac{if (j = 0, P - 1, P)!}{(if (j = 0, P - 1, P) - C (l) (j))!} \in ℕ$
66	65	nnzd	$⊢ (((φ \land l \in dom C) \land j \in (0 \dots M)) \land \neg if (j = 0, P - 1, P) < C (l) (j)) \to \frac{if (j = 0, P - 1, P)!}{(if (j = 0, P - 1, P) - C (l) (j))!} \in ℤ$
67	9	ad3antrrr	$⊢ (((φ \land l \in dom C) \land j \in (0 \dots M)) \land \neg if (j = 0, P - 1, P) < C (l) (j)) \to J \in ℤ$
68		elfzelz	$⊢ j \in (0 \dots M) \to j \in ℤ$
69	68	ad2antlr	$⊢ (((φ \land l \in dom C) \land j \in (0 \dots M)) \land \neg if (j = 0, P - 1, P) < C (l) (j)) \to j \in ℤ$
70	67 69	zsubcld	$⊢ (((φ \land l \in dom C) \land j \in (0 \dots M)) \land \neg if (j = 0, P - 1, P) < C (l) (j)) \to J - j \in ℤ$
71		elnn0z	$⊢ if (j = 0, P - 1, P) - C (l) (j) \in ℕ_{0} \leftrightarrow (if (j = 0, P - 1, P) - C (l) (j) \in ℤ \land 0 \leq if (j = 0, P - 1, P) - C (l) (j))$
72	46 52 71	sylanbrc	$⊢ (((φ \land l \in dom C) \land j \in (0 \dots M)) \land \neg if (j = 0, P - 1, P) < C (l) (j)) \to if (j = 0, P - 1, P) - C (l) (j) \in ℕ_{0}$
73		zexpcl	$⊢ (J - j \in ℤ \land if (j = 0, P - 1, P) - C (l) (j) \in ℕ_{0}) \to {(J - j)}^{if (j = 0, P - 1, P) - C (l) (j)} \in ℤ$
74	70 72 73	syl2anc	$⊢ (((φ \land l \in dom C) \land j \in (0 \dots M)) \land \neg if (j = 0, P - 1, P) < C (l) (j)) \to {(J - j)}^{if (j = 0, P - 1, P) - C (l) (j)} \in ℤ$
75	66 74	zmulcld	$⊢ (((φ \land l \in dom C) \land j \in (0 \dots M)) \land \neg if (j = 0, P - 1, P) < C (l) (j)) \to (\frac{if (j = 0, P - 1, P)!}{(if (j = 0, P - 1, P) - C (l) (j))!}) {(J - j)}^{if (j = 0, P - 1, P) - C (l) (j)} \in ℤ$
76	37 75	ifcld	$⊢ (((φ \land l \in dom C) \land j \in (0 \dots M)) \land \neg if (j = 0, P - 1, P) < C (l) (j)) \to if (if (j = 0, P - 1, P) < C (l) (j), 0, (\frac{if (j = 0, P - 1, P)!}{(if (j = 0, P - 1, P) - C (l) (j))!}) {(J - j)}^{if (j = 0, P - 1, P) - C (l) (j)}) \in ℤ$
77	36 76	pm2.61dan	$⊢ ((φ \land l \in dom C) \land j \in (0 \dots M)) \to if (if (j = 0, P - 1, P) < C (l) (j), 0, (\frac{if (j = 0, P - 1, P)!}{(if (j = 0, P - 1, P) - C (l) (j))!}) {(J - j)}^{if (j = 0, P - 1, P) - C (l) (j)}) \in ℤ$
78	32 77	eqeltrd	$⊢ ((φ \land l \in dom C) \land j \in (0 \dots M)) \to (S D^{n} H (j)) (C (l) (j)) (J) \in ℤ$
79	15 78	fprodzcl	$⊢ (φ \land l \in dom C) \to \prod_{j = 0}^{M} (S D^{n} H (j)) (C (l) (j)) (J) \in ℤ$
80	14 79	fsumzcl	$⊢ φ \to \sum_{l \in dom C} \prod_{j = 0}^{M} (S D^{n} H (j)) (C (l) (j)) (J) \in ℤ$
81	31 80	eqeltrd	$⊢ φ \to G (J) \in ℤ$

Metamath Proof Explorer

Theorem etransclem27

Proof