This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvnxpaek

Description: The n -th derivative of the polynomial ( x + A ) ^ K . (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses dvnxpaek.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
dvnxpaek.x ⊢ ( 𝜑 → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
dvnxpaek.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
dvnxpaek.k ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
dvnxpaek.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 + 𝐴 ) ↑ 𝐾 ) )
Assertion dvnxpaek ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) = ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < 𝑁 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑁 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑁 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dvnxpaek.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2 dvnxpaek.x ⊢ ( 𝜑 → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
3 dvnxpaek.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
4 dvnxpaek.k ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
5 dvnxpaek.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 + 𝐴 ) ↑ 𝐾 ) )
6 fveq2 ⊢ ( 𝑛 = 0 → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) )
7 breq2 ⊢ ( 𝑛 = 0 → ( 𝐾 < 𝑛 ↔ 𝐾 < 0 ) )
8 eqidd ⊢ ( 𝑛 = 0 → 0 = 0 )
9 oveq2 ⊢ ( 𝑛 = 0 → ( 𝐾 − 𝑛 ) = ( 𝐾 − 0 ) )
10 9 fveq2d ⊢ ( 𝑛 = 0 → ( ! ‘ ( 𝐾 − 𝑛 ) ) = ( ! ‘ ( 𝐾 − 0 ) ) )
11 10 oveq2d ⊢ ( 𝑛 = 0 → ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑛 ) ) ) = ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 0 ) ) ) )
12 9 oveq2d ⊢ ( 𝑛 = 0 → ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑛 ) ) = ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 0 ) ) )
13 11 12 oveq12d ⊢ ( 𝑛 = 0 → ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑛 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑛 ) ) ) = ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 0 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 0 ) ) ) )
14 7 8 13 ifbieq12d ⊢ ( 𝑛 = 0 → if ( 𝐾 < 𝑛 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑛 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑛 ) ) ) ) = if ( 𝐾 < 0 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 0 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 0 ) ) ) ) )
15 14 mpteq2dv ⊢ ( 𝑛 = 0 → ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < 𝑛 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑛 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑛 ) ) ) ) ) = ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < 0 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 0 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 0 ) ) ) ) ) )
16 6 15 eqeq12d ⊢ ( 𝑛 = 0 → ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) = ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < 𝑛 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑛 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑛 ) ) ) ) ) ↔ ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) = ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < 0 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 0 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 0 ) ) ) ) ) ) )
17 fveq2 ⊢ ( 𝑛 = 𝑚 → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑚 ) )
18 breq2 ⊢ ( 𝑛 = 𝑚 → ( 𝐾 < 𝑛 ↔ 𝐾 < 𝑚 ) )
19 eqidd ⊢ ( 𝑛 = 𝑚 → 0 = 0 )
20 oveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝐾 − 𝑛 ) = ( 𝐾 − 𝑚 ) )
21 20 fveq2d ⊢ ( 𝑛 = 𝑚 → ( ! ‘ ( 𝐾 − 𝑛 ) ) = ( ! ‘ ( 𝐾 − 𝑚 ) ) )
22 21 oveq2d ⊢ ( 𝑛 = 𝑚 → ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑛 ) ) ) = ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) )
23 20 oveq2d ⊢ ( 𝑛 = 𝑚 → ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑛 ) ) = ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) )
24 22 23 oveq12d ⊢ ( 𝑛 = 𝑚 → ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑛 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑛 ) ) ) = ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) )
25 18 19 24 ifbieq12d ⊢ ( 𝑛 = 𝑚 → if ( 𝐾 < 𝑛 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑛 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑛 ) ) ) ) = if ( 𝐾 < 𝑚 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) ) )
26 25 mpteq2dv ⊢ ( 𝑛 = 𝑚 → ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < 𝑛 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑛 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑛 ) ) ) ) ) = ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < 𝑚 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) ) ) )
27 17 26 eqeq12d ⊢ ( 𝑛 = 𝑚 → ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) = ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < 𝑛 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑛 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑛 ) ) ) ) ) ↔ ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑚 ) = ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < 𝑚 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) ) ) ) )
28 fveq2 ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑚 + 1 ) ) )
29 breq2 ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( 𝐾 < 𝑛 ↔ 𝐾 < ( 𝑚 + 1 ) ) )
30 eqidd ⊢ ( 𝑛 = ( 𝑚 + 1 ) → 0 = 0 )
31 oveq2 ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( 𝐾 − 𝑛 ) = ( 𝐾 − ( 𝑚 + 1 ) ) )
32 31 fveq2d ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ! ‘ ( 𝐾 − 𝑛 ) ) = ( ! ‘ ( 𝐾 − ( 𝑚 + 1 ) ) ) )
33 32 oveq2d ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑛 ) ) ) = ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) )
34 31 oveq2d ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑛 ) ) = ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − ( 𝑚 + 1 ) ) ) )
35 33 34 oveq12d ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑛 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑛 ) ) ) = ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) )
36 29 30 35 ifbieq12d ⊢ ( 𝑛 = ( 𝑚 + 1 ) → if ( 𝐾 < 𝑛 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑛 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑛 ) ) ) ) = if ( 𝐾 < ( 𝑚 + 1 ) , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) ) )
37 36 mpteq2dv ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < 𝑛 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑛 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑛 ) ) ) ) ) = ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < ( 𝑚 + 1 ) , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) ) ) )
38 28 37 eqeq12d ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) = ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < 𝑛 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑛 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑛 ) ) ) ) ) ↔ ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑚 + 1 ) ) = ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < ( 𝑚 + 1 ) , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) ) ) ) )
39 fveq2 ⊢ ( 𝑛 = 𝑁 → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) = ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) )
40 breq2 ⊢ ( 𝑛 = 𝑁 → ( 𝐾 < 𝑛 ↔ 𝐾 < 𝑁 ) )
41 eqidd ⊢ ( 𝑛 = 𝑁 → 0 = 0 )
42 oveq2 ⊢ ( 𝑛 = 𝑁 → ( 𝐾 − 𝑛 ) = ( 𝐾 − 𝑁 ) )
43 42 fveq2d ⊢ ( 𝑛 = 𝑁 → ( ! ‘ ( 𝐾 − 𝑛 ) ) = ( ! ‘ ( 𝐾 − 𝑁 ) ) )
44 43 oveq2d ⊢ ( 𝑛 = 𝑁 → ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑛 ) ) ) = ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑁 ) ) ) )
45 42 oveq2d ⊢ ( 𝑛 = 𝑁 → ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑛 ) ) = ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑁 ) ) )
46 44 45 oveq12d ⊢ ( 𝑛 = 𝑁 → ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑛 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑛 ) ) ) = ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑁 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑁 ) ) ) )
47 40 41 46 ifbieq12d ⊢ ( 𝑛 = 𝑁 → if ( 𝐾 < 𝑛 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑛 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑛 ) ) ) ) = if ( 𝐾 < 𝑁 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑁 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑁 ) ) ) ) )
48 47 mpteq2dv ⊢ ( 𝑛 = 𝑁 → ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < 𝑛 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑛 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑛 ) ) ) ) ) = ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < 𝑁 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑁 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑁 ) ) ) ) ) )
49 39 48 eqeq12d ⊢ ( 𝑛 = 𝑁 → ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑛 ) = ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < 𝑛 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑛 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑛 ) ) ) ) ) ↔ ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) = ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < 𝑁 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑁 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑁 ) ) ) ) ) ) )
50 recnprss ⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ )
51 1 50 syl ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
52 cnex ⊢ ℂ ∈ V
53 52 a1i ⊢ ( 𝜑 → ℂ ∈ V )
54 restsspw ⊢ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ⊆ 𝒫 𝑆
55 id ⊢ ( 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
56 54 55 sselid ⊢ ( 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) → 𝑋 ∈ 𝒫 𝑆 )
57 elpwi ⊢ ( 𝑋 ∈ 𝒫 𝑆 → 𝑋 ⊆ 𝑆 )
58 56 57 syl ⊢ ( 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) → 𝑋 ⊆ 𝑆 )
59 2 58 syl ⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
60 59 51 sstrd ⊢ ( 𝜑 → 𝑋 ⊆ ℂ )
61 60 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑋 ⊆ ℂ )
62 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
63 61 62 sseldd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ ℂ )
64 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
65 63 64 addcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 + 𝐴 ) ∈ ℂ )
66 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐾 ∈ ℕ0 )
67 65 66 expcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑥 + 𝐴 ) ↑ 𝐾 ) ∈ ℂ )
68 67 5 fmptd ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
69 elpm2r ⊢ ( ( ( ℂ ∈ V ∧ 𝑆 ∈ { ℝ , ℂ } ) ∧ ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ 𝑆 ) ) → 𝐹 ∈ ( ℂ ↑pm 𝑆 ) )
70 53 1 68 59 69 syl22anc ⊢ ( 𝜑 → 𝐹 ∈ ( ℂ ↑pm 𝑆 ) )
71 dvn0 ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) = 𝐹 )
72 51 70 71 syl2anc ⊢ ( 𝜑 → ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) = 𝐹 )
73 5 a1i ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 + 𝐴 ) ↑ 𝐾 ) ) )
74 4 nn0ge0d ⊢ ( 𝜑 → 0 ≤ 𝐾 )
75 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
76 4 nn0red ⊢ ( 𝜑 → 𝐾 ∈ ℝ )
77 75 76 lenltd ⊢ ( 𝜑 → ( 0 ≤ 𝐾 ↔ ¬ 𝐾 < 0 ) )
78 74 77 mpbid ⊢ ( 𝜑 → ¬ 𝐾 < 0 )
79 78 iffalsed ⊢ ( 𝜑 → if ( 𝐾 < 0 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 0 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 0 ) ) ) ) = ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 0 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 0 ) ) ) )
80 79 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → if ( 𝐾 < 0 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 0 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 0 ) ) ) ) = ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 0 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 0 ) ) ) )
81 4 nn0cnd ⊢ ( 𝜑 → 𝐾 ∈ ℂ )
82 81 subid1d ⊢ ( 𝜑 → ( 𝐾 − 0 ) = 𝐾 )
83 82 fveq2d ⊢ ( 𝜑 → ( ! ‘ ( 𝐾 − 0 ) ) = ( ! ‘ 𝐾 ) )
84 83 oveq2d ⊢ ( 𝜑 → ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 0 ) ) ) = ( ( ! ‘ 𝐾 ) / ( ! ‘ 𝐾 ) ) )
85 faccl ⊢ ( 𝐾 ∈ ℕ0 → ( ! ‘ 𝐾 ) ∈ ℕ )
86 4 85 syl ⊢ ( 𝜑 → ( ! ‘ 𝐾 ) ∈ ℕ )
87 86 nncnd ⊢ ( 𝜑 → ( ! ‘ 𝐾 ) ∈ ℂ )
88 86 nnne0d ⊢ ( 𝜑 → ( ! ‘ 𝐾 ) ≠ 0 )
89 87 88 dividd ⊢ ( 𝜑 → ( ( ! ‘ 𝐾 ) / ( ! ‘ 𝐾 ) ) = 1 )
90 84 89 eqtrd ⊢ ( 𝜑 → ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 0 ) ) ) = 1 )
91 82 oveq2d ⊢ ( 𝜑 → ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 0 ) ) = ( ( 𝑥 + 𝐴 ) ↑ 𝐾 ) )
92 90 91 oveq12d ⊢ ( 𝜑 → ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 0 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 0 ) ) ) = ( 1 · ( ( 𝑥 + 𝐴 ) ↑ 𝐾 ) ) )
93 92 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 0 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 0 ) ) ) = ( 1 · ( ( 𝑥 + 𝐴 ) ↑ 𝐾 ) ) )
94 67 mullidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 1 · ( ( 𝑥 + 𝐴 ) ↑ 𝐾 ) ) = ( ( 𝑥 + 𝐴 ) ↑ 𝐾 ) )
95 80 93 94 3eqtrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑥 + 𝐴 ) ↑ 𝐾 ) = if ( 𝐾 < 0 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 0 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 0 ) ) ) ) )
96 95 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 + 𝐴 ) ↑ 𝐾 ) ) = ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < 0 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 0 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 0 ) ) ) ) ) )
97 72 73 96 3eqtrd ⊢ ( 𝜑 → ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) = ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < 0 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 0 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 0 ) ) ) ) ) )
98 51 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → 𝑆 ⊆ ℂ )
99 70 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → 𝐹 ∈ ( ℂ ↑pm 𝑆 ) )
100 simpr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → 𝑚 ∈ ℕ0 )
101 dvnp1 ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑚 + 1 ) ) = ( 𝑆 D ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑚 ) ) )
102 98 99 100 101 syl3anc ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑚 + 1 ) ) = ( 𝑆 D ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑚 ) ) )
103 102 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑚 ) = ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < 𝑚 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) ) ) ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑚 + 1 ) ) = ( 𝑆 D ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑚 ) ) )
104 oveq2 ⊢ ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑚 ) = ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < 𝑚 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) ) ) → ( 𝑆 D ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑚 ) ) = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < 𝑚 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) ) ) ) )
105 104 adantl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑚 ) = ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < 𝑚 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) ) ) ) → ( 𝑆 D ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑚 ) ) = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < 𝑚 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) ) ) ) )
106 iftrue ⊢ ( 𝐾 < 𝑚 → if ( 𝐾 < 𝑚 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) ) = 0 )
107 106 mpteq2dv ⊢ ( 𝐾 < 𝑚 → ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < 𝑚 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) ) ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) )
108 107 oveq2d ⊢ ( 𝐾 < 𝑚 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < 𝑚 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) ) ) ) = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 0 ) ) )
109 108 adantl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝐾 < 𝑚 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < 𝑚 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) ) ) ) = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 0 ) ) )
110 0cnd ⊢ ( 𝜑 → 0 ∈ ℂ )
111 1 2 110 dvmptconst ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 0 ) ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) )
112 111 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝐾 < 𝑚 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 0 ) ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) )
113 76 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝐾 < 𝑚 ) → 𝐾 ∈ ℝ )
114 nn0re ⊢ ( 𝑚 ∈ ℕ0 → 𝑚 ∈ ℝ )
115 114 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝐾 < 𝑚 ) → 𝑚 ∈ ℝ )
116 simpr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝐾 < 𝑚 ) → 𝐾 < 𝑚 )
117 113 115 116 ltled ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝐾 < 𝑚 ) → 𝐾 ≤ 𝑚 )
118 4 nn0zd ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
119 118 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → 𝐾 ∈ ℤ )
120 100 nn0zd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → 𝑚 ∈ ℤ )
121 zleltp1 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑚 ∈ ℤ ) → ( 𝐾 ≤ 𝑚 ↔ 𝐾 < ( 𝑚 + 1 ) ) )
122 119 120 121 syl2anc ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( 𝐾 ≤ 𝑚 ↔ 𝐾 < ( 𝑚 + 1 ) ) )
123 122 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝐾 < 𝑚 ) → ( 𝐾 ≤ 𝑚 ↔ 𝐾 < ( 𝑚 + 1 ) ) )
124 117 123 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝐾 < 𝑚 ) → 𝐾 < ( 𝑚 + 1 ) )
125 124 iftrued ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝐾 < 𝑚 ) → if ( 𝐾 < ( 𝑚 + 1 ) , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) ) = 0 )
126 125 mpteq2dv ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝐾 < 𝑚 ) → ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < ( 𝑚 + 1 ) , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) ) ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) )
127 126 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝐾 < 𝑚 ) → ( 𝑥 ∈ 𝑋 ↦ 0 ) = ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < ( 𝑚 + 1 ) , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) ) ) )
128 109 112 127 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝐾 < 𝑚 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < 𝑚 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) ) ) ) = ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < ( 𝑚 + 1 ) , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) ) ) )
129 simpl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ¬ 𝐾 < 𝑚 ) → ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) )
130 simpr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ¬ 𝐾 < 𝑚 ) → ¬ 𝐾 < 𝑚 )
131 129 100 114 3syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ¬ 𝐾 < 𝑚 ) → 𝑚 ∈ ℝ )
132 76 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ¬ 𝐾 < 𝑚 ) → 𝐾 ∈ ℝ )
133 131 132 lenltd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ¬ 𝐾 < 𝑚 ) → ( 𝑚 ≤ 𝐾 ↔ ¬ 𝐾 < 𝑚 ) )
134 130 133 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ¬ 𝐾 < 𝑚 ) → 𝑚 ≤ 𝐾 )
135 simpr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 = 𝐾 ) → 𝑚 = 𝐾 )
136 114 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 = 𝐾 ) → 𝑚 ∈ ℝ )
137 76 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 = 𝐾 ) → 𝐾 ∈ ℝ )
138 136 137 lttri3d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 = 𝐾 ) → ( 𝑚 = 𝐾 ↔ ( ¬ 𝑚 < 𝐾 ∧ ¬ 𝐾 < 𝑚 ) ) )
139 135 138 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 = 𝐾 ) → ( ¬ 𝑚 < 𝐾 ∧ ¬ 𝐾 < 𝑚 ) )
140 simpr ⊢ ( ( ¬ 𝑚 < 𝐾 ∧ ¬ 𝐾 < 𝑚 ) → ¬ 𝐾 < 𝑚 )
141 139 140 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 = 𝐾 ) → ¬ 𝐾 < 𝑚 )
142 141 iffalsed ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 = 𝐾 ) → if ( 𝐾 < 𝑚 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) ) = ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) )
143 142 mpteq2dv ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 = 𝐾 ) → ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < 𝑚 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) ) )
144 143 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 = 𝐾 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < 𝑚 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) ) ) ) = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) ) ) )
145 oveq2 ⊢ ( 𝑚 = 𝐾 → ( 𝐾 − 𝑚 ) = ( 𝐾 − 𝐾 ) )
146 145 fveq2d ⊢ ( 𝑚 = 𝐾 → ( ! ‘ ( 𝐾 − 𝑚 ) ) = ( ! ‘ ( 𝐾 − 𝐾 ) ) )
147 146 adantl ⊢ ( ( 𝜑 ∧ 𝑚 = 𝐾 ) → ( ! ‘ ( 𝐾 − 𝑚 ) ) = ( ! ‘ ( 𝐾 − 𝐾 ) ) )
148 81 subidd ⊢ ( 𝜑 → ( 𝐾 − 𝐾 ) = 0 )
149 148 fveq2d ⊢ ( 𝜑 → ( ! ‘ ( 𝐾 − 𝐾 ) ) = ( ! ‘ 0 ) )
150 fac0 ⊢ ( ! ‘ 0 ) = 1
151 150 a1i ⊢ ( 𝜑 → ( ! ‘ 0 ) = 1 )
152 149 151 eqtrd ⊢ ( 𝜑 → ( ! ‘ ( 𝐾 − 𝐾 ) ) = 1 )
153 152 adantr ⊢ ( ( 𝜑 ∧ 𝑚 = 𝐾 ) → ( ! ‘ ( 𝐾 − 𝐾 ) ) = 1 )
154 147 153 eqtrd ⊢ ( ( 𝜑 ∧ 𝑚 = 𝐾 ) → ( ! ‘ ( 𝐾 − 𝑚 ) ) = 1 )
155 154 oveq2d ⊢ ( ( 𝜑 ∧ 𝑚 = 𝐾 ) → ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) = ( ( ! ‘ 𝐾 ) / 1 ) )
156 87 div1d ⊢ ( 𝜑 → ( ( ! ‘ 𝐾 ) / 1 ) = ( ! ‘ 𝐾 ) )
157 156 adantr ⊢ ( ( 𝜑 ∧ 𝑚 = 𝐾 ) → ( ( ! ‘ 𝐾 ) / 1 ) = ( ! ‘ 𝐾 ) )
158 155 157 eqtrd ⊢ ( ( 𝜑 ∧ 𝑚 = 𝐾 ) → ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) = ( ! ‘ 𝐾 ) )
159 158 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 = 𝐾 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) = ( ! ‘ 𝐾 ) )
160 145 adantl ⊢ ( ( 𝜑 ∧ 𝑚 = 𝐾 ) → ( 𝐾 − 𝑚 ) = ( 𝐾 − 𝐾 ) )
161 148 adantr ⊢ ( ( 𝜑 ∧ 𝑚 = 𝐾 ) → ( 𝐾 − 𝐾 ) = 0 )
162 160 161 eqtrd ⊢ ( ( 𝜑 ∧ 𝑚 = 𝐾 ) → ( 𝐾 − 𝑚 ) = 0 )
163 162 oveq2d ⊢ ( ( 𝜑 ∧ 𝑚 = 𝐾 ) → ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) = ( ( 𝑥 + 𝐴 ) ↑ 0 ) )
164 163 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 = 𝐾 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) = ( ( 𝑥 + 𝐴 ) ↑ 0 ) )
165 65 exp0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑥 + 𝐴 ) ↑ 0 ) = 1 )
166 165 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑚 = 𝐾 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑥 + 𝐴 ) ↑ 0 ) = 1 )
167 164 166 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑚 = 𝐾 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) = 1 )
168 159 167 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑚 = 𝐾 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) = ( ( ! ‘ 𝐾 ) · 1 ) )
169 87 mulridd ⊢ ( 𝜑 → ( ( ! ‘ 𝐾 ) · 1 ) = ( ! ‘ 𝐾 ) )
170 169 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 = 𝐾 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ! ‘ 𝐾 ) · 1 ) = ( ! ‘ 𝐾 ) )
171 168 170 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑚 = 𝐾 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) = ( ! ‘ 𝐾 ) )
172 171 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑚 = 𝐾 ) → ( 𝑥 ∈ 𝑋 ↦ ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ! ‘ 𝐾 ) ) )
173 172 oveq2d ⊢ ( ( 𝜑 ∧ 𝑚 = 𝐾 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) ) ) = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( ! ‘ 𝐾 ) ) ) )
174 1 2 87 dvmptconst ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( ! ‘ 𝐾 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) )
175 174 adantr ⊢ ( ( 𝜑 ∧ 𝑚 = 𝐾 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( ! ‘ 𝐾 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) )
176 173 175 eqtrd ⊢ ( ( 𝜑 ∧ 𝑚 = 𝐾 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) ) ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) )
177 176 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 = 𝐾 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) ) ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) )
178 137 ltp1d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 = 𝐾 ) → 𝐾 < ( 𝐾 + 1 ) )
179 oveq1 ⊢ ( 𝑚 = 𝐾 → ( 𝑚 + 1 ) = ( 𝐾 + 1 ) )
180 179 eqcomd ⊢ ( 𝑚 = 𝐾 → ( 𝐾 + 1 ) = ( 𝑚 + 1 ) )
181 180 adantl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 = 𝐾 ) → ( 𝐾 + 1 ) = ( 𝑚 + 1 ) )
182 178 181 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 = 𝐾 ) → 𝐾 < ( 𝑚 + 1 ) )
183 182 iftrued ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 = 𝐾 ) → if ( 𝐾 < ( 𝑚 + 1 ) , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) ) = 0 )
184 183 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 = 𝐾 ) → 0 = if ( 𝐾 < ( 𝑚 + 1 ) , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) ) )
185 184 mpteq2dv ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 = 𝐾 ) → ( 𝑥 ∈ 𝑋 ↦ 0 ) = ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < ( 𝑚 + 1 ) , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) ) ) )
186 144 177 185 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 = 𝐾 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < 𝑚 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) ) ) ) = ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < ( 𝑚 + 1 ) , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) ) ) )
187 186 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 ≤ 𝐾 ) ∧ 𝑚 = 𝐾 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < 𝑚 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) ) ) ) = ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < ( 𝑚 + 1 ) , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) ) ) )
188 simpll ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 ≤ 𝐾 ) ∧ ¬ 𝑚 = 𝐾 ) → ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) )
189 188 100 114 3syl ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 ≤ 𝐾 ) ∧ ¬ 𝑚 = 𝐾 ) → 𝑚 ∈ ℝ )
190 76 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 ≤ 𝐾 ) ∧ ¬ 𝑚 = 𝐾 ) → 𝐾 ∈ ℝ )
191 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 ≤ 𝐾 ) ∧ ¬ 𝑚 = 𝐾 ) → 𝑚 ≤ 𝐾 )
192 neqne ⊢ ( ¬ 𝑚 = 𝐾 → 𝑚 ≠ 𝐾 )
193 192 necomd ⊢ ( ¬ 𝑚 = 𝐾 → 𝐾 ≠ 𝑚 )
194 193 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 ≤ 𝐾 ) ∧ ¬ 𝑚 = 𝐾 ) → 𝐾 ≠ 𝑚 )
195 189 190 191 194 leneltd ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 ≤ 𝐾 ) ∧ ¬ 𝑚 = 𝐾 ) → 𝑚 < 𝐾 )
196 114 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → 𝑚 ∈ ℝ )
197 76 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → 𝐾 ∈ ℝ )
198 simpr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → 𝑚 < 𝐾 )
199 196 197 198 ltled ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → 𝑚 ≤ 𝐾 )
200 196 197 lenltd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( 𝑚 ≤ 𝐾 ↔ ¬ 𝐾 < 𝑚 ) )
201 199 200 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ¬ 𝐾 < 𝑚 )
202 201 iffalsed ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → if ( 𝐾 < 𝑚 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) ) = ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) )
203 202 mpteq2dv ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < 𝑚 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) ) )
204 203 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < 𝑚 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) ) ) ) = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) ) ) )
205 1 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → 𝑆 ∈ { ℝ , ℂ } )
206 205 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → 𝑆 ∈ { ℝ , ℂ } )
207 87 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( ! ‘ 𝐾 ) ∈ ℂ )
208 100 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → 𝑚 ∈ ℕ0 )
209 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → 𝐾 ∈ ℕ0 )
210 nn0sub ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑚 ≤ 𝐾 ↔ ( 𝐾 − 𝑚 ) ∈ ℕ0 ) )
211 208 209 210 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( 𝑚 ≤ 𝐾 ↔ ( 𝐾 − 𝑚 ) ∈ ℕ0 ) )
212 199 211 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( 𝐾 − 𝑚 ) ∈ ℕ0 )
213 faccl ⊢ ( ( 𝐾 − 𝑚 ) ∈ ℕ0 → ( ! ‘ ( 𝐾 − 𝑚 ) ) ∈ ℕ )
214 212 213 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( ! ‘ ( 𝐾 − 𝑚 ) ) ∈ ℕ )
215 214 nncnd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( ! ‘ ( 𝐾 − 𝑚 ) ) ∈ ℂ )
216 214 nnne0d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( ! ‘ ( 𝐾 − 𝑚 ) ) ≠ 0 )
217 207 215 216 divcld ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) ∈ ℂ )
218 217 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) ∈ ℂ )
219 75 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) ∧ 𝑥 ∈ 𝑋 ) → 0 ∈ ℝ )
220 2 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
221 220 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
222 206 221 217 dvmptconst ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) ) ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) )
223 65 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 + 𝐴 ) ∈ ℂ )
224 223 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 + 𝐴 ) ∈ ℂ )
225 212 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝐾 − 𝑚 ) ∈ ℕ0 )
226 224 225 expcld ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ∈ ℂ )
227 225 nn0cnd ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝐾 − 𝑚 ) ∈ ℂ )
228 212 nn0zd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( 𝐾 − 𝑚 ) ∈ ℤ )
229 196 197 posdifd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( 𝑚 < 𝐾 ↔ 0 < ( 𝐾 − 𝑚 ) ) )
230 198 229 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → 0 < ( 𝐾 − 𝑚 ) )
231 228 230 jca ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( ( 𝐾 − 𝑚 ) ∈ ℤ ∧ 0 < ( 𝐾 − 𝑚 ) ) )
232 elnnz ⊢ ( ( 𝐾 − 𝑚 ) ∈ ℕ ↔ ( ( 𝐾 − 𝑚 ) ∈ ℤ ∧ 0 < ( 𝐾 − 𝑚 ) ) )
233 231 232 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( 𝐾 − 𝑚 ) ∈ ℕ )
234 nnm1nn0 ⊢ ( ( 𝐾 − 𝑚 ) ∈ ℕ → ( ( 𝐾 − 𝑚 ) − 1 ) ∈ ℕ0 )
235 233 234 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( ( 𝐾 − 𝑚 ) − 1 ) ∈ ℕ0 )
236 235 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐾 − 𝑚 ) − 1 ) ∈ ℕ0 )
237 224 236 expcld ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑥 + 𝐴 ) ↑ ( ( 𝐾 − 𝑚 ) − 1 ) ) ∈ ℂ )
238 227 237 mulcld ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐾 − 𝑚 ) · ( ( 𝑥 + 𝐴 ) ↑ ( ( 𝐾 − 𝑚 ) − 1 ) ) ) ∈ ℂ )
239 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → 𝐴 ∈ ℂ )
240 206 221 239 233 dvxpaek ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐾 − 𝑚 ) · ( ( 𝑥 + 𝐴 ) ↑ ( ( 𝐾 − 𝑚 ) − 1 ) ) ) ) )
241 206 218 219 222 226 238 240 dvmptmul ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 0 · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) + ( ( ( 𝐾 − 𝑚 ) · ( ( 𝑥 + 𝐴 ) ↑ ( ( 𝐾 − 𝑚 ) − 1 ) ) ) · ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) ) ) ) )
242 226 mul02d ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) ∧ 𝑥 ∈ 𝑋 ) → ( 0 · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) = 0 )
243 242 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 0 · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) + ( ( ( 𝐾 − 𝑚 ) · ( ( 𝑥 + 𝐴 ) ↑ ( ( 𝐾 − 𝑚 ) − 1 ) ) ) · ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) ) ) = ( 0 + ( ( ( 𝐾 − 𝑚 ) · ( ( 𝑥 + 𝐴 ) ↑ ( ( 𝐾 − 𝑚 ) − 1 ) ) ) · ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) ) ) )
244 238 218 mulcld ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝐾 − 𝑚 ) · ( ( 𝑥 + 𝐴 ) ↑ ( ( 𝐾 − 𝑚 ) − 1 ) ) ) · ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) ) ∈ ℂ )
245 244 addlidd ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) ∧ 𝑥 ∈ 𝑋 ) → ( 0 + ( ( ( 𝐾 − 𝑚 ) · ( ( 𝑥 + 𝐴 ) ↑ ( ( 𝐾 − 𝑚 ) − 1 ) ) ) · ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) ) ) = ( ( ( 𝐾 − 𝑚 ) · ( ( 𝑥 + 𝐴 ) ↑ ( ( 𝐾 − 𝑚 ) − 1 ) ) ) · ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) ) )
246 120 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → 𝑚 ∈ ℤ )
247 119 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → 𝐾 ∈ ℤ )
248 zltp1le ⊢ ( ( 𝑚 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑚 < 𝐾 ↔ ( 𝑚 + 1 ) ≤ 𝐾 ) )
249 246 247 248 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( 𝑚 < 𝐾 ↔ ( 𝑚 + 1 ) ≤ 𝐾 ) )
250 198 249 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( 𝑚 + 1 ) ≤ 𝐾 )
251 peano2re ⊢ ( 𝑚 ∈ ℝ → ( 𝑚 + 1 ) ∈ ℝ )
252 196 251 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( 𝑚 + 1 ) ∈ ℝ )
253 252 197 lenltd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( ( 𝑚 + 1 ) ≤ 𝐾 ↔ ¬ 𝐾 < ( 𝑚 + 1 ) ) )
254 250 253 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ¬ 𝐾 < ( 𝑚 + 1 ) )
255 254 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) ∧ 𝑥 ∈ 𝑋 ) → ¬ 𝐾 < ( 𝑚 + 1 ) )
256 255 iffalsed ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) ∧ 𝑥 ∈ 𝑋 ) → if ( 𝐾 < ( 𝑚 + 1 ) , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) ) = ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) )
257 218 227 237 mulassd ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( 𝐾 − 𝑚 ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( ( 𝐾 − 𝑚 ) − 1 ) ) ) = ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝐾 − 𝑚 ) · ( ( 𝑥 + 𝐴 ) ↑ ( ( 𝐾 − 𝑚 ) − 1 ) ) ) ) )
258 257 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝐾 − 𝑚 ) · ( ( 𝑥 + 𝐴 ) ↑ ( ( 𝐾 − 𝑚 ) − 1 ) ) ) ) = ( ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( 𝐾 − 𝑚 ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( ( 𝐾 − 𝑚 ) − 1 ) ) ) )
259 233 nncnd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( 𝐾 − 𝑚 ) ∈ ℂ )
260 207 215 259 216 div32d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( 𝐾 − 𝑚 ) ) = ( ( ! ‘ 𝐾 ) · ( ( 𝐾 − 𝑚 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) ) )
261 facnn2 ⊢ ( ( 𝐾 − 𝑚 ) ∈ ℕ → ( ! ‘ ( 𝐾 − 𝑚 ) ) = ( ( ! ‘ ( ( 𝐾 − 𝑚 ) − 1 ) ) · ( 𝐾 − 𝑚 ) ) )
262 233 261 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( ! ‘ ( 𝐾 − 𝑚 ) ) = ( ( ! ‘ ( ( 𝐾 − 𝑚 ) − 1 ) ) · ( 𝐾 − 𝑚 ) ) )
263 262 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( ( 𝐾 − 𝑚 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) = ( ( 𝐾 − 𝑚 ) / ( ( ! ‘ ( ( 𝐾 − 𝑚 ) − 1 ) ) · ( 𝐾 − 𝑚 ) ) ) )
264 faccl ⊢ ( ( ( 𝐾 − 𝑚 ) − 1 ) ∈ ℕ0 → ( ! ‘ ( ( 𝐾 − 𝑚 ) − 1 ) ) ∈ ℕ )
265 234 264 syl ⊢ ( ( 𝐾 − 𝑚 ) ∈ ℕ → ( ! ‘ ( ( 𝐾 − 𝑚 ) − 1 ) ) ∈ ℕ )
266 265 nncnd ⊢ ( ( 𝐾 − 𝑚 ) ∈ ℕ → ( ! ‘ ( ( 𝐾 − 𝑚 ) − 1 ) ) ∈ ℂ )
267 233 266 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( ! ‘ ( ( 𝐾 − 𝑚 ) − 1 ) ) ∈ ℂ )
268 235 264 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( ! ‘ ( ( 𝐾 − 𝑚 ) − 1 ) ) ∈ ℕ )
269 nnne0 ⊢ ( ( ! ‘ ( ( 𝐾 − 𝑚 ) − 1 ) ) ∈ ℕ → ( ! ‘ ( ( 𝐾 − 𝑚 ) − 1 ) ) ≠ 0 )
270 268 269 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( ! ‘ ( ( 𝐾 − 𝑚 ) − 1 ) ) ≠ 0 )
271 nnne0 ⊢ ( ( 𝐾 − 𝑚 ) ∈ ℕ → ( 𝐾 − 𝑚 ) ≠ 0 )
272 233 271 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( 𝐾 − 𝑚 ) ≠ 0 )
273 267 259 270 272 divcan8d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( ( 𝐾 − 𝑚 ) / ( ( ! ‘ ( ( 𝐾 − 𝑚 ) − 1 ) ) · ( 𝐾 − 𝑚 ) ) ) = ( 1 / ( ! ‘ ( ( 𝐾 − 𝑚 ) − 1 ) ) ) )
274 263 273 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( ( 𝐾 − 𝑚 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) = ( 1 / ( ! ‘ ( ( 𝐾 − 𝑚 ) − 1 ) ) ) )
275 274 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( ( ! ‘ 𝐾 ) · ( ( 𝐾 − 𝑚 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) ) = ( ( ! ‘ 𝐾 ) · ( 1 / ( ! ‘ ( ( 𝐾 − 𝑚 ) − 1 ) ) ) ) )
276 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( ( ! ‘ 𝐾 ) · ( 1 / ( ! ‘ ( ( 𝐾 − 𝑚 ) − 1 ) ) ) ) = ( ( ! ‘ 𝐾 ) · ( 1 / ( ! ‘ ( ( 𝐾 − 𝑚 ) − 1 ) ) ) ) )
277 260 275 276 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( 𝐾 − 𝑚 ) ) = ( ( ! ‘ 𝐾 ) · ( 1 / ( ! ‘ ( ( 𝐾 − 𝑚 ) − 1 ) ) ) ) )
278 277 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( 𝐾 − 𝑚 ) ) = ( ( ! ‘ 𝐾 ) · ( 1 / ( ! ‘ ( ( 𝐾 − 𝑚 ) − 1 ) ) ) ) )
279 81 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → 𝐾 ∈ ℂ )
280 100 nn0cnd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → 𝑚 ∈ ℂ )
281 1cnd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → 1 ∈ ℂ )
282 279 280 281 subsub4d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝐾 − 𝑚 ) − 1 ) = ( 𝐾 − ( 𝑚 + 1 ) ) )
283 282 oveq2d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝑥 + 𝐴 ) ↑ ( ( 𝐾 − 𝑚 ) − 1 ) ) = ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − ( 𝑚 + 1 ) ) ) )
284 283 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑥 + 𝐴 ) ↑ ( ( 𝐾 − 𝑚 ) − 1 ) ) = ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − ( 𝑚 + 1 ) ) ) )
285 278 284 oveq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( 𝐾 − 𝑚 ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( ( 𝐾 − 𝑚 ) − 1 ) ) ) = ( ( ( ! ‘ 𝐾 ) · ( 1 / ( ! ‘ ( ( 𝐾 − 𝑚 ) − 1 ) ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) )
286 282 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( ( 𝐾 − 𝑚 ) − 1 ) = ( 𝐾 − ( 𝑚 + 1 ) ) )
287 286 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( 𝐾 − ( 𝑚 + 1 ) ) = ( ( 𝐾 − 𝑚 ) − 1 ) )
288 287 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( ! ‘ ( 𝐾 − ( 𝑚 + 1 ) ) ) = ( ! ‘ ( ( 𝐾 − 𝑚 ) − 1 ) ) )
289 288 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) = ( ( ! ‘ 𝐾 ) / ( ! ‘ ( ( 𝐾 − 𝑚 ) − 1 ) ) ) )
290 207 267 270 divrecd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( ( ! ‘ 𝐾 ) / ( ! ‘ ( ( 𝐾 − 𝑚 ) − 1 ) ) ) = ( ( ! ‘ 𝐾 ) · ( 1 / ( ! ‘ ( ( 𝐾 − 𝑚 ) − 1 ) ) ) ) )
291 289 290 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( ( ! ‘ 𝐾 ) · ( 1 / ( ! ‘ ( ( 𝐾 − 𝑚 ) − 1 ) ) ) ) = ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) )
292 291 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ! ‘ 𝐾 ) · ( 1 / ( ! ‘ ( ( 𝐾 − 𝑚 ) − 1 ) ) ) ) = ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) )
293 292 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ( ! ‘ 𝐾 ) · ( 1 / ( ! ‘ ( ( 𝐾 − 𝑚 ) − 1 ) ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) = ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) )
294 258 285 293 3eqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) = ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝐾 − 𝑚 ) · ( ( 𝑥 + 𝐴 ) ↑ ( ( 𝐾 − 𝑚 ) − 1 ) ) ) ) )
295 218 238 mulcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝐾 − 𝑚 ) · ( ( 𝑥 + 𝐴 ) ↑ ( ( 𝐾 − 𝑚 ) − 1 ) ) ) ) = ( ( ( 𝐾 − 𝑚 ) · ( ( 𝑥 + 𝐴 ) ↑ ( ( 𝐾 − 𝑚 ) − 1 ) ) ) · ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) ) )
296 256 294 295 3eqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝐾 − 𝑚 ) · ( ( 𝑥 + 𝐴 ) ↑ ( ( 𝐾 − 𝑚 ) − 1 ) ) ) · ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) ) = if ( 𝐾 < ( 𝑚 + 1 ) , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) ) )
297 243 245 296 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 0 · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) + ( ( ( 𝐾 − 𝑚 ) · ( ( 𝑥 + 𝐴 ) ↑ ( ( 𝐾 − 𝑚 ) − 1 ) ) ) · ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) ) ) = if ( 𝐾 < ( 𝑚 + 1 ) , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) ) )
298 297 mpteq2dva ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( 𝑥 ∈ 𝑋 ↦ ( ( 0 · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) + ( ( ( 𝐾 − 𝑚 ) · ( ( 𝑥 + 𝐴 ) ↑ ( ( 𝐾 − 𝑚 ) − 1 ) ) ) · ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) ) ) ) = ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < ( 𝑚 + 1 ) , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) ) ) )
299 204 241 298 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 < 𝐾 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < 𝑚 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) ) ) ) = ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < ( 𝑚 + 1 ) , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) ) ) )
300 188 195 299 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 ≤ 𝐾 ) ∧ ¬ 𝑚 = 𝐾 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < 𝑚 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) ) ) ) = ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < ( 𝑚 + 1 ) , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) ) ) )
301 187 300 pm2.61dan ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑚 ≤ 𝐾 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < 𝑚 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) ) ) ) = ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < ( 𝑚 + 1 ) , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) ) ) )
302 129 134 301 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ¬ 𝐾 < 𝑚 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < 𝑚 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) ) ) ) = ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < ( 𝑚 + 1 ) , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) ) ) )
303 128 302 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < 𝑚 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) ) ) ) = ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < ( 𝑚 + 1 ) , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) ) ) )
304 303 adantr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑚 ) = ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < 𝑚 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) ) ) ) → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < 𝑚 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) ) ) ) = ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < ( 𝑚 + 1 ) , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) ) ) )
305 103 105 304 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ0 ) ∧ ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑚 ) = ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < 𝑚 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑚 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑚 ) ) ) ) ) ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑚 + 1 ) ) = ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < ( 𝑚 + 1 ) , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − ( 𝑚 + 1 ) ) ) ) ) ) )
306 16 27 38 49 97 305 nn0indd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) = ( 𝑥 ∈ 𝑋 ↦ if ( 𝐾 < 𝑁 , 0 , ( ( ( ! ‘ 𝐾 ) / ( ! ‘ ( 𝐾 − 𝑁 ) ) ) · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 𝑁 ) ) ) ) ) )