Metamath Proof Explorer

Theorem bcled

Description: Inequality for binomial coefficients. (Contributed by metakunt, 12-May-2025)

Ref Expression
Hypotheses bcled.1 
|- ( ph -> A e. NN0 )
bcled.2 
|- ( ph -> B e. NN0 )
bcled.3 
|- ( ph -> C e. ZZ )
bcled.4 
|- ( ph -> A <_ B )
Assertion bcled 
|- ( ph -> ( A _C C ) <_ ( B _C C ) )

Proof

Step Hyp Ref Expression
1 bcled.1 
 |-  ( ph -> A e. NN0 )
2 bcled.2 
 |-  ( ph -> B e. NN0 )
3 bcled.3 
 |-  ( ph -> C e. ZZ )
4 bcled.4 
 |-  ( ph -> A <_ B )
5 bcval2 
 |-  ( C e. ( 0 ... A ) -> ( A _C C ) = ( ( ! ` A ) / ( ( ! ` ( A - C ) ) x. ( ! ` C ) ) ) )
6 5 adantl 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( A _C C ) = ( ( ! ` A ) / ( ( ! ` ( A - C ) ) x. ( ! ` C ) ) ) )
7 1 adantr 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> A e. NN0 )
8 7 faccld 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( ! ` A ) e. NN )
9 8 nncnd 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( ! ` A ) e. CC )
10 7 nn0zd 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> A e. ZZ )
11 3 adantr 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> C e. ZZ )
12 10 11 zsubcld 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( A - C ) e. ZZ )
13 11 zred 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> C e. RR )
14 7 nn0red 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> A e. RR )
15 0red 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> 0 e. RR )
16 elfzle2 
 |-  ( C e. ( 0 ... A ) -> C <_ A )
17 16 adantl 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> C <_ A )
18 14 recnd 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> A e. CC )
19 18 subid1d 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( A - 0 ) = A )
20 19 eqcomd 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> A = ( A - 0 ) )
21 17 20 breqtrd 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> C <_ ( A - 0 ) )
22 13 14 15 21 lesubd 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> 0 <_ ( A - C ) )
23 12 22 jca 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( ( A - C ) e. ZZ /\ 0 <_ ( A - C ) ) )
24 elnn0z 
 |-  ( ( A - C ) e. NN0 <-> ( ( A - C ) e. ZZ /\ 0 <_ ( A - C ) ) )
25 23 24 sylibr 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( A - C ) e. NN0 )
26 25 faccld 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( ! ` ( A - C ) ) e. NN )
27 26 nncnd 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( ! ` ( A - C ) ) e. CC )
28 elfznn0 
 |-  ( C e. ( 0 ... A ) -> C e. NN0 )
29 28 adantl 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> C e. NN0 )
30 29 faccld 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( ! ` C ) e. NN )
31 30 nncnd 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( ! ` C ) e. CC )
32 26 nnne0d 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( ! ` ( A - C ) ) =/= 0 )
33 30 nnne0d 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( ! ` C ) =/= 0 )
34 9 27 31 32 33 divdiv1d 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( ( ( ! ` A ) / ( ! ` ( A - C ) ) ) / ( ! ` C ) ) = ( ( ! ` A ) / ( ( ! ` ( A - C ) ) x. ( ! ` C ) ) ) )
35 34 eqcomd 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( ( ! ` A ) / ( ( ! ` ( A - C ) ) x. ( ! ` C ) ) ) = ( ( ( ! ` A ) / ( ! ` ( A - C ) ) ) / ( ! ` C ) ) )
36 8 nnred 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( ! ` A ) e. RR )
37 26 nnred 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( ! ` ( A - C ) ) e. RR )
38 36 37 32 redivcld 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( ( ! ` A ) / ( ! ` ( A - C ) ) ) e. RR )
39 2 adantr 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> B e. NN0 )
40 39 faccld 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( ! ` B ) e. NN )
41 40 nnred 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( ! ` B ) e. RR )
42 39 nn0zd 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> B e. ZZ )
43 42 11 zsubcld 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( B - C ) e. ZZ )
44 39 nn0red 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> B e. RR )
45 4 adantr 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> A <_ B )
46 13 14 44 17 45 letrd 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> C <_ B )
47 44 recnd 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> B e. CC )
48 47 subid1d 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( B - 0 ) = B )
49 48 eqcomd 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> B = ( B - 0 ) )
50 46 49 breqtrd 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> C <_ ( B - 0 ) )
51 13 44 15 50 lesubd 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> 0 <_ ( B - C ) )
52 43 51 jca 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( ( B - C ) e. ZZ /\ 0 <_ ( B - C ) ) )
53 elnn0z 
 |-  ( ( B - C ) e. NN0 <-> ( ( B - C ) e. ZZ /\ 0 <_ ( B - C ) ) )
