Metamath Proof Explorer

Theorem lcmineqlem12

Description: Base case for induction. (Contributed by metakunt, 12-May-2024)

Ref Expression
Hypothesis lcmineqlem12.1 
|- ( ph -> N e. NN )
Assertion lcmineqlem12 
|- ( ph -> S. ( 0 [,] 1 ) ( ( t ^ ( 1 - 1 ) ) x. ( ( 1 - t ) ^ ( N - 1 ) ) ) _d t = ( 1 / ( 1 x. ( N _C 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 lcmineqlem12.1 
 |-  ( ph -> N e. NN )
2 elunitcn 
 |-  ( t e. ( 0 [,] 1 ) -> t e. CC )
3 1m1e0 
 |-  ( 1 - 1 ) = 0
4 3 oveq2i 
 |-  ( t ^ ( 1 - 1 ) ) = ( t ^ 0 )
5 simpr 
 |-  ( ( ph /\ t e. CC ) -> t e. CC )
6 5 exp0d 
 |-  ( ( ph /\ t e. CC ) -> ( t ^ 0 ) = 1 )
7 4 6 syl5eq 
 |-  ( ( ph /\ t e. CC ) -> ( t ^ ( 1 - 1 ) ) = 1 )
8 7 oveq1d 
 |-  ( ( ph /\ t e. CC ) -> ( ( t ^ ( 1 - 1 ) ) x. ( ( 1 - t ) ^ ( N - 1 ) ) ) = ( 1 x. ( ( 1 - t ) ^ ( N - 1 ) ) ) )
9 1cnd 
 |-  ( ( ph /\ t e. CC ) -> 1 e. CC )
10 9 5 subcld 
 |-  ( ( ph /\ t e. CC ) -> ( 1 - t ) e. CC )
11 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
12 1 11 syl 
 |-  ( ph -> ( N - 1 ) e. NN0 )
13 12 adantr 
 |-  ( ( ph /\ t e. CC ) -> ( N - 1 ) e. NN0 )
14 10 13 expcld 
 |-  ( ( ph /\ t e. CC ) -> ( ( 1 - t ) ^ ( N - 1 ) ) e. CC )
15 14 mulid2d 
 |-  ( ( ph /\ t e. CC ) -> ( 1 x. ( ( 1 - t ) ^ ( N - 1 ) ) ) = ( ( 1 - t ) ^ ( N - 1 ) ) )
16 8 15 eqtrd 
 |-  ( ( ph /\ t e. CC ) -> ( ( t ^ ( 1 - 1 ) ) x. ( ( 1 - t ) ^ ( N - 1 ) ) ) = ( ( 1 - t ) ^ ( N - 1 ) ) )
17 2 16 sylan2 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( ( t ^ ( 1 - 1 ) ) x. ( ( 1 - t ) ^ ( N - 1 ) ) ) = ( ( 1 - t ) ^ ( N - 1 ) ) )
18 17 itgeq2dv 
 |-  ( ph -> S. ( 0 [,] 1 ) ( ( t ^ ( 1 - 1 ) ) x. ( ( 1 - t ) ^ ( N - 1 ) ) ) _d t = S. ( 0 [,] 1 ) ( ( 1 - t ) ^ ( N - 1 ) ) _d t )
19 0red 
 |-  ( ph -> 0 e. RR )
20 1red 
 |-  ( ph -> 1 e. RR )
21 2 14 sylan2 
 |-  ( ( ph /\ t e. ( 0 [,] 1 ) ) -> ( ( 1 - t ) ^ ( N - 1 ) ) e. CC )
22 19 20 21 itgioo 
 |-  ( ph -> S. ( 0 (,) 1 ) ( ( 1 - t ) ^ ( N - 1 ) ) _d t = S. ( 0 [,] 1 ) ( ( 1 - t ) ^ ( N - 1 ) ) _d t )
23 eqidd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( x e. ( 0 (,) 1 ) |-> ( ( 1 - x ) ^ ( N - 1 ) ) ) = ( x e. ( 0 (,) 1 ) |-> ( ( 1 - x ) ^ ( N - 1 ) ) ) )
24 oveq2 
 |-  ( x = t -> ( 1 - x ) = ( 1 - t ) )
25 24 oveq1d 
 |-  ( x = t -> ( ( 1 - x ) ^ ( N - 1 ) ) = ( ( 1 - t ) ^ ( N - 1 ) ) )
26 25 adantl 
 |-  ( ( ph /\ x = t ) -> ( ( 1 - x ) ^ ( N - 1 ) ) = ( ( 1 - t ) ^ ( N - 1 ) ) )
27 26 adantlr 
 |-  ( ( ( ph /\ t e. ( 0 (,) 1 ) ) /\ x = t ) -> ( ( 1 - x ) ^ ( N - 1 ) ) = ( ( 1 - t ) ^ ( N - 1 ) ) )
28 simpr 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> t e. ( 0 (,) 1 ) )
29 1cnd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> 1 e. CC )
30 elioore 
 |-  ( t e. ( 0 (,) 1 ) -> t e. RR )
