etransclem44

Description: The given finite sum is nonzero. This is the claim proved after equation (7) in Juillerat p. 12 . (Contributed by Glauco Siliprandi, 5-Apr-2020)

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

Proof

Step	Hyp	Ref	Expression
1		etransclem44.a	$⊢ φ \to A : ℕ_{0} ⟶ ℤ$
2		etransclem44.a0	$⊢ φ \to A (0) \neq 0$
3		etransclem44.m	$⊢ φ \to M \in ℕ_{0}$
4		etransclem44.p	$⊢ φ \to P \in ℙ$
5		etransclem44.ap	$⊢ φ \to \|A (0)\| < P$
6		etransclem44.mp	$⊢ φ \to M! < P$
7		etransclem44.f	$⊢ F = (x \in ℝ ⟼ x^{P - 1} \prod_{j = 1}^{M} {(x - j)}^{P})$
8		etransclem44.k	$⊢ K = \frac{\sum_{k \in (0 \dots M) \times (0 \dots M P + P - 1)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!}$
9	8	a1i	$⊢ φ \to K = \frac{\sum_{k \in (0 \dots M) \times (0 \dots M P + P - 1)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!}$
10		nfv	$⊢ Ⅎ k φ$
11		nfcv	$⊢ \underline{Ⅎ} k A (0) (ℝ D^{n} F) (P - 1) (0)$
12		fzfi	$⊢ (0 \dots M) \in Fin$
13		fzfi	$⊢ (0 \dots M P + P - 1) \in Fin$
14		xpfi	$⊢ ((0 \dots M) \in Fin \land (0 \dots M P + P - 1) \in Fin) \to (0 \dots M) \times (0 \dots M P + P - 1) \in Fin$
15	12 13 14	mp2an	$⊢ (0 \dots M) \times (0 \dots M P + P - 1) \in Fin$
16	15	a1i	$⊢ φ \to (0 \dots M) \times (0 \dots M P + P - 1) \in Fin$
17	1	adantr	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots M P + P - 1))) \to A : ℕ_{0} ⟶ ℤ$
18		fzssnn0	$⊢ (0 \dots M) \subseteq ℕ_{0}$
19		xp1st	$⊢ k \in ((0 \dots M) \times (0 \dots M P + P - 1)) \to 1^{st} (k) \in (0 \dots M)$
20	18 19	sseldi	$⊢ k \in ((0 \dots M) \times (0 \dots M P + P - 1)) \to 1^{st} (k) \in ℕ_{0}$
21	20	adantl	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots M P + P - 1))) \to 1^{st} (k) \in ℕ_{0}$
22	17 21	ffvelrnd	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots M P + P - 1))) \to A (1^{st} (k)) \in ℤ$
23		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
24	23	a1i	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots M P + P - 1))) \to ℝ \in \{ℝ, ℂ\}$
25		reopn	$⊢ ℝ \in topGen (ran (.))$
26		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
27	26	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
28	25 27	eleqtri	$⊢ ℝ \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
29	28	a1i	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots M P + P - 1))) \to ℝ \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
30		prmnn	$⊢ P \in ℙ \to P \in ℕ$
31	4 30	syl	$⊢ φ \to P \in ℕ$
32	31	adantr	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots M P + P - 1))) \to P \in ℕ$
33	3	adantr	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots M P + P - 1))) \to M \in ℕ_{0}$
34		xp2nd	$⊢ k \in ((0 \dots M) \times (0 \dots M P + P - 1)) \to 2^{nd} (k) \in (0 \dots M P + P - 1)$
35		elfznn0	$⊢ 2^{nd} (k) \in (0 \dots M P + P - 1) \to 2^{nd} (k) \in ℕ_{0}$
36	34 35	syl	$⊢ k \in ((0 \dots M) \times (0 \dots M P + P - 1)) \to 2^{nd} (k) \in ℕ_{0}$
37	36	adantl	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots M P + P - 1))) \to 2^{nd} (k) \in ℕ_{0}$
38	21	nn0red	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots M P + P - 1))) \to 1^{st} (k) \in ℝ$
39	21	nn0zd	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots M P + P - 1))) \to 1^{st} (k) \in ℤ$
40	24 29 32 33 7 37 38 39	etransclem42	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots M P + P - 1))) \to (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k)) \in ℤ$
41	22 40	zmulcld	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots M P + P - 1))) \to A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k)) \in ℤ$
42	41	zcnd	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots M P + P - 1))) \to A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k)) \in ℂ$
43		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
44	3 43	eleqtrdi	$⊢ φ \to M \in ℤ_{\geq 0}$
45		eluzfz1	$⊢ M \in ℤ_{\geq 0} \to 0 \in (0 \dots M)$
46	44 45	syl	$⊢ φ \to 0 \in (0 \dots M)$
47		0zd	$⊢ φ \to 0 \in ℤ$
48	3	nn0zd	$⊢ φ \to M \in ℤ$
49	31	nnzd	$⊢ φ \to P \in ℤ$
50	48 49	zmulcld	$⊢ φ \to M P \in ℤ$
51		nnm1nn0	$⊢ P \in ℕ \to P - 1 \in ℕ_{0}$
52	31 51	syl	$⊢ φ \to P - 1 \in ℕ_{0}$
53	52	nn0zd	$⊢ φ \to P - 1 \in ℤ$
54	50 53	zaddcld	$⊢ φ \to M P + P - 1 \in ℤ$
55	52	nn0ge0d	$⊢ φ \to 0 \leq P - 1$
56	31	nnnn0d	$⊢ φ \to P \in ℕ_{0}$
57	3 56	nn0mulcld	$⊢ φ \to M P \in ℕ_{0}$
58	57	nn0ge0d	$⊢ φ \to 0 \leq M P$
59	52	nn0red	$⊢ φ \to P - 1 \in ℝ$
60	50	zred	$⊢ φ \to M P \in ℝ$
61	59 60	addge02d	$⊢ φ \to (0 \leq M P \leftrightarrow P - 1 \leq M P + P - 1)$
62	58 61	mpbid	$⊢ φ \to P - 1 \leq M P + P - 1$
63	47 54 53 55 62	elfzd	$⊢ φ \to P - 1 \in (0 \dots M P + P - 1)$
64		opelxp	$⊢ ⟨0, P - 1⟩ \in ((0 \dots M) \times (0 \dots M P + P - 1)) \leftrightarrow (0 \in (0 \dots M) \land P - 1 \in (0 \dots M P + P - 1))$
65	46 63 64	sylanbrc	$⊢ φ \to ⟨0, P - 1⟩ \in ((0 \dots M) \times (0 \dots M P + P - 1))$
66		fveq2	$⊢ k = ⟨0, P - 1⟩ \to 1^{st} (k) = 1^{st} (⟨0, P - 1⟩)$
67		0re	$⊢ 0 \in ℝ$
68		ovex	$⊢ P - 1 \in V$
69		op1stg	$⊢ (0 \in ℝ \land P - 1 \in V) \to 1^{st} (⟨0, P - 1⟩) = 0$
70	67 68 69	mp2an	$⊢ 1^{st} (⟨0, P - 1⟩) = 0$
71	66 70	eqtrdi	$⊢ k = ⟨0, P - 1⟩ \to 1^{st} (k) = 0$
72	71	fveq2d	$⊢ k = ⟨0, P - 1⟩ \to A (1^{st} (k)) = A (0)$
73		fveq2	$⊢ k = ⟨0, P - 1⟩ \to 2^{nd} (k) = 2^{nd} (⟨0, P - 1⟩)$
74		op2ndg	$⊢ (0 \in ℝ \land P - 1 \in V) \to 2^{nd} (⟨0, P - 1⟩) = P - 1$
75	67 68 74	mp2an	$⊢ 2^{nd} (⟨0, P - 1⟩) = P - 1$
76	73 75	eqtrdi	$⊢ k = ⟨0, P - 1⟩ \to 2^{nd} (k) = P - 1$
77	76	fveq2d	$⊢ k = ⟨0, P - 1⟩ \to (ℝ D^{n} F) (2^{nd} (k)) = (ℝ D^{n} F) (P - 1)$
78	77 71	fveq12d	$⊢ k = ⟨0, P - 1⟩ \to (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k)) = (ℝ D^{n} F) (P - 1) (0)$
79	72 78	oveq12d	$⊢ k = ⟨0, P - 1⟩ \to A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k)) = A (0) (ℝ D^{n} F) (P - 1) (0)$
80	10 11 16 42 65 79	fsumsplit1	$⊢ φ \to \sum_{k \in (0 \dots M) \times (0 \dots M P + P - 1)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k)) = A (0) (ℝ D^{n} F) (P - 1) (0) + \sum_{k \in ((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\}} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))$
81	80	oveq1d	$⊢ φ \to \frac{\sum_{k \in (0 \dots M) \times (0 \dots M P + P - 1)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!} = \frac{A (0) (ℝ D^{n} F) (P - 1) (0) + \sum_{k \in ((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\}} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!}$
82	18 46	sseldi	$⊢ φ \to 0 \in ℕ_{0}$
83	1 82	ffvelrnd	$⊢ φ \to A (0) \in ℤ$
84	23	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
85	28	a1i	$⊢ φ \to ℝ \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
86	67	a1i	$⊢ φ \to 0 \in ℝ$
87	84 85 31 3 7 52 86 47	etransclem42	$⊢ φ \to (ℝ D^{n} F) (P - 1) (0) \in ℤ$
88	83 87	zmulcld	$⊢ φ \to A (0) (ℝ D^{n} F) (P - 1) (0) \in ℤ$
89	88	zcnd	$⊢ φ \to A (0) (ℝ D^{n} F) (P - 1) (0) \in ℂ$
90		difss	$⊢ ((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\} \subseteq (0 \dots M) \times (0 \dots M P + P - 1)$
91		ssfi	$⊢ ((0 \dots M) \times (0 \dots M P + P - 1) \in Fin \land ((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\} \subseteq (0 \dots M) \times (0 \dots M P + P - 1)) \to ((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\} \in Fin$
92	15 90 91	mp2an	$⊢ ((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\} \in Fin$
93	92	a1i	$⊢ φ \to ((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\} \in Fin$
94		eldifi	$⊢ k \in (((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\}) \to k \in ((0 \dots M) \times (0 \dots M P + P - 1))$
95	94 41	sylan2	$⊢ (φ \land k \in (((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\})) \to A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k)) \in ℤ$
96	93 95	fsumzcl	$⊢ φ \to \sum_{k \in ((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\}} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k)) \in ℤ$
97	96	zcnd	$⊢ φ \to \sum_{k \in ((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\}} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k)) \in ℂ$
98	52	faccld	$⊢ φ \to (P - 1)! \in ℕ$
99	98	nncnd	$⊢ φ \to (P - 1)! \in ℂ$
100	98	nnne0d	$⊢ φ \to (P - 1)! \neq 0$
101	89 97 99 100	divdird	$⊢ φ \to \frac{A (0) (ℝ D^{n} F) (P - 1) (0) + \sum_{k \in ((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\}} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!} = (\frac{A (0) (ℝ D^{n} F) (P - 1) (0)}{(P - 1)!}) + (\frac{\sum_{k \in ((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\}} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!})$
102	9 81 101	3eqtrd	$⊢ φ \to K = (\frac{A (0) (ℝ D^{n} F) (P - 1) (0)}{(P - 1)!}) + (\frac{\sum_{k \in ((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\}} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!})$
103	31	nnne0d	$⊢ φ \to P \neq 0$
104	83	zcnd	$⊢ φ \to A (0) \in ℂ$
105	87	zcnd	$⊢ φ \to (ℝ D^{n} F) (P - 1) (0) \in ℂ$
106	104 105 99 100	divassd	$⊢ φ \to \frac{A (0) (ℝ D^{n} F) (P - 1) (0)}{(P - 1)!} = A (0) (\frac{(ℝ D^{n} F) (P - 1) (0)}{(P - 1)!})$
107		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)}))$
108		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\})$
109	84 85 31 3 7 52 107 108 46 86	etransclem37	$⊢ φ \to (P - 1)! ∥ (ℝ D^{n} F) (P - 1) (0)$
110	98	nnzd	$⊢ φ \to (P - 1)! \in ℤ$
111		dvdsval2	$⊢ ((P - 1)! \in ℤ \land (P - 1)! \neq 0 \land (ℝ D^{n} F) (P - 1) (0) \in ℤ) \to ((P - 1)! ∥ (ℝ D^{n} F) (P - 1) (0) \leftrightarrow \frac{(ℝ D^{n} F) (P - 1) (0)}{(P - 1)!} \in ℤ)$
112	110 100 87 111	syl3anc	$⊢ φ \to ((P - 1)! ∥ (ℝ D^{n} F) (P - 1) (0) \leftrightarrow \frac{(ℝ D^{n} F) (P - 1) (0)}{(P - 1)!} \in ℤ)$
113	109 112	mpbid	$⊢ φ \to \frac{(ℝ D^{n} F) (P - 1) (0)}{(P - 1)!} \in ℤ$
114	83 113	zmulcld	$⊢ φ \to A (0) (\frac{(ℝ D^{n} F) (P - 1) (0)}{(P - 1)!}) \in ℤ$
115	106 114	eqeltrd	$⊢ φ \to \frac{A (0) (ℝ D^{n} F) (P - 1) (0)}{(P - 1)!} \in ℤ$
116	94 42	sylan2	$⊢ (φ \land k \in (((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\})) \to A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k)) \in ℂ$
117	93 99 116 100	fsumdivc	$⊢ φ \to \frac{\sum_{k \in ((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\}} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!} = \sum_{k \in ((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\}} (\frac{A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!})$
118	22	zcnd	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots M P + P - 1))) \to A (1^{st} (k)) \in ℂ$
119	94 118	sylan2	$⊢ (φ \land k \in (((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\})) \to A (1^{st} (k)) \in ℂ$
120	94 40	sylan2	$⊢ (φ \land k \in (((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\})) \to (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k)) \in ℤ$
121	120	zcnd	$⊢ (φ \land k \in (((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\})) \to (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k)) \in ℂ$
122	99	adantr	$⊢ (φ \land k \in (((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\})) \to (P - 1)! \in ℂ$
123	100	adantr	$⊢ (φ \land k \in (((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\})) \to (P - 1)! \neq 0$
124	119 121 122 123	divassd	$⊢ (φ \land k \in (((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\})) \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)!})$
125	94 22	sylan2	$⊢ (φ \land k \in (((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\})) \to A (1^{st} (k)) \in ℤ$
126	23	a1i	$⊢ (φ \land k \in (((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\})) \to ℝ \in \{ℝ, ℂ\}$
127	28	a1i	$⊢ (φ \land k \in (((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\})) \to ℝ \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
128	31	adantr	$⊢ (φ \land k \in (((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\})) \to P \in ℕ$
129	3	adantr	$⊢ (φ \land k \in (((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\})) \to M \in ℕ_{0}$
130	94	adantl	$⊢ (φ \land k \in (((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\})) \to k \in ((0 \dots M) \times (0 \dots M P + P - 1))$
131	130 36	syl	$⊢ (φ \land k \in (((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\})) \to 2^{nd} (k) \in ℕ_{0}$
132	130 19	syl	$⊢ (φ \land k \in (((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\})) \to 1^{st} (k) \in (0 \dots M)$
133	94 38	sylan2	$⊢ (φ \land k \in (((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\})) \to 1^{st} (k) \in ℝ$
134	126 127 128 129 7 131 107 108 132 133	etransclem37	$⊢ (φ \land k \in (((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\})) \to (P - 1)! ∥ (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))$
135	110	adantr	$⊢ (φ \land k \in (((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\})) \to (P - 1)! \in ℤ$
136		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 ℤ)$
137	135 123 120 136	syl3anc	$⊢ (φ \land k \in (((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\})) \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 ℤ)$
138	134 137	mpbid	$⊢ (φ \land k \in (((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\})) \to \frac{(ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!} \in ℤ$
139	125 138	zmulcld	$⊢ (φ \land k \in (((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\})) \to A (1^{st} (k)) (\frac{(ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!}) \in ℤ$
140	124 139	eqeltrd	$⊢ (φ \land k \in (((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\})) \to \frac{A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!} \in ℤ$
141	93 140	fsumzcl	$⊢ φ \to \sum_{k \in ((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\}} (\frac{A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!}) \in ℤ$
142	117 141	eqeltrd	$⊢ φ \to \frac{\sum_{k \in ((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\}} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!} \in ℤ$
143		1zzd	$⊢ φ \to 1 \in ℤ$
144		zabscl	$⊢ A (0) \in ℤ \to \|A (0)\| \in ℤ$
145	83 144	syl	$⊢ φ \to \|A (0)\| \in ℤ$
146		nn0abscl	$⊢ A (0) \in ℤ \to \|A (0)\| \in ℕ_{0}$
147	83 146	syl	$⊢ φ \to \|A (0)\| \in ℕ_{0}$
148	104 2	absne0d	$⊢ φ \to \|A (0)\| \neq 0$
149		elnnne0	$⊢ \|A (0)\| \in ℕ \leftrightarrow (\|A (0)\| \in ℕ_{0} \land \|A (0)\| \neq 0)$
150	147 148 149	sylanbrc	$⊢ φ \to \|A (0)\| \in ℕ$
151	150	nnge1d	$⊢ φ \to 1 \leq \|A (0)\|$
152		zltlem1	$⊢ (\|A (0)\| \in ℤ \land P \in ℤ) \to (\|A (0)\| < P \leftrightarrow \|A (0)\| \leq P - 1)$
153	145 49 152	syl2anc	$⊢ φ \to (\|A (0)\| < P \leftrightarrow \|A (0)\| \leq P - 1)$
154	5 153	mpbid	$⊢ φ \to \|A (0)\| \leq P - 1$
155	143 53 145 151 154	elfzd	$⊢ φ \to \|A (0)\| \in (1 \dots P - 1)$
156		fzm1ndvds	$⊢ (P \in ℕ \land \|A (0)\| \in (1 \dots P - 1)) \to \neg P ∥ \|A (0)\|$
157	31 155 156	syl2anc	$⊢ φ \to \neg P ∥ \|A (0)\|$
158		dvdsabsb	$⊢ (P \in ℤ \land A (0) \in ℤ) \to (P ∥ A (0) \leftrightarrow P ∥ \|A (0)\|)$
159	49 83 158	syl2anc	$⊢ φ \to (P ∥ A (0) \leftrightarrow P ∥ \|A (0)\|)$
160	157 159	mtbird	$⊢ φ \to \neg P ∥ A (0)$
161	3 4 6 7	etransclem41	$⊢ φ \to \neg P ∥ (\frac{(ℝ D^{n} F) (P - 1) (0)}{(P - 1)!})$
162	160 161	jca	$⊢ φ \to (\neg P ∥ A (0) \land \neg P ∥ (\frac{(ℝ D^{n} F) (P - 1) (0)}{(P - 1)!}))$
163		pm4.56	$⊢ (\neg P ∥ A (0) \land \neg P ∥ (\frac{(ℝ D^{n} F) (P - 1) (0)}{(P - 1)!})) \leftrightarrow \neg (P ∥ A (0) \lor P ∥ (\frac{(ℝ D^{n} F) (P - 1) (0)}{(P - 1)!}))$
164	162 163	sylib	$⊢ φ \to \neg (P ∥ A (0) \lor P ∥ (\frac{(ℝ D^{n} F) (P - 1) (0)}{(P - 1)!}))$
165		euclemma	$⊢ (P \in ℙ \land A (0) \in ℤ \land \frac{(ℝ D^{n} F) (P - 1) (0)}{(P - 1)!} \in ℤ) \to (P ∥ A (0) (\frac{(ℝ D^{n} F) (P - 1) (0)}{(P - 1)!}) \leftrightarrow (P ∥ A (0) \lor P ∥ (\frac{(ℝ D^{n} F) (P - 1) (0)}{(P - 1)!})))$
166	4 83 113 165	syl3anc	$⊢ φ \to (P ∥ A (0) (\frac{(ℝ D^{n} F) (P - 1) (0)}{(P - 1)!}) \leftrightarrow (P ∥ A (0) \lor P ∥ (\frac{(ℝ D^{n} F) (P - 1) (0)}{(P - 1)!})))$
167	164 166	mtbird	$⊢ φ \to \neg P ∥ A (0) (\frac{(ℝ D^{n} F) (P - 1) (0)}{(P - 1)!})$
168	106	breq2d	$⊢ φ \to (P ∥ (\frac{A (0) (ℝ D^{n} F) (P - 1) (0)}{(P - 1)!}) \leftrightarrow P ∥ A (0) (\frac{(ℝ D^{n} F) (P - 1) (0)}{(P - 1)!}))$
169	167 168	mtbird	$⊢ φ \to \neg P ∥ (\frac{A (0) (ℝ D^{n} F) (P - 1) (0)}{(P - 1)!})$
170	49	adantr	$⊢ (φ \land k \in (((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\})) \to P \in ℤ$
171	170 125 138	3jca	$⊢ (φ \land k \in (((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\})) \to (P \in ℤ \land A (1^{st} (k)) \in ℤ \land \frac{(ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!} \in ℤ)$
172		eldifn	$⊢ k \in (((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\}) \to \neg k \in \{⟨0, P - 1⟩\}$
173	94	adantr	$⊢ (k \in (((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\}) \land (2^{nd} (k) = P - 1 \land 1^{st} (k) = 0)) \to k \in ((0 \dots M) \times (0 \dots M P + P - 1))$
174		1st2nd2	$⊢ k \in ((0 \dots M) \times (0 \dots M P + P - 1)) \to k = ⟨1^{st} (k), 2^{nd} (k)⟩$
175	173 174	syl	$⊢ (k \in (((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\}) \land (2^{nd} (k) = P - 1 \land 1^{st} (k) = 0)) \to k = ⟨1^{st} (k), 2^{nd} (k)⟩$
176		simpr	$⊢ (2^{nd} (k) = P - 1 \land 1^{st} (k) = 0) \to 1^{st} (k) = 0$
177		simpl	$⊢ (2^{nd} (k) = P - 1 \land 1^{st} (k) = 0) \to 2^{nd} (k) = P - 1$
178	176 177	opeq12d	$⊢ (2^{nd} (k) = P - 1 \land 1^{st} (k) = 0) \to ⟨1^{st} (k), 2^{nd} (k)⟩ = ⟨0, P - 1⟩$
179	178	adantl	$⊢ (k \in (((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\}) \land (2^{nd} (k) = P - 1 \land 1^{st} (k) = 0)) \to ⟨1^{st} (k), 2^{nd} (k)⟩ = ⟨0, P - 1⟩$
180	175 179	eqtrd	$⊢ (k \in (((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\}) \land (2^{nd} (k) = P - 1 \land 1^{st} (k) = 0)) \to k = ⟨0, P - 1⟩$
181		velsn	$⊢ k \in \{⟨0, P - 1⟩\} \leftrightarrow k = ⟨0, P - 1⟩$
182	180 181	sylibr	$⊢ (k \in (((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\}) \land (2^{nd} (k) = P - 1 \land 1^{st} (k) = 0)) \to k \in \{⟨0, P - 1⟩\}$
183	172 182	mtand	$⊢ k \in (((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\}) \to \neg (2^{nd} (k) = P - 1 \land 1^{st} (k) = 0)$
184	183	adantl	$⊢ (φ \land k \in (((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\})) \to \neg (2^{nd} (k) = P - 1 \land 1^{st} (k) = 0)$
185	128 129 7 131 132 184 108	etransclem38	$⊢ (φ \land k \in (((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\})) \to P ∥ (\frac{(ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!})$
186		dvdsmultr2	$⊢ (P \in ℤ \land A (1^{st} (k)) \in ℤ \land \frac{(ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!} \in ℤ) \to (P ∥ (\frac{(ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!}) \to P ∥ A (1^{st} (k)) (\frac{(ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!}))$
187	171 185 186	sylc	$⊢ (φ \land k \in (((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\})) \to P ∥ A (1^{st} (k)) (\frac{(ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!})$
188	187 124	breqtrrd	$⊢ (φ \land k \in (((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\})) \to P ∥ (\frac{A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!})$
189	93 49 140 188	fsumdvds	$⊢ φ \to P ∥ \sum_{k \in ((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\}} (\frac{A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!})$
190	189 117	breqtrrd	$⊢ φ \to P ∥ (\frac{\sum_{k \in ((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\}} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!})$
191	49 103 115 142 169 190	etransclem9	$⊢ φ \to (\frac{A (0) (ℝ D^{n} F) (P - 1) (0)}{(P - 1)!}) + (\frac{\sum_{k \in ((0 \dots M) \times (0 \dots M P + P - 1)) ∖ \{⟨0, P - 1⟩\}} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!}) \neq 0$
192	102 191	eqnetrd	$⊢ φ \to K \neq 0$

Metamath Proof Explorer

Theorem etransclem44

Proof