54 52 53 sylibr 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( B - C ) e. NN0 )
55 54 faccld 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( ! ` ( B - C ) ) e. NN )
56 55 nnred 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( ! ` ( B - C ) ) e. RR )
57 55 nnne0d 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( ! ` ( B - C ) ) =/= 0 )
58 41 56 57 redivcld 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( ( ! ` B ) / ( ! ` ( B - C ) ) ) e. RR )
59 30 nnrpd 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( ! ` C ) e. RR+ )
60 nfv 
 |-  F/ k ( ph /\ C e. ( 0 ... A ) )
61 fzfid 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( 0 ... ( C - 1 ) ) e. Fin )
62 14 adantr 
 |-  ( ( ( ph /\ C e. ( 0 ... A ) ) /\ k e. ( 0 ... ( C - 1 ) ) ) -> A e. RR )
63 elfzelz 
 |-  ( k e. ( 0 ... ( C - 1 ) ) -> k e. ZZ )
64 63 adantl 
 |-  ( ( ( ph /\ C e. ( 0 ... A ) ) /\ k e. ( 0 ... ( C - 1 ) ) ) -> k e. ZZ )
65 64 zred 
 |-  ( ( ( ph /\ C e. ( 0 ... A ) ) /\ k e. ( 0 ... ( C - 1 ) ) ) -> k e. RR )
66 62 65 resubcld 
 |-  ( ( ( ph /\ C e. ( 0 ... A ) ) /\ k e. ( 0 ... ( C - 1 ) ) ) -> ( A - k ) e. RR )
67 0red 
 |-  ( ( ( ph /\ C e. ( 0 ... A ) ) /\ k e. ( 0 ... ( C - 1 ) ) ) -> 0 e. RR )
68 29 nn0red 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> C e. RR )
69 68 adantr 
 |-  ( ( ( ph /\ C e. ( 0 ... A ) ) /\ k e. ( 0 ... ( C - 1 ) ) ) -> C e. RR )
70 1red 
 |-  ( ( ( ph /\ C e. ( 0 ... A ) ) /\ k e. ( 0 ... ( C - 1 ) ) ) -> 1 e. RR )
71 69 70 resubcld 
 |-  ( ( ( ph /\ C e. ( 0 ... A ) ) /\ k e. ( 0 ... ( C - 1 ) ) ) -> ( C - 1 ) e. RR )
72 62 67 resubcld 
 |-  ( ( ( ph /\ C e. ( 0 ... A ) ) /\ k e. ( 0 ... ( C - 1 ) ) ) -> ( A - 0 ) e. RR )
73 elfzle2 
 |-  ( k e. ( 0 ... ( C - 1 ) ) -> k <_ ( C - 1 ) )
74 73 adantl 
 |-  ( ( ( ph /\ C e. ( 0 ... A ) ) /\ k e. ( 0 ... ( C - 1 ) ) ) -> k <_ ( C - 1 ) )
75 17 adantr 
 |-  ( ( ( ph /\ C e. ( 0 ... A ) ) /\ k e. ( 0 ... ( C - 1 ) ) ) -> C <_ A )
76 0le1 
 |-  0 <_ 1
77 76 a1i 
 |-  ( ( ( ph /\ C e. ( 0 ... A ) ) /\ k e. ( 0 ... ( C - 1 ) ) ) -> 0 <_ 1 )
78 69 67 62 70 75 77 le2subd 
 |-  ( ( ( ph /\ C e. ( 0 ... A ) ) /\ k e. ( 0 ... ( C - 1 ) ) ) -> ( C - 1 ) <_ ( A - 0 ) )
79 65 71 72 74 78 letrd 
 |-  ( ( ( ph /\ C e. ( 0 ... A ) ) /\ k e. ( 0 ... ( C - 1 ) ) ) -> k <_ ( A - 0 ) )
80 65 62 67 79 lesubd 
 |-  ( ( ( ph /\ C e. ( 0 ... A ) ) /\ k e. ( 0 ... ( C - 1 ) ) ) -> 0 <_ ( A - k ) )
81 44 adantr 
 |-  ( ( ( ph /\ C e. ( 0 ... A ) ) /\ k e. ( 0 ... ( C - 1 ) ) ) -> B e. RR )
