etransclem45

Description: K is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	etransclem45.p	$⊢ φ \to P \in ℕ$
	etransclem45.m	$⊢ φ \to M \in ℕ_{0}$
	etransclem45.f	$⊢ F = (x \in ℝ ⟼ x^{P - 1} \prod_{j = 1}^{M} {(x - j)}^{P})$
	etransclem45.a	$⊢ φ \to A : ℕ_{0} ⟶ ℤ$
	etransclem45.k	$⊢ K = \frac{\sum_{k \in (0 \dots M) \times (0 \dots R)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!}$
Assertion	etransclem45	$⊢ φ \to K \in ℤ$

Proof

Step	Hyp	Ref	Expression
1		etransclem45.p	$⊢ φ \to P \in ℕ$
2		etransclem45.m	$⊢ φ \to M \in ℕ_{0}$
3		etransclem45.f	$⊢ F = (x \in ℝ ⟼ x^{P - 1} \prod_{j = 1}^{M} {(x - j)}^{P})$
4		etransclem45.a	$⊢ φ \to A : ℕ_{0} ⟶ ℤ$
5		etransclem45.k	$⊢ K = \frac{\sum_{k \in (0 \dots M) \times (0 \dots R)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!}$
6		fzfi	$⊢ (0 \dots M) \in Fin$
7		fzfi	$⊢ (0 \dots R) \in Fin$
8		xpfi	$⊢ ((0 \dots M) \in Fin \land (0 \dots R) \in Fin) \to (0 \dots M) \times (0 \dots R) \in Fin$
9	6 7 8	mp2an	$⊢ (0 \dots M) \times (0 \dots R) \in Fin$
10	9	a1i	$⊢ φ \to (0 \dots M) \times (0 \dots R) \in Fin$
11		nnm1nn0	$⊢ P \in ℕ \to P - 1 \in ℕ_{0}$
12	1 11	syl	$⊢ φ \to P - 1 \in ℕ_{0}$
13	12	faccld	$⊢ φ \to (P - 1)! \in ℕ$
14	13	nncnd	$⊢ φ \to (P - 1)! \in ℂ$
15	4	adantr	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots R))) \to A : ℕ_{0} ⟶ ℤ$
16		xp1st	$⊢ k \in ((0 \dots M) \times (0 \dots R)) \to 1^{st} (k) \in (0 \dots M)$
17		elfznn0	$⊢ 1^{st} (k) \in (0 \dots M) \to 1^{st} (k) \in ℕ_{0}$
18	16 17	syl	$⊢ k \in ((0 \dots M) \times (0 \dots R)) \to 1^{st} (k) \in ℕ_{0}$
19	18	adantl	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots R))) \to 1^{st} (k) \in ℕ_{0}$
20	15 19	ffvelcdmd	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots R))) \to A (1^{st} (k)) \in ℤ$
21	20	zcnd	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots R))) \to A (1^{st} (k)) \in ℂ$
22		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
23	22	a1i	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots R))) \to ℝ \in \{ℝ, ℂ\}$
24		reopn	$⊢ ℝ \in topGen (ran (.))$
25		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
26	25	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
27	24 26	eleqtri	$⊢ ℝ \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
28	27	a1i	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots R))) \to ℝ \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
29	1	adantr	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots R))) \to P \in ℕ$
30	2	adantr	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots R))) \to M \in ℕ_{0}$
31		xp2nd	$⊢ k \in ((0 \dots M) \times (0 \dots R)) \to 2^{nd} (k) \in (0 \dots R)$
32		elfznn0	$⊢ 2^{nd} (k) \in (0 \dots R) \to 2^{nd} (k) \in ℕ_{0}$
33	31 32	syl	$⊢ k \in ((0 \dots M) \times (0 \dots R)) \to 2^{nd} (k) \in ℕ_{0}$
34	33	adantl	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots R))) \to 2^{nd} (k) \in ℕ_{0}$
35	23 28 29 30 3 34	etransclem33	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots R))) \to (ℝ D^{n} F) (2^{nd} (k)) : ℝ ⟶ ℂ$
36	19	nn0red	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots R))) \to 1^{st} (k) \in ℝ$
37	35 36	ffvelcdmd	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots R))) \to (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k)) \in ℂ$
38	21 37	mulcld	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots R))) \to A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k)) \in ℂ$
39	13	nnne0d	$⊢ φ \to (P - 1)! \neq 0$
40	10 14 38 39	fsumdivc	$⊢ φ \to \frac{\sum_{k \in (0 \dots M) \times (0 \dots R)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!} = \sum_{k \in (0 \dots M) \times (0 \dots R)} (\frac{A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!})$
41	14	adantr	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots R))) \to (P - 1)! \in ℂ$
42	39	adantr	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots R))) \to (P - 1)! \neq 0$
43	21 37 41 42	divassd	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots R))) \to \frac{A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!} = A (1^{st} (k)) (\frac{(ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!})$
44		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)}))$
45		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\})$
46	16	adantl	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots R))) \to 1^{st} (k) \in (0 \dots M)$
47	23 28 29 30 3 34 44 45 46 36	etransclem37	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots R))) \to (P - 1)! ∥ (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))$
48	13	nnzd	$⊢ φ \to (P - 1)! \in ℤ$
49	48	adantr	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots R))) \to (P - 1)! \in ℤ$
50	19	nn0zd	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots R))) \to 1^{st} (k) \in ℤ$
51	23 28 29 30 3 34 36 50	etransclem42	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots R))) \to (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k)) \in ℤ$
52		dvdsval2	$⊢ ((P - 1)! \in ℤ \land (P - 1)! \neq 0 \land (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k)) \in ℤ) \to ((P - 1)! ∥ (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k)) \leftrightarrow \frac{(ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!} \in ℤ)$
53	49 42 51 52	syl3anc	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots R))) \to ((P - 1)! ∥ (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k)) \leftrightarrow \frac{(ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!} \in ℤ)$
54	47 53	mpbid	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots R))) \to \frac{(ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!} \in ℤ$
55	20 54	zmulcld	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots R))) \to A (1^{st} (k)) (\frac{(ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!}) \in ℤ$
56	43 55	eqeltrd	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots R))) \to \frac{A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!} \in ℤ$
57	10 56	fsumzcl	$⊢ φ \to \sum_{k \in (0 \dots M) \times (0 \dots R)} (\frac{A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!}) \in ℤ$
58	40 57	eqeltrd	$⊢ φ \to \frac{\sum_{k \in (0 \dots M) \times (0 \dots R)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!} \in ℤ$
59	5 58	eqeltrid	$⊢ φ \to K \in ℤ$

Metamath Proof Explorer

Theorem etransclem45

Proof