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 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 sseldi ( 𝜑 → 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 )