Metamath Proof Explorer

Theorem lcmineqlem13

Description: Induction proof for lcm integral. (Contributed by metakunt, 12-May-2024)

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

Proof

Step Hyp Ref Expression
1 lcmineqlem13.1 
 |-  F = S. ( 0 [,] 1 ) ( ( x ^ ( M - 1 ) ) x. ( ( 1 - x ) ^ ( N - M ) ) ) _d x
2 lcmineqlem13.2 
 |-  ( ph -> M e. NN )
3 lcmineqlem13.3 
 |-  ( ph -> N e. NN )
4 lcmineqlem13.4 
 |-  ( ph -> M <_ N )
5 2 nnzd 
 |-  ( ph -> M e. ZZ )
6 nnge1 
 |-  ( M e. NN -> 1 <_ M )
7 2 6 syl 
 |-  ( ph -> 1 <_ M )
8 5 7 4 3jca 
 |-  ( ph -> ( M e. ZZ /\ 1 <_ M /\ M <_ N ) )
9 oveq1 
 |-  ( i = 1 -> ( i - 1 ) = ( 1 - 1 ) )
10 9 oveq2d 
 |-  ( i = 1 -> ( x ^ ( i - 1 ) ) = ( x ^ ( 1 - 1 ) ) )
11 oveq2 
 |-  ( i = 1 -> ( N - i ) = ( N - 1 ) )
12 11 oveq2d 
 |-  ( i = 1 -> ( ( 1 - x ) ^ ( N - i ) ) = ( ( 1 - x ) ^ ( N - 1 ) ) )
13 10 12 oveq12d 
 |-  ( i = 1 -> ( ( x ^ ( i - 1 ) ) x. ( ( 1 - x ) ^ ( N - i ) ) ) = ( ( x ^ ( 1 - 1 ) ) x. ( ( 1 - x ) ^ ( N - 1 ) ) ) )
14 13 adantr 
 |-  ( ( i = 1 /\ x e. ( 0 [,] 1 ) ) -> ( ( x ^ ( i - 1 ) ) x. ( ( 1 - x ) ^ ( N - i ) ) ) = ( ( x ^ ( 1 - 1 ) ) x. ( ( 1 - x ) ^ ( N - 1 ) ) ) )
15 14 itgeq2dv 
 |-  ( i = 1 -> S. ( 0 [,] 1 ) ( ( x ^ ( i - 1 ) ) x. ( ( 1 - x ) ^ ( N - i ) ) ) _d x = S. ( 0 [,] 1 ) ( ( x ^ ( 1 - 1 ) ) x. ( ( 1 - x ) ^ ( N - 1 ) ) ) _d x )
16 id 
 |-  ( i = 1 -> i = 1 )
17 oveq2 
 |-  ( i = 1 -> ( N _C i ) = ( N _C 1 ) )
18 16 17 oveq12d 
 |-  ( i = 1 -> ( i x. ( N _C i ) ) = ( 1 x. ( N _C 1 ) ) )
19 18 oveq2d 
 |-  ( i = 1 -> ( 1 / ( i x. ( N _C i ) ) ) = ( 1 / ( 1 x. ( N _C 1 ) ) ) )
20 15 19 eqeq12d 
 |-  ( i = 1 -> ( S. ( 0 [,] 1 ) ( ( x ^ ( i - 1 ) ) x. ( ( 1 - x ) ^ ( N - i ) ) ) _d x = ( 1 / ( i x. ( N _C i ) ) ) <-> S. ( 0 [,] 1 ) ( ( x ^ ( 1 - 1 ) ) x. ( ( 1 - x ) ^ ( N - 1 ) ) ) _d x = ( 1 / ( 1 x. ( N _C 1 ) ) ) ) )
21 oveq1 
 |-  ( i = m -> ( i - 1 ) = ( m - 1 ) )
22 21 oveq2d 
 |-  ( i = m -> ( x ^ ( i - 1 ) ) = ( x ^ ( m - 1 ) ) )
23 oveq2 
 |-  ( i = m -> ( N - i ) = ( N - m ) )
24 23 oveq2d 
 |-  ( i = m -> ( ( 1 - x ) ^ ( N - i ) ) = ( ( 1 - x ) ^ ( N - m ) ) )
25 22 24 oveq12d 
 |-  ( i = m -> ( ( x ^ ( i - 1 ) ) x. ( ( 1 - x ) ^ ( N - i ) ) ) = ( ( x ^ ( m - 1 ) ) x. ( ( 1 - x ) ^ ( N - m ) ) ) )
