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