Metamath Proof Explorer

Theorem lcmineqlem11

Description: Induction step, continuation for binomial coefficients. (Contributed by metakunt, 12-May-2024)

Ref Expression
Hypotheses lcmineqlem11.1 
|- ( ph -> M e. NN )
lcmineqlem11.2 
|- ( ph -> N e. NN )
lcmineqlem11.3 
|- ( ph -> M < N )
Assertion lcmineqlem11 
|- ( ph -> ( 1 / ( ( M + 1 ) x. ( N _C ( M + 1 ) ) ) ) = ( ( M / ( N - M ) ) x. ( 1 / ( M x. ( N _C M ) ) ) ) )

Proof

Step Hyp Ref Expression
1 lcmineqlem11.1 
 |-  ( ph -> M e. NN )
2 lcmineqlem11.2 
 |-  ( ph -> N e. NN )
3 lcmineqlem11.3 
 |-  ( ph -> M < N )
4 1 nncnd 
 |-  ( ph -> M e. CC )
5 1cnd 
 |-  ( ph -> 1 e. CC )
6 4 5 addcld 
 |-  ( ph -> ( M + 1 ) e. CC )
7 1 nnnn0d 
 |-  ( ph -> M e. NN0 )
8 1nn0 
 |-  1 e. NN0
9 8 a1i 
 |-  ( ph -> 1 e. NN0 )
10 7 9 nn0addcld 
 |-  ( ph -> ( M + 1 ) e. NN0 )
11 1 nnzd 
 |-  ( ph -> M e. ZZ )
12 2 nnzd 
 |-  ( ph -> N e. ZZ )
13 zltp1le 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M < N <-> ( M + 1 ) <_ N ) )
14 11 12 13 syl2anc 
 |-  ( ph -> ( M < N <-> ( M + 1 ) <_ N ) )
15 3 14 mpbid 
 |-  ( ph -> ( M + 1 ) <_ N )
16 2 10 15 bccl2d 
 |-  ( ph -> ( N _C ( M + 1 ) ) e. NN )
17 16 nncnd 
 |-  ( ph -> ( N _C ( M + 1 ) ) e. CC )
18 6 17 mulcld 
 |-  ( ph -> ( ( M + 1 ) x. ( N _C ( M + 1 ) ) ) e. CC )
19 18 div1d 
 |-  ( ph -> ( ( ( M + 1 ) x. ( N _C ( M + 1 ) ) ) / 1 ) = ( ( M + 1 ) x. ( N _C ( M + 1 ) ) ) )
20 11 peano2zd 
 |-  ( ph -> ( M + 1 ) e. ZZ )
21 1 peano2nnd 
 |-  ( ph -> ( M + 1 ) e. NN )
22 21 nnge1d 
 |-  ( ph -> 1 <_ ( M + 1 ) )
23 20 22 15 3jca 
 |-  ( ph -> ( ( M + 1 ) e. ZZ /\ 1 <_ ( M + 1 ) /\ ( M + 1 ) <_ N ) )
24 1z 
 |-  1 e. ZZ
25 elfz1 
 |-  ( ( 1 e. ZZ /\ N e. ZZ ) -> ( ( M + 1 ) e. ( 1 ... N ) <-> ( ( M + 1 ) e. ZZ /\ 1 <_ ( M + 1 ) /\ ( M + 1 ) <_ N ) ) )
26 24 25 mpan 
 |-  ( N e. ZZ -> ( ( M + 1 ) e. ( 1 ... N ) <-> ( ( M + 1 ) e. ZZ /\ 1 <_ ( M + 1 ) /\ ( M + 1 ) <_ N ) ) )
27 12 26 syl 
 |-  ( ph -> ( ( M + 1 ) e. ( 1 ... N ) <-> ( ( M + 1 ) e. ZZ /\ 1 <_ ( M + 1 ) /\ ( M + 1 ) <_ N ) ) )
28 23 27 mpbird 
 |-  ( ph -> ( M + 1 ) e. ( 1 ... N ) )
29 bcm1k 
 |-  ( ( M + 1 ) e. ( 1 ... N ) -> ( N _C ( M + 1 ) ) = ( ( N _C ( ( M + 1 ) - 1 ) ) x. ( ( N - ( ( M + 1 ) - 1 ) ) / ( M + 1 ) ) ) )