26 25 adantr 
 |-  ( ( i = m /\ x e. ( 0 [,] 1 ) ) -> ( ( x ^ ( i - 1 ) ) x. ( ( 1 - x ) ^ ( N - i ) ) ) = ( ( x ^ ( m - 1 ) ) x. ( ( 1 - x ) ^ ( N - m ) ) ) )
27 26 itgeq2dv 
 |-  ( i = m -> S. ( 0 [,] 1 ) ( ( x ^ ( i - 1 ) ) x. ( ( 1 - x ) ^ ( N - i ) ) ) _d x = S. ( 0 [,] 1 ) ( ( x ^ ( m - 1 ) ) x. ( ( 1 - x ) ^ ( N - m ) ) ) _d x )
28 id 
 |-  ( i = m -> i = m )
29 oveq2 
 |-  ( i = m -> ( N _C i ) = ( N _C m ) )
30 28 29 oveq12d 
 |-  ( i = m -> ( i x. ( N _C i ) ) = ( m x. ( N _C m ) ) )
31 30 oveq2d 
 |-  ( i = m -> ( 1 / ( i x. ( N _C i ) ) ) = ( 1 / ( m x. ( N _C m ) ) ) )
32 27 31 eqeq12d 
 |-  ( i = m -> ( S. ( 0 [,] 1 ) ( ( x ^ ( i - 1 ) ) x. ( ( 1 - x ) ^ ( N - i ) ) ) _d x = ( 1 / ( i x. ( N _C i ) ) ) <-> S. ( 0 [,] 1 ) ( ( x ^ ( m - 1 ) ) x. ( ( 1 - x ) ^ ( N - m ) ) ) _d x = ( 1 / ( m x. ( N _C m ) ) ) ) )
33 oveq1 
 |-  ( i = ( m + 1 ) -> ( i - 1 ) = ( ( m + 1 ) - 1 ) )
34 33 oveq2d 
 |-  ( i = ( m + 1 ) -> ( x ^ ( i - 1 ) ) = ( x ^ ( ( m + 1 ) - 1 ) ) )
35 oveq2 
 |-  ( i = ( m + 1 ) -> ( N - i ) = ( N - ( m + 1 ) ) )
36 35 oveq2d 
 |-  ( i = ( m + 1 ) -> ( ( 1 - x ) ^ ( N - i ) ) = ( ( 1 - x ) ^ ( N - ( m + 1 ) ) ) )
37 34 36 oveq12d 
 |-  ( i = ( m + 1 ) -> ( ( x ^ ( i - 1 ) ) x. ( ( 1 - x ) ^ ( N - i ) ) ) = ( ( x ^ ( ( m + 1 ) - 1 ) ) x. ( ( 1 - x ) ^ ( N - ( m + 1 ) ) ) ) )
38 37 adantr 
 |-  ( ( i = ( m + 1 ) /\ x e. ( 0 [,] 1 ) ) -> ( ( x ^ ( i - 1 ) ) x. ( ( 1 - x ) ^ ( N - i ) ) ) = ( ( x ^ ( ( m + 1 ) - 1 ) ) x. ( ( 1 - x ) ^ ( N - ( m + 1 ) ) ) ) )
39 38 itgeq2dv 
 |-  ( i = ( m + 1 ) -> S. ( 0 [,] 1 ) ( ( x ^ ( i - 1 ) ) x. ( ( 1 - x ) ^ ( N - i ) ) ) _d x = S. ( 0 [,] 1 ) ( ( x ^ ( ( m + 1 ) - 1 ) ) x. ( ( 1 - x ) ^ ( N - ( m + 1 ) ) ) ) _d x )
40 id 
 |-  ( i = ( m + 1 ) -> i = ( m + 1 ) )
41 oveq2 
 |-  ( i = ( m + 1 ) -> ( N _C i ) = ( N _C ( m + 1 ) ) )
42 40 41 oveq12d 
 |-  ( i = ( m + 1 ) -> ( i x. ( N _C i ) ) = ( ( m + 1 ) x. ( N _C ( m + 1 ) ) ) )
43 42 oveq2d 
 |-  ( i = ( m + 1 ) -> ( 1 / ( i x. ( N _C i ) ) ) = ( 1 / ( ( m + 1 ) x. ( N _C ( m + 1 ) ) ) ) )
44 39 43 eqeq12d 
 |-  ( i = ( m + 1 ) -> ( S. ( 0 [,] 1 ) ( ( x ^ ( i - 1 ) ) x. ( ( 1 - x ) ^ ( N - i ) ) ) _d x = ( 1 / ( i x. ( N _C i ) ) ) <-> S. ( 0 [,] 1 ) ( ( x ^ ( ( m + 1 ) - 1 ) ) x. ( ( 1 - x ) ^ ( N - ( m + 1 ) ) ) ) _d x = ( 1 / ( ( m + 1 ) x. ( N _C ( m + 1 ) ) ) ) ) )
45 oveq1 
 |-  ( i = M -> ( i - 1 ) = ( M - 1 ) )
46 45 oveq2d 
 |-  ( i = M -> ( x ^ ( i - 1 ) ) = ( x ^ ( M - 1 ) ) )
47 oveq2 
 |-  ( i = M -> ( N - i ) = ( N - M ) )
48 47 oveq2d 
 |-  ( i = M -> ( ( 1 - x ) ^ ( N - i ) ) = ( ( 1 - x ) ^ ( N - M ) ) )
49 46 48 oveq12d 
 |-  ( i = M -> ( ( x ^ ( i - 1 ) ) x. ( ( 1 - x ) ^ ( N - i ) ) ) = ( ( x ^ ( M - 1 ) ) x. ( ( 1 - x ) ^ ( N - M ) ) ) )
50 49 adantr 
 |-  ( ( i = M /\ x e. ( 0 [,] 1 ) ) -> ( ( x ^ ( i - 1 ) ) x. ( ( 1 - x ) ^ ( N - i ) ) ) = ( ( x ^ ( M - 1 ) ) x. ( ( 1 - x ) ^ ( N - M ) ) ) )
51 50 itgeq2dv 
 |-  ( i = M -> S. ( 0 [,] 1 ) ( ( x ^ ( i - 1 ) ) x. ( ( 1 - x ) ^ ( N - i ) ) ) _d x = S. ( 0 [,] 1 ) ( ( x ^ ( M - 1 ) ) x. ( ( 1 - x ) ^ ( N - M ) ) ) _d x )
52 id 
 |-  ( i = M -> i = M )
53 oveq2 
 |-  ( i = M -> ( N _C i ) = ( N _C M ) )
54 52 53 oveq12d 
 |-  ( i = M -> ( i x. ( N _C i ) ) = ( M x. ( N _C M ) ) )
55 54 oveq2d 
 |-  ( i = M -> ( 1 / ( i x. ( N _C i ) ) ) = ( 1 / ( M x. ( N _C M ) ) ) )
56 51 55 eqeq12d 
 |-  ( i = M -> ( S. ( 0 [,] 1 ) ( ( x ^ ( i - 1 ) ) x. ( ( 1 - x ) ^ ( N - i ) ) ) _d x = ( 1 / ( i x. ( N _C i ) ) ) <-> S. ( 0 [,] 1 ) ( ( x ^ ( M - 1 ) ) x. ( ( 1 - x ) ^ ( N - M ) ) ) _d x = ( 1 / ( M x. ( N _C M ) ) ) ) )
57 3 lcmineqlem12 
 |-  ( ph -> S. ( 0 [,] 1 ) ( ( x ^ ( 1 - 1 ) ) x. ( ( 1 - x ) ^ ( N - 1 ) ) ) _d x = ( 1 / ( 1 x. ( N _C 1 ) ) ) )
58 elnnz1 
 |-  ( m e. NN <-> ( m e. ZZ /\ 1 <_ m ) )
59 58 biimpri 
 |-  ( ( m e. ZZ /\ 1 <_ m ) -> m e. NN )
60 59 3adant3 
 |-  ( ( m e. ZZ /\ 1 <_ m /\ m < N ) -> m e. NN )
61 60 adantl 
 |-  ( ( ph /\ ( m e. ZZ /\ 1 <_ m /\ m < N ) ) -> m e. NN )
62 3 adantr 
 |-  ( ( ph /\ ( m e. ZZ /\ 1 <_ m /\ m < N ) ) -> N e. NN )
63 simpr3 
 |-  ( ( ph /\ ( m e. ZZ /\ 1 <_ m /\ m < N ) ) -> m < N )
64 61 62 63 lcmineqlem10 
 |-  ( ( ph /\ ( m e. ZZ /\ 1 <_ m /\ m < N ) ) -> 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 ) )
65 64 3adant3 
 |-  ( ( ph /\ ( m e. ZZ /\ 1 <_ m /\ m < N ) /\ S. ( 0 [,] 1 ) ( ( x ^ ( m - 1 ) ) x. ( ( 1 - x ) ^ ( N - m ) ) ) _d x = ( 1 / ( m x. ( N _C m ) ) ) ) -> 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 ) )
66 oveq2 
 |-  ( S. ( 0 [,] 1 ) ( ( x ^ ( m - 1 ) ) x. ( ( 1 - x ) ^ ( N - m ) ) ) _d x = ( 1 / ( m x. ( N _C m ) ) ) -> ( ( m / ( N - m ) ) x. S. ( 0 [,] 1 ) ( ( x ^ ( m - 1 ) ) x. ( ( 1 - x ) ^ ( N - m ) ) ) _d x ) = ( ( m / ( N - m ) ) x. ( 1 / ( m x. ( N _C m ) ) ) ) )
67 66 3ad2ant3 
 |-  ( ( ph /\ ( m e. ZZ /\ 1 <_ m /\ m < N ) /\ S. ( 0 [,] 1 ) ( ( x ^ ( m - 1 ) ) x. ( ( 1 - x ) ^ ( N - m ) ) ) _d x = ( 1 / ( m x. ( N _C m ) ) ) ) -> ( ( m / ( N - m ) ) x. S. ( 0 [,] 1 ) ( ( x ^ ( m - 1 ) ) x. ( ( 1 - x ) ^ ( N - m ) ) ) _d x ) = ( ( m / ( N - m ) ) x. ( 1 / ( m x. ( N _C m ) ) ) ) )
68 65 67 eqtrd 
 |-  ( ( ph /\ ( m e. ZZ /\ 1 <_ m /\ m < N ) /\ S. ( 0 [,] 1 ) ( ( x ^ ( m - 1 ) ) x. ( ( 1 - x ) ^ ( N - m ) ) ) _d x = ( 1 / ( m x. ( N _C m ) ) ) ) -> S. ( 0 [,] 1 ) ( ( x ^ ( ( m + 1 ) - 1 ) ) x. ( ( 1 - x ) ^ ( N - ( m + 1 ) ) ) ) _d x = ( ( m / ( N - m ) ) x. ( 1 / ( m x. ( N _C m ) ) ) ) )
69 61 62 63 lcmineqlem11 
 |-  ( ( ph /\ ( m e. ZZ /\ 1 <_ m /\ m < N ) ) -> ( 1 / ( ( m + 1 ) x. ( N _C ( m + 1 ) ) ) ) = ( ( m / ( N - m ) ) x. ( 1 / ( m x. ( N _C m ) ) ) ) )
70 69 3adant3 
 |-  ( ( ph /\ ( m e. ZZ /\ 1 <_ m /\ m < N ) /\ S. ( 0 [,] 1 ) ( ( x ^ ( m - 1 ) ) x. ( ( 1 - x ) ^ ( N - m ) ) ) _d x = ( 1 / ( m x. ( N _C m ) ) ) ) -> ( 1 / ( ( m + 1 ) x. ( N _C ( m + 1 ) ) ) ) = ( ( m / ( N - m ) ) x. ( 1 / ( m x. ( N _C m ) ) ) ) )
71 68 70 eqtr4d 
 |-  ( ( ph /\ ( m e. ZZ /\ 1 <_ m /\ m < N ) /\ S. ( 0 [,] 1 ) ( ( x ^ ( m - 1 ) ) x. ( ( 1 - x ) ^ ( N - m ) ) ) _d x = ( 1 / ( m x. ( N _C m ) ) ) ) -> S. ( 0 [,] 1 ) ( ( x ^ ( ( m + 1 ) - 1 ) ) x. ( ( 1 - x ) ^ ( N - ( m + 1 ) ) ) ) _d x = ( 1 / ( ( m + 1 ) x. ( N _C ( m + 1 ) ) ) ) )
72 1zzd 
 |-  ( ph -> 1 e. ZZ )
73 3 nnzd 
 |-  ( ph -> N e. ZZ )
74 3 nnge1d 
 |-  ( ph -> 1 <_ N )
75 20 32 44 56 57 71 72 73 74 fzindd 
 |-  ( ( ph /\ ( M e. ZZ /\ 1 <_ M /\ M <_ N ) ) -> S. ( 0 [,] 1 ) ( ( x ^ ( M - 1 ) ) x. ( ( 1 - x ) ^ ( N - M ) ) ) _d x = ( 1 / ( M x. ( N _C M ) ) ) )
76 8 75 mpdan 
 |-  ( ph -> S. ( 0 [,] 1 ) ( ( x ^ ( M - 1 ) ) x. ( ( 1 - x ) ^ ( N - M ) ) ) _d x = ( 1 / ( M x. ( N _C M ) ) ) )
77 1 76 syl5eq 
 |-  ( ph -> F = ( 1 / ( M x. ( N _C M ) ) ) )