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 ) ) ) )