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		tgioo4	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
26	24 25	eleqtri	$⊢ ℝ \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
27	26	a1i	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots R))) \to ℝ \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
28	1	adantr	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots R))) \to P \in ℕ$
29	2	adantr	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots R))) \to M \in ℕ_{0}$
30		xp2nd	$⊢ k \in ((0 \dots M) \times (0 \dots R)) \to 2^{nd} (k) \in (0 \dots R)$
31		elfznn0	$⊢ 2^{nd} (k) \in (0 \dots R) \to 2^{nd} (k) \in ℕ_{0}$
32	30 31	syl	$⊢ k \in ((0 \dots M) \times (0 \dots R)) \to 2^{nd} (k) \in ℕ_{0}$
33	32	adantl	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots R))) \to 2^{nd} (k) \in ℕ_{0}$
34	23 27 28 29 3 33	etransclem33	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots R))) \to (ℝ D^{n} F) (2^{nd} (k)) : ℝ ⟶ ℂ$
35	19	nn0red	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots R))) \to 1^{st} (k) \in ℝ$
36	34 35	ffvelcdmd	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots R))) \to (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k)) \in ℂ$
37	21 36	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 ℂ$
38	13	nnne0d	$⊢ φ \to (P - 1)! \neq 0$
39	10 14 37 38	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)!})$
40	14	adantr	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots R))) \to (P - 1)! \in ℂ$
41	38	adantr	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots R))) \to (P - 1)! \neq 0$
42	21 36 40 41	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)!})$
43		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)}))$
44		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\})$
45	16	adantl	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots R))) \to 1^{st} (k) \in (0 \dots M)$
46	23 27 28 29 3 33 43 44 45 35	etransclem37	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots R))) \to (P - 1)! ∥ (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))$
47	13	nnzd	$⊢ φ \to (P - 1)! \in ℤ$
48	47	adantr	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots R))) \to (P - 1)! \in ℤ$
49	19	nn0zd	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots R))) \to 1^{st} (k) \in ℤ$
50	23 27 28 29 3 33 35 49	etransclem42	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots R))) \to (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k)) \in ℤ$
51		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 ℤ)$
52	48 41 50 51	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 ℤ)$
53	46 52	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 ℤ$
54	20 53	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 ℤ$
55	42 54	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 ℤ$
56	10 55	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 ℤ$
57	39 56	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 ℤ$
58	5 57	eqeltrid	$⊢ φ \to K \in ℤ$

Metamath Proof Explorer

Theorem etransclem45

Proof