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 ) )