Metamath Proof Explorer

Theorem etransclem45

Description: K is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020)

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

Proof

Step Hyp Ref Expression
1 etransclem45.p ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
2 etransclem45.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
3 etransclem45.f ⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) )
4 etransclem45.a ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℤ )
5 etransclem45.k ⊢ 𝐾 = ( Σ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... 𝑅 ) ) ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) )
6 fzfi ⊢ ( 0 ... 𝑀 ) ∈ Fin
7 fzfi ⊢ ( 0 ... 𝑅 ) ∈ Fin
8 xpfi ⊢ ( ( ( 0 ... 𝑀 ) ∈ Fin ∧ ( 0 ... 𝑅 ) ∈ Fin ) → ( ( 0 ... 𝑀 ) × ( 0 ... 𝑅 ) ) ∈ Fin )
9 6 7 8 mp2an ⊢ ( ( 0 ... 𝑀 ) × ( 0 ... 𝑅 ) ) ∈ Fin
10 9 a1i ⊢ ( 𝜑 → ( ( 0 ... 𝑀 ) × ( 0 ... 𝑅 ) ) ∈ Fin )
11 nnm1nn0 ⊢ ( 𝑃 ∈ ℕ → ( 𝑃 − 1 ) ∈ ℕ0 )
12 1 11 syl ⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℕ0 )
13 12 faccld ⊢ ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℕ )
14 13 nncnd ⊢ ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℂ )
15 4 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... 𝑅 ) ) ) → 𝐴 : ℕ0 ⟶ ℤ )
16 xp1st ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... 𝑅 ) ) → ( 1st ‘ 𝑘 ) ∈ ( 0 ... 𝑀 ) )
17 elfznn0 ⊢ ( ( 1st ‘ 𝑘 ) ∈ ( 0 ... 𝑀 ) → ( 1st ‘ 𝑘 ) ∈ ℕ0 )
18 16 17 syl ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... 𝑅 ) ) → ( 1st ‘ 𝑘 ) ∈ ℕ0 )
19 18 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... 𝑅 ) ) ) → ( 1st ‘ 𝑘 ) ∈ ℕ0 )
20 15 19 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... 𝑅 ) ) ) → ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) ∈ ℤ )
21 20 zcnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... 𝑅 ) ) ) → ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) ∈ ℂ )
22 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
23 22 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... 𝑅 ) ) ) → ℝ ∈ { ℝ , ℂ } )
24 reopn ⊢ ℝ ∈ ( topGen ‘ ran (,) )
25 tgioo4 ⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
26 24 25 eleqtri ⊢ ℝ ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
27 26 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... 𝑅 ) ) ) → ℝ ∈ ( ( TopOpen ‘ ℂfld ) ↾t ℝ ) )
28 1 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... 𝑅 ) ) ) → 𝑃 ∈ ℕ )
29 2 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... 𝑅 ) ) ) → 𝑀 ∈ ℕ0 )
30 xp2nd ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... 𝑅 ) ) → ( 2nd ‘ 𝑘 ) ∈ ( 0 ... 𝑅 ) )
31 elfznn0 ⊢ ( ( 2nd ‘ 𝑘 ) ∈ ( 0 ... 𝑅 ) → ( 2nd ‘ 𝑘 ) ∈ ℕ0 )
32 30 31 syl ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... 𝑅 ) ) → ( 2nd ‘ 𝑘 ) ∈ ℕ0 )
33 32 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... 𝑅 ) ) ) → ( 2nd ‘ 𝑘 ) ∈ ℕ0 )
34 23 27 28 29 3 33 etransclem33 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... 𝑅 ) ) ) → ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) : ℝ ⟶ ℂ )
35 19 nn0red ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... 𝑅 ) ) ) → ( 1st ‘ 𝑘 ) ∈ ℝ )
36 34 35 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... 𝑅 ) ) ) → ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ∈ ℂ )
37 21 36 mulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... 𝑅 ) ) ) → ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) ∈ ℂ )
38 13 nnne0d ⊢ ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ≠ 0 )
39 10 14 37 38 fsumdivc ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... 𝑅 ) ) ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) = Σ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... 𝑅 ) ) ( ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) )
40 14 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... 𝑅 ) ) ) → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℂ )
41 38 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... 𝑅 ) ) ) → ( ! ‘ ( 𝑃 − 1 ) ) ≠ 0 )
42 21 36 40 41 divassd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... 𝑅 ) ) ) → ( ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) = ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ) )
43 etransclem5 ⊢ ( 𝑘 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑦 ∈ ℝ ↦ ( ( 𝑦 − 𝑘 ) ↑ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ) = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ ℝ ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
44 etransclem11 ⊢ ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) = ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑛 } )
45 16 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... 𝑅 ) ) ) → ( 1st ‘ 𝑘 ) ∈ ( 0 ... 𝑀 ) )
46 23 27 28 29 3 33 43 44 45 35 etransclem37 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... 𝑅 ) ) ) → ( ! ‘ ( 𝑃 − 1 ) ) ∥ ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) )
47 13 nnzd ⊢ ( 𝜑 → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℤ )
48 47 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... 𝑅 ) ) ) → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℤ )
49 19 nn0zd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... 𝑅 ) ) ) → ( 1st ‘ 𝑘 ) ∈ ℤ )
50 23 27 28 29 3 33 35 49 etransclem42 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... 𝑅 ) ) ) → ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ∈ ℤ )
51 dvdsval2 ⊢ ( ( ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℤ ∧ ( ! ‘ ( 𝑃 − 1 ) ) ≠ 0 ∧ ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ∈ ℤ ) → ( ( ! ‘ ( 𝑃 − 1 ) ) ∥ ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ↔ ( ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ∈ ℤ ) )
52 48 41 50 51 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... 𝑅 ) ) ) → ( ( ! ‘ ( 𝑃 − 1 ) ) ∥ ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ↔ ( ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ∈ ℤ ) )
53 46 52 mpbid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... 𝑅 ) ) ) → ( ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ∈ ℤ )
54 20 53 zmulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... 𝑅 ) ) ) → ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ) ∈ ℤ )
55 42 54 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... 𝑅 ) ) ) → ( ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ∈ ℤ )
56 10 55 fsumzcl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... 𝑅 ) ) ( ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ∈ ℤ )
57 39 56 eqeltrd ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( ( 0 ... 𝑀 ) × ( 0 ... 𝑅 ) ) ( ( 𝐴 ‘ ( 1st ‘ 𝑘 ) ) · ( ( ( ℝ D𝑛 𝐹 ) ‘ ( 2nd ‘ 𝑘 ) ) ‘ ( 1st ‘ 𝑘 ) ) ) / ( ! ‘ ( 𝑃 − 1 ) ) ) ∈ ℤ )
58 5 57 eqeltrid ⊢ ( 𝜑 → 𝐾 ∈ ℤ )