31 recn 
 |-  ( t e. RR -> t e. CC )
32 28 30 31 3syl 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> t e. CC )
33 29 32 subcld 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( 1 - t ) e. CC )
34 12 adantr 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( N - 1 ) e. NN0 )
35 33 34 expcld 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( ( 1 - t ) ^ ( N - 1 ) ) e. CC )
36 23 27 28 35 fvmptd 
 |-  ( ( ph /\ t e. ( 0 (,) 1 ) ) -> ( ( x e. ( 0 (,) 1 ) |-> ( ( 1 - x ) ^ ( N - 1 ) ) ) ` t ) = ( ( 1 - t ) ^ ( N - 1 ) ) )
37 36 itgeq2dv 
 |-  ( ph -> S. ( 0 (,) 1 ) ( ( x e. ( 0 (,) 1 ) |-> ( ( 1 - x ) ^ ( N - 1 ) ) ) ` t ) _d t = S. ( 0 (,) 1 ) ( ( 1 - t ) ^ ( N - 1 ) ) _d t )
38 cnelprrecn 
 |-  CC e. { RR , CC }
39 38 a1i 
 |-  ( ph -> CC e. { RR , CC } )
40 1cnd 
 |-  ( ( ph /\ x e. CC ) -> 1 e. CC )
41 simpr 
 |-  ( ( ph /\ x e. CC ) -> x e. CC )
42 40 41 subcld 
 |-  ( ( ph /\ x e. CC ) -> ( 1 - x ) e. CC )
43 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
44 1 43 syl 
 |-  ( ph -> N e. NN0 )
45 44 adantr 
 |-  ( ( ph /\ x e. CC ) -> N e. NN0 )
46 42 45 expcld 
 |-  ( ( ph /\ x e. CC ) -> ( ( 1 - x ) ^ N ) e. CC )
47 45 nn0cnd 
 |-  ( ( ph /\ x e. CC ) -> N e. CC )
48 12 adantr 
 |-  ( ( ph /\ x e. CC ) -> ( N - 1 ) e. NN0 )
49 42 48 expcld 
 |-  ( ( ph /\ x e. CC ) -> ( ( 1 - x ) ^ ( N - 1 ) ) e. CC )
50 47 49 mulcld 
 |-  ( ( ph /\ x e. CC ) -> ( N x. ( ( 1 - x ) ^ ( N - 1 ) ) ) e. CC )
51 40 negcld 
 |-  ( ( ph /\ x e. CC ) -> -u 1 e. CC )
52 50 51 mulcld 
 |-  ( ( ph /\ x e. CC ) -> ( ( N x. ( ( 1 - x ) ^ ( N - 1 ) ) ) x. -u 1 ) e. CC )
53 simpr 
 |-  ( ( ph /\ y e. CC ) -> y e. CC )
54 44 adantr 
 |-  ( ( ph /\ y e. CC ) -> N e. NN0 )
55 53 54 expcld 
 |-  ( ( ph /\ y e. CC ) -> ( y ^ N ) e. CC )
56 54 nn0cnd 
 |-  ( ( ph /\ y e. CC ) -> N e. CC )
57 12 adantr 
 |-  ( ( ph /\ y e. CC ) -> ( N - 1 ) e. NN0 )
58 53 57 expcld 
 |-  ( ( ph /\ y e. CC ) -> ( y ^ ( N - 1 ) ) e. CC )
59 56 58 mulcld 
 |-  ( ( ph /\ y e. CC ) -> ( N x. ( y ^ ( N - 1 ) ) ) e. CC )
60 0cnd 
 |-  ( ( ph /\ x e. CC ) -> 0 e. CC )
61 1cnd 
 |-  ( ph -> 1 e. CC )
62 39 61 dvmptc 
 |-  ( ph -> ( CC _D ( x e. CC |-> 1 ) ) = ( x e. CC |-> 0 ) )
63 39 dvmptid 
 |-  ( ph -> ( CC _D ( x e. CC |-> x ) ) = ( x e. CC |-> 1 ) )
64 39 40 60 62 41 40 63 dvmptsub 
 |-  ( ph -> ( CC _D ( x e. CC |-> ( 1 - x ) ) ) = ( x e. CC |-> ( 0 - 1 ) ) )
65 df-neg 
 |-  -u 1 = ( 0 - 1 )
66 65 a1i 
 |-  ( ph -> -u 1 = ( 0 - 1 ) )