30 28 29 syl 
 |-  ( ph -> ( N _C ( M + 1 ) ) = ( ( N _C ( ( M + 1 ) - 1 ) ) x. ( ( N - ( ( M + 1 ) - 1 ) ) / ( M + 1 ) ) ) )
31 4 5 pncand 
 |-  ( ph -> ( ( M + 1 ) - 1 ) = M )
32 31 oveq2d 
 |-  ( ph -> ( N _C ( ( M + 1 ) - 1 ) ) = ( N _C M ) )
33 31 oveq2d 
 |-  ( ph -> ( N - ( ( M + 1 ) - 1 ) ) = ( N - M ) )
34 33 oveq1d 
 |-  ( ph -> ( ( N - ( ( M + 1 ) - 1 ) ) / ( M + 1 ) ) = ( ( N - M ) / ( M + 1 ) ) )
35 32 34 oveq12d 
 |-  ( ph -> ( ( N _C ( ( M + 1 ) - 1 ) ) x. ( ( N - ( ( M + 1 ) - 1 ) ) / ( M + 1 ) ) ) = ( ( N _C M ) x. ( ( N - M ) / ( M + 1 ) ) ) )
36 30 35 eqtrd 
 |-  ( ph -> ( N _C ( M + 1 ) ) = ( ( N _C M ) x. ( ( N - M ) / ( M + 1 ) ) ) )
37 1 nnred 
 |-  ( ph -> M e. RR )
38 2 nnred 
 |-  ( ph -> N e. RR )
39 37 38 3 ltled 
 |-  ( ph -> M <_ N )
40 2 7 39 bccl2d 
 |-  ( ph -> ( N _C M ) e. NN )
41 40 nncnd 
 |-  ( ph -> ( N _C M ) e. CC )
42 2 nncnd 
 |-  ( ph -> N e. CC )
43 42 4 subcld 
 |-  ( ph -> ( N - M ) e. CC )
44 21 nnne0d 
 |-  ( ph -> ( M + 1 ) =/= 0 )
45 41 43 6 44 divassd 
 |-  ( ph -> ( ( ( N _C M ) x. ( N - M ) ) / ( M + 1 ) ) = ( ( N _C M ) x. ( ( N - M ) / ( M + 1 ) ) ) )
46 36 45 eqtr4d 
 |-  ( ph -> ( N _C ( M + 1 ) ) = ( ( ( N _C M ) x. ( N - M ) ) / ( M + 1 ) ) )
47 46 eqcomd 
 |-  ( ph -> ( ( ( N _C M ) x. ( N - M ) ) / ( M + 1 ) ) = ( N _C ( M + 1 ) ) )
48 41 43 mulcld 
 |-  ( ph -> ( ( N _C M ) x. ( N - M ) ) e. CC )
49 48 17 6 44 divmul2d 
 |-  ( ph -> ( ( ( ( N _C M ) x. ( N - M ) ) / ( M + 1 ) ) = ( N _C ( M + 1 ) ) <-> ( ( N _C M ) x. ( N - M ) ) = ( ( M + 1 ) x. ( N _C ( M + 1 ) ) ) ) )
50 47 49 mpbid 
 |-  ( ph -> ( ( N _C M ) x. ( N - M ) ) = ( ( M + 1 ) x. ( N _C ( M + 1 ) ) ) )
51 50 eqcomd 
 |-  ( ph -> ( ( M + 1 ) x. ( N _C ( M + 1 ) ) ) = ( ( N _C M ) x. ( N - M ) ) )
52 41 43 mulcomd 
 |-  ( ph -> ( ( N _C M ) x. ( N - M ) ) = ( ( N - M ) x. ( N _C M ) ) )
53 51 52 eqtrd 
 |-  ( ph -> ( ( M + 1 ) x. ( N _C ( M + 1 ) ) ) = ( ( N - M ) x. ( N _C M ) ) )
54 19 53 eqtrd 
 |-  ( ph -> ( ( ( M + 1 ) x. ( N _C ( M + 1 ) ) ) / 1 ) = ( ( N - M ) x. ( N _C M ) ) )
55 43 41 mulcld 
 |-  ( ph -> ( ( N - M ) x. ( N _C M ) ) e. CC )
56 1 nnne0d 
 |-  ( ph -> M =/= 0 )