82 81 65 resubcld 
 |-  ( ( ( ph /\ C e. ( 0 ... A ) ) /\ k e. ( 0 ... ( C - 1 ) ) ) -> ( B - k ) e. RR )
83 4 ad2antrr 
 |-  ( ( ( ph /\ C e. ( 0 ... A ) ) /\ k e. ( 0 ... ( C - 1 ) ) ) -> A <_ B )
84 62 81 65 83 lesub1dd 
 |-  ( ( ( ph /\ C e. ( 0 ... A ) ) /\ k e. ( 0 ... ( C - 1 ) ) ) -> ( A - k ) <_ ( B - k ) )
85 60 61 66 80 82 84 fprodle 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> prod_ k e. ( 0 ... ( C - 1 ) ) ( A - k ) <_ prod_ k e. ( 0 ... ( C - 1 ) ) ( B - k ) )
86 7 nn0cnd 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> A e. CC )
87 fallfacval 
 |-  ( ( A e. CC /\ C e. NN0 ) -> ( A FallFac C ) = prod_ k e. ( 0 ... ( C - 1 ) ) ( A - k ) )
88 86 29 87 syl2anc 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( A FallFac C ) = prod_ k e. ( 0 ... ( C - 1 ) ) ( A - k ) )
89 88 eqcomd 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> prod_ k e. ( 0 ... ( C - 1 ) ) ( A - k ) = ( A FallFac C ) )
90 39 nn0cnd 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> B e. CC )
91 fallfacval 
 |-  ( ( B e. CC /\ C e. NN0 ) -> ( B FallFac C ) = prod_ k e. ( 0 ... ( C - 1 ) ) ( B - k ) )
92 90 29 91 syl2anc 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( B FallFac C ) = prod_ k e. ( 0 ... ( C - 1 ) ) ( B - k ) )
93 92 eqcomd 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> prod_ k e. ( 0 ... ( C - 1 ) ) ( B - k ) = ( B FallFac C ) )
94 85 89 93 3brtr3d 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( A FallFac C ) <_ ( B FallFac C ) )
95 fallfacval4 
 |-  ( C e. ( 0 ... A ) -> ( A FallFac C ) = ( ( ! ` A ) / ( ! ` ( A - C ) ) ) )
96 95 adantl 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( A FallFac C ) = ( ( ! ` A ) / ( ! ` ( A - C ) ) ) )
97 0zd 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> 0 e. ZZ )
98 29 nn0ge0d 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> 0 <_ C )
99 68 14 44 17 45 letrd 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> C <_ B )
100 97 42 11 98 99 elfzd 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> C e. ( 0 ... B ) )
101 fallfacval4 
 |-  ( C e. ( 0 ... B ) -> ( B FallFac C ) = ( ( ! ` B ) / ( ! ` ( B - C ) ) ) )
102 100 101 syl 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( B FallFac C ) = ( ( ! ` B ) / ( ! ` ( B - C ) ) ) )
103 94 96 102 3brtr3d 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( ( ! ` A ) / ( ! ` ( A - C ) ) ) <_ ( ( ! ` B ) / ( ! ` ( B - C ) ) ) )
104 38 58 59 103 lediv1dd 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( ( ( ! ` A ) / ( ! ` ( A - C ) ) ) / ( ! ` C ) ) <_ ( ( ( ! ` B ) / ( ! ` ( B - C ) ) ) / ( ! ` C ) ) )
105 40 nncnd 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( ! ` B ) e. CC )
106 55 nncnd 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( ! ` ( B - C ) ) e. CC )
107 105 106 31 57 33 divdiv1d 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( ( ( ! ` B ) / ( ! ` ( B - C ) ) ) / ( ! ` C ) ) = ( ( ! ` B ) / ( ( ! ` ( B - C ) ) x. ( ! ` C ) ) ) )
108 104 107 breqtrd 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( ( ( ! ` A ) / ( ! ` ( A - C ) ) ) / ( ! ` C ) ) <_ ( ( ! ` B ) / ( ( ! ` ( B - C ) ) x. ( ! ` C ) ) ) )
109 35 108 eqbrtrd 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( ( ! ` A ) / ( ( ! ` ( A - C ) ) x. ( ! ` C ) ) ) <_ ( ( ! ` B ) / ( ( ! ` ( B - C ) ) x. ( ! ` C ) ) ) )
110 2 nn0zd 
 |-  ( ph -> B e. ZZ )
111 110 adantr 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> B e. ZZ )
112 elfzle1 
 |-  ( C e. ( 0 ... A ) -> 0 <_ C )
113 112 adantl 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> 0 <_ C )
114 1 nn0red 
 |-  ( ph -> A e. RR )