67 66 mpteq2dv 
 |-  ( ph -> ( x e. CC |-> -u 1 ) = ( x e. CC |-> ( 0 - 1 ) ) )
68 64 67 eqtr4d 
 |-  ( ph -> ( CC _D ( x e. CC |-> ( 1 - x ) ) ) = ( x e. CC |-> -u 1 ) )
69 dvexp 
 |-  ( N e. NN -> ( CC _D ( y e. CC |-> ( y ^ N ) ) ) = ( y e. CC |-> ( N x. ( y ^ ( N - 1 ) ) ) ) )
70 1 69 syl 
 |-  ( ph -> ( CC _D ( y e. CC |-> ( y ^ N ) ) ) = ( y e. CC |-> ( N x. ( y ^ ( N - 1 ) ) ) ) )
71 oveq1 
 |-  ( y = ( 1 - x ) -> ( y ^ N ) = ( ( 1 - x ) ^ N ) )
72 oveq1 
 |-  ( y = ( 1 - x ) -> ( y ^ ( N - 1 ) ) = ( ( 1 - x ) ^ ( N - 1 ) ) )
73 72 oveq2d 
 |-  ( y = ( 1 - x ) -> ( N x. ( y ^ ( N - 1 ) ) ) = ( N x. ( ( 1 - x ) ^ ( N - 1 ) ) ) )
74 39 39 42 51 55 59 68 70 71 73 dvmptco 
 |-  ( ph -> ( CC _D ( x e. CC |-> ( ( 1 - x ) ^ N ) ) ) = ( x e. CC |-> ( ( N x. ( ( 1 - x ) ^ ( N - 1 ) ) ) x. -u 1 ) ) )
75 61 negcld 
 |-  ( ph -> -u 1 e. CC )
76 1 nncnd 
 |-  ( ph -> N e. CC )
77 1 nnne0d 
 |-  ( ph -> N =/= 0 )
78 75 76 77 divcld 
 |-  ( ph -> ( -u 1 / N ) e. CC )
79 39 46 52 74 78 dvmptcmul 
 |-  ( ph -> ( CC _D ( x e. CC |-> ( ( -u 1 / N ) x. ( ( 1 - x ) ^ N ) ) ) ) = ( x e. CC |-> ( ( -u 1 / N ) x. ( ( N x. ( ( 1 - x ) ^ ( N - 1 ) ) ) x. -u 1 ) ) ) )
80 78 adantr 
 |-  ( ( ph /\ x e. CC ) -> ( -u 1 / N ) e. CC )
81 80 50 51 mulassd 
 |-  ( ( ph /\ x e. CC ) -> ( ( ( -u 1 / N ) x. ( N x. ( ( 1 - x ) ^ ( N - 1 ) ) ) ) x. -u 1 ) = ( ( -u 1 / N ) x. ( ( N x. ( ( 1 - x ) ^ ( N - 1 ) ) ) x. -u 1 ) ) )
82 81 eqcomd 
 |-  ( ( ph /\ x e. CC ) -> ( ( -u 1 / N ) x. ( ( N x. ( ( 1 - x ) ^ ( N - 1 ) ) ) x. -u 1 ) ) = ( ( ( -u 1 / N ) x. ( N x. ( ( 1 - x ) ^ ( N - 1 ) ) ) ) x. -u 1 ) )
83 80 47 49 mulassd 
 |-  ( ( ph /\ x e. CC ) -> ( ( ( -u 1 / N ) x. N ) x. ( ( 1 - x ) ^ ( N - 1 ) ) ) = ( ( -u 1 / N ) x. ( N x. ( ( 1 - x ) ^ ( N - 1 ) ) ) ) )
84 83 oveq1d 
 |-  ( ( ph /\ x e. CC ) -> ( ( ( ( -u 1 / N ) x. N ) x. ( ( 1 - x ) ^ ( N - 1 ) ) ) x. -u 1 ) = ( ( ( -u 1 / N ) x. ( N x. ( ( 1 - x ) ^ ( N - 1 ) ) ) ) x. -u 1 ) )
85 84 eqcomd 
 |-  ( ( ph /\ x e. CC ) -> ( ( ( -u 1 / N ) x. ( N x. ( ( 1 - x ) ^ ( N - 1 ) ) ) ) x. -u 1 ) = ( ( ( ( -u 1 / N ) x. N ) x. ( ( 1 - x ) ^ ( N - 1 ) ) ) x. -u 1 ) )
86 82 85 eqtrd 
 |-  ( ( ph /\ x e. CC ) -> ( ( -u 1 / N ) x. ( ( N x. ( ( 1 - x ) ^ ( N - 1 ) ) ) x. -u 1 ) ) = ( ( ( ( -u 1 / N ) x. N ) x. ( ( 1 - x ) ^ ( N - 1 ) ) ) x. -u 1 ) )