57 55 4 56 divcan3d 
 |-  ( ph -> ( ( M x. ( ( N - M ) x. ( N _C M ) ) ) / M ) = ( ( N - M ) x. ( N _C M ) ) )
58 54 57 eqtr4d 
 |-  ( ph -> ( ( ( M + 1 ) x. ( N _C ( M + 1 ) ) ) / 1 ) = ( ( M x. ( ( N - M ) x. ( N _C M ) ) ) / M ) )
59 4 43 41 mul12d 
 |-  ( ph -> ( M x. ( ( N - M ) x. ( N _C M ) ) ) = ( ( N - M ) x. ( M x. ( N _C M ) ) ) )
60 59 oveq1d 
 |-  ( ph -> ( ( M x. ( ( N - M ) x. ( N _C M ) ) ) / M ) = ( ( ( N - M ) x. ( M x. ( N _C M ) ) ) / M ) )
61 58 60 eqtrd 
 |-  ( ph -> ( ( ( M + 1 ) x. ( N _C ( M + 1 ) ) ) / 1 ) = ( ( ( N - M ) x. ( M x. ( N _C M ) ) ) / M ) )
62 0ne1 
 |-  0 =/= 1
63 62 a1i 
 |-  ( ph -> 0 =/= 1 )
64 63 necomd 
 |-  ( ph -> 1 =/= 0 )
65 16 nnne0d 
 |-  ( ph -> ( N _C ( M + 1 ) ) =/= 0 )
66 6 17 44 65 mulne0d 
 |-  ( ph -> ( ( M + 1 ) x. ( N _C ( M + 1 ) ) ) =/= 0 )
67 4 41 mulcld 
 |-  ( ph -> ( M x. ( N _C M ) ) e. CC )
68 43 67 mulcld 
 |-  ( ph -> ( ( N - M ) x. ( M x. ( N _C M ) ) ) e. CC )
69 37 3 gtned 
 |-  ( ph -> N =/= M )
70 42 4 69 subne0d 
 |-  ( ph -> ( N - M ) =/= 0 )
71 40 nnne0d 
 |-  ( ph -> ( N _C M ) =/= 0 )
72 4 41 56 71 mulne0d 
 |-  ( ph -> ( M x. ( N _C M ) ) =/= 0 )
73 43 67 70 72 mulne0d 
 |-  ( ph -> ( ( N - M ) x. ( M x. ( N _C M ) ) ) =/= 0 )
74 5 64 18 66 4 56 68 73 recbothd 
 |-  ( ph -> ( ( 1 / ( ( M + 1 ) x. ( N _C ( M + 1 ) ) ) ) = ( M / ( ( N - M ) x. ( M x. ( N _C M ) ) ) ) <-> ( ( ( M + 1 ) x. ( N _C ( M + 1 ) ) ) / 1 ) = ( ( ( N - M ) x. ( M x. ( N _C M ) ) ) / M ) ) )
75 61 74 mpbird 
 |-  ( ph -> ( 1 / ( ( M + 1 ) x. ( N _C ( M + 1 ) ) ) ) = ( M / ( ( N - M ) x. ( M x. ( N _C M ) ) ) ) )
76 4 mulid1d 
 |-  ( ph -> ( M x. 1 ) = M )
77 76 oveq1d 
 |-  ( ph -> ( ( M x. 1 ) / ( ( N - M ) x. ( M x. ( N _C M ) ) ) ) = ( M / ( ( N - M ) x. ( M x. ( N _C M ) ) ) ) )
78 75 77 eqtr4d 
 |-  ( ph -> ( 1 / ( ( M + 1 ) x. ( N _C ( M + 1 ) ) ) ) = ( ( M x. 1 ) / ( ( N - M ) x. ( M x. ( N _C M ) ) ) ) )
79 4 43 5 67 70 72 divmuldivd 
 |-  ( ph -> ( ( M / ( N - M ) ) x. ( 1 / ( M x. ( N _C M ) ) ) ) = ( ( M x. 1 ) / ( ( N - M ) x. ( M x. ( N _C M ) ) ) ) )
80 78 79 eqtr4d 
 |-  ( ph -> ( 1 / ( ( M + 1 ) x. ( N _C ( M + 1 ) ) ) ) = ( ( M / ( N - M ) ) x. ( 1 / ( M x. ( N _C M ) ) ) ) )