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