87 77 adantr 
 |-  ( ( ph /\ x e. CC ) -> N =/= 0 )
88 51 47 87 divcan1d 
 |-  ( ( ph /\ x e. CC ) -> ( ( -u 1 / N ) x. N ) = -u 1 )
89 88 oveq1d 
 |-  ( ( ph /\ x e. CC ) -> ( ( ( -u 1 / N ) x. N ) x. ( ( 1 - x ) ^ ( N - 1 ) ) ) = ( -u 1 x. ( ( 1 - x ) ^ ( N - 1 ) ) ) )
90 89 oveq1d 
 |-  ( ( ph /\ x e. CC ) -> ( ( ( ( -u 1 / N ) x. N ) x. ( ( 1 - x ) ^ ( N - 1 ) ) ) x. -u 1 ) = ( ( -u 1 x. ( ( 1 - x ) ^ ( N - 1 ) ) ) x. -u 1 ) )
91 86 90 eqtrd 
 |-  ( ( ph /\ x e. CC ) -> ( ( -u 1 / N ) x. ( ( N x. ( ( 1 - x ) ^ ( N - 1 ) ) ) x. -u 1 ) ) = ( ( -u 1 x. ( ( 1 - x ) ^ ( N - 1 ) ) ) x. -u 1 ) )
92 51 51 49 mul32d 
 |-  ( ( ph /\ x e. CC ) -> ( ( -u 1 x. -u 1 ) x. ( ( 1 - x ) ^ ( N - 1 ) ) ) = ( ( -u 1 x. ( ( 1 - x ) ^ ( N - 1 ) ) ) x. -u 1 ) )
93 92 eqcomd 
 |-  ( ( ph /\ x e. CC ) -> ( ( -u 1 x. ( ( 1 - x ) ^ ( N - 1 ) ) ) x. -u 1 ) = ( ( -u 1 x. -u 1 ) x. ( ( 1 - x ) ^ ( N - 1 ) ) ) )
94 91 93 eqtrd 
 |-  ( ( ph /\ x e. CC ) -> ( ( -u 1 / N ) x. ( ( N x. ( ( 1 - x ) ^ ( N - 1 ) ) ) x. -u 1 ) ) = ( ( -u 1 x. -u 1 ) x. ( ( 1 - x ) ^ ( N - 1 ) ) ) )
95 40 40 mul2negd 
 |-  ( ( ph /\ x e. CC ) -> ( -u 1 x. -u 1 ) = ( 1 x. 1 ) )
96 1t1e1 
 |-  ( 1 x. 1 ) = 1
97 95 96 eqtrdi 
 |-  ( ( ph /\ x e. CC ) -> ( -u 1 x. -u 1 ) = 1 )
98 97 oveq1d 
 |-  ( ( ph /\ x e. CC ) -> ( ( -u 1 x. -u 1 ) x. ( ( 1 - x ) ^ ( N - 1 ) ) ) = ( 1 x. ( ( 1 - x ) ^ ( N - 1 ) ) ) )
99 49 mulid2d 
 |-  ( ( ph /\ x e. CC ) -> ( 1 x. ( ( 1 - x ) ^ ( N - 1 ) ) ) = ( ( 1 - x ) ^ ( N - 1 ) ) )
100 98 99 eqtrd 
 |-  ( ( ph /\ x e. CC ) -> ( ( -u 1 x. -u 1 ) x. ( ( 1 - x ) ^ ( N - 1 ) ) ) = ( ( 1 - x ) ^ ( N - 1 ) ) )
101 94 100 eqtrd 
 |-  ( ( ph /\ x e. CC ) -> ( ( -u 1 / N ) x. ( ( N x. ( ( 1 - x ) ^ ( N - 1 ) ) ) x. -u 1 ) ) = ( ( 1 - x ) ^ ( N - 1 ) ) )
102 101 mpteq2dva 
 |-  ( ph -> ( x e. CC |-> ( ( -u 1 / N ) x. ( ( N x. ( ( 1 - x ) ^ ( N - 1 ) ) ) x. -u 1 ) ) ) = ( x e. CC |-> ( ( 1 - x ) ^ ( N - 1 ) ) ) )
103 79 102 eqtrd 
 |-  ( ph -> ( CC _D ( x e. CC |-> ( ( -u 1 / N ) x. ( ( 1 - x ) ^ N ) ) ) ) = ( x e. CC |-> ( ( 1 - x ) ^ ( N - 1 ) ) ) )
104 80 46 mulcld 
 |-  ( ( ph /\ x e. CC ) -> ( ( -u 1 / N ) x. ( ( 1 - x ) ^ N ) ) e. CC )
