etransclem41

Description: P does not divide the P-1 -th derivative of F applied to 0 . This is the first part of case 2: proven in in Juillerat p. 13 . (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	etransclem41.m	$⊢ φ \to M \in ℕ_{0}$
	etransclem41.p	$⊢ φ \to P \in ℙ$
	etransclem41.mp	$⊢ φ \to M! < P$
	etransclem41.f	$⊢ F = (x \in ℝ ⟼ x^{P - 1} \prod_{j = 1}^{M} {(x - j)}^{P})$
Assertion	etransclem41	$⊢ φ \to \neg P ∥ (\frac{(ℝ D^{n} F) (P - 1) (0)}{(P - 1)!})$

Proof

Step	Hyp	Ref	Expression
1		etransclem41.m	$⊢ φ \to M \in ℕ_{0}$
2		etransclem41.p	$⊢ φ \to P \in ℙ$
3		etransclem41.mp	$⊢ φ \to M! < P$
4		etransclem41.f	$⊢ F = (x \in ℝ ⟼ x^{P - 1} \prod_{j = 1}^{M} {(x - j)}^{P})$
5	1	faccld	$⊢ φ \to M! \in ℕ$
6	5	nnred	$⊢ φ \to M! \in ℝ$
7		prmnn	$⊢ P \in ℙ \to P \in ℕ$
8	2 7	syl	$⊢ φ \to P \in ℕ$
9	8	nnred	$⊢ φ \to P \in ℝ$
10	6 9	ltnled	$⊢ φ \to (M! < P \leftrightarrow \neg P \leq M!)$
11	3 10	mpbid	$⊢ φ \to \neg P \leq M!$
12	8	nnzd	$⊢ φ \to P \in ℤ$
13	12 5	jca	$⊢ φ \to (P \in ℤ \land M! \in ℕ)$
14	13	adantr	$⊢ (φ \land P ∥ M!) \to (P \in ℤ \land M! \in ℕ)$
15		simpr	$⊢ (φ \land P ∥ M!) \to P ∥ M!$
16		dvdsle	$⊢ (P \in ℤ \land M! \in ℕ) \to (P ∥ M! \to P \leq M!)$
17	14 15 16	sylc	$⊢ (φ \land P ∥ M!) \to P \leq M!$
18	11 17	mtand	$⊢ φ \to \neg P ∥ M!$
19		fzfid	$⊢ ⊤ \to (1 \dots M) \in Fin$
20		elfzelz	$⊢ j \in (1 \dots M) \to j \in ℤ$
21	20	znegcld	$⊢ j \in (1 \dots M) \to - j \in ℤ$
22	21	zcnd	$⊢ j \in (1 \dots M) \to - j \in ℂ$
23	22	adantl	$⊢ (⊤ \land j \in (1 \dots M)) \to - j \in ℂ$
24	19 23	fprodabs2	$⊢ ⊤ \to \|\prod_{j = 1}^{M} (- j)\| = \prod_{j = 1}^{M} \|- j\|$
25	24	mptru	$⊢ \|\prod_{j = 1}^{M} (- j)\| = \prod_{j = 1}^{M} \|- j\|$
26	20	zcnd	$⊢ j \in (1 \dots M) \to j \in ℂ$
27	26	absnegd	$⊢ j \in (1 \dots M) \to \|- j\| = \|j\|$
28	20	zred	$⊢ j \in (1 \dots M) \to j \in ℝ$
29		0red	$⊢ j \in (1 \dots M) \to 0 \in ℝ$
30		1red	$⊢ j \in (1 \dots M) \to 1 \in ℝ$
31		0lt1	$⊢ 0 < 1$
32	31	a1i	$⊢ j \in (1 \dots M) \to 0 < 1$
33		elfzle1	$⊢ j \in (1 \dots M) \to 1 \leq j$
34	29 30 28 32 33	ltletrd	$⊢ j \in (1 \dots M) \to 0 < j$
35	29 28 34	ltled	$⊢ j \in (1 \dots M) \to 0 \leq j$
36	28 35	absidd	$⊢ j \in (1 \dots M) \to \|j\| = j$
37	27 36	eqtrd	$⊢ j \in (1 \dots M) \to \|- j\| = j$
38	37	prodeq2i	$⊢ \prod_{j = 1}^{M} \|- j\| = \prod_{j = 1}^{M} j$
39	25 38	eqtri	$⊢ \|\prod_{j = 1}^{M} (- j)\| = \prod_{j = 1}^{M} j$
40		fprodfac	$⊢ M \in ℕ_{0} \to M! = \prod_{j = 1}^{M} j$
41	1 40	syl	$⊢ φ \to M! = \prod_{j = 1}^{M} j$
42	39 41	eqtr4id	$⊢ φ \to \|\prod_{j = 1}^{M} (- j)\| = M!$
43	42	breq2d	$⊢ φ \to (P ∥ \|\prod_{j = 1}^{M} (- j)\| \leftrightarrow P ∥ M!)$
44	18 43	mtbird	$⊢ φ \to \neg P ∥ \|\prod_{j = 1}^{M} (- j)\|$
45		fzfid	$⊢ φ \to (1 \dots M) \in Fin$
46	21	adantl	$⊢ (φ \land j \in (1 \dots M)) \to - j \in ℤ$
47	45 46	fprodzcl	$⊢ φ \to \prod_{j = 1}^{M} (- j) \in ℤ$
48		dvdsabsb	$⊢ (P \in ℤ \land \prod_{j = 1}^{M} (- j) \in ℤ) \to (P ∥ \prod_{j = 1}^{M} (- j) \leftrightarrow P ∥ \|\prod_{j = 1}^{M} (- j)\|)$
49	12 47 48	syl2anc	$⊢ φ \to (P ∥ \prod_{j = 1}^{M} (- j) \leftrightarrow P ∥ \|\prod_{j = 1}^{M} (- j)\|)$
50	44 49	mtbird	$⊢ φ \to \neg P ∥ \prod_{j = 1}^{M} (- j)$
51		prmdvdsexp	$⊢ (P \in ℙ \land \prod_{j = 1}^{M} (- j) \in ℤ \land P \in ℕ) \to (P ∥ {\prod_{j = 1}^{M} (- j)}^{P} \leftrightarrow P ∥ \prod_{j = 1}^{M} (- j))$
52	2 47 8 51	syl3anc	$⊢ φ \to (P ∥ {\prod_{j = 1}^{M} (- j)}^{P} \leftrightarrow P ∥ \prod_{j = 1}^{M} (- j))$
53	50 52	mtbird	$⊢ φ \to \neg P ∥ {\prod_{j = 1}^{M} (- j)}^{P}$
54		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\})$
55		eqeq1	$⊢ k = j \to (k = 0 \leftrightarrow j = 0)$
56	55	ifbid	$⊢ k = j \to if (k = 0, P - 1, 0) = if (j = 0, P - 1, 0)$
57	56	cbvmptv	$⊢ (k \in (0 \dots M) ⟼ if (k = 0, P - 1, 0)) = (j \in (0 \dots M) ⟼ if (j = 0, P - 1, 0))$
58	8 1 4 54 57	etransclem35	$⊢ φ \to (ℝ D^{n} F) (P - 1) (0) = (P - 1)! {\prod_{j = 1}^{M} (- j)}^{P}$
59	58	oveq1d	$⊢ φ \to \frac{(ℝ D^{n} F) (P - 1) (0)}{(P - 1)!} = \frac{(P - 1)! {\prod_{j = 1}^{M} (- j)}^{P}}{(P - 1)!}$
60	22	adantl	$⊢ (φ \land j \in (1 \dots M)) \to - j \in ℂ$
61	45 60	fprodcl	$⊢ φ \to \prod_{j = 1}^{M} (- j) \in ℂ$
62	8	nnnn0d	$⊢ φ \to P \in ℕ_{0}$
63	61 62	expcld	$⊢ φ \to {\prod_{j = 1}^{M} (- j)}^{P} \in ℂ$
64		nnm1nn0	$⊢ P \in ℕ \to P - 1 \in ℕ_{0}$
65	8 64	syl	$⊢ φ \to P - 1 \in ℕ_{0}$
66	65	faccld	$⊢ φ \to (P - 1)! \in ℕ$
67	66	nncnd	$⊢ φ \to (P - 1)! \in ℂ$
68	66	nnne0d	$⊢ φ \to (P - 1)! \neq 0$
69	63 67 68	divcan3d	$⊢ φ \to \frac{(P - 1)! {\prod_{j = 1}^{M} (- j)}^{P}}{(P - 1)!} = {\prod_{j = 1}^{M} (- j)}^{P}$
70	59 69	eqtrd	$⊢ φ \to \frac{(ℝ D^{n} F) (P - 1) (0)}{(P - 1)!} = {\prod_{j = 1}^{M} (- j)}^{P}$
71	70	breq2d	$⊢ φ \to (P ∥ (\frac{(ℝ D^{n} F) (P - 1) (0)}{(P - 1)!}) \leftrightarrow P ∥ {\prod_{j = 1}^{M} (- j)}^{P})$
72	53 71	mtbird	$⊢ φ \to \neg P ∥ (\frac{(ℝ D^{n} F) (P - 1) (0)}{(P - 1)!})$

Metamath Proof Explorer

Theorem etransclem41

Proof