Metamath Proof Explorer

Theorem lcmineqlem10

Description: Induction step of lcmineqlem13 (deduction form). (Contributed by metakunt, 12-May-2024)

Ref Expression
Hypotheses lcmineqlem10.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
lcmineqlem10.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
lcmineqlem10.3 ⊢ ( 𝜑 → 𝑀 < 𝑁 )
Assertion lcmineqlem10 ( 𝜑 → ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( ( 𝑀 + 1 ) − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − ( 𝑀 + 1 ) ) ) ) d 𝑥 = ( ( 𝑀 / ( 𝑁 − 𝑀 ) ) · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 ) )

Proof

Step Hyp Ref Expression
1 lcmineqlem10.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 lcmineqlem10.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3 lcmineqlem10.3 ⊢ ( 𝜑 → 𝑀 < 𝑁 )
4 2 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
5 1 nncnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
6 4 5 subcld ⊢ ( 𝜑 → ( 𝑁 − 𝑀 ) ∈ ℂ )
7 elunitcn ⊢ ( 𝑥 ∈ ( 0 [,] 1 ) → 𝑥 ∈ ℂ )
8 1 nnnn0d ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
9 expcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑥 ↑ 𝑀 ) ∈ ℂ )
10 8 9 sylan2 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝜑 ) → ( 𝑥 ↑ 𝑀 ) ∈ ℂ )
11 10 ancoms ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝑥 ↑ 𝑀 ) ∈ ℂ )
12 7 11 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( 𝑥 ↑ 𝑀 ) ∈ ℂ )
13 1cnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 1 ∈ ℂ )
14 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝑥 ∈ ℂ )
15 13 14 subcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 1 − 𝑥 ) ∈ ℂ )
16 1 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
17 2 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
18 znnsub ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 < 𝑁 ↔ ( 𝑁 − 𝑀 ) ∈ ℕ ) )
19 16 17 18 syl2anc ⊢ ( 𝜑 → ( 𝑀 < 𝑁 ↔ ( 𝑁 − 𝑀 ) ∈ ℕ ) )
20 3 19 mpbid ⊢ ( 𝜑 → ( 𝑁 − 𝑀 ) ∈ ℕ )
21 nnm1nn0 ⊢ ( ( 𝑁 − 𝑀 ) ∈ ℕ → ( ( 𝑁 − 𝑀 ) − 1 ) ∈ ℕ0 )
22 20 21 syl ⊢ ( 𝜑 → ( ( 𝑁 − 𝑀 ) − 1 ) ∈ ℕ0 )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( 𝑁 − 𝑀 ) − 1 ) ∈ ℕ0 )
24 15 23 expcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ∈ ℂ )
25 7 24 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ∈ ℂ )
26 12 25 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( ( 𝑥 ↑ 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) ∈ ℂ )
27 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
28 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
29 expcncf ⊢ ( 𝑀 ∈ ℕ0 → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑀 ) ) ∈ ( ℂ –cn→ ℂ ) )
30 8 29 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑀 ) ) ∈ ( ℂ –cn→ ℂ ) )
31 1nn ⊢ 1 ∈ ℕ
32 31 a1i ⊢ ( 𝜑 → 1 ∈ ℕ )
33 20 nnge1d ⊢ ( 𝜑 → 1 ≤ ( 𝑁 − 𝑀 ) )
34 32 20 33 lcmineqlem9 ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) ∈ ( ℂ –cn→ ℂ ) )
35 30 34 mulcncf ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( ( 𝑥 ↑ 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) ) ∈ ( ℂ –cn→ ℂ ) )
36 35 resclunitintvd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑥 ↑ 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) )
37 cnicciblnc ⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑥 ↑ 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑥 ↑ 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) ) ∈ 𝐿1 )
38 27 28 36 37 syl3anc ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑥 ↑ 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) ) ∈ 𝐿1 )
39 26 38 itgcl ⊢ ( 𝜑 → ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) d 𝑥 ∈ ℂ )
40 6 39 mulneg1d ⊢ ( 𝜑 → ( - ( 𝑁 − 𝑀 ) · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) d 𝑥 ) = - ( ( 𝑁 − 𝑀 ) · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) d 𝑥 ) )
41 6 negcld ⊢ ( 𝜑 → - ( 𝑁 − 𝑀 ) ∈ ℂ )
42 41 26 38 itgmulc2 ⊢ ( 𝜑 → ( - ( 𝑁 − 𝑀 ) · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) d 𝑥 ) = ∫ ( 0 [,] 1 ) ( - ( 𝑁 − 𝑀 ) · ( ( 𝑥 ↑ 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) ) d 𝑥 )
43 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝑁 ∈ ℂ )
44 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝑀 ∈ ℂ )
45 43 44 subcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝑁 − 𝑀 ) ∈ ℂ )
46 45 negcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → - ( 𝑁 − 𝑀 ) ∈ ℂ )
47 11 46 24 mul12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( 𝑥 ↑ 𝑀 ) · ( - ( 𝑁 − 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) ) = ( - ( 𝑁 − 𝑀 ) · ( ( 𝑥 ↑ 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) ) )
48 7 47 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( ( 𝑥 ↑ 𝑀 ) · ( - ( 𝑁 − 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) ) = ( - ( 𝑁 − 𝑀 ) · ( ( 𝑥 ↑ 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) ) )
49 48 itgeq2dv ⊢ ( 𝜑 → ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ 𝑀 ) · ( - ( 𝑁 − 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) ) d 𝑥 = ∫ ( 0 [,] 1 ) ( - ( 𝑁 − 𝑀 ) · ( ( 𝑥 ↑ 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) ) d 𝑥 )
50 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → 𝑁 ∈ ℂ )
51 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → 𝑀 ∈ ℂ )
52 50 51 subcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( 𝑁 − 𝑀 ) ∈ ℂ )
53 52 negcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → - ( 𝑁 − 𝑀 ) ∈ ℂ )
54 53 25 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( - ( 𝑁 − 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) ∈ ℂ )
55 12 54 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( ( 𝑥 ↑ 𝑀 ) · ( - ( 𝑁 − 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) ) ∈ ℂ )
56 27 28 55 itgioo ⊢ ( 𝜑 → ∫ ( 0 (,) 1 ) ( ( 𝑥 ↑ 𝑀 ) · ( - ( 𝑁 − 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) ) d 𝑥 = ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ 𝑀 ) · ( - ( 𝑁 − 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) ) d 𝑥 )
57 0le1 ⊢ 0 ≤ 1
58 57 a1i ⊢ ( 𝜑 → 0 ≤ 1 )
59 30 resclunitintvd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ↑ 𝑀 ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) )
60 1 nnred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
61 2 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
62 ltle ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑀 < 𝑁 → 𝑀 ≤ 𝑁 ) )
63 60 61 62 syl2anc ⊢ ( 𝜑 → ( 𝑀 < 𝑁 → 𝑀 ≤ 𝑁 ) )
64 3 63 mpd ⊢ ( 𝜑 → 𝑀 ≤ 𝑁 )
65 1 2 64 lcmineqlem9 ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) ∈ ( ℂ –cn→ ℂ ) )
66 65 resclunitintvd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) )
67 ssid ⊢ ℂ ⊆ ℂ
68 cncfmptc ⊢ ( ( 𝑀 ∈ ℂ ∧ ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑥 ∈ ℂ ↦ 𝑀 ) ∈ ( ℂ –cn→ ℂ ) )
69 67 67 68 mp3an23 ⊢ ( 𝑀 ∈ ℂ → ( 𝑥 ∈ ℂ ↦ 𝑀 ) ∈ ( ℂ –cn→ ℂ ) )
70 5 69 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ 𝑀 ) ∈ ( ℂ –cn→ ℂ ) )
71 70 resopunitintvd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 (,) 1 ) ↦ 𝑀 ) ∈ ( ( 0 (,) 1 ) –cn→ ℂ ) )
72 nnm1nn0 ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 − 1 ) ∈ ℕ0 )
73 expcncf ⊢ ( ( 𝑀 − 1 ) ∈ ℕ0 → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) ∈ ( ℂ –cn→ ℂ ) )
74 1 72 73 3syl ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) ∈ ( ℂ –cn→ ℂ ) )
75 74 resopunitintvd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 (,) 1 ) ↦ ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) ∈ ( ( 0 (,) 1 ) –cn→ ℂ ) )
76 71 75 mulcncf ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 (,) 1 ) ↦ ( 𝑀 · ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) ) ∈ ( ( 0 (,) 1 ) –cn→ ℂ ) )
77 cncfmptc ⊢ ( ( - ( 𝑁 − 𝑀 ) ∈ ℂ ∧ ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑥 ∈ ℂ ↦ - ( 𝑁 − 𝑀 ) ) ∈ ( ℂ –cn→ ℂ ) )
78 67 67 77 mp3an23 ⊢ ( - ( 𝑁 − 𝑀 ) ∈ ℂ → ( 𝑥 ∈ ℂ ↦ - ( 𝑁 − 𝑀 ) ) ∈ ( ℂ –cn→ ℂ ) )
79 41 78 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ - ( 𝑁 − 𝑀 ) ) ∈ ( ℂ –cn→ ℂ ) )
80 79 resopunitintvd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 (,) 1 ) ↦ - ( 𝑁 − 𝑀 ) ) ∈ ( ( 0 (,) 1 ) –cn→ ℂ ) )
81 34 resopunitintvd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 (,) 1 ) ↦ ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) ∈ ( ( 0 (,) 1 ) –cn→ ℂ ) )
82 80 81 mulcncf ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 (,) 1 ) ↦ ( - ( 𝑁 − 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) ) ∈ ( ( 0 (,) 1 ) –cn→ ℂ ) )
83 ioossicc ⊢ ( 0 (,) 1 ) ⊆ ( 0 [,] 1 )
84 83 a1i ⊢ ( 𝜑 → ( 0 (,) 1 ) ⊆ ( 0 [,] 1 ) )
85 ioombl ⊢ ( 0 (,) 1 ) ∈ dom vol
86 85 a1i ⊢ ( 𝜑 → ( 0 (,) 1 ) ∈ dom vol )
87 79 34 mulcncf ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( - ( 𝑁 − 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) ) ∈ ( ℂ –cn→ ℂ ) )
88 30 87 mulcncf ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( ( 𝑥 ↑ 𝑀 ) · ( - ( 𝑁 − 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) ) ) ∈ ( ℂ –cn→ ℂ ) )
89 88 resclunitintvd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑥 ↑ 𝑀 ) · ( - ( 𝑁 − 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) )
90 cnicciblnc ⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑥 ↑ 𝑀 ) · ( - ( 𝑁 − 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑥 ↑ 𝑀 ) · ( - ( 𝑁 − 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) ) ) ∈ 𝐿1 )
91 27 28 89 90 syl3anc ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑥 ↑ 𝑀 ) · ( - ( 𝑁 − 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) ) ) ∈ 𝐿1 )
92 84 86 55 91 iblss ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 (,) 1 ) ↦ ( ( 𝑥 ↑ 𝑀 ) · ( - ( 𝑁 − 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) ) ) ∈ 𝐿1 )
93 1 72 syl ⊢ ( 𝜑 → ( 𝑀 − 1 ) ∈ ℕ0 )
94 expcl ⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝑀 − 1 ) ∈ ℕ0 ) → ( 𝑥 ↑ ( 𝑀 − 1 ) ) ∈ ℂ )
95 93 94 sylan2 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝜑 ) → ( 𝑥 ↑ ( 𝑀 − 1 ) ) ∈ ℂ )
96 95 ancoms ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝑥 ↑ ( 𝑀 − 1 ) ) ∈ ℂ )
97 7 96 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( 𝑥 ↑ ( 𝑀 − 1 ) ) ∈ ℂ )
98 51 97 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( 𝑀 · ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) ∈ ℂ )
99 20 nnnn0d ⊢ ( 𝜑 → ( 𝑁 − 𝑀 ) ∈ ℕ0 )
100 99 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝑁 − 𝑀 ) ∈ ℕ0 )
101 15 100 expcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ∈ ℂ )
102 7 101 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ∈ ℂ )
103 98 102 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( ( 𝑀 · ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) ∈ ℂ )
104 70 74 mulcncf ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( 𝑀 · ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) ) ∈ ( ℂ –cn→ ℂ ) )
105 104 65 mulcncf ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( ( 𝑀 · ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) ) ∈ ( ℂ –cn→ ℂ ) )
106 105 resclunitintvd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑀 · ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) )
107 cnicciblnc ⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑀 · ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑀 · ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) ) ∈ 𝐿1 )
108 27 28 106 107 syl3anc ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑀 · ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) ) ∈ 𝐿1 )
109 84 86 103 108 iblss ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 (,) 1 ) ↦ ( ( 𝑀 · ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) ) ∈ 𝐿1 )
110 dvexp ⊢ ( 𝑀 ∈ ℕ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑀 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑀 · ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) ) )
111 1 110 syl ⊢ ( 𝜑 → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑀 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑀 · ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) ) )
112 44 96 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝑀 · ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) ∈ ℂ )
113 111 11 112 resdvopclptsd ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 ↑ 𝑀 ) ) ) = ( 𝑥 ∈ ( 0 (,) 1 ) ↦ ( 𝑀 · ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) ) )
114 1 2 3 lcmineqlem8 ⊢ ( 𝜑 → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( - ( 𝑁 − 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) ) )
115 46 24 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( - ( 𝑁 − 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) ∈ ℂ )
116 114 101 115 resdvopclptsd ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) ) = ( 𝑥 ∈ ( 0 (,) 1 ) ↦ ( - ( 𝑁 − 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) ) )
117 oveq1 ⊢ ( 𝑥 = 0 → ( 𝑥 ↑ 𝑀 ) = ( 0 ↑ 𝑀 ) )
118 117 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = 0 ) → ( 𝑥 ↑ 𝑀 ) = ( 0 ↑ 𝑀 ) )
119 1 0expd ⊢ ( 𝜑 → ( 0 ↑ 𝑀 ) = 0 )
120 119 adantr ⊢ ( ( 𝜑 ∧ 𝑥 = 0 ) → ( 0 ↑ 𝑀 ) = 0 )
121 118 120 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 = 0 ) → ( 𝑥 ↑ 𝑀 ) = 0 )
122 121 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 = 0 ) → ( ( 𝑥 ↑ 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) = ( 0 · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) )
123 0cn ⊢ 0 ∈ ℂ
124 eleq1 ⊢ ( 𝑥 = 0 → ( 𝑥 ∈ ℂ ↔ 0 ∈ ℂ ) )
125 123 124 mpbiri ⊢ ( 𝑥 = 0 → 𝑥 ∈ ℂ )
126 101 mul02d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 0 · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) = 0 )
127 125 126 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 = 0 ) → ( 0 · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) = 0 )
128 122 127 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 = 0 ) → ( ( 𝑥 ↑ 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) = 0 )
129 oveq2 ⊢ ( 𝑥 = 1 → ( 1 − 𝑥 ) = ( 1 − 1 ) )
130 1m1e0 ⊢ ( 1 − 1 ) = 0
131 129 130 eqtrdi ⊢ ( 𝑥 = 1 → ( 1 − 𝑥 ) = 0 )
132 131 oveq1d ⊢ ( 𝑥 = 1 → ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) = ( 0 ↑ ( 𝑁 − 𝑀 ) ) )
133 132 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = 1 ) → ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) = ( 0 ↑ ( 𝑁 − 𝑀 ) ) )
134 20 0expd ⊢ ( 𝜑 → ( 0 ↑ ( 𝑁 − 𝑀 ) ) = 0 )
135 134 adantr ⊢ ( ( 𝜑 ∧ 𝑥 = 1 ) → ( 0 ↑ ( 𝑁 − 𝑀 ) ) = 0 )
136 133 135 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 = 1 ) → ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) = 0 )
137 136 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 = 1 ) → ( ( 𝑥 ↑ 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) = ( ( 𝑥 ↑ 𝑀 ) · 0 ) )
138 ax-1cn ⊢ 1 ∈ ℂ
139 eleq1 ⊢ ( 𝑥 = 1 → ( 𝑥 ∈ ℂ ↔ 1 ∈ ℂ ) )
140 138 139 mpbiri ⊢ ( 𝑥 = 1 → 𝑥 ∈ ℂ )
141 11 mul01d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( 𝑥 ↑ 𝑀 ) · 0 ) = 0 )
142 140 141 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 = 1 ) → ( ( 𝑥 ↑ 𝑀 ) · 0 ) = 0 )
143 137 142 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 = 1 ) → ( ( 𝑥 ↑ 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) = 0 )
144 27 28 58 59 66 76 82 92 109 113 116 128 143 itgparts ⊢ ( 𝜑 → ∫ ( 0 (,) 1 ) ( ( 𝑥 ↑ 𝑀 ) · ( - ( 𝑁 − 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) ) d 𝑥 = ( ( 0 − 0 ) − ∫ ( 0 (,) 1 ) ( ( 𝑀 · ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 ) )
145 56 144 eqtr3d ⊢ ( 𝜑 → ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ 𝑀 ) · ( - ( 𝑁 − 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) ) d 𝑥 = ( ( 0 − 0 ) − ∫ ( 0 (,) 1 ) ( ( 𝑀 · ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 ) )
146 27 28 103 itgioo ⊢ ( 𝜑 → ∫ ( 0 (,) 1 ) ( ( 𝑀 · ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 = ∫ ( 0 [,] 1 ) ( ( 𝑀 · ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 )
147 146 oveq2d ⊢ ( 𝜑 → ( ( 0 − 0 ) − ∫ ( 0 (,) 1 ) ( ( 𝑀 · ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 ) = ( ( 0 − 0 ) − ∫ ( 0 [,] 1 ) ( ( 𝑀 · ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 ) )
148 145 147 eqtrd ⊢ ( 𝜑 → ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ 𝑀 ) · ( - ( 𝑁 − 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) ) d 𝑥 = ( ( 0 − 0 ) − ∫ ( 0 [,] 1 ) ( ( 𝑀 · ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 ) )
149 0m0e0 ⊢ ( 0 − 0 ) = 0
150 149 oveq1i ⊢ ( ( 0 − 0 ) − ∫ ( 0 [,] 1 ) ( ( 𝑀 · ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 ) = ( 0 − ∫ ( 0 [,] 1 ) ( ( 𝑀 · ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 )
151 148 150 eqtrdi ⊢ ( 𝜑 → ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ 𝑀 ) · ( - ( 𝑁 − 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) ) d 𝑥 = ( 0 − ∫ ( 0 [,] 1 ) ( ( 𝑀 · ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 ) )
152 49 151 eqtr3d ⊢ ( 𝜑 → ∫ ( 0 [,] 1 ) ( - ( 𝑁 − 𝑀 ) · ( ( 𝑥 ↑ 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) ) d 𝑥 = ( 0 − ∫ ( 0 [,] 1 ) ( ( 𝑀 · ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 ) )
153 42 152 eqtrd ⊢ ( 𝜑 → ( - ( 𝑁 − 𝑀 ) · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) d 𝑥 ) = ( 0 − ∫ ( 0 [,] 1 ) ( ( 𝑀 · ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 ) )
154 44 96 101 mulassd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( 𝑀 · ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) = ( 𝑀 · ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) ) )
155 7 154 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( ( 𝑀 · ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) = ( 𝑀 · ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) ) )
156 155 itgeq2dv ⊢ ( 𝜑 → ∫ ( 0 [,] 1 ) ( ( 𝑀 · ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 = ∫ ( 0 [,] 1 ) ( 𝑀 · ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) ) d 𝑥 )
157 156 oveq2d ⊢ ( 𝜑 → ( 0 − ∫ ( 0 [,] 1 ) ( ( 𝑀 · ( 𝑥 ↑ ( 𝑀 − 1 ) ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 ) = ( 0 − ∫ ( 0 [,] 1 ) ( 𝑀 · ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) ) d 𝑥 ) )
158 153 157 eqtrd ⊢ ( 𝜑 → ( - ( 𝑁 − 𝑀 ) · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) d 𝑥 ) = ( 0 − ∫ ( 0 [,] 1 ) ( 𝑀 · ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) ) d 𝑥 ) )
159 97 102 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) ∈ ℂ )
160 74 65 mulcncf ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) ) ∈ ( ℂ –cn→ ℂ ) )
161 160 resclunitintvd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) )
162 cnicciblnc ⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) ) ∈ ( ( 0 [,] 1 ) –cn→ ℂ ) ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) ) ∈ 𝐿1 )
163 27 28 161 162 syl3anc ⊢ ( 𝜑 → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) ) ∈ 𝐿1 )
164 5 159 163 itgmulc2 ⊢ ( 𝜑 → ( 𝑀 · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 ) = ∫ ( 0 [,] 1 ) ( 𝑀 · ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) ) d 𝑥 )
165 164 oveq2d ⊢ ( 𝜑 → ( 0 − ( 𝑀 · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 ) ) = ( 0 − ∫ ( 0 [,] 1 ) ( 𝑀 · ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) ) d 𝑥 ) )
166 158 165 eqtr4d ⊢ ( 𝜑 → ( - ( 𝑁 − 𝑀 ) · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) d 𝑥 ) = ( 0 − ( 𝑀 · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 ) ) )
167 df-neg ⊢ - ( 𝑀 · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 ) = ( 0 − ( 𝑀 · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 ) )
168 166 167 eqtr4di ⊢ ( 𝜑 → ( - ( 𝑁 − 𝑀 ) · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) d 𝑥 ) = - ( 𝑀 · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 ) )
169 40 168 eqtr3d ⊢ ( 𝜑 → - ( ( 𝑁 − 𝑀 ) · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) d 𝑥 ) = - ( 𝑀 · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 ) )
170 6 39 mulcld ⊢ ( 𝜑 → ( ( 𝑁 − 𝑀 ) · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) d 𝑥 ) ∈ ℂ )
171 159 163 itgcl ⊢ ( 𝜑 → ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 ∈ ℂ )
172 5 171 mulcld ⊢ ( 𝜑 → ( 𝑀 · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 ) ∈ ℂ )
173 170 172 neg11ad ⊢ ( 𝜑 → ( - ( ( 𝑁 − 𝑀 ) · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) d 𝑥 ) = - ( 𝑀 · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 ) ↔ ( ( 𝑁 − 𝑀 ) · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) d 𝑥 ) = ( 𝑀 · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 ) ) )
174 169 173 mpbid ⊢ ( 𝜑 → ( ( 𝑁 − 𝑀 ) · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) d 𝑥 ) = ( 𝑀 · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 ) )
175 20 nnne0d ⊢ ( 𝜑 → ( 𝑁 − 𝑀 ) ≠ 0 )
176 172 6 39 175 divmuld ⊢ ( 𝜑 → ( ( ( 𝑀 · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 ) / ( 𝑁 − 𝑀 ) ) = ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) d 𝑥 ↔ ( ( 𝑁 − 𝑀 ) · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) d 𝑥 ) = ( 𝑀 · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 ) ) )
177 174 176 mpbird ⊢ ( 𝜑 → ( ( 𝑀 · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 ) / ( 𝑁 − 𝑀 ) ) = ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) d 𝑥 )
178 138 a1i ⊢ ( 𝜑 → 1 ∈ ℂ )
179 5 178 pncand ⊢ ( 𝜑 → ( ( 𝑀 + 1 ) − 1 ) = 𝑀 )
180 179 eqcomd ⊢ ( 𝜑 → 𝑀 = ( ( 𝑀 + 1 ) − 1 ) )
181 180 oveq2d ⊢ ( 𝜑 → ( 𝑥 ↑ 𝑀 ) = ( 𝑥 ↑ ( ( 𝑀 + 1 ) − 1 ) ) )
182 4 5 178 subsub4d ⊢ ( 𝜑 → ( ( 𝑁 − 𝑀 ) − 1 ) = ( 𝑁 − ( 𝑀 + 1 ) ) )
183 182 oveq2d ⊢ ( 𝜑 → ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) = ( ( 1 − 𝑥 ) ↑ ( 𝑁 − ( 𝑀 + 1 ) ) ) )
184 181 183 oveq12d ⊢ ( 𝜑 → ( ( 𝑥 ↑ 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) = ( ( 𝑥 ↑ ( ( 𝑀 + 1 ) − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − ( 𝑀 + 1 ) ) ) ) )
185 184 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] 1 ) ) → ( ( 𝑥 ↑ 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) = ( ( 𝑥 ↑ ( ( 𝑀 + 1 ) − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − ( 𝑀 + 1 ) ) ) ) )
186 185 itgeq2dv ⊢ ( 𝜑 → ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ 𝑀 ) · ( ( 1 − 𝑥 ) ↑ ( ( 𝑁 − 𝑀 ) − 1 ) ) ) d 𝑥 = ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( ( 𝑀 + 1 ) − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − ( 𝑀 + 1 ) ) ) ) d 𝑥 )
187 177 186 eqtrd ⊢ ( 𝜑 → ( ( 𝑀 · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 ) / ( 𝑁 − 𝑀 ) ) = ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( ( 𝑀 + 1 ) − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − ( 𝑀 + 1 ) ) ) ) d 𝑥 )
188 187 eqcomd ⊢ ( 𝜑 → ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( ( 𝑀 + 1 ) − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − ( 𝑀 + 1 ) ) ) ) d 𝑥 = ( ( 𝑀 · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 ) / ( 𝑁 − 𝑀 ) ) )
189 5 171 6 175 div23d ⊢ ( 𝜑 → ( ( 𝑀 · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 ) / ( 𝑁 − 𝑀 ) ) = ( ( 𝑀 / ( 𝑁 − 𝑀 ) ) · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 ) )
190 188 189 eqtrd ⊢ ( 𝜑 → ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( ( 𝑀 + 1 ) − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − ( 𝑀 + 1 ) ) ) ) d 𝑥 = ( ( 𝑀 / ( 𝑁 − 𝑀 ) ) · ∫ ( 0 [,] 1 ) ( ( 𝑥 ↑ ( 𝑀 − 1 ) ) · ( ( 1 − 𝑥 ) ↑ ( 𝑁 − 𝑀 ) ) ) d 𝑥 ) )