Theorem 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	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
	etransclem41.p	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
	etransclem41.mp	⊢ ( 𝜑 → ( ! ‘ 𝑀 ) < 𝑃 )
	etransclem41.f	⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) )
Assertion	etransclem41	⊢ ( 𝜑 → ¬ 𝑃 ∥ ( ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		etransclem41.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
2		etransclem41.p	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
3		etransclem41.mp	⊢ ( 𝜑 → ( ! ‘ 𝑀 ) < 𝑃 )
4		etransclem41.f	⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) )
5	1	faccld	⊢ ( 𝜑 → ( ! ‘ 𝑀 ) ∈ ℕ )
6	5	nnred	⊢ ( 𝜑 → ( ! ‘ 𝑀 ) ∈ ℝ )
7		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
8	2 7	syl	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
9	8	nnred	⊢ ( 𝜑 → 𝑃 ∈ ℝ )
10	6 9	ltnled	⊢ ( 𝜑 → ( ( ! ‘ 𝑀 ) < 𝑃 ↔ ¬ 𝑃 ≤ ( ! ‘ 𝑀 ) ) )
11	3 10	mpbid	⊢ ( 𝜑 → ¬ 𝑃 ≤ ( ! ‘ 𝑀 ) )
12	8	nnzd	⊢ ( 𝜑 → 𝑃 ∈ ℤ )
13	12 5	jca	⊢ ( 𝜑 → ( 𝑃 ∈ ℤ ∧ ( ! ‘ 𝑀 ) ∈ ℕ ) )
14	13	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ! ‘ 𝑀 ) ) → ( 𝑃 ∈ ℤ ∧ ( ! ‘ 𝑀 ) ∈ ℕ ) )
15		simpr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ! ‘ 𝑀 ) ) → 𝑃 ∥ ( ! ‘ 𝑀 ) )
16		dvdsle	⊢ ( ( 𝑃 ∈ ℤ ∧ ( ! ‘ 𝑀 ) ∈ ℕ ) → ( 𝑃 ∥ ( ! ‘ 𝑀 ) → 𝑃 ≤ ( ! ‘ 𝑀 ) ) )
17	14 15 16	sylc	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ! ‘ 𝑀 ) ) → 𝑃 ≤ ( ! ‘ 𝑀 ) )
18	11 17	mtand	⊢ ( 𝜑 → ¬ 𝑃 ∥ ( ! ‘ 𝑀 ) )
19		fzfid	⊢ ( ⊤ → ( 1 ... 𝑀 ) ∈ Fin )
20		elfzelz	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 𝑗 ∈ ℤ )
21	20	znegcld	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → - 𝑗 ∈ ℤ )
22	21	zcnd	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → - 𝑗 ∈ ℂ )
23	22	adantl	⊢ ( ( ⊤ ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → - 𝑗 ∈ ℂ )
24	19 23	fprodabs2	⊢ ( ⊤ → ( abs ‘ ∏ 𝑗 ∈ ( 1 ... 𝑀 ) - 𝑗 ) = ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( abs ‘ - 𝑗 ) )
25	24	mptru	⊢ ( abs ‘ ∏ 𝑗 ∈ ( 1 ... 𝑀 ) - 𝑗 ) = ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( abs ‘ - 𝑗 )
26	20	zcnd	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 𝑗 ∈ ℂ )
27	26	absnegd	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → ( abs ‘ - 𝑗 ) = ( abs ‘ 𝑗 ) )
28	20	zred	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 𝑗 ∈ ℝ )
29		0red	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 0 ∈ ℝ )
30		1red	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 1 ∈ ℝ )
31		0lt1	⊢ 0 < 1
32	31	a1i	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 0 < 1 )
33		elfzle1	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 1 ≤ 𝑗 )
34	29 30 28 32 33	ltletrd	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 0 < 𝑗 )
35	29 28 34	ltled	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 0 ≤ 𝑗 )
36	28 35	absidd	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → ( abs ‘ 𝑗 ) = 𝑗 )
37	27 36	eqtrd	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → ( abs ‘ - 𝑗 ) = 𝑗 )
38	37	prodeq2i	⊢ ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( abs ‘ - 𝑗 ) = ∏ 𝑗 ∈ ( 1 ... 𝑀 ) 𝑗
39	25 38	eqtri	⊢ ( abs ‘ ∏ 𝑗 ∈ ( 1 ... 𝑀 ) - 𝑗 ) = ∏ 𝑗 ∈ ( 1 ... 𝑀 ) 𝑗
40		fprodfac	⊢ ( 𝑀 ∈ ℕ0 → ( ! ‘ 𝑀 ) = ∏ 𝑗 ∈ ( 1 ... 𝑀 ) 𝑗 )
41	1 40	syl	⊢ ( 𝜑 → ( ! ‘ 𝑀 ) = ∏ 𝑗 ∈ ( 1 ... 𝑀 ) 𝑗 )
42	39 41	eqtr4id	⊢ ( 𝜑 → ( abs ‘ ∏ 𝑗 ∈ ( 1 ... 𝑀 ) - 𝑗 ) = ( ! ‘ 𝑀 ) )
43	42	breq2d	⊢ ( 𝜑 → ( 𝑃 ∥ ( abs ‘ ∏ 𝑗 ∈ ( 1 ... 𝑀 ) - 𝑗 ) ↔ 𝑃 ∥ ( ! ‘ 𝑀 ) ) )
44	18 43	mtbird	⊢ ( 𝜑 → ¬ 𝑃 ∥ ( abs ‘ ∏ 𝑗 ∈ ( 1 ... 𝑀 ) - 𝑗 ) )
45		fzfid	⊢ ( 𝜑 → ( 1 ... 𝑀 ) ∈ Fin )
46	21	adantl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → - 𝑗 ∈ ℤ )
47	45 46	fprodzcl	⊢ ( 𝜑 → ∏ 𝑗 ∈ ( 1 ... 𝑀 ) - 𝑗 ∈ ℤ )
48		dvdsabsb	⊢ ( ( 𝑃 ∈ ℤ ∧ ∏ 𝑗 ∈ ( 1 ... 𝑀 ) - 𝑗 ∈ ℤ ) → ( 𝑃 ∥ ∏ 𝑗 ∈ ( 1 ... 𝑀 ) - 𝑗 ↔ 𝑃 ∥ ( abs ‘ ∏ 𝑗 ∈ ( 1 ... 𝑀 ) - 𝑗 ) ) )
49	12 47 48	syl2anc	⊢ ( 𝜑 → ( 𝑃 ∥ ∏ 𝑗 ∈ ( 1 ... 𝑀 ) - 𝑗 ↔ 𝑃 ∥ ( abs ‘ ∏ 𝑗 ∈ ( 1 ... 𝑀 ) - 𝑗 ) ) )
50	44 49	mtbird	⊢ ( 𝜑 → ¬ 𝑃 ∥ ∏ 𝑗 ∈ ( 1 ... 𝑀 ) - 𝑗 )
51		prmdvdsexp	⊢ ( ( 𝑃 ∈ ℙ ∧ ∏ 𝑗 ∈ ( 1 ... 𝑀 ) - 𝑗 ∈ ℤ ∧ 𝑃 ∈ ℕ ) → ( 𝑃 ∥ ( ∏ 𝑗 ∈ ( 1 ... 𝑀 ) - 𝑗 ↑ 𝑃 ) ↔ 𝑃 ∥ ∏ 𝑗 ∈ ( 1 ... 𝑀 ) - 𝑗 ) )
52	2 47 8 51	syl3anc	⊢ ( 𝜑 → ( 𝑃 ∥ ( ∏ 𝑗 ∈ ( 1 ... 𝑀 ) - 𝑗 ↑ 𝑃 ) ↔ 𝑃 ∥ ∏ 𝑗 ∈ ( 1 ... 𝑀 ) - 𝑗 ) )
53	50 52	mtbird	⊢ ( 𝜑 → ¬ 𝑃 ∥ ( ∏ 𝑗 ∈ ( 1 ... 𝑀 ) - 𝑗 ↑ 𝑃 ) )
54		etransclem11	⊢ ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) = ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑛 } )
55		eqeq1	⊢ ( 𝑘 = 𝑗 → ( 𝑘 = 0 ↔ 𝑗 = 0 ) )
56	55	ifbid	⊢ ( 𝑘 = 𝑗 → if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 0 ) = if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 0 ) )
57	56	cbvmptv	⊢ ( 𝑘 ∈ ( 0 ... 𝑀 ) ↦ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 0 ) ) = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 0 ) )
58	8 1 4 54 57	etransclem35	⊢ ( 𝜑 → ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) = ( ( ! ‘ ( 𝑃 − 1 ) ) · ( ∏ 𝑗 ∈ ( 1 ... 𝑀 ) - 𝑗 ↑ 𝑃 ) ) )
59	58	oveq1d	⊢ ( 𝜑 → ( ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) / ( ! ‘ ( 𝑃 − 1 ) ) ) = ( ( ( ! ‘ ( 𝑃 − 1 ) ) · ( ∏ 𝑗 ∈ ( 1 ... 𝑀 ) - 𝑗 ↑ 𝑃 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )
60	22	adantl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → - 𝑗 ∈ ℂ )
61	45 60	fprodcl	⊢ ( 𝜑 → ∏ 𝑗 ∈ ( 1 ... 𝑀 ) - 𝑗 ∈ ℂ )
62	8	nnnn0d	⊢ ( 𝜑 → 𝑃 ∈ ℕ0 )
63	61 62	expcld	⊢ ( 𝜑 → ( ∏ 𝑗 ∈ ( 1 ... 𝑀 ) - 𝑗 ↑ 𝑃 ) ∈ ℂ )
64		nnm1nn0	⊢ ( 𝑃 ∈ ℕ → ( 𝑃 − 1 ) ∈ ℕ0 )
65	8 64	syl	⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℕ0 )
66	65	faccld	⊢ ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℕ )
67	66	nncnd	⊢ ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℂ )
68	66	nnne0d	⊢ ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ≠ 0 )
69	63 67 68	divcan3d	⊢ ( 𝜑 → ( ( ( ! ‘ ( 𝑃 − 1 ) ) · ( ∏ 𝑗 ∈ ( 1 ... 𝑀 ) - 𝑗 ↑ 𝑃 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) = ( ∏ 𝑗 ∈ ( 1 ... 𝑀 ) - 𝑗 ↑ 𝑃 ) )
70	59 69	eqtrd	⊢ ( 𝜑 → ( ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) / ( ! ‘ ( 𝑃 − 1 ) ) ) = ( ∏ 𝑗 ∈ ( 1 ... 𝑀 ) - 𝑗 ↑ 𝑃 ) )
71	70	breq2d	⊢ ( 𝜑 → ( 𝑃 ∥ ( ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ↔ 𝑃 ∥ ( ∏ 𝑗 ∈ ( 1 ... 𝑀 ) - 𝑗 ↑ 𝑃 ) ) )
72	53 71	mtbird	⊢ ( 𝜑 → ¬ 𝑃 ∥ ( ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )