Metamath Proof Explorer

Theorem lcmineqlem18

Description: Technical lemma to shift factors in binomial coefficient. (Contributed by metakunt, 12-May-2024)

Ref Expression
Hypothesis lcmineqlem18.1 
|- ( ph -> N e. NN )
Assertion lcmineqlem18 
|- ( ph -> ( ( N + 1 ) x. ( ( ( 2 x. N ) + 1 ) _C ( N + 1 ) ) ) = ( ( ( 2 x. N ) + 1 ) x. ( ( 2 x. N ) _C N ) ) )

Proof

Step Hyp Ref Expression
1 lcmineqlem18.1 
 |-  ( ph -> N e. NN )
2 0zd 
 |-  ( ph -> 0 e. ZZ )
3 2z 
 |-  2 e. ZZ
4 3 a1i 
 |-  ( ph -> 2 e. ZZ )
5 1 nnzd 
 |-  ( ph -> N e. ZZ )
6 4 5 zmulcld 
 |-  ( ph -> ( 2 x. N ) e. ZZ )
7 6 peano2zd 
 |-  ( ph -> ( ( 2 x. N ) + 1 ) e. ZZ )
8 5 peano2zd 
 |-  ( ph -> ( N + 1 ) e. ZZ )
9 1 nnred 
 |-  ( ph -> N e. RR )
10 1red 
 |-  ( ph -> 1 e. RR )
11 1 nnnn0d 
 |-  ( ph -> N e. NN0 )
12 11 nn0ge0d 
 |-  ( ph -> 0 <_ N )
13 0le1 
 |-  0 <_ 1
14 13 a1i 
 |-  ( ph -> 0 <_ 1 )
15 9 10 12 14 addge0d 
 |-  ( ph -> 0 <_ ( N + 1 ) )
16 9 10 readdcld 
 |-  ( ph -> ( N + 1 ) e. RR )
17 16 9 addge01d 
 |-  ( ph -> ( 0 <_ N <-> ( N + 1 ) <_ ( ( N + 1 ) + N ) ) )
18 12 17 mpbid 
 |-  ( ph -> ( N + 1 ) <_ ( ( N + 1 ) + N ) )
19 9 recnd 
 |-  ( ph -> N e. CC )
20 1cnd 
 |-  ( ph -> 1 e. CC )
21 19 20 19 add32d 
 |-  ( ph -> ( ( N + 1 ) + N ) = ( ( N + N ) + 1 ) )
22 19 2timesd 
 |-  ( ph -> ( 2 x. N ) = ( N + N ) )
23 22 oveq1d 
 |-  ( ph -> ( ( 2 x. N ) + 1 ) = ( ( N + N ) + 1 ) )
24 23 eqcomd 
 |-  ( ph -> ( ( N + N ) + 1 ) = ( ( 2 x. N ) + 1 ) )
25 21 24 eqtrd 
 |-  ( ph -> ( ( N + 1 ) + N ) = ( ( 2 x. N ) + 1 ) )
26 18 25 breqtrd 
 |-  ( ph -> ( N + 1 ) <_ ( ( 2 x. N ) + 1 ) )
27 2 7 8 15 26 elfzd 
 |-  ( ph -> ( N + 1 ) e. ( 0 ... ( ( 2 x. N ) + 1 ) ) )
28 bcval2 
 |-  ( ( N + 1 ) e. ( 0 ... ( ( 2 x. N ) + 1 ) ) -> ( ( ( 2 x. N ) + 1 ) _C ( N + 1 ) ) = ( ( ! ` ( ( 2 x. N ) + 1 ) ) / ( ( ! ` ( ( ( 2 x. N ) + 1 ) - ( N + 1 ) ) ) x. ( ! ` ( N + 1 ) ) ) ) )
29 27 28 syl 
 |-  ( ph -> ( ( ( 2 x. N ) + 1 ) _C ( N + 1 ) ) = ( ( ! ` ( ( 2 x. N ) + 1 ) ) / ( ( ! ` ( ( ( 2 x. N ) + 1 ) - ( N + 1 ) ) ) x. ( ! ` ( N + 1 ) ) ) ) )
30 6 zcnd 
 |-  ( ph -> ( 2 x. N ) e. CC )
31 30 20 19 20 addsub4d 
 |-  ( ph -> ( ( ( 2 x. N ) + 1 ) - ( N + 1 ) ) = ( ( ( 2 x. N ) - N ) + ( 1 - 1 ) ) )
32 22 oveq1d 
 |-  ( ph -> ( ( 2 x. N ) - N ) = ( ( N + N ) - N ) )
33 19 19 pncand 
 |-  ( ph -> ( ( N + N ) - N ) = N )
34 32 33 eqtrd 
 |-  ( ph -> ( ( 2 x. N ) - N ) = N )
35 1m1e0 
 |-  ( 1 - 1 ) = 0
36 35 a1i 
 |-  ( ph -> ( 1 - 1 ) = 0 )
37 34 36 oveq12d 
 |-  ( ph -> ( ( ( 2 x. N ) - N ) + ( 1 - 1 ) ) = ( N + 0 ) )
38 19 addid1d 
 |-  ( ph -> ( N + 0 ) = N )
39 37 38 eqtrd 
 |-  ( ph -> ( ( ( 2 x. N ) - N ) + ( 1 - 1 ) ) = N )
40 31 39 eqtrd 
 |-  ( ph -> ( ( ( 2 x. N ) + 1 ) - ( N + 1 ) ) = N )
41 40 fveq2d 
 |-  ( ph -> ( ! ` ( ( ( 2 x. N ) + 1 ) - ( N + 1 ) ) ) = ( ! ` N ) )
42 41 oveq1d 
 |-  ( ph -> ( ( ! ` ( ( ( 2 x. N ) + 1 ) - ( N + 1 ) ) ) x. ( ! ` ( N + 1 ) ) ) = ( ( ! ` N ) x. ( ! ` ( N + 1 ) ) ) )
43 42 oveq2d 
 |-  ( ph -> ( ( ! ` ( ( 2 x. N ) + 1 ) ) / ( ( ! ` ( ( ( 2 x. N ) + 1 ) - ( N + 1 ) ) ) x. ( ! ` ( N + 1 ) ) ) ) = ( ( ! ` ( ( 2 x. N ) + 1 ) ) / ( ( ! ` N ) x. ( ! ` ( N + 1 ) ) ) ) )
44 29 43 eqtrd 
 |-  ( ph -> ( ( ( 2 x. N ) + 1 ) _C ( N + 1 ) ) = ( ( ! ` ( ( 2 x. N ) + 1 ) ) / ( ( ! ` N ) x. ( ! ` ( N + 1 ) ) ) ) )
45 faccl 
 |-  ( N e. NN0 -> ( ! ` N ) e. NN )
46 11 45 syl 
 |-  ( ph -> ( ! ` N ) e. NN )
47 46 nncnd 
 |-  ( ph -> ( ! ` N ) e. CC )
48 1nn0 
 |-  1 e. NN0
49 48 a1i 
 |-  ( ph -> 1 e. NN0 )
50 11 49 nn0addcld 
 |-  ( ph -> ( N + 1 ) e. NN0 )
51 faccl 
 |-  ( ( N + 1 ) e. NN0 -> ( ! ` ( N + 1 ) ) e. NN )
52 50 51 syl 
 |-  ( ph -> ( ! ` ( N + 1 ) ) e. NN )
53 52 nncnd 
 |-  ( ph -> ( ! ` ( N + 1 ) ) e. CC )
54 47 53 mulcomd 
 |-  ( ph -> ( ( ! ` N ) x. ( ! ` ( N + 1 ) ) ) = ( ( ! ` ( N + 1 ) ) x. ( ! ` N ) ) )
55 facp1 
 |-  ( N e. NN0 -> ( ! ` ( N + 1 ) ) = ( ( ! ` N ) x. ( N + 1 ) ) )
56 11 55 syl 
 |-  ( ph -> ( ! ` ( N + 1 ) ) = ( ( ! ` N ) x. ( N + 1 ) ) )
57 19 20 addcld 
 |-  ( ph -> ( N + 1 ) e. CC )
58 47 57 mulcomd 
 |-  ( ph -> ( ( ! ` N ) x. ( N + 1 ) ) = ( ( N + 1 ) x. ( ! ` N ) ) )
59 56 58 eqtrd 
 |-  ( ph -> ( ! ` ( N + 1 ) ) = ( ( N + 1 ) x. ( ! ` N ) ) )
60 59 oveq1d 
 |-  ( ph -> ( ( ! ` ( N + 1 ) ) x. ( ! ` N ) ) = ( ( ( N + 1 ) x. ( ! ` N ) ) x. ( ! ` N ) ) )
61 57 47 47 mulassd 
 |-  ( ph -> ( ( ( N + 1 ) x. ( ! ` N ) ) x. ( ! ` N ) ) = ( ( N + 1 ) x. ( ( ! ` N ) x. ( ! ` N ) ) ) )
62 60 61 eqtrd 
 |-  ( ph -> ( ( ! ` ( N + 1 ) ) x. ( ! ` N ) ) = ( ( N + 1 ) x. ( ( ! ` N ) x. ( ! ` N ) ) ) )
63 54 62 eqtrd 
 |-  ( ph -> ( ( ! ` N ) x. ( ! ` ( N + 1 ) ) ) = ( ( N + 1 ) x. ( ( ! ` N ) x. ( ! ` N ) ) ) )
64 63 oveq2d 
 |-  ( ph -> ( ( ! ` ( ( 2 x. N ) + 1 ) ) / ( ( ! ` N ) x. ( ! ` ( N + 1 ) ) ) ) = ( ( ! ` ( ( 2 x. N ) + 1 ) ) / ( ( N + 1 ) x. ( ( ! ` N ) x. ( ! ` N ) ) ) ) )
65 44 64 eqtrd 
 |-  ( ph -> ( ( ( 2 x. N ) + 1 ) _C ( N + 1 ) ) = ( ( ! ` ( ( 2 x. N ) + 1 ) ) / ( ( N + 1 ) x. ( ( ! ` N ) x. ( ! ` N ) ) ) ) )
66 2nn0 
 |-  2 e. NN0
67 66 a1i 
 |-  ( ph -> 2 e. NN0 )
68 67 11 nn0mulcld 
 |-  ( ph -> ( 2 x. N ) e. NN0 )
69 facp1 
 |-  ( ( 2 x. N ) e. NN0 -> ( ! ` ( ( 2 x. N ) + 1 ) ) = ( ( ! ` ( 2 x. N ) ) x. ( ( 2 x. N ) + 1 ) ) )
70 68 69 syl 
 |-  ( ph -> ( ! ` ( ( 2 x. N ) + 1 ) ) = ( ( ! ` ( 2 x. N ) ) x. ( ( 2 x. N ) + 1 ) ) )
71 faccl 
 |-  ( ( 2 x. N ) e. NN0 -> ( ! ` ( 2 x. N ) ) e. NN )
72 68 71 syl 
 |-  ( ph -> ( ! ` ( 2 x. N ) ) e. NN )
73 72 nncnd 
 |-  ( ph -> ( ! ` ( 2 x. N ) ) e. CC )
74 30 20 addcld 
 |-  ( ph -> ( ( 2 x. N ) + 1 ) e. CC )
75 73 74 mulcomd 
 |-  ( ph -> ( ( ! ` ( 2 x. N ) ) x. ( ( 2 x. N ) + 1 ) ) = ( ( ( 2 x. N ) + 1 ) x. ( ! ` ( 2 x. N ) ) ) )
76 70 75 eqtrd 
 |-  ( ph -> ( ! ` ( ( 2 x. N ) + 1 ) ) = ( ( ( 2 x. N ) + 1 ) x. ( ! ` ( 2 x. N ) ) ) )
77 76 oveq1d 
 |-  ( ph -> ( ( ! ` ( ( 2 x. N ) + 1 ) ) / ( ( N + 1 ) x. ( ( ! ` N ) x. ( ! ` N ) ) ) ) = ( ( ( ( 2 x. N ) + 1 ) x. ( ! ` ( 2 x. N ) ) ) / ( ( N + 1 ) x. ( ( ! ` N ) x. ( ! ` N ) ) ) ) )
78 65 77 eqtrd 
 |-  ( ph -> ( ( ( 2 x. N ) + 1 ) _C ( N + 1 ) ) = ( ( ( ( 2 x. N ) + 1 ) x. ( ! ` ( 2 x. N ) ) ) / ( ( N + 1 ) x. ( ( ! ` N ) x. ( ! ` N ) ) ) ) )
79 78 oveq2d 
 |-  ( ph -> ( ( N + 1 ) x. ( ( ( 2 x. N ) + 1 ) _C ( N + 1 ) ) ) = ( ( N + 1 ) x. ( ( ( ( 2 x. N ) + 1 ) x. ( ! ` ( 2 x. N ) ) ) / ( ( N + 1 ) x. ( ( ! ` N ) x. ( ! ` N ) ) ) ) ) )
80 74 73 mulcld 
 |-  ( ph -> ( ( ( 2 x. N ) + 1 ) x. ( ! ` ( 2 x. N ) ) ) e. CC )
81 47 47 mulcld 
 |-  ( ph -> ( ( ! ` N ) x. ( ! ` N ) ) e. CC )
82 57 81 mulcld 
 |-  ( ph -> ( ( N + 1 ) x. ( ( ! ` N ) x. ( ! ` N ) ) ) e. CC )
83 1 peano2nnd 
 |-  ( ph -> ( N + 1 ) e. NN )
84 83 nnne0d 
 |-  ( ph -> ( N + 1 ) =/= 0 )
85 46 nnne0d 
 |-  ( ph -> ( ! ` N ) =/= 0 )
86 47 47 85 85 mulne0d 
 |-  ( ph -> ( ( ! ` N ) x. ( ! ` N ) ) =/= 0 )
87 57 81 84 86 mulne0d 
 |-  ( ph -> ( ( N + 1 ) x. ( ( ! ` N ) x. ( ! ` N ) ) ) =/= 0 )
88 57 80 82 87 divassd 
 |-  ( ph -> ( ( ( N + 1 ) x. ( ( ( 2 x. N ) + 1 ) x. ( ! ` ( 2 x. N ) ) ) ) / ( ( N + 1 ) x. ( ( ! ` N ) x. ( ! ` N ) ) ) ) = ( ( N + 1 ) x. ( ( ( ( 2 x. N ) + 1 ) x. ( ! ` ( 2 x. N ) ) ) / ( ( N + 1 ) x. ( ( ! ` N ) x. ( ! ` N ) ) ) ) ) )
89 88 eqcomd 
 |-  ( ph -> ( ( N + 1 ) x. ( ( ( ( 2 x. N ) + 1 ) x. ( ! ` ( 2 x. N ) ) ) / ( ( N + 1 ) x. ( ( ! ` N ) x. ( ! ` N ) ) ) ) ) = ( ( ( N + 1 ) x. ( ( ( 2 x. N ) + 1 ) x. ( ! ` ( 2 x. N ) ) ) ) / ( ( N + 1 ) x. ( ( ! ` N ) x. ( ! ` N ) ) ) ) )
90 79 89 eqtrd 
 |-  ( ph -> ( ( N + 1 ) x. ( ( ( 2 x. N ) + 1 ) _C ( N + 1 ) ) ) = ( ( ( N + 1 ) x. ( ( ( 2 x. N ) + 1 ) x. ( ! ` ( 2 x. N ) ) ) ) / ( ( N + 1 ) x. ( ( ! ` N ) x. ( ! ` N ) ) ) ) )
91 57 57 80 81 84 86 divmuldivd 
 |-  ( ph -> ( ( ( N + 1 ) / ( N + 1 ) ) x. ( ( ( ( 2 x. N ) + 1 ) x. ( ! ` ( 2 x. N ) ) ) / ( ( ! ` N ) x. ( ! ` N ) ) ) ) = ( ( ( N + 1 ) x. ( ( ( 2 x. N ) + 1 ) x. ( ! ` ( 2 x. N ) ) ) ) / ( ( N + 1 ) x. ( ( ! ` N ) x. ( ! ` N ) ) ) ) )
92 91 eqcomd 
 |-  ( ph -> ( ( ( N + 1 ) x. ( ( ( 2 x. N ) + 1 ) x. ( ! ` ( 2 x. N ) ) ) ) / ( ( N + 1 ) x. ( ( ! ` N ) x. ( ! ` N ) ) ) ) = ( ( ( N + 1 ) / ( N + 1 ) ) x. ( ( ( ( 2 x. N ) + 1 ) x. ( ! ` ( 2 x. N ) ) ) / ( ( ! ` N ) x. ( ! ` N ) ) ) ) )
93 90 92 eqtrd 
 |-  ( ph -> ( ( N + 1 ) x. ( ( ( 2 x. N ) + 1 ) _C ( N + 1 ) ) ) = ( ( ( N + 1 ) / ( N + 1 ) ) x. ( ( ( ( 2 x. N ) + 1 ) x. ( ! ` ( 2 x. N ) ) ) / ( ( ! ` N ) x. ( ! ` N ) ) ) ) )
94 57 84 dividd 
 |-  ( ph -> ( ( N + 1 ) / ( N + 1 ) ) = 1 )
95 94 oveq1d 
 |-  ( ph -> ( ( ( N + 1 ) / ( N + 1 ) ) x. ( ( ( ( 2 x. N ) + 1 ) x. ( ! ` ( 2 x. N ) ) ) / ( ( ! ` N ) x. ( ! ` N ) ) ) ) = ( 1 x. ( ( ( ( 2 x. N ) + 1 ) x. ( ! ` ( 2 x. N ) ) ) / ( ( ! ` N ) x. ( ! ` N ) ) ) ) )
96 80 81 86 divcld 
 |-  ( ph -> ( ( ( ( 2 x. N ) + 1 ) x. ( ! ` ( 2 x. N ) ) ) / ( ( ! ` N ) x. ( ! ` N ) ) ) e. CC )
97 96 mulid2d 
 |-  ( ph -> ( 1 x. ( ( ( ( 2 x. N ) + 1 ) x. ( ! ` ( 2 x. N ) ) ) / ( ( ! ` N ) x. ( ! ` N ) ) ) ) = ( ( ( ( 2 x. N ) + 1 ) x. ( ! ` ( 2 x. N ) ) ) / ( ( ! ` N ) x. ( ! ` N ) ) ) )
98 95 97 eqtrd 
 |-  ( ph -> ( ( ( N + 1 ) / ( N + 1 ) ) x. ( ( ( ( 2 x. N ) + 1 ) x. ( ! ` ( 2 x. N ) ) ) / ( ( ! ` N ) x. ( ! ` N ) ) ) ) = ( ( ( ( 2 x. N ) + 1 ) x. ( ! ` ( 2 x. N ) ) ) / ( ( ! ` N ) x. ( ! ` N ) ) ) )
99 93 98 eqtrd 
 |-  ( ph -> ( ( N + 1 ) x. ( ( ( 2 x. N ) + 1 ) _C ( N + 1 ) ) ) = ( ( ( ( 2 x. N ) + 1 ) x. ( ! ` ( 2 x. N ) ) ) / ( ( ! ` N ) x. ( ! ` N ) ) ) )
100 74 73 81 86 divassd 
 |-  ( ph -> ( ( ( ( 2 x. N ) + 1 ) x. ( ! ` ( 2 x. N ) ) ) / ( ( ! ` N ) x. ( ! ` N ) ) ) = ( ( ( 2 x. N ) + 1 ) x. ( ( ! ` ( 2 x. N ) ) / ( ( ! ` N ) x. ( ! ` N ) ) ) ) )
101 99 100 eqtrd 
 |-  ( ph -> ( ( N + 1 ) x. ( ( ( 2 x. N ) + 1 ) _C ( N + 1 ) ) ) = ( ( ( 2 x. N ) + 1 ) x. ( ( ! ` ( 2 x. N ) ) / ( ( ! ` N ) x. ( ! ` N ) ) ) ) )
102 9 9 addge01d 
 |-  ( ph -> ( 0 <_ N <-> N <_ ( N + N ) ) )
103 22 breq2d 
 |-  ( ph -> ( N <_ ( 2 x. N ) <-> N <_ ( N + N ) ) )
104 102 103 bitr4d 
 |-  ( ph -> ( 0 <_ N <-> N <_ ( 2 x. N ) ) )
105 12 104 mpbid 
 |-  ( ph -> N <_ ( 2 x. N ) )
106 2 6 5 12 105 elfzd 
 |-  ( ph -> N e. ( 0 ... ( 2 x. N ) ) )
107 bcval2 
 |-  ( N e. ( 0 ... ( 2 x. N ) ) -> ( ( 2 x. N ) _C N ) = ( ( ! ` ( 2 x. N ) ) / ( ( ! ` ( ( 2 x. N ) - N ) ) x. ( ! ` N ) ) ) )
108 106 107 syl 
 |-  ( ph -> ( ( 2 x. N ) _C N ) = ( ( ! ` ( 2 x. N ) ) / ( ( ! ` ( ( 2 x. N ) - N ) ) x. ( ! ` N ) ) ) )
109 34 fveq2d 
 |-  ( ph -> ( ! ` ( ( 2 x. N ) - N ) ) = ( ! ` N ) )
110 109 oveq1d 
 |-  ( ph -> ( ( ! ` ( ( 2 x. N ) - N ) ) x. ( ! ` N ) ) = ( ( ! ` N ) x. ( ! ` N ) ) )
111 110 oveq2d 
 |-  ( ph -> ( ( ! ` ( 2 x. N ) ) / ( ( ! ` ( ( 2 x. N ) - N ) ) x. ( ! ` N ) ) ) = ( ( ! ` ( 2 x. N ) ) / ( ( ! ` N ) x. ( ! ` N ) ) ) )
112 108 111 eqtrd 
 |-  ( ph -> ( ( 2 x. N ) _C N ) = ( ( ! ` ( 2 x. N ) ) / ( ( ! ` N ) x. ( ! ` N ) ) ) )
113 112 oveq2d 
 |-  ( ph -> ( ( ( 2 x. N ) + 1 ) x. ( ( 2 x. N ) _C N ) ) = ( ( ( 2 x. N ) + 1 ) x. ( ( ! ` ( 2 x. N ) ) / ( ( ! ` N ) x. ( ! ` N ) ) ) ) )
114 113 eqcomd 
 |-  ( ph -> ( ( ( 2 x. N ) + 1 ) x. ( ( ! ` ( 2 x. N ) ) / ( ( ! ` N ) x. ( ! ` N ) ) ) ) = ( ( ( 2 x. N ) + 1 ) x. ( ( 2 x. N ) _C N ) ) )
115 101 114 eqtrd 
 |-  ( ph -> ( ( N + 1 ) x. ( ( ( 2 x. N ) + 1 ) _C ( N + 1 ) ) ) = ( ( ( 2 x. N ) + 1 ) x. ( ( 2 x. N ) _C N ) ) )