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

Metamath Proof Explorer

Theorem etransclem44

Proof