105 103 104 49 resdvopclptsd 
 |-  ( ph -> ( RR _D ( x e. ( 0 [,] 1 ) |-> ( ( -u 1 / N ) x. ( ( 1 - x ) ^ N ) ) ) ) = ( x e. ( 0 (,) 1 ) |-> ( ( 1 - x ) ^ ( N - 1 ) ) ) )
106 105 fveq1d 
 |-  ( ph -> ( ( RR _D ( x e. ( 0 [,] 1 ) |-> ( ( -u 1 / N ) x. ( ( 1 - x ) ^ N ) ) ) ) ` t ) = ( ( x e. ( 0 (,) 1 ) |-> ( ( 1 - x ) ^ ( N - 1 ) ) ) ` t ) )
107 106 ralrimivw 
 |-  ( ph -> A. t e. ( 0 (,) 1 ) ( ( RR _D ( x e. ( 0 [,] 1 ) |-> ( ( -u 1 / N ) x. ( ( 1 - x ) ^ N ) ) ) ) ` t ) = ( ( x e. ( 0 (,) 1 ) |-> ( ( 1 - x ) ^ ( N - 1 ) ) ) ` t ) )
108 itgeq2 
 |-  ( A. t e. ( 0 (,) 1 ) ( ( RR _D ( x e. ( 0 [,] 1 ) |-> ( ( -u 1 / N ) x. ( ( 1 - x ) ^ N ) ) ) ) ` t ) = ( ( x e. ( 0 (,) 1 ) |-> ( ( 1 - x ) ^ ( N - 1 ) ) ) ` t ) -> S. ( 0 (,) 1 ) ( ( RR _D ( x e. ( 0 [,] 1 ) |-> ( ( -u 1 / N ) x. ( ( 1 - x ) ^ N ) ) ) ) ` t ) _d t = S. ( 0 (,) 1 ) ( ( x e. ( 0 (,) 1 ) |-> ( ( 1 - x ) ^ ( N - 1 ) ) ) ` t ) _d t )
109 107 108 syl 
 |-  ( ph -> S. ( 0 (,) 1 ) ( ( RR _D ( x e. ( 0 [,] 1 ) |-> ( ( -u 1 / N ) x. ( ( 1 - x ) ^ N ) ) ) ) ` t ) _d t = S. ( 0 (,) 1 ) ( ( x e. ( 0 (,) 1 ) |-> ( ( 1 - x ) ^ ( N - 1 ) ) ) ` t ) _d t )
110 0le1 
 |-  0 <_ 1
111 110 a1i 
 |-  ( ph -> 0 <_ 1 )
112 nfv 
 |-  F/ x ph
113 ax-1cn 
 |-  1 e. CC
114 ssid 
 |-  CC C_ CC
115 cncfmptc 
 |-  ( ( 1 e. CC /\ CC C_ CC /\ CC C_ CC ) -> ( x e. CC |-> 1 ) e. ( CC -cn-> CC ) )
116 113 114 114 115 mp3an 
 |-  ( x e. CC |-> 1 ) e. ( CC -cn-> CC )
117 116 a1i 
 |-  ( ph -> ( x e. CC |-> 1 ) e. ( CC -cn-> CC ) )
118 cncfmptid 
 |-  ( ( CC C_ CC /\ CC C_ CC ) -> ( x e. CC |-> x ) e. ( CC -cn-> CC ) )
119 114 114 118 mp2an 
 |-  ( x e. CC |-> x ) e. ( CC -cn-> CC )
120 119 a1i 
 |-  ( ph -> ( x e. CC |-> x ) e. ( CC -cn-> CC ) )
121 117 120 subcncf 
 |-  ( ph -> ( x e. CC |-> ( 1 - x ) ) e. ( CC -cn-> CC ) )
122 expcncf 
 |-  ( ( N - 1 ) e. NN0 -> ( y e. CC |-> ( y ^ ( N - 1 ) ) ) e. ( CC -cn-> CC ) )
123 12 122 syl 
 |-  ( ph -> ( y e. CC |-> ( y ^ ( N - 1 ) ) ) e. ( CC -cn-> CC ) )
124 ssidd 
 |-  ( ph -> CC C_ CC )
125 112 121 123 124 72 cncfcompt2 
 |-  ( ph -> ( x e. CC |-> ( ( 1 - x ) ^ ( N - 1 ) ) ) e. ( CC -cn-> CC ) )
126 125 resopunitintvd 
 |-  ( ph -> ( x e. ( 0 (,) 1 ) |-> ( ( 1 - x ) ^ ( N - 1 ) ) ) e. ( ( 0 (,) 1 ) -cn-> CC ) )
127 105 eleq1d 
 |-  ( ph -> ( ( RR _D ( x e. ( 0 [,] 1 ) |-> ( ( -u 1 / N ) x. ( ( 1 - x ) ^ N ) ) ) ) e. ( ( 0 (,) 1 ) -cn-> CC ) <-> ( x e. ( 0 (,) 1 ) |-> ( ( 1 - x ) ^ ( N - 1 ) ) ) e. ( ( 0 (,) 1 ) -cn-> CC ) ) )
128 126 127 mpbird 
 |-  ( ph -> ( RR _D ( x e. ( 0 [,] 1 ) |-> ( ( -u 1 / N ) x. ( ( 1 - x ) ^ N ) ) ) ) e. ( ( 0 (,) 1 ) -cn-> CC ) )
129 ioossicc 
 |-  ( 0 (,) 1 ) C_ ( 0 [,] 1 )
130 129 a1i 
 |-  ( ph -> ( 0 (,) 1 ) C_ ( 0 [,] 1 ) )
131 ioombl 
 |-  ( 0 (,) 1 ) e. dom vol
132 131 a1i 
 |-  ( ph -> ( 0 (,) 1 ) e. dom vol )
133 elunitcn 
 |-  ( x e. ( 0 [,] 1 ) -> x e. CC )
134 133 49 sylan2 
 |-  ( ( ph /\ x e. ( 0 [,] 1 ) ) -> ( ( 1 - x ) ^ ( N - 1 ) ) e. CC )
135 114 a1i 
 |-  ( ph -> CC C_ CC )
136 112 121 123 135 72 cncfcompt2 
 |-  ( ph -> ( x e. CC |-> ( ( 1 - x ) ^ ( N - 1 ) ) ) e. ( CC -cn-> CC ) )
137 136 resclunitintvd 
 |-  ( ph -> ( x e. ( 0 [,] 1 ) |-> ( ( 1 - x ) ^ ( N - 1 ) ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
138 19 20 137 3jca 
 |-  ( ph -> ( 0 e. RR /\ 1 e. RR /\ ( x e. ( 0 [,] 1 ) |-> ( ( 1 - x ) ^ ( N - 1 ) ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) ) )
139 cnicciblnc 
 |-  ( ( 0 e. RR /\ 1 e. RR /\ ( x e. ( 0 [,] 1 ) |-> ( ( 1 - x ) ^ ( N - 1 ) ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) ) -> ( x e. ( 0 [,] 1 ) |-> ( ( 1 - x ) ^ ( N - 1 ) ) ) e. L^1 )
140 138 139 syl 
 |-  ( ph -> ( x e. ( 0 [,] 1 ) |-> ( ( 1 - x ) ^ ( N - 1 ) ) ) e. L^1 )
141 130 132 134 140 iblss 
 |-  ( ph -> ( x e. ( 0 (,) 1 ) |-> ( ( 1 - x ) ^ ( N - 1 ) ) ) e. L^1 )
142 105 141 eqeltrd 
 |-  ( ph -> ( RR _D ( x e. ( 0 [,] 1 ) |-> ( ( -u 1 / N ) x. ( ( 1 - x ) ^ N ) ) ) ) e. L^1 )
143 cncfmptc 
 |-  ( ( ( -u 1 / N ) e. CC /\ CC C_ CC /\ CC C_ CC ) -> ( x e. CC |-> ( -u 1 / N ) ) e. ( CC -cn-> CC ) )
144 114 114 143 mp3an23 
 |-  ( ( -u 1 / N ) e. CC -> ( x e. CC |-> ( -u 1 / N ) ) e. ( CC -cn-> CC ) )
145 78 144 syl 
 |-  ( ph -> ( x e. CC |-> ( -u 1 / N ) ) e. ( CC -cn-> CC ) )
146 145 resclunitintvd 
 |-  ( ph -> ( x e. ( 0 [,] 1 ) |-> ( -u 1 / N ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
147 expcncf 
 |-  ( N e. NN0 -> ( y e. CC |-> ( y ^ N ) ) e. ( CC -cn-> CC ) )
148 44 147 syl 
 |-  ( ph -> ( y e. CC |-> ( y ^ N ) ) e. ( CC -cn-> CC ) )
149 112 121 148 124 71 cncfcompt2 
 |-  ( ph -> ( x e. CC |-> ( ( 1 - x ) ^ N ) ) e. ( CC -cn-> CC ) )
150 149 resclunitintvd 
 |-  ( ph -> ( x e. ( 0 [,] 1 ) |-> ( ( 1 - x ) ^ N ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
151 146 150 mulcncf 
 |-  ( ph -> ( x e. ( 0 [,] 1 ) |-> ( ( -u 1 / N ) x. ( ( 1 - x ) ^ N ) ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
152 19 20 111 128 142 151 ftc2 
 |-  ( ph -> S. ( 0 (,) 1 ) ( ( RR _D ( x e. ( 0 [,] 1 ) |-> ( ( -u 1 / N ) x. ( ( 1 - x ) ^ N ) ) ) ) ` t ) _d t = ( ( ( x e. ( 0 [,] 1 ) |-> ( ( -u 1 / N ) x. ( ( 1 - x ) ^ N ) ) ) ` 1 ) - ( ( x e. ( 0 [,] 1 ) |-> ( ( -u 1 / N ) x. ( ( 1 - x ) ^ N ) ) ) ` 0 ) ) )
153 eqidd 
 |-  ( ph -> ( x e. ( 0 [,] 1 ) |-> ( ( -u 1 / N ) x. ( ( 1 - x ) ^ N ) ) ) = ( x e. ( 0 [,] 1 ) |-> ( ( -u 1 / N ) x. ( ( 1 - x ) ^ N ) ) ) )
154 simpr 
 |-  ( ( ph /\ x = 1 ) -> x = 1 )
155 154 oveq2d 
 |-  ( ( ph /\ x = 1 ) -> ( 1 - x ) = ( 1 - 1 ) )
156 155 3 eqtrdi 
 |-  ( ( ph /\ x = 1 ) -> ( 1 - x ) = 0 )
157 156 oveq1d 
 |-  ( ( ph /\ x = 1 ) -> ( ( 1 - x ) ^ N ) = ( 0 ^ N ) )
158 0exp 
 |-  ( N e. NN -> ( 0 ^ N ) = 0 )
159 1 158 syl 
 |-  ( ph -> ( 0 ^ N ) = 0 )
160 159 adantr 
 |-  ( ( ph /\ x = 1 ) -> ( 0 ^ N ) = 0 )
161 157 160 eqtrd 
 |-  ( ( ph /\ x = 1 ) -> ( ( 1 - x ) ^ N ) = 0 )
162 161 oveq2d 
 |-  ( ( ph /\ x = 1 ) -> ( ( -u 1 / N ) x. ( ( 1 - x ) ^ N ) ) = ( ( -u 1 / N ) x. 0 ) )
163 78 mul01d 
 |-  ( ph -> ( ( -u 1 / N ) x. 0 ) = 0 )
164 163 adantr 
 |-  ( ( ph /\ x = 1 ) -> ( ( -u 1 / N ) x. 0 ) = 0 )
165 162 164 eqtrd 
 |-  ( ( ph /\ x = 1 ) -> ( ( -u 1 / N ) x. ( ( 1 - x ) ^ N ) ) = 0 )
166 1elunit 
 |-  1 e. ( 0 [,] 1 )
167 166 a1i 
 |-  ( ph -> 1 e. ( 0 [,] 1 ) )
168 0cnd 
 |-  ( ph -> 0 e. CC )
169 153 165 167 168 fvmptd 
 |-  ( ph -> ( ( x e. ( 0 [,] 1 ) |-> ( ( -u 1 / N ) x. ( ( 1 - x ) ^ N ) ) ) ` 1 ) = 0 )
170 simpr 
 |-  ( ( ph /\ x = 0 ) -> x = 0 )
171 170 oveq2d 
 |-  ( ( ph /\ x = 0 ) -> ( 1 - x ) = ( 1 - 0 ) )
172 1m0e1 
 |-  ( 1 - 0 ) = 1
173 171 172 eqtrdi 
 |-  ( ( ph /\ x = 0 ) -> ( 1 - x ) = 1 )
174 173 oveq1d 
 |-  ( ( ph /\ x = 0 ) -> ( ( 1 - x ) ^ N ) = ( 1 ^ N ) )
175 44 nn0zd 
 |-  ( ph -> N e. ZZ )
176 1exp 
 |-  ( N e. ZZ -> ( 1 ^ N ) = 1 )
177 175 176 syl 
 |-  ( ph -> ( 1 ^ N ) = 1 )
178 177 adantr 
 |-  ( ( ph /\ x = 0 ) -> ( 1 ^ N ) = 1 )
179 174 178 eqtrd 
 |-  ( ( ph /\ x = 0 ) -> ( ( 1 - x ) ^ N ) = 1 )
180 179 oveq2d 
 |-  ( ( ph /\ x = 0 ) -> ( ( -u 1 / N ) x. ( ( 1 - x ) ^ N ) ) = ( ( -u 1 / N ) x. 1 ) )
181 78 adantr 
 |-  ( ( ph /\ x = 0 ) -> ( -u 1 / N ) e. CC )
182 181 mulid1d 
 |-  ( ( ph /\ x = 0 ) -> ( ( -u 1 / N ) x. 1 ) = ( -u 1 / N ) )
183 180 182 eqtrd 
 |-  ( ( ph /\ x = 0 ) -> ( ( -u 1 / N ) x. ( ( 1 - x ) ^ N ) ) = ( -u 1 / N ) )
184 0elunit 
 |-  0 e. ( 0 [,] 1 )
185 184 a1i 
 |-  ( ph -> 0 e. ( 0 [,] 1 ) )
186 153 183 185 78 fvmptd 
 |-  ( ph -> ( ( x e. ( 0 [,] 1 ) |-> ( ( -u 1 / N ) x. ( ( 1 - x ) ^ N ) ) ) ` 0 ) = ( -u 1 / N ) )
187 169 186 oveq12d 
 |-  ( ph -> ( ( ( x e. ( 0 [,] 1 ) |-> ( ( -u 1 / N ) x. ( ( 1 - x ) ^ N ) ) ) ` 1 ) - ( ( x e. ( 0 [,] 1 ) |-> ( ( -u 1 / N ) x. ( ( 1 - x ) ^ N ) ) ) ` 0 ) ) = ( 0 - ( -u 1 / N ) ) )
188 152 187 eqtrd 
 |-  ( ph -> S. ( 0 (,) 1 ) ( ( RR _D ( x e. ( 0 [,] 1 ) |-> ( ( -u 1 / N ) x. ( ( 1 - x ) ^ N ) ) ) ) ` t ) _d t = ( 0 - ( -u 1 / N ) ) )
189 df-neg 
 |-  -u -u ( 1 / N ) = ( 0 - -u ( 1 / N ) )
190 189 a1i 
 |-  ( ph -> -u -u ( 1 / N ) = ( 0 - -u ( 1 / N ) ) )
191 61 76 77 divnegd 
 |-  ( ph -> -u ( 1 / N ) = ( -u 1 / N ) )
192 191 oveq2d 
 |-  ( ph -> ( 0 - -u ( 1 / N ) ) = ( 0 - ( -u 1 / N ) ) )
193 190 192 eqtr2d 
 |-  ( ph -> ( 0 - ( -u 1 / N ) ) = -u -u ( 1 / N ) )
194 76 77 reccld 
 |-  ( ph -> ( 1 / N ) e. CC )
195 194 negnegd 
 |-  ( ph -> -u -u ( 1 / N ) = ( 1 / N ) )
196 193 195 eqtrd 
 |-  ( ph -> ( 0 - ( -u 1 / N ) ) = ( 1 / N ) )
197 188 196 eqtrd 
 |-  ( ph -> S. ( 0 (,) 1 ) ( ( RR _D ( x e. ( 0 [,] 1 ) |-> ( ( -u 1 / N ) x. ( ( 1 - x ) ^ N ) ) ) ) ` t ) _d t = ( 1 / N ) )
198 109 197 eqtr3d 
 |-  ( ph -> S. ( 0 (,) 1 ) ( ( x e. ( 0 (,) 1 ) |-> ( ( 1 - x ) ^ ( N - 1 ) ) ) ` t ) _d t = ( 1 / N ) )
199 37 198 eqtr3d 
 |-  ( ph -> S. ( 0 (,) 1 ) ( ( 1 - t ) ^ ( N - 1 ) ) _d t = ( 1 / N ) )
200 22 199 eqtr3d 
 |-  ( ph -> S. ( 0 [,] 1 ) ( ( 1 - t ) ^ ( N - 1 ) ) _d t = ( 1 / N ) )
201 bcn1 
 |-  ( N e. NN0 -> ( N _C 1 ) = N )
202 44 201 syl 
 |-  ( ph -> ( N _C 1 ) = N )
203 202 oveq2d 
 |-  ( ph -> ( 1 x. ( N _C 1 ) ) = ( 1 x. N ) )
204 76 mulid2d 
 |-  ( ph -> ( 1 x. N ) = N )
205 203 204 eqtrd 
 |-  ( ph -> ( 1 x. ( N _C 1 ) ) = N )
206 205 oveq2d 
 |-  ( ph -> ( 1 / ( 1 x. ( N _C 1 ) ) ) = ( 1 / N ) )
207 200 206 eqtr4d 
 |-  ( ph -> S. ( 0 [,] 1 ) ( ( 1 - t ) ^ ( N - 1 ) ) _d t = ( 1 / ( 1 x. ( N _C 1 ) ) ) )
208 18 207 eqtrd 
 |-  ( ph -> S. ( 0 [,] 1 ) ( ( t ^ ( 1 - 1 ) ) x. ( ( 1 - t ) ^ ( N - 1 ) ) ) _d t = ( 1 / ( 1 x. ( N _C 1 ) ) ) )