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	ffvelrnda	$⊢ (φ \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	ffvelrnda	$⊢ ((φ \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	ffvelrnd	$⊢ ((φ \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	37 43 46	3jca	$⊢ (((φ \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 ℤ \land if (j = 0, P - 1, P) \in ℤ \land if (j = 0, P - 1, P) - C (l) (j) \in ℤ)$
48	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 ℝ$
49	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 ℝ$
50		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)$
51	48 49 50	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)$
52	49 48	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))$
53	51 52	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)$
54		0red	$⊢ ((φ \land l \in dom C) \land j \in (0 \dots M)) \to 0 \in ℝ$
55	25	nn0red	$⊢ ((φ \land l \in dom C) \land j \in (0 \dots M)) \to C (l) (j) \in ℝ$
56	41	nn0red	$⊢ φ \to if (j = 0, P - 1, P) \in ℝ$
57	56	ad2antrr	$⊢ ((φ \land l \in dom C) \land j \in (0 \dots M)) \to if (j = 0, P - 1, P) \in ℝ$
58	25	nn0ge0d	$⊢ ((φ \land l \in dom C) \land j \in (0 \dots M)) \to 0 \leq C (l) (j)$
59	54 55 57 58	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$
60	57	recnd	$⊢ ((φ \land l \in dom C) \land j \in (0 \dots M)) \to if (j = 0, P - 1, P) \in ℂ$
61	60	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)$
62	59 61	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)$
63	62	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)$
64	47 53 63	jca32	$⊢ (((φ \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 ℤ \land if (j = 0, P - 1, P) \in ℤ \land if (j = 0, P - 1, P) - C (l) (j) \in ℤ) \land (0 \leq if (j = 0, P - 1, P) - C (l) (j) \land if (j = 0, P - 1, P) - C (l) (j) \leq if (j = 0, P - 1, P)))$
65		elfz2	$⊢ if (j = 0, P - 1, P) - C (l) (j) \in (0 \dots if (j = 0, P - 1, P)) \leftrightarrow ((0 \in ℤ \land if (j = 0, P - 1, P) \in ℤ \land if (j = 0, P - 1, P) - C (l) (j) \in ℤ) \land (0 \leq if (j = 0, P - 1, P) - C (l) (j) \land if (j = 0, P - 1, P) - C (l) (j) \leq if (j = 0, P - 1, P)))$
66	64 65	sylibr	$⊢ (((φ \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))$
67		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 ℕ$
68	66 67	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 ℕ$
69	68	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 ℤ$
70	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 ℤ$
71		elfzelz	$⊢ j \in (0 \dots M) \to j \in ℤ$
72	71	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 ℤ$
73	70 72	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 ℤ$
74		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))$
75	46 53 74	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}$
76		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 ℤ$
77	73 75 76	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 ℤ$
78	69 77	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 ℤ$
79	37 78	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 ℤ$
80	36 79	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 ℤ$
81	32 80	eqeltrd	$⊢ ((φ \land l \in dom C) \land j \in (0 \dots M)) \to (S D^{n} H (j)) (C (l) (j)) (J) \in ℤ$
82	15 81	fprodzcl	$⊢ (φ \land l \in dom C) \to \prod_{j = 0}^{M} (S D^{n} H (j)) (C (l) (j)) (J) \in ℤ$
83	14 82	fsumzcl	$⊢ φ \to \sum_{l \in dom C} \prod_{j = 0}^{M} (S D^{n} H (j)) (C (l) (j)) (J) \in ℤ$
84	31 83	eqeltrd	$⊢ φ \to G (J) \in ℤ$

Metamath Proof Explorer

Theorem etransclem27

Proof