115 114 adantr 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> A e. RR )
116 111 zred 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> B e. RR )
117 13 115 116 17 45 letrd 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> C <_ B )
118 97 111 11 113 117 elfzd 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> C e. ( 0 ... B ) )
119 bcval2 
 |-  ( C e. ( 0 ... B ) -> ( B _C C ) = ( ( ! ` B ) / ( ( ! ` ( B - C ) ) x. ( ! ` C ) ) ) )
120 118 119 syl 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( B _C C ) = ( ( ! ` B ) / ( ( ! ` ( B - C ) ) x. ( ! ` C ) ) ) )
121 120 eqcomd 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( ( ! ` B ) / ( ( ! ` ( B - C ) ) x. ( ! ` C ) ) ) = ( B _C C ) )
122 109 121 breqtrd 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( ( ! ` A ) / ( ( ! ` ( A - C ) ) x. ( ! ` C ) ) ) <_ ( B _C C ) )
123 6 122 eqbrtrd 
 |-  ( ( ph /\ C e. ( 0 ... A ) ) -> ( A _C C ) <_ ( B _C C ) )
124 1 adantr 
 |-  ( ( ph /\ -. C e. ( 0 ... A ) ) -> A e. NN0 )
125 3 adantr 
 |-  ( ( ph /\ -. C e. ( 0 ... A ) ) -> C e. ZZ )
126 simpr 
 |-  ( ( ph /\ -. C e. ( 0 ... A ) ) -> -. C e. ( 0 ... A ) )
127 bcval3 
 |-  ( ( A e. NN0 /\ C e. ZZ /\ -. C e. ( 0 ... A ) ) -> ( A _C C ) = 0 )
128 124 125 126 127 syl3anc 
 |-  ( ( ph /\ -. C e. ( 0 ... A ) ) -> ( A _C C ) = 0 )
129 bccl2 
 |-  ( C e. ( 0 ... B ) -> ( B _C C ) e. NN )
130 129 adantl 
 |-  ( ( ( ph /\ -. C e. ( 0 ... A ) ) /\ C e. ( 0 ... B ) ) -> ( B _C C ) e. NN )
131 130 nnnn0d 
 |-  ( ( ( ph /\ -. C e. ( 0 ... A ) ) /\ C e. ( 0 ... B ) ) -> ( B _C C ) e. NN0 )
132 131 nn0ge0d 
 |-  ( ( ( ph /\ -. C e. ( 0 ... A ) ) /\ C e. ( 0 ... B ) ) -> 0 <_ ( B _C C ) )
133 0le0 
 |-  0 <_ 0
134 133 a1i 
 |-  ( ( ( ph /\ -. C e. ( 0 ... A ) ) /\ -. C e. ( 0 ... B ) ) -> 0 <_ 0 )
135 2 ad2antrr 
 |-  ( ( ( ph /\ -. C e. ( 0 ... A ) ) /\ -. C e. ( 0 ... B ) ) -> B e. NN0 )
136 125 adantr 
 |-  ( ( ( ph /\ -. C e. ( 0 ... A ) ) /\ -. C e. ( 0 ... B ) ) -> C e. ZZ )
137 simpr 
 |-  ( ( ( ph /\ -. C e. ( 0 ... A ) ) /\ -. C e. ( 0 ... B ) ) -> -. C e. ( 0 ... B ) )
138 bcval3 
 |-  ( ( B e. NN0 /\ C e. ZZ /\ -. C e. ( 0 ... B ) ) -> ( B _C C ) = 0 )
139 135 136 137 138 syl3anc 
 |-  ( ( ( ph /\ -. C e. ( 0 ... A ) ) /\ -. C e. ( 0 ... B ) ) -> ( B _C C ) = 0 )
140 139 eqcomd 
 |-  ( ( ( ph /\ -. C e. ( 0 ... A ) ) /\ -. C e. ( 0 ... B ) ) -> 0 = ( B _C C ) )
141 134 140 breqtrd 
 |-  ( ( ( ph /\ -. C e. ( 0 ... A ) ) /\ -. C e. ( 0 ... B ) ) -> 0 <_ ( B _C C ) )
142 132 141 pm2.61dan 
 |-  ( ( ph /\ -. C e. ( 0 ... A ) ) -> 0 <_ ( B _C C ) )
143 128 142 eqbrtrd 
 |-  ( ( ph /\ -. C e. ( 0 ... A ) ) -> ( A _C C ) <_ ( B _C C ) )
144 123 143 pm2.61dan 
 |-  ( ph -> ( A _C C ) <_ ( B _C C ) )