Metamath Proof Explorer

Theorem etransclem32

Description: This is the proof for the last equation in the proof of the derivative calculated in Juillerat p. 12, just after equation *(6) . (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem32.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
etransclem32.x ⊢ ( 𝜑 → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
etransclem32.p ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
etransclem32.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
etransclem32.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) )
etransclem32.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
etransclem32.ngt ⊢ ( 𝜑 → ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) < 𝑁 )
etransclem32.h ⊢ 𝐻 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
Assertion etransclem32 ( 𝜑 → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) )

Proof

Step Hyp Ref Expression
1 etransclem32.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2 etransclem32.x ⊢ ( 𝜑 → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
3 etransclem32.p ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
4 etransclem32.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
5 etransclem32.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) )
6 etransclem32.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
7 etransclem32.ngt ⊢ ( 𝜑 → ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) < 𝑁 )
8 etransclem32.h ⊢ 𝐻 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
9 etransclem11 ⊢ ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) = ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑛 } )
10 1 2 3 4 5 6 8 9 etransclem30 ⊢ ( 𝜑 → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) ‘ 𝑥 ) ) ) )
11 simpr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) ‘ 𝑁 ) ) → 𝑐 ∈ ( ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) ‘ 𝑁 ) )
12 9 6 etransclem12 ⊢ ( 𝜑 → ( ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) ‘ 𝑁 ) = { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } )
13 12 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) ‘ 𝑁 ) ) → ( ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) ‘ 𝑁 ) = { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } )
14 11 13 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) ‘ 𝑁 ) ) → 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } )
15 14 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ ( ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) ‘ 𝑁 ) ) → 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } )
16 nfv ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } )
17 nfre1 ⊢ Ⅎ 𝑘 ∃ 𝑘 ∈ ( 0 ... 𝑀 ) if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑘 )
18 17 nfn ⊢ Ⅎ 𝑘 ¬ ∃ 𝑘 ∈ ( 0 ... 𝑀 ) if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑘 )
19 16 18 nfan ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ ¬ ∃ 𝑘 ∈ ( 0 ... 𝑀 ) if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑘 ) )
20 fzssre ⊢ ( 0 ... 𝑁 ) ⊆ ℝ
21 rabid ⊢ ( 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ↔ ( 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∧ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 ) )
22 21 simplbi ⊢ ( 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } → 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) )
23 elmapi ⊢ ( 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) → 𝑐 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) )
24 22 23 syl ⊢ ( 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } → 𝑐 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) )
25 24 adantl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) → 𝑐 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) )
26 25 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( 𝑐 ‘ 𝑘 ) ∈ ( 0 ... 𝑁 ) )
27 20 26 sselid ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( 𝑐 ‘ 𝑘 ) ∈ ℝ )
28 27 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ ¬ ∃ 𝑘 ∈ ( 0 ... 𝑀 ) if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑘 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( 𝑐 ‘ 𝑘 ) ∈ ℝ )
29 nnm1nn0 ⊢ ( 𝑃 ∈ ℕ → ( 𝑃 − 1 ) ∈ ℕ0 )
30 3 29 syl ⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℕ0 )
31 30 nn0red ⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℝ )
32 3 nnred ⊢ ( 𝜑 → 𝑃 ∈ ℝ )
33 31 32 ifcld ⊢ ( 𝜑 → if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℝ )
34 33 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ ¬ ∃ 𝑘 ∈ ( 0 ... 𝑀 ) if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑘 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℝ )
35 ralnex ⊢ ( ∀ 𝑘 ∈ ( 0 ... 𝑀 ) ¬ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑘 ) ↔ ¬ ∃ 𝑘 ∈ ( 0 ... 𝑀 ) if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑘 ) )
36 35 biimpri ⊢ ( ¬ ∃ 𝑘 ∈ ( 0 ... 𝑀 ) if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑘 ) → ∀ 𝑘 ∈ ( 0 ... 𝑀 ) ¬ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑘 ) )
37 36 r19.21bi ⊢ ( ( ¬ ∃ 𝑘 ∈ ( 0 ... 𝑀 ) if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑘 ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ¬ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑘 ) )
38 37 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ ¬ ∃ 𝑘 ∈ ( 0 ... 𝑀 ) if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑘 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ¬ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑘 ) )
39 28 34 38 nltled ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ ¬ ∃ 𝑘 ∈ ( 0 ... 𝑀 ) if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑘 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( 𝑐 ‘ 𝑘 ) ≤ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) )
40 39 ex ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ ¬ ∃ 𝑘 ∈ ( 0 ... 𝑀 ) if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑘 ) ) → ( 𝑘 ∈ ( 0 ... 𝑀 ) → ( 𝑐 ‘ 𝑘 ) ≤ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )
41 19 40 ralrimi ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ ¬ ∃ 𝑘 ∈ ( 0 ... 𝑀 ) if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑘 ) ) → ∀ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑘 ) ≤ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) )
42 21 simprbi ⊢ ( 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } → Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 )
43 fveq2 ⊢ ( 𝑗 = 𝑘 → ( 𝑐 ‘ 𝑗 ) = ( 𝑐 ‘ 𝑘 ) )
44 43 cbvsumv ⊢ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑘 )
45 42 44 eqtr3di ⊢ ( 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } → 𝑁 = Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑘 ) )
46 45 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ ∀ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑘 ) ≤ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) → 𝑁 = Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑘 ) )
47 fveq2 ⊢ ( 𝑘 = ℎ → ( 𝑐 ‘ 𝑘 ) = ( 𝑐 ‘ ℎ ) )
48 47 cbvsumv ⊢ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑘 ) = Σ ℎ ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ ℎ )
49 fzfid ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ ∀ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑘 ) ≤ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) → ( 0 ... 𝑀 ) ∈ Fin )
50 25 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → ( 𝑐 ‘ ℎ ) ∈ ( 0 ... 𝑁 ) )
51 20 50 sselid ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → ( 𝑐 ‘ ℎ ) ∈ ℝ )
52 51 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ ∀ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑘 ) ≤ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → ( 𝑐 ‘ ℎ ) ∈ ℝ )
53 31 32 ifcld ⊢ ( 𝜑 → if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℝ )
54 53 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ ∀ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑘 ) ≤ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℝ )
55 eqeq1 ⊢ ( 𝑘 = ℎ → ( 𝑘 = 0 ↔ ℎ = 0 ) )
56 55 ifbid ⊢ ( 𝑘 = ℎ → if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) = if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) )
57 47 56 breq12d ⊢ ( 𝑘 = ℎ → ( ( 𝑐 ‘ 𝑘 ) ≤ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ↔ ( 𝑐 ‘ ℎ ) ≤ if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )
58 57 rspccva ⊢ ( ( ∀ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑘 ) ≤ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → ( 𝑐 ‘ ℎ ) ≤ if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) )
59 58 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ ∀ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑘 ) ≤ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → ( 𝑐 ‘ ℎ ) ≤ if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) )
60 49 52 54 59 fsumle ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ ∀ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑘 ) ≤ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) → Σ ℎ ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ ℎ ) ≤ Σ ℎ ∈ ( 0 ... 𝑀 ) if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) )
61 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
62 4 61 eleqtrdi ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 0 ) )
63 3 nnnn0d ⊢ ( 𝜑 → 𝑃 ∈ ℕ0 )
64 30 63 ifcld ⊢ ( 𝜑 → if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℕ0 )
65 64 adantr ⊢ ( ( 𝜑 ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℕ0 )
66 65 nn0cnd ⊢ ( ( 𝜑 ∧ ℎ ∈ ( 0 ... 𝑀 ) ) → if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℂ )
67 iftrue ⊢ ( ℎ = 0 → if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) = ( 𝑃 − 1 ) )
68 62 66 67 fsum1p ⊢ ( 𝜑 → Σ ℎ ∈ ( 0 ... 𝑀 ) if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) = ( ( 𝑃 − 1 ) + Σ ℎ ∈ ( ( 0 + 1 ) ... 𝑀 ) if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )
69 0p1e1 ⊢ ( 0 + 1 ) = 1
70 69 oveq1i ⊢ ( ( 0 + 1 ) ... 𝑀 ) = ( 1 ... 𝑀 )
71 70 a1i ⊢ ( 𝜑 → ( ( 0 + 1 ) ... 𝑀 ) = ( 1 ... 𝑀 ) )
72 71 sumeq1d ⊢ ( 𝜑 → Σ ℎ ∈ ( ( 0 + 1 ) ... 𝑀 ) if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) = Σ ℎ ∈ ( 1 ... 𝑀 ) if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) )
73 0red ⊢ ( ℎ ∈ ( 1 ... 𝑀 ) → 0 ∈ ℝ )
74 1red ⊢ ( ℎ ∈ ( 1 ... 𝑀 ) → 1 ∈ ℝ )
75 elfzelz ⊢ ( ℎ ∈ ( 1 ... 𝑀 ) → ℎ ∈ ℤ )
76 75 zred ⊢ ( ℎ ∈ ( 1 ... 𝑀 ) → ℎ ∈ ℝ )
77 0lt1 ⊢ 0 < 1
78 77 a1i ⊢ ( ℎ ∈ ( 1 ... 𝑀 ) → 0 < 1 )
79 elfzle1 ⊢ ( ℎ ∈ ( 1 ... 𝑀 ) → 1 ≤ ℎ )
80 73 74 76 78 79 ltletrd ⊢ ( ℎ ∈ ( 1 ... 𝑀 ) → 0 < ℎ )
81 80 gt0ne0d ⊢ ( ℎ ∈ ( 1 ... 𝑀 ) → ℎ ≠ 0 )
82 81 neneqd ⊢ ( ℎ ∈ ( 1 ... 𝑀 ) → ¬ ℎ = 0 )
83 82 iffalsed ⊢ ( ℎ ∈ ( 1 ... 𝑀 ) → if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) = 𝑃 )
84 83 adantl ⊢ ( ( 𝜑 ∧ ℎ ∈ ( 1 ... 𝑀 ) ) → if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) = 𝑃 )
85 84 sumeq2dv ⊢ ( 𝜑 → Σ ℎ ∈ ( 1 ... 𝑀 ) if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) = Σ ℎ ∈ ( 1 ... 𝑀 ) 𝑃 )
86 fzfid ⊢ ( 𝜑 → ( 1 ... 𝑀 ) ∈ Fin )
87 3 nncnd ⊢ ( 𝜑 → 𝑃 ∈ ℂ )
88 fsumconst ⊢ ( ( ( 1 ... 𝑀 ) ∈ Fin ∧ 𝑃 ∈ ℂ ) → Σ ℎ ∈ ( 1 ... 𝑀 ) 𝑃 = ( ( ♯ ‘ ( 1 ... 𝑀 ) ) · 𝑃 ) )
89 86 87 88 syl2anc ⊢ ( 𝜑 → Σ ℎ ∈ ( 1 ... 𝑀 ) 𝑃 = ( ( ♯ ‘ ( 1 ... 𝑀 ) ) · 𝑃 ) )
90 hashfz1 ⊢ ( 𝑀 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝑀 ) ) = 𝑀 )
91 4 90 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 1 ... 𝑀 ) ) = 𝑀 )
92 91 oveq1d ⊢ ( 𝜑 → ( ( ♯ ‘ ( 1 ... 𝑀 ) ) · 𝑃 ) = ( 𝑀 · 𝑃 ) )
93 89 92 eqtrd ⊢ ( 𝜑 → Σ ℎ ∈ ( 1 ... 𝑀 ) 𝑃 = ( 𝑀 · 𝑃 ) )
94 72 85 93 3eqtrd ⊢ ( 𝜑 → Σ ℎ ∈ ( ( 0 + 1 ) ... 𝑀 ) if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) = ( 𝑀 · 𝑃 ) )
95 94 oveq2d ⊢ ( 𝜑 → ( ( 𝑃 − 1 ) + Σ ℎ ∈ ( ( 0 + 1 ) ... 𝑀 ) if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) = ( ( 𝑃 − 1 ) + ( 𝑀 · 𝑃 ) ) )
96 30 nn0cnd ⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℂ )
97 4 63 nn0mulcld ⊢ ( 𝜑 → ( 𝑀 · 𝑃 ) ∈ ℕ0 )
98 97 nn0cnd ⊢ ( 𝜑 → ( 𝑀 · 𝑃 ) ∈ ℂ )
99 96 98 addcomd ⊢ ( 𝜑 → ( ( 𝑃 − 1 ) + ( 𝑀 · 𝑃 ) ) = ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) )
100 68 95 99 3eqtrd ⊢ ( 𝜑 → Σ ℎ ∈ ( 0 ... 𝑀 ) if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) = ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) )
101 100 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ ∀ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑘 ) ≤ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) → Σ ℎ ∈ ( 0 ... 𝑀 ) if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) = ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) )
102 60 101 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ ∀ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑘 ) ≤ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) → Σ ℎ ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ ℎ ) ≤ ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) )
103 48 102 eqbrtrid ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ ∀ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑘 ) ≤ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) → Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑘 ) ≤ ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) )
104 46 103 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ ∀ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑘 ) ≤ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) → 𝑁 ≤ ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) )
105 41 104 syldan ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ ¬ ∃ 𝑘 ∈ ( 0 ... 𝑀 ) if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑘 ) ) → 𝑁 ≤ ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) )
106 97 30 nn0addcld ⊢ ( 𝜑 → ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ∈ ℕ0 )
107 106 nn0red ⊢ ( 𝜑 → ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ∈ ℝ )
108 6 nn0red ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
109 107 108 ltnled ⊢ ( 𝜑 → ( ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) < 𝑁 ↔ ¬ 𝑁 ≤ ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) ) )
110 7 109 mpbid ⊢ ( 𝜑 → ¬ 𝑁 ≤ ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) )
111 110 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ ¬ ∃ 𝑘 ∈ ( 0 ... 𝑀 ) if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑘 ) ) → ¬ 𝑁 ≤ ( ( 𝑀 · 𝑃 ) + ( 𝑃 − 1 ) ) )
112 105 111 condan ⊢ ( ( 𝜑 ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) → ∃ 𝑘 ∈ ( 0 ... 𝑀 ) if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑘 ) )
113 112 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) → ∃ 𝑘 ∈ ( 0 ... 𝑀 ) if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑘 ) )
114 nfv ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑥 ∈ 𝑋 )
115 nfcv ⊢ Ⅎ 𝑗 ( 0 ... 𝑀 )
116 115 nfsum1 ⊢ Ⅎ 𝑗 Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 )
117 116 nfeq1 ⊢ Ⅎ 𝑗 Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁
118 nfcv ⊢ Ⅎ 𝑗 ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) )
119 117 118 nfrabw ⊢ Ⅎ 𝑗 { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 }
120 119 nfcri ⊢ Ⅎ 𝑗 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 }
121 114 120 nfan ⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } )
122 nfv ⊢ Ⅎ 𝑗 𝑘 ∈ ( 0 ... 𝑀 )
123 nfv ⊢ Ⅎ 𝑗 if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑘 )
124 121 122 123 nf3an ⊢ Ⅎ 𝑗 ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ∧ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑘 ) )
125 nfcv ⊢ Ⅎ 𝑗 ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑘 ) ) ‘ ( 𝑐 ‘ 𝑘 ) ) ‘ 𝑥 )
126 fzfid ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ∧ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑘 ) ) → ( 0 ... 𝑀 ) ∈ Fin )
127 1 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑆 ∈ { ℝ , ℂ } )
128 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
129 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑃 ∈ ℕ )
130 etransclem5 ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ) = ( 𝑘 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑦 ∈ 𝑋 ↦ ( ( 𝑦 − 𝑘 ) ↑ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
131 8 130 eqtri ⊢ 𝐻 = ( 𝑘 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑦 ∈ 𝑋 ↦ ( ( 𝑦 − 𝑘 ) ↑ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
132 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
133 24 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑐 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) )
134 simpr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
135 133 134 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝑐 ‘ 𝑗 ) ∈ ( 0 ... 𝑁 ) )
136 135 adantllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝑐 ‘ 𝑗 ) ∈ ( 0 ... 𝑁 ) )
137 elfznn0 ⊢ ( ( 𝑐 ‘ 𝑗 ) ∈ ( 0 ... 𝑁 ) → ( 𝑐 ‘ 𝑗 ) ∈ ℕ0 )
138 136 137 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝑐 ‘ 𝑗 ) ∈ ℕ0 )
139 127 128 129 131 132 138 etransclem20 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) : 𝑋 ⟶ ℂ )
140 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑥 ∈ 𝑋 )
141 139 140 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) ‘ 𝑥 ) ∈ ℂ )
142 141 3ad2antl1 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ∧ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑘 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) ‘ 𝑥 ) ∈ ℂ )
143 fveq2 ⊢ ( 𝑗 = 𝑘 → ( 𝐻 ‘ 𝑗 ) = ( 𝐻 ‘ 𝑘 ) )
144 143 oveq2d ⊢ ( 𝑗 = 𝑘 → ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) = ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑘 ) ) )
145 144 43 fveq12d ⊢ ( 𝑗 = 𝑘 → ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) = ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑘 ) ) ‘ ( 𝑐 ‘ 𝑘 ) ) )
146 145 fveq1d ⊢ ( 𝑗 = 𝑘 → ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) ‘ 𝑥 ) = ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑘 ) ) ‘ ( 𝑐 ‘ 𝑘 ) ) ‘ 𝑥 ) )
147 simp2 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ∧ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑘 ) ) → 𝑘 ∈ ( 0 ... 𝑀 ) )
148 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) → 𝑆 ∈ { ℝ , ℂ } )
149 148 3ad2ant1 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ∧ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑘 ) ) → 𝑆 ∈ { ℝ , ℂ } )
150 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
151 150 3ad2ant1 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ∧ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑘 ) ) → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
152 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) → 𝑃 ∈ ℕ )
153 152 3ad2ant1 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ∧ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑘 ) ) → 𝑃 ∈ ℕ )
154 etransclem5 ⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ) = ( ℎ ∈ ( 0 ... 𝑀 ) ↦ ( 𝑦 ∈ 𝑋 ↦ ( ( 𝑦 − ℎ ) ↑ if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
155 8 154 eqtri ⊢ 𝐻 = ( ℎ ∈ ( 0 ... 𝑀 ) ↦ ( 𝑦 ∈ 𝑋 ↦ ( ( 𝑦 − ℎ ) ↑ if ( ℎ = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
156 26 elfzelzd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( 𝑐 ‘ 𝑘 ) ∈ ℤ )
157 156 adantllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( 𝑐 ‘ 𝑘 ) ∈ ℤ )
158 157 3adant3 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ∧ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑘 ) ) → ( 𝑐 ‘ 𝑘 ) ∈ ℤ )
159 simp3 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ∧ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑘 ) ) → if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑘 ) )
160 149 151 153 155 147 158 159 etransclem19 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ∧ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑘 ) ) → ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑘 ) ) ‘ ( 𝑐 ‘ 𝑘 ) ) = ( 𝑦 ∈ 𝑋 ↦ 0 ) )
161 eqidd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ∧ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑘 ) ) ∧ 𝑦 = 𝑥 ) → 0 = 0 )
162 simp1lr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ∧ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑘 ) ) → 𝑥 ∈ 𝑋 )
163 0red ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ∧ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑘 ) ) → 0 ∈ ℝ )
164 160 161 162 163 fvmptd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ∧ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑘 ) ) → ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑘 ) ) ‘ ( 𝑐 ‘ 𝑘 ) ) ‘ 𝑥 ) = 0 )
165 124 125 126 142 146 147 164 fprod0 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ∧ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑘 ) ) → ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) ‘ 𝑥 ) = 0 )
166 165 rexlimdv3a ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) → ( ∃ 𝑘 ∈ ( 0 ... 𝑀 ) if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑘 ) → ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) ‘ 𝑥 ) = 0 ) )
167 113 166 mpd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ) → ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) ‘ 𝑥 ) = 0 )
168 15 167 syldan ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ ( ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) ‘ 𝑁 ) ) → ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) ‘ 𝑥 ) = 0 )
169 168 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ ( ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) ‘ 𝑁 ) ) → ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) ‘ 𝑥 ) ) = ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · 0 ) )
170 6 faccld ⊢ ( 𝜑 → ( ! ‘ 𝑁 ) ∈ ℕ )
171 170 nncnd ⊢ ( 𝜑 → ( ! ‘ 𝑁 ) ∈ ℂ )
172 171 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) ‘ 𝑁 ) ) → ( ! ‘ 𝑁 ) ∈ ℂ )
173 fzfid ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) ‘ 𝑁 ) ) → ( 0 ... 𝑀 ) ∈ Fin )
174 simpll ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) ‘ 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝜑 )
175 14 adantr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) ‘ 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } )
176 simpr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) ‘ 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
177 174 175 176 135 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) ‘ 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝑐 ‘ 𝑗 ) ∈ ( 0 ... 𝑁 ) )
178 177 137 syl ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) ‘ 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝑐 ‘ 𝑗 ) ∈ ℕ0 )
179 178 faccld ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) ‘ 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ∈ ℕ )
180 179 nncnd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) ‘ 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ∈ ℂ )
181 173 180 fprodcl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) ‘ 𝑁 ) ) → ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ∈ ℂ )
182 179 nnne0d ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) ‘ 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ≠ 0 )
183 173 180 182 fprodn0 ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) ‘ 𝑁 ) ) → ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ≠ 0 )
184 172 181 183 divcld ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) ‘ 𝑁 ) ) → ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) ∈ ℂ )
185 184 mul01d ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) ‘ 𝑁 ) ) → ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · 0 ) = 0 )
186 185 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ ( ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) ‘ 𝑁 ) ) → ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · 0 ) = 0 )
187 169 186 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑐 ∈ ( ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) ‘ 𝑁 ) ) → ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) ‘ 𝑥 ) ) = 0 )
188 187 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → Σ 𝑐 ∈ ( ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) ‘ 𝑥 ) ) = Σ 𝑐 ∈ ( ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) ‘ 𝑁 ) 0 )
189 eqid ⊢ ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) = ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } )
190 189 6 etransclem16 ⊢ ( 𝜑 → ( ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) ‘ 𝑁 ) ∈ Fin )
191 190 olcd ⊢ ( 𝜑 → ( ( ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) ‘ 𝑁 ) ⊆ ( ℤ≥ ‘ 𝐴 ) ∨ ( ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) ‘ 𝑁 ) ∈ Fin ) )
192 191 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) ‘ 𝑁 ) ⊆ ( ℤ≥ ‘ 𝐴 ) ∨ ( ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) ‘ 𝑁 ) ∈ Fin ) )
193 sumz ⊢ ( ( ( ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) ‘ 𝑁 ) ⊆ ( ℤ≥ ‘ 𝐴 ) ∨ ( ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) ‘ 𝑁 ) ∈ Fin ) → Σ 𝑐 ∈ ( ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) ‘ 𝑁 ) 0 = 0 )
194 192 193 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → Σ 𝑐 ∈ ( ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) ‘ 𝑁 ) 0 = 0 )
195 188 194 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → Σ 𝑐 ∈ ( ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) ‘ 𝑥 ) ) = 0 )
196 195 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) )
197 10 196 eqtrd ⊢ ( 𝜑 → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) )