Metamath Proof Explorer


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 φ M 0
etransclem41.p φ P
etransclem41.mp φ M ! < P
etransclem41.f F = x x P 1 j = 1 M x j P
Assertion etransclem41 φ ¬ P D n F P 1 0 P 1 !

Proof

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