lcmineqlem10

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

	Ref	Expression
Hypotheses	lcmineqlem10.1	$⊢ φ \to M \in ℕ$
	lcmineqlem10.2	$⊢ φ \to N \in ℕ$
	lcmineqlem10.3	$⊢ φ \to M < N$
Assertion	lcmineqlem10	$⊢ φ \to \int_{[0, 1]} x^{M + 1 - 1} {(1 - x)}^{N - (M + 1)} d x = (\frac{M}{N - M}) \int_{[0, 1]} x^{M - 1} {(1 - x)}^{N - M} d x$

Proof

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

Metamath Proof Explorer

Theorem lcmineqlem10

Proof