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 ( 𝜑𝑀 ∈ ℕ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 ) ) ) )