Metamath Proof Explorer

Theorem etransclem27

Description: The N -th derivative of F applied to J is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem27.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
etransclem27.x ⊢ ( 𝜑 → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
etransclem27.p ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
etransclem27.h ⊢ 𝐻 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
etransclem27.cfi ⊢ ( 𝜑 → 𝐶 ∈ Fin )
etransclem27.cf ⊢ ( 𝜑 → 𝐶 : dom 𝐶 ⟶ ( ℕ0 ↑m ( 0 ... 𝑀 ) ) )
etransclem27.g ⊢ 𝐺 = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑙 ∈ dom 𝐶 ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ‘ 𝑥 ) )
etransclem27.jx ⊢ ( 𝜑 → 𝐽 ∈ 𝑋 )
etransclem27.jz ⊢ ( 𝜑 → 𝐽 ∈ ℤ )
Assertion etransclem27 ( 𝜑 → ( 𝐺 ‘ 𝐽 ) ∈ ℤ )

Proof

Step Hyp Ref Expression
1 etransclem27.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2 etransclem27.x ⊢ ( 𝜑 → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
3 etransclem27.p ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
4 etransclem27.h ⊢ 𝐻 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
5 etransclem27.cfi ⊢ ( 𝜑 → 𝐶 ∈ Fin )
6 etransclem27.cf ⊢ ( 𝜑 → 𝐶 : dom 𝐶 ⟶ ( ℕ0 ↑m ( 0 ... 𝑀 ) ) )
7 etransclem27.g ⊢ 𝐺 = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑙 ∈ dom 𝐶 ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ‘ 𝑥 ) )
8 etransclem27.jx ⊢ ( 𝜑 → 𝐽 ∈ 𝑋 )
9 etransclem27.jz ⊢ ( 𝜑 → 𝐽 ∈ ℤ )
10 fveq2 ⊢ ( 𝑥 = 𝐽 → ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ‘ 𝑥 ) = ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ‘ 𝐽 ) )
11 10 prodeq2ad ⊢ ( 𝑥 = 𝐽 → ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ‘ 𝑥 ) = ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ‘ 𝐽 ) )
12 11 sumeq2sdv ⊢ ( 𝑥 = 𝐽 → Σ 𝑙 ∈ dom 𝐶 ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ‘ 𝑥 ) = Σ 𝑙 ∈ dom 𝐶 ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ‘ 𝐽 ) )
13 dmfi ⊢ ( 𝐶 ∈ Fin → dom 𝐶 ∈ Fin )
14 5 13 syl ⊢ ( 𝜑 → dom 𝐶 ∈ Fin )
15 fzfid ⊢ ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) → ( 0 ... 𝑀 ) ∈ Fin )
16 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑆 ∈ { ℝ , ℂ } )
17 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
18 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑃 ∈ ℕ )
19 etransclem5 ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ) = ( 𝑧 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑦 ∈ 𝑋 ↦ ( ( 𝑦 − 𝑧 ) ↑ if ( 𝑧 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
20 4 19 eqtri ⊢ 𝐻 = ( 𝑧 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑦 ∈ 𝑋 ↦ ( ( 𝑦 − 𝑧 ) ↑ if ( 𝑧 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
21 simpr ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
22 6 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) → ( 𝐶 ‘ 𝑙 ) ∈ ( ℕ0 ↑m ( 0 ... 𝑀 ) ) )
23 elmapi ⊢ ( ( 𝐶 ‘ 𝑙 ) ∈ ( ℕ0 ↑m ( 0 ... 𝑀 ) ) → ( 𝐶 ‘ 𝑙 ) : ( 0 ... 𝑀 ) ⟶ ℕ0 )
24 22 23 syl ⊢ ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) → ( 𝐶 ‘ 𝑙 ) : ( 0 ... 𝑀 ) ⟶ ℕ0 )
25 24 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ∈ ℕ0 )
26 16 17 18 20 21 25 etransclem20 ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) : 𝑋 ⟶ ℂ )
27 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝐽 ∈ 𝑋 )
28 26 27 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ‘ 𝐽 ) ∈ ℂ )
29 15 28 fprodcl ⊢ ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) → ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ‘ 𝐽 ) ∈ ℂ )
30 14 29 fsumcl ⊢ ( 𝜑 → Σ 𝑙 ∈ dom 𝐶 ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ‘ 𝐽 ) ∈ ℂ )
31 7 12 8 30 fvmptd3 ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐽 ) = Σ 𝑙 ∈ dom 𝐶 ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ‘ 𝐽 ) )
32 16 17 18 20 21 25 27 etransclem21 ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ‘ 𝐽 ) = if ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) , 0 , ( ( ( ! ‘ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ) ) ) )
33 iftrue ⊢ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) → if ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) , 0 , ( ( ( ! ‘ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ) ) ) = 0 )
34 0zd ⊢ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) → 0 ∈ ℤ )
35 33 34 eqeltrd ⊢ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) → if ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) , 0 , ( ( ( ! ‘ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ) ) ) ∈ ℤ )
36 35 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → if ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) , 0 , ( ( ( ! ‘ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ) ) ) ∈ ℤ )
37 0zd ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → 0 ∈ ℤ )
38 nnm1nn0 ⊢ ( 𝑃 ∈ ℕ → ( 𝑃 − 1 ) ∈ ℕ0 )
39 3 38 syl ⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℕ0 )
40 3 nnnn0d ⊢ ( 𝜑 → 𝑃 ∈ ℕ0 )
41 39 40 ifcld ⊢ ( 𝜑 → if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℕ0 )
42 41 nn0zd ⊢ ( 𝜑 → if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℤ )
43 42 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℤ )
44 25 nn0zd ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ∈ ℤ )
45 44 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ∈ ℤ )
46 43 45 zsubcld ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ∈ ℤ )
47 45 zred ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ∈ ℝ )
48 43 zred ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℝ )
49 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) )
50 47 48 49 nltled ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ≤ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) )
51 48 47 subge0d ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → ( 0 ≤ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ↔ ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ≤ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )
52 50 51 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → 0 ≤ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) )
53 0red ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 0 ∈ ℝ )
54 25 nn0red ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ∈ ℝ )
55 41 nn0red ⊢ ( 𝜑 → if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℝ )
56 55 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℝ )
57 25 nn0ge0d ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 0 ≤ ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) )
58 53 54 56 57 lesub2dd ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ≤ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 0 ) )
59 56 recnd ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℂ )
60 59 subid1d ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 0 ) = if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) )
61 58 60 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ≤ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) )
62 61 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ≤ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) )
63 37 43 46 52 62 elfzd ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ∈ ( 0 ... if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )
64 permnn ⊢ ( ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ∈ ( 0 ... if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) → ( ( ! ‘ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ) ) ∈ ℕ )
65 63 64 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → ( ( ! ‘ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ) ) ∈ ℕ )
66 65 nnzd ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → ( ( ! ‘ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ) ) ∈ ℤ )
67 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → 𝐽 ∈ ℤ )
68 elfzelz ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑗 ∈ ℤ )
69 68 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → 𝑗 ∈ ℤ )
70 67 69 zsubcld ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → ( 𝐽 − 𝑗 ) ∈ ℤ )
71 elnn0z ⊢ ( ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ∈ ℕ0 ↔ ( ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ∈ ℤ ∧ 0 ≤ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ) )
72 46 52 71 sylanbrc ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ∈ ℕ0 )
73 zexpcl ⊢ ( ( ( 𝐽 − 𝑗 ) ∈ ℤ ∧ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ∈ ℕ0 ) → ( ( 𝐽 − 𝑗 ) ↑ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ) ∈ ℤ )
74 70 72 73 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → ( ( 𝐽 − 𝑗 ) ↑ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ) ∈ ℤ )
75 66 74 zmulcld ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → ( ( ( ! ‘ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ) ) ∈ ℤ )
76 37 75 ifcld ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → if ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) , 0 , ( ( ( ! ‘ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ) ) ) ∈ ℤ )
77 36 76 pm2.61dan ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → if ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) , 0 , ( ( ( ! ‘ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ) ) ) ∈ ℤ )
78 32 77 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ‘ 𝐽 ) ∈ ℤ )
79 15 78 fprodzcl ⊢ ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) → ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ‘ 𝐽 ) ∈ ℤ )
80 14 79 fsumzcl ⊢ ( 𝜑 → Σ 𝑙 ∈ dom 𝐶 ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ‘ 𝐽 ) ∈ ℤ )
81 31 80 eqeltrd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐽 ) ∈ ℤ )