Metamath Proof Explorer

Theorem lcmineqlem10

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

Ref Expression
Hypotheses lcmineqlem10.1 
|- ( ph -> M e. NN )
lcmineqlem10.2 
|- ( ph -> N e. NN )
lcmineqlem10.3 
|- ( ph -> M < N )
Assertion lcmineqlem10 
|- ( ph -> S. ( 0 [,] 1 ) ( ( x ^ ( ( M + 1 ) - 1 ) ) x. ( ( 1 - x ) ^ ( N - ( M + 1 ) ) ) ) _d x = ( ( M / ( N - M ) ) x. S. ( 0 [,] 1 ) ( ( x ^ ( M - 1 ) ) x. ( ( 1 - x ) ^ ( N - M ) ) ) _d x ) )

Proof

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