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