Metamath Proof Explorer

Theorem etransclem44

Description: The given finite sum is nonzero. This is the claim proved after equation (7) in Juillerat p. 12 . (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem44.a ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℤ )
etransclem44.a0 ⊢ ( 𝜑 → ( 𝐴 ‘ 0 ) ≠ 0 )
etransclem44.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
etransclem44.p ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
etransclem44.ap ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 ‘ 0 ) ) < 𝑃 )
etransclem44.mp ⊢ ( 𝜑 → ( ! ‘ 𝑀 ) < 𝑃 )
etransclem44.f ⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) )
etransclem44.k ⊢ 𝐾 = ( Σ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) )
Assertion etransclem44 ( 𝜑 → 𝐾 ≠ 0 )

Proof

Step Hyp Ref Expression
1 etransclem44.a ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℤ )
2 etransclem44.a0 ⊢ ( 𝜑 → ( 𝐴 ‘ 0 ) ≠ 0 )
3 etransclem44.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
4 etransclem44.p ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
5 etransclem44.ap ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 ‘ 0 ) ) < 𝑃 )
6 etransclem44.mp ⊢ ( 𝜑 → ( ! ‘ 𝑀 ) < 𝑃 )
7 etransclem44.f ⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) )
8 etransclem44.k ⊢ 𝐾 = ( Σ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) )
9 8 a1i ⊢ ( 𝜑 → 𝐾 = ( Σ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )
10 nfv ⊢ Ⅎ 𝑘 𝜑
11 nfcv ⊢ Ⅎ 𝑘 ( ( 𝐴 ‘ 0 ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) )
12 fzfi ⊢ ( 0 ... 𝑀 ) ∈ Fin
13 fzfi ⊢ ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ∈ Fin
14 xpfi ⊢ ( ( ( 0 ... 𝑀 ) ∈ Fin ∧ ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ∈ Fin ) → ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∈ Fin )
15 12 13 14 mp2an ⊢ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∈ Fin
16 15 a1i ⊢ ( 𝜑 → ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∈ Fin )
17 1 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ) → 𝐴 : ℕ0 ⟶ ℤ )
18 fzssnn0 ⊢ ( 0 ... 𝑀 ) ⊆ ℕ0
19 xp1st ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) → ( 1st ‘ 𝑘 ) ∈ ( 0 ... 𝑀 ) )
20 18 19 sselid ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) → ( 1st ‘ 𝑘 ) ∈ ℕ0 )
21 20 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ) → ( 1st ‘ 𝑘 ) ∈ ℕ0 )
22 17 21 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ) → ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) ∈ ℤ )
23 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
24 23 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ) → ℝ ∈ { ℝ , ℂ } )
25 reopn ⊢ ℝ ∈ ( topGen ‘ ran (,) )
26 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
27 25 26 eleqtri ⊢ ℝ ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
28 27 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ) → ℝ ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
29 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
30 4 29 syl ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
31 30 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ) → 𝑃 ∈ ℕ )
32 3 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ) → 𝑀 ∈ ℕ0 )
33 xp2nd ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) → ( 2nd ‘ 𝑘 ) ∈ ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) )
34 elfznn0 ⊢ ( ( 2nd ‘ 𝑘 ) ∈ ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) → ( 2nd ‘ 𝑘 ) ∈ ℕ0 )
35 33 34 syl ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) → ( 2nd ‘ 𝑘 ) ∈ ℕ0 )
36 35 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ) → ( 2nd ‘ 𝑘 ) ∈ ℕ0 )
37 21 nn0red ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ) → ( 1st ‘ 𝑘 ) ∈ ℝ )
38 21 nn0zd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ) → ( 1st ‘ 𝑘 ) ∈ ℤ )
39 24 28 31 32 7 36 37 38 etransclem42 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ) → ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ∈ ℤ )
40 22 39 zmulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ) → ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) ∈ ℤ )
41 40 zcnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ) → ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) ∈ ℂ )
42 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
43 3 42 eleqtrdi ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 0 ) )
44 eluzfz1 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 0 ) → 0 ∈ ( 0 ... 𝑀 ) )
45 43 44 syl ⊢ ( 𝜑 → 0 ∈ ( 0 ... 𝑀 ) )
46 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
47 3 nn0zd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
48 30 nnzd ⊢ ( 𝜑 → 𝑃 ∈ ℤ )
49 47 48 zmulcld ⊢ ( 𝜑 → ( 𝑀 · 𝑃 ) ∈ ℤ )
50 nnm1nn0 ⊢ ( 𝑃 ∈ ℕ → ( 𝑃 − 1 ) ∈ ℕ0 )
51 30 50 syl ⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℕ0 )
52 51 nn0zd ⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℤ )
53 49 52 zaddcld ⊢ ( 𝜑 → ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ∈ ℤ )
54 51 nn0ge0d ⊢ ( 𝜑 → 0 ≤ ( 𝑃 − 1 ) )
55 30 nnnn0d ⊢ ( 𝜑 → 𝑃 ∈ ℕ0 )
56 3 55 nn0mulcld ⊢ ( 𝜑 → ( 𝑀 · 𝑃 ) ∈ ℕ0 )
57 56 nn0ge0d ⊢ ( 𝜑 → 0 ≤ ( 𝑀 · 𝑃 ) )
58 51 nn0red ⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℝ )
59 49 zred ⊢ ( 𝜑 → ( 𝑀 · 𝑃 ) ∈ ℝ )
60 58 59 addge02d ⊢ ( 𝜑 → ( 0 ≤ ( 𝑀 · 𝑃 ) ↔ ( 𝑃 − 1 ) ≤ ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) )
61 57 60 mpbid ⊢ ( 𝜑 → ( 𝑃 − 1 ) ≤ ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) )
62 46 53 52 54 61 elfzd ⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) )
63 opelxp ⊢ ( ⟨ 0 , ( 𝑃 − 1 ) ⟩ ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ↔ ( 0 ∈ ( 0 ... 𝑀 ) ∧ ( 𝑃 − 1 ) ∈ ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) )
64 45 62 63 sylanbrc ⊢ ( 𝜑 → ⟨ 0 , ( 𝑃 − 1 ) ⟩ ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) )
65 fveq2 ⊢ ( 𝑘 = ⟨ 0 , ( 𝑃 − 1 ) ⟩ → ( 1st ‘ 𝑘 ) = ( 1st ‘ ⟨ 0 , ( 𝑃 − 1 ) ⟩ ) )
66 0re ⊢ 0 ∈ ℝ
67 ovex ⊢ ( 𝑃 − 1 ) ∈ V
68 op1stg ⊢ ( ( 0 ∈ ℝ ∧ ( 𝑃 − 1 ) ∈ V ) → ( 1st ‘ ⟨ 0 , ( 𝑃 − 1 ) ⟩ ) = 0 )
69 66 67 68 mp2an ⊢ ( 1st ‘ ⟨ 0 , ( 𝑃 − 1 ) ⟩ ) = 0
70 65 69 eqtrdi ⊢ ( 𝑘 = ⟨ 0 , ( 𝑃 − 1 ) ⟩ → ( 1st ‘ 𝑘 ) = 0 )
71 70 fveq2d ⊢ ( 𝑘 = ⟨ 0 , ( 𝑃 − 1 ) ⟩ → ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) = ( 𝐴 ‘ 0 ) )
72 fveq2 ⊢ ( 𝑘 = ⟨ 0 , ( 𝑃 − 1 ) ⟩ → ( 2nd ‘ 𝑘 ) = ( 2nd ‘ ⟨ 0 , ( 𝑃 − 1 ) ⟩ ) )
73 op2ndg ⊢ ( ( 0 ∈ ℝ ∧ ( 𝑃 − 1 ) ∈ V ) → ( 2nd ‘ ⟨ 0 , ( 𝑃 − 1 ) ⟩ ) = ( 𝑃 − 1 ) )
74 66 67 73 mp2an ⊢ ( 2nd ‘ ⟨ 0 , ( 𝑃 − 1 ) ⟩ ) = ( 𝑃 − 1 )
75 72 74 eqtrdi ⊢ ( 𝑘 = ⟨ 0 , ( 𝑃 − 1 ) ⟩ → ( 2nd ‘ 𝑘 ) = ( 𝑃 − 1 ) )
76 75 fveq2d ⊢ ( 𝑘 = ⟨ 0 , ( 𝑃 − 1 ) ⟩ → ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) = ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) )
77 76 70 fveq12d ⊢ ( 𝑘 = ⟨ 0 , ( 𝑃 − 1 ) ⟩ → ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) = ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) )
78 71 77 oveq12d ⊢ ( 𝑘 = ⟨ 0 , ( 𝑃 − 1 ) ⟩ → ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) = ( ( 𝐴 ‘ 0 ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) ) )
79 10 11 16 41 64 78 fsumsplit1 ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) = ( ( ( 𝐴 ‘ 0 ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) ) + Σ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) ) )
80 79 oveq1d ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) = ( ( ( ( 𝐴 ‘ 0 ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) ) + Σ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )
81 18 45 sselid ⊢ ( 𝜑 → 0 ∈ ℕ0 )
82 1 81 ffvelcdmd ⊢ ( 𝜑 → ( 𝐴 ‘ 0 ) ∈ ℤ )
83 23 a1i ⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
84 27 a1i ⊢ ( 𝜑 → ℝ ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
85 66 a1i ⊢ ( 𝜑 → 0 ∈ ℝ )
86 83 84 30 3 7 51 85 46 etransclem42 ⊢ ( 𝜑 → ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) ∈ ℤ )
87 82 86 zmulcld ⊢ ( 𝜑 → ( ( 𝐴 ‘ 0 ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) ) ∈ ℤ )
88 87 zcnd ⊢ ( 𝜑 → ( ( 𝐴 ‘ 0 ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) ) ∈ ℂ )
89 difss ⊢ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ⊆ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) )
90 ssfi ⊢ ( ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∈ Fin ∧ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ⊆ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ) → ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ∈ Fin )
91 15 89 90 mp2an ⊢ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ∈ Fin
92 91 a1i ⊢ ( 𝜑 → ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ∈ Fin )
93 eldifi ⊢ ( 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) → 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) )
94 93 40 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ) → ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) ∈ ℤ )
95 92 94 fsumzcl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) ∈ ℤ )
96 95 zcnd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) ∈ ℂ )
97 51 faccld ⊢ ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℕ )
98 97 nncnd ⊢ ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℂ )
99 97 nnne0d ⊢ ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ≠ 0 )
100 88 96 98 99 divdird ⊢ ( 𝜑 → ( ( ( ( 𝐴 ‘ 0 ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) ) + Σ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) = ( ( ( ( 𝐴 ‘ 0 ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) + ( Σ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ) )
101 9 80 100 3eqtrd ⊢ ( 𝜑 → 𝐾 = ( ( ( ( 𝐴 ‘ 0 ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) + ( Σ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ) )
102 30 nnne0d ⊢ ( 𝜑 → 𝑃 ≠ 0 )
103 82 zcnd ⊢ ( 𝜑 → ( 𝐴 ‘ 0 ) ∈ ℂ )
104 86 zcnd ⊢ ( 𝜑 → ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) ∈ ℂ )
105 103 104 98 99 divassd ⊢ ( 𝜑 → ( ( ( 𝐴 ‘ 0 ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) = ( ( 𝐴 ‘ 0 ) · ( ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ) )
106 etransclem5 ⊢ ( 𝑘 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑦 ∈ ℝ ↦ ( ( 𝑦 − 𝑘 ) ↑ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ) = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ ℝ ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
107 etransclem11 ⊢ ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) = ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑛 } )
108 83 84 30 3 7 51 106 107 45 85 etransclem37 ⊢ ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ∥ ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) )
109 97 nnzd ⊢ ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℤ )
110 dvdsval2 ⊢ ( ( ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℤ ∧ ( ! ‘ ( 𝑃 − 1 ) ) ≠ 0 ∧ ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) ∈ ℤ ) → ( ( ! ‘ ( 𝑃 − 1 ) ) ∥ ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) ↔ ( ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ∈ ℤ ) )
111 109 99 86 110 syl3anc ⊢ ( 𝜑 → ( ( ! ‘ ( 𝑃 − 1 ) ) ∥ ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) ↔ ( ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ∈ ℤ ) )
112 108 111 mpbid ⊢ ( 𝜑 → ( ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ∈ ℤ )
113 82 112 zmulcld ⊢ ( 𝜑 → ( ( 𝐴 ‘ 0 ) · ( ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ) ∈ ℤ )
114 105 113 eqeltrd ⊢ ( 𝜑 → ( ( ( 𝐴 ‘ 0 ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ∈ ℤ )
115 93 41 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ) → ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) ∈ ℂ )
116 92 98 115 99 fsumdivc ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) = Σ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ( ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )
117 22 zcnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ) → ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) ∈ ℂ )
118 93 117 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ) → ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) ∈ ℂ )
119 93 39 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ) → ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ∈ ℤ )
120 119 zcnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ) → ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ∈ ℂ )
121 98 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ) → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℂ )
122 99 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ) → ( ! ‘ ( 𝑃 − 1 ) ) ≠ 0 )
123 118 120 121 122 divassd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ) → ( ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) = ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ) )
124 93 22 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ) → ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) ∈ ℤ )
125 23 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ) → ℝ ∈ { ℝ , ℂ } )
126 27 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ) → ℝ ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
127 30 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ) → 𝑃 ∈ ℕ )
128 3 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ) → 𝑀 ∈ ℕ0 )
129 93 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ) → 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) )
130 129 35 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ) → ( 2nd ‘ 𝑘 ) ∈ ℕ0 )
131 129 19 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ) → ( 1st ‘ 𝑘 ) ∈ ( 0 ... 𝑀 ) )
132 93 37 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ) → ( 1st ‘ 𝑘 ) ∈ ℝ )
133 125 126 127 128 7 130 106 107 131 132 etransclem37 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ) → ( ! ‘ ( 𝑃 − 1 ) ) ∥ ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) )
134 109 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ) → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℤ )
135 dvdsval2 ⊢ ( ( ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℤ ∧ ( ! ‘ ( 𝑃 − 1 ) ) ≠ 0 ∧ ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ∈ ℤ ) → ( ( ! ‘ ( 𝑃 − 1 ) ) ∥ ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ↔ ( ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ∈ ℤ ) )
136 134 122 119 135 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ) → ( ( ! ‘ ( 𝑃 − 1 ) ) ∥ ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ↔ ( ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ∈ ℤ ) )
137 133 136 mpbid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ) → ( ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ∈ ℤ )
138 124 137 zmulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ) → ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ) ∈ ℤ )
139 123 138 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ) → ( ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ∈ ℤ )
140 92 139 fsumzcl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ( ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ∈ ℤ )
141 116 140 eqeltrd ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ∈ ℤ )
142 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
143 zabscl ⊢ ( ( 𝐴 ‘ 0 ) ∈ ℤ → ( abs ‘ ( 𝐴 ‘ 0 ) ) ∈ ℤ )
144 82 143 syl ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 ‘ 0 ) ) ∈ ℤ )
145 nn0abscl ⊢ ( ( 𝐴 ‘ 0 ) ∈ ℤ → ( abs ‘ ( 𝐴 ‘ 0 ) ) ∈ ℕ0 )
146 82 145 syl ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 ‘ 0 ) ) ∈ ℕ0 )
147 103 2 absne0d ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 ‘ 0 ) ) ≠ 0 )
148 elnnne0 ⊢ ( ( abs ‘ ( 𝐴 ‘ 0 ) ) ∈ ℕ ↔ ( ( abs ‘ ( 𝐴 ‘ 0 ) ) ∈ ℕ0 ∧ ( abs ‘ ( 𝐴 ‘ 0 ) ) ≠ 0 ) )
149 146 147 148 sylanbrc ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 ‘ 0 ) ) ∈ ℕ )
150 149 nnge1d ⊢ ( 𝜑 → 1 ≤ ( abs ‘ ( 𝐴 ‘ 0 ) ) )
151 zltlem1 ⊢ ( ( ( abs ‘ ( 𝐴 ‘ 0 ) ) ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( abs ‘ ( 𝐴 ‘ 0 ) ) < 𝑃 ↔ ( abs ‘ ( 𝐴 ‘ 0 ) ) ≤ ( 𝑃 − 1 ) ) )
152 144 48 151 syl2anc ⊢ ( 𝜑 → ( ( abs ‘ ( 𝐴 ‘ 0 ) ) < 𝑃 ↔ ( abs ‘ ( 𝐴 ‘ 0 ) ) ≤ ( 𝑃 − 1 ) ) )
153 5 152 mpbid ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 ‘ 0 ) ) ≤ ( 𝑃 − 1 ) )
154 142 52 144 150 153 elfzd ⊢ ( 𝜑 → ( abs ‘ ( 𝐴 ‘ 0 ) ) ∈ ( 1 ... ( 𝑃 − 1 ) ) )
155 fzm1ndvds ⊢ ( ( 𝑃 ∈ ℕ ∧ ( abs ‘ ( 𝐴 ‘ 0 ) ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ¬ 𝑃 ∥ ( abs ‘ ( 𝐴 ‘ 0 ) ) )
156 30 154 155 syl2anc ⊢ ( 𝜑 → ¬ 𝑃 ∥ ( abs ‘ ( 𝐴 ‘ 0 ) ) )
157 dvdsabsb ⊢ ( ( 𝑃 ∈ ℤ ∧ ( 𝐴 ‘ 0 ) ∈ ℤ ) → ( 𝑃 ∥ ( 𝐴 ‘ 0 ) ↔ 𝑃 ∥ ( abs ‘ ( 𝐴 ‘ 0 ) ) ) )
158 48 82 157 syl2anc ⊢ ( 𝜑 → ( 𝑃 ∥ ( 𝐴 ‘ 0 ) ↔ 𝑃 ∥ ( abs ‘ ( 𝐴 ‘ 0 ) ) ) )
159 156 158 mtbird ⊢ ( 𝜑 → ¬ 𝑃 ∥ ( 𝐴 ‘ 0 ) )
160 3 4 6 7 etransclem41 ⊢ ( 𝜑 → ¬ 𝑃 ∥ ( ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )
161 159 160 jca ⊢ ( 𝜑 → ( ¬ 𝑃 ∥ ( 𝐴 ‘ 0 ) ∧ ¬ 𝑃 ∥ ( ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ) )
162 pm4.56 ⊢ ( ( ¬ 𝑃 ∥ ( 𝐴 ‘ 0 ) ∧ ¬ 𝑃 ∥ ( ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ) ↔ ¬ ( 𝑃 ∥ ( 𝐴 ‘ 0 ) ∨ 𝑃 ∥ ( ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ) )
163 161 162 sylib ⊢ ( 𝜑 → ¬ ( 𝑃 ∥ ( 𝐴 ‘ 0 ) ∨ 𝑃 ∥ ( ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ) )
164 euclemma ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ‘ 0 ) ∈ ℤ ∧ ( ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ∈ ℤ ) → ( 𝑃 ∥ ( ( 𝐴 ‘ 0 ) · ( ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ) ↔ ( 𝑃 ∥ ( 𝐴 ‘ 0 ) ∨ 𝑃 ∥ ( ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ) ) )
165 4 82 112 164 syl3anc ⊢ ( 𝜑 → ( 𝑃 ∥ ( ( 𝐴 ‘ 0 ) · ( ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ) ↔ ( 𝑃 ∥ ( 𝐴 ‘ 0 ) ∨ 𝑃 ∥ ( ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ) ) )
166 163 165 mtbird ⊢ ( 𝜑 → ¬ 𝑃 ∥ ( ( 𝐴 ‘ 0 ) · ( ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ) )
167 105 breq2d ⊢ ( 𝜑 → ( 𝑃 ∥ ( ( ( 𝐴 ‘ 0 ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ↔ 𝑃 ∥ ( ( 𝐴 ‘ 0 ) · ( ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ) ) )
168 166 167 mtbird ⊢ ( 𝜑 → ¬ 𝑃 ∥ ( ( ( 𝐴 ‘ 0 ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )
169 48 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ) → 𝑃 ∈ ℤ )
170 169 124 137 3jca ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ) → ( 𝑃 ∈ ℤ ∧ ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) ∈ ℤ ∧ ( ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ∈ ℤ ) )
171 eldifn ⊢ ( 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) → ¬ 𝑘 ∈ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } )
172 93 adantr ⊢ ( ( 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ∧ ( ( 2nd ‘ 𝑘 ) = ( 𝑃 − 1 ) ∧ ( 1st ‘ 𝑘 ) = 0 ) ) → 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) )
173 1st2nd2 ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) → 𝑘 = ⟨ ( 1st ‘ 𝑘 ) , ( 2nd ‘ 𝑘 ) ⟩ )
174 172 173 syl ⊢ ( ( 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ∧ ( ( 2nd ‘ 𝑘 ) = ( 𝑃 − 1 ) ∧ ( 1st ‘ 𝑘 ) = 0 ) ) → 𝑘 = ⟨ ( 1st ‘ 𝑘 ) , ( 2nd ‘ 𝑘 ) ⟩ )
175 simpr ⊢ ( ( ( 2nd ‘ 𝑘 ) = ( 𝑃 − 1 ) ∧ ( 1st ‘ 𝑘 ) = 0 ) → ( 1st ‘ 𝑘 ) = 0 )
176 simpl ⊢ ( ( ( 2nd ‘ 𝑘 ) = ( 𝑃 − 1 ) ∧ ( 1st ‘ 𝑘 ) = 0 ) → ( 2nd ‘ 𝑘 ) = ( 𝑃 − 1 ) )
177 175 176 opeq12d ⊢ ( ( ( 2nd ‘ 𝑘 ) = ( 𝑃 − 1 ) ∧ ( 1st ‘ 𝑘 ) = 0 ) → ⟨ ( 1st ‘ 𝑘 ) , ( 2nd ‘ 𝑘 ) ⟩ = ⟨ 0 , ( 𝑃 − 1 ) ⟩ )
178 177 adantl ⊢ ( ( 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ∧ ( ( 2nd ‘ 𝑘 ) = ( 𝑃 − 1 ) ∧ ( 1st ‘ 𝑘 ) = 0 ) ) → ⟨ ( 1st ‘ 𝑘 ) , ( 2nd ‘ 𝑘 ) ⟩ = ⟨ 0 , ( 𝑃 − 1 ) ⟩ )
179 174 178 eqtrd ⊢ ( ( 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ∧ ( ( 2nd ‘ 𝑘 ) = ( 𝑃 − 1 ) ∧ ( 1st ‘ 𝑘 ) = 0 ) ) → 𝑘 = ⟨ 0 , ( 𝑃 − 1 ) ⟩ )
180 velsn ⊢ ( 𝑘 ∈ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ↔ 𝑘 = ⟨ 0 , ( 𝑃 − 1 ) ⟩ )
181 179 180 sylibr ⊢ ( ( 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ∧ ( ( 2nd ‘ 𝑘 ) = ( 𝑃 − 1 ) ∧ ( 1st ‘ 𝑘 ) = 0 ) ) → 𝑘 ∈ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } )
182 171 181 mtand ⊢ ( 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) → ¬ ( ( 2nd ‘ 𝑘 ) = ( 𝑃 − 1 ) ∧ ( 1st ‘ 𝑘 ) = 0 ) )
183 182 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ) → ¬ ( ( 2nd ‘ 𝑘 ) = ( 𝑃 − 1 ) ∧ ( 1st ‘ 𝑘 ) = 0 ) )
184 127 128 7 130 131 183 107 etransclem38 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ) → 𝑃 ∥ ( ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )
185 dvdsmultr2 ⊢ ( ( 𝑃 ∈ ℤ ∧ ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) ∈ ℤ ∧ ( ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ∈ ℤ ) → ( 𝑃 ∥ ( ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) → 𝑃 ∥ ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ) ) )
186 170 184 185 sylc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ) → 𝑃 ∥ ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ) )
187 186 123 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ) → 𝑃 ∥ ( ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )
188 92 48 139 187 fsumdvds ⊢ ( 𝜑 → 𝑃 ∥ Σ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ( ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )
189 188 116 breqtrrd ⊢ ( 𝜑 → 𝑃 ∥ ( Σ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )
190 48 102 114 141 168 189 etransclem9 ⊢ ( 𝜑 → ( ( ( ( 𝐴 ‘ 0 ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 𝑃 − 1 ) ) ‘ 0 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) + ( Σ 𝑘 ∈ ( ( ( 0 ... 𝑀 ) × ( 0 ... ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) ) ∖ { ⟨ 0 , ( 𝑃 − 1 ) ⟩ } ) ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ) ≠ 0 )
191 101 190 eqnetrd ⊢ ( 𝜑 → 𝐾 ≠ 0 )