Nearby theorems
|
|
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > ILE Home > Th. List > bcmono | Unicode version | ||
| Description: The binomial coefficient is monotone in its second argument, up to the midway point. (Contributed by Mario Carneiro, 5-Mar-2014.) |
| Ref | Expression |
|---|---|
| bcmono |
     ![/\](wedge.gif "/\"){kind=small} 
         |
are mutually distinct and distinct from all other
variables.| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | simpl2 1032 |
. . 3
 | |
| 2 | simpl1 1031 |
. . 3
| |
| 3 | eluzel2 9943 |
. . . . . 6
 | |
| 4 | 3 | 3ad2ant2 1050 |
. . . . 5
|
| 5 | 4 | anim1i 340 |
. . . 4
|
| 6 | elnn0z 9669 |
. . . 4
 | |
| 7 | 5, 6 | sylibr 134 |
. . 3
|
| 8 | simpl3 1033 |
. . 3
| |
| 9 | breq1 4134 |
. . . . . . 7
| |
| 10 | oveq2 6096 |
. . . . . . . 8
| |
| 11 | 10 | breq2d 4143 |
. . . . . . 7
|
| 12 | 9, 11 | imbi12d 234 |
. . . . . 6
|
| 13 | 12 | imbi2d 230 |
. . . . 5
|
| 14 | breq1 4134 |
. . . . . . 7
| |
| 15 | oveq2 6096 |
. . . . . . . 8
| |
| 16 | 15 | breq2d 4143 |
. . . . . . 7
|
| 17 | 14, 16 | imbi12d 234 |
. . . . . 6
|
| 18 | 17 | imbi2d 230 |
. . . . 5
|
| 19 | breq1 4134 |
. . . . . . 7
 
| |
| 20 | oveq2 6096 |
. . . . . . . 8
| |
| 21 | 20 | breq2d 4143 |
. . . . . . 7
|
| 22 | 19, 21 | imbi12d 234 |
. . . . . 6
|
| 23 | 22 | imbi2d 230 |
. . . . 5
|
| 24 | breq1 4134 |
. . . . . . 7
| |
| 25 | oveq2 6096 |
. . . . . . . 8
| |
| 26 | 25 | breq2d 4143 |
. . . . . . 7
|
| 27 | 24, 26 | imbi12d 234 |
. . . . . 6
|
| 28 | 27 | imbi2d 230 |
. . . . 5
|
| 29 | bccl 11228 |
. . . . . . . . . 10
| |
| 30 | 29 | nn0red 9633 |
. . . . . . . . 9
 |
| 31 | 30 | leidd 8850 |
. . . . . . . 8
|
| 32 | 31 | a1d 22 |
. . . . . . 7
|
| 33 | 32 | expcom 116 |
. . . . . 6
|
| 34 | 33 | adantrd 279 |
. . . . 5
|
| 35 | eluzelz 9948 |
. . . . . . . . . . . . 13
| |
| 36 | 35 | 3ad2ant1 1049 |
. . . . . . . . . . . 12
|
| 37 | 36 | zred 9780 |
. . . . . . . . . . 11
|
| 38 | 37 | lep1d 9270 |
. . . . . . . . . 10
|
| 39 | peano2re 8470 |
. . . . . . . . . . . 12
| |
| 40 | 37, 39 | syl 14 |
. . . . . . . . . . 11
|
| 41 | nn0re 9584 |
. . . . . . . . . . . . 13
| |
| 42 | 41 | 3ad2ant2 1050 |
. . . . . . . . . . . 12
|
| 43 | 42 | rehalfcld 9564 |
. . . . . . . . . . 11
|
| 44 | letr 8415 |
. . . . . . . . . . 11
| |
| 45 | 37, 40, 43, 44 | syl3anc 1278 |
. . . . . . . . . 10
|
| 46 | 38, 45 | mpand 433 |
. . . . . . . . 9
|
| 47 | 46 | imim1d 75 |
. . . . . . . 8
|
| 48 | eluznn0 10016 |
. . . . . . . . . . . . 13
| |
| 49 | 41 | 3ad2ant2 1050 |
. . . . . . . . . . . . . . . . 17
|
| 50 | nn0re 9584 |
. . . . . . . . . . . . . . . . . 18
| |
| 51 | 50 | 3ad2ant1 1049 |
. . . . . . . . . . . . . . . . 17
|
| 52 | nn0p1nn 9614 |
. . . . . . . . . . . . . . . . . . . 20
 | |
| 53 | 52 | 3ad2ant1 1049 |
. . . . . . . . . . . . . . . . . . 19
|
| 54 | 53 | nnnn0d 9632 |
. . . . . . . . . . . . . . . . . 18
|
| 55 | 54 | nn0red 9633 |
. . . . . . . . . . . . . . . . 17
|
| 56 | 53 | nncnd 9328 |
. . . . . . . . . . . . . . . . . . 19
 |
| 57 | 56 | 2timesd 9560 |
. . . . . . . . . . . . . . . . . 18
 |
| 58 | simp3 1030 |
. . . . . . . . . . . . . . . . . . 19
| |
| 59 | 2re 9384 |
. . . . . . . . . . . . . . . . . . . . . 22
| |
| 60 | 2pos 9405 |
. . . . . . . . . . . . . . . . . . . . . 22
 | |
| 61 | 59, 60 | pm3.2i 272 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 62 | 61 | a1i 9 |
. . . . . . . . . . . . . . . . . . . 20
|
| 63 | lemuldiv2 9221 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 64 | 55, 49, 62, 63 | syl3anc 1278 |
. . . . . . . . . . . . . . . . . . 19
|
| 65 | 58, 64 | mpbird 167 |
. . . . . . . . . . . . . . . . . 18
|
| 66 | 57, 65 | eqbrtrrd 4155 |
. . . . . . . . . . . . . . . . 17
|
| 67 | 51 | lep1d 9270 |
. . . . . . . . . . . . . . . . 17
|
| 68 | 49, 51, 55, 55, 66, 67 | lesub3d 8899 |
. . . . . . . . . . . . . . . 16
 |
| 69 | nnre 9321 |
. . . . . . . . . . . . . . . . . . 19
| |
| 70 | nngt0 9339 |
. . . . . . . . . . . . . . . . . . 19
| |
| 71 | 69, 70 | jca 306 |
. . . . . . . . . . . . . . . . . 18
|
| 72 | 53, 71 | syl 14 |
. . . . . . . . . . . . . . . . 17
|
| 73 | nn0z 9676 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 74 | 73 | 3ad2ant2 1050 |
. . . . . . . . . . . . . . . . . . . 20
|
| 75 | nn0z 9676 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 76 | 75 | 3ad2ant1 1049 |
. . . . . . . . . . . . . . . . . . . 20
|
| 77 | 74, 76 | zsubcld 9785 |
. . . . . . . . . . . . . . . . . . 19
|
| 78 | 49 | rehalfcld 9564 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 79 | 49, 59 | jctir 313 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 80 | nn0ge0 9600 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
| |
| 81 | 80 | 3ad2ant2 1050 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 82 | 1le2 9525 |
. . . . . . . . . . . . . . . . . . . . . . . 24
| |
| 83 | 81, 82 | jctir 313 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 84 | lemulge12 9206 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 85 | 79, 83, 84 | syl2anc 415 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 86 | ledivmul 9216 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 87 | 49, 49, 62, 86 | syl3anc 1278 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 88 | 85, 87 | mpbird 167 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 89 | 55, 78, 49, 58, 88 | letrd 8458 |
. . . . . . . . . . . . . . . . . . . 20
|
| 90 | 1red 8348 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 91 | 51, 90, 49 | leaddsub2d 8883 |
. . . . . . . . . . . . . . . . . . . 20
|
| 92 | 89, 91 | mpbid 147 |
. . . . . . . . . . . . . . . . . . 19
|
| 93 | elnnz1 9679 |
. . . . . . . . . . . . . . . . . . 19
| |
| 94 | 77, 92, 93 | sylanbrc 421 |
. . . . . . . . . . . . . . . . . 18
|
| 95 | nnre 9321 |
. . . . . . . . . . . . . . . . . . 19
| |
| 96 | nngt0 9339 |
. . . . . . . . . . . . . . . . . . 19
| |
| 97 | 95, 96 | jca 306 |
. . . . . . . . . . . . . . . . . 18
|
| 98 | 94, 97 | syl 14 |
. . . . . . . . . . . . . . . . 17
|
| 99 | faccl 11196 |
. . . . . . . . . . . . . . . . . . . 20
 | |
| 100 | 99 | 3ad2ant2 1050 |
. . . . . . . . . . . . . . . . . . 19
|
| 101 | nnm1nn0 9616 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 102 | faccl 11196 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 103 | 94, 101, 102 | 3syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
| 104 | faccl 11196 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 105 | 104 | 3ad2ant1 1049 |
. . . . . . . . . . . . . . . . . . . 20
|
| 106 | 103, 105 | nnmulcld 9363 |
. . . . . . . . . . . . . . . . . . 19
|
| 107 | nnrp 10082 |
. . . . . . . . . . . . . . . . . . . 20
 | |
| 108 | nnrp 10082 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 109 | rpdivcl 10098 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 110 | 107, 108, 109 | syl2an 289 |
. . . . . . . . . . . . . . . . . . 19
|
| 111 | 100, 106, 110 | syl2anc 415 |
. . . . . . . . . . . . . . . . . 18
|
| 112 | 111 | rpregt0d 10122 |
. . . . . . . . . . . . . . . . 17
|
| 113 | lediv2 9230 |
. . . . . . . . . . . . . . . . 17
| |
| 114 | 72, 98, 112, 113 | syl3anc 1278 |
. . . . . . . . . . . . . . . 16
|
| 115 | 68, 114 | mpbid 147 |
. . . . . . . . . . . . . . 15
|
| 116 | facnn2 11195 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 117 | 94, 116 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
|
| 118 | 117 | oveq1d 6103 |
. . . . . . . . . . . . . . . . . 18
|
| 119 | 103 | nncnd 9328 |
. . . . . . . . . . . . . . . . . . 19
|
| 120 | 105 | nncnd 9328 |
. . . . . . . . . . . . . . . . . . 19
|
| 121 | 77 | zcnd 9781 |
. . . . . . . . . . . . . . . . . . 19
|
| 122 | 119, 120, 121 | mul32d 8487 |
. . . . . . . . . . . . . . . . . 18
|
| 123 | 118, 122 | eqtr4d 2274 |
. . . . . . . . . . . . . . . . 17
|
| 124 | 123 | oveq2d 6104 |
. . . . . . . . . . . . . . . 16
|
| 125 | 0zd 9668 |
. . . . . . . . . . . . . . . . . 18
| |
| 126 | nn0ge0 9600 |
. . . . . . . . . . . . . . . . . . 19
| |
| 127 | 126 | 3ad2ant1 1049 |
. . . . . . . . . . . . . . . . . 18
|
| 128 | 51, 55, 49, 67, 89 | letrd 8458 |
. . . . . . . . . . . . . . . . . 18
|
| 129 | 125, 74, 76, 127, 128 | elfzd 10437 |
. . . . . . . . . . . . . . . . 17
 |
| 130 | bcval2 11211 |
. . . . . . . . . . . . . . . . 17
| |
| 131 | 129, 130 | syl 14 |
. . . . . . . . . . . . . . . 16
|
| 132 | 100 | nncnd 9328 |
. . . . . . . . . . . . . . . . 17
|
| 133 | 106 | nncnd 9328 |
. . . . . . . . . . . . . . . . 17
|
| 134 | 106 | nnap0d 9360 |
. . . . . . . . . . . . . . . . 17
# |
| 135 | 94 | nnap0d 9360 |
. . . . . . . . . . . . . . . . 17
# |
| 136 | 132, 133, 121, 134, 135 | divdivap1d 9161 |
. . . . . . . . . . . . . . . 16
|
| 137 | 124, 131, 136 | 3eqtr4d 2281 |
. . . . . . . . . . . . . . 15
|
| 138 | nn0cn 9585 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 139 | 138 | 3ad2ant2 1050 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 140 | nn0cn 9585 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 141 | 140 | 3ad2ant1 1049 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 142 | 1cnd 8349 |
. . . . . . . . . . . . . . . . . . . . . 22
| |
| 143 | 139, 141, 142 | subsub4d 8676 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 144 | 143 | eqcomd 2244 |
. . . . . . . . . . . . . . . . . . . 20
|
| 145 | 144 | fveq2d 5702 |
. . . . . . . . . . . . . . . . . . 19
|
| 146 | facp1 11191 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 147 | 146 | 3ad2ant1 1049 |
. . . . . . . . . . . . . . . . . . 19
|
| 148 | 145, 147 | oveq12d 6106 |
. . . . . . . . . . . . . . . . . 18
|
| 149 | 119, 120, 56 | mulassd 8356 |
. . . . . . . . . . . . . . . . . 18
|
| 150 | 148, 149 | eqtr4d 2274 |
. . . . . . . . . . . . . . . . 17
|
| 151 | 150 | oveq2d 6104 |
. . . . . . . . . . . . . . . 16
|
| 152 | 53 | nnzd 9779 |
. . . . . . . . . . . . . . . . . 18
|
| 153 | 54 | nn0ge0d 9635 |
. . . . . . . . . . . . . . . . . 18
|
| 154 | 125, 74, 152, 153, 89 | elfzd 10437 |
. . . . . . . . . . . . . . . . 17
|
| 155 | bcval2 11211 |
. . . . . . . . . . . . . . . . 17
| |
| 156 | 154, 155 | syl 14 |
. . . . . . . . . . . . . . . 16
|
| 157 | 53 | nnap0d 9360 |
. . . . . . . . . . . . . . . . 17
# |
| 158 | 132, 133, 56, 134, 157 | divdivap1d 9161 |
. . . . . . . . . . . . . . . 16
|
| 159 | 151, 156, 158 | 3eqtr4d 2281 |
. . . . . . . . . . . . . . 15
|
| 160 | 115, 137, 159 | 3brtr4d 4163 |
. . . . . . . . . . . . . 14
|
| 161 | 160 | 3exp 1233 |
. . . . . . . . . . . . 13
|
| 162 | 48, 161 | syl 14 |
. . . . . . . . . . . 12
|
| 163 | 162 | 3impia 1231 |
. . . . . . . . . . 11
|
| 164 | 163 | 3coml 1241 |
. . . . . . . . . 10
|
| 165 | simp2 1029 |
. . . . . . . . . . . . . 14
| |
| 166 | nn0z 9676 |
. . . . . . . . . . . . . . 15
| |
| 167 | 166 | 3ad2ant3 1051 |
. . . . . . . . . . . . . 14
|
| 168 | 165, 167, 29 | syl2anc 415 |
. . . . . . . . . . . . 13
|
| 169 | 168 | nn0red 9633 |
. . . . . . . . . . . 12
|
| 170 | bccl 11228 |
. . . . . . . . . . . . . 14
| |
| 171 | 165, 36, 170 | syl2anc 415 |
. . . . . . . . . . . . 13
|
| 172 | 171 | nn0red 9633 |
. . . . . . . . . . . 12
|
| 173 | 36 | peano2zd 9783 |
. . . . . . . . . . . . . 14
|
| 174 | bccl 11228 |
. . . . . . . . . . . . . 14
| |
| 175 | 165, 173, 174 | syl2anc 415 |
. . . . . . . . . . . . 13
|
| 176 | 175 | nn0red 9633 |
. . . . . . . . . . . 12
|
| 177 | letr 8415 |
. . . . . . . . . . . 12
| |
| 178 | 169, 172, 176, 177 | syl3anc 1278 |
. . . . . . . . . . 11
|
| 179 | 178 | expcomd 1491 |
. . . . . . . . . 10
|
| 180 | 164, 179 | syld 45 |
. . . . . . . . 9
|
| 181 | 180 | a2d 26 |
. . . . . . . 8
|
| 182 | 47, 181 | syld 45 |
. . . . . . 7
|
| 183 | 182 | 3expib 1237 |
. . . . . 6
|
| 184 | 183 | a2d 26 |
. . . . 5
|
| 185 | 13, 18, 23, 28, 34, 184 | uzind4 10005 |
. . . 4
|
| 186 | 185 | 3imp 1224 |
. . 3
|
| 187 | 1, 2, 7, 8, 186 | syl121anc 1283 |
. 2
|
| 188 | simpl1 1031 |
. . . 4
| |
| 189 | 4 | adantr 276 |
. . . 4
|
| 190 | animorrl 838 |
. . . 4
 | |
| 191 | bcval4 11213 |
. . . 4
| |
| 192 | 188, 189, 190, 191 | syl3anc 1278 |
. . 3
|
| 193 | simpl2 1032 |
. . . . . 6
| |
| 194 | eluzelz 9948 |
. . . . . 6
| |
| 195 | 193, 194 | syl 14 |
. . . . 5
|
| 196 | bccl 11228 |
. . . . 5
| |
| 197 | 188, 195, 196 | syl2anc 415 |
. . . 4
|
| 198 | 197 | nn0ge0d 9635 |
. . 3
|
| 199 | 192, 198 | eqbrtrd 4153 |
. 2
|
| 200 | 0z 9667 |
. . 3
| |
| 201 | zlelttric 9701 |
. . 3
| |
| 202 | 200, 4, 201 | sylancr 418 |
. 2
|
| 203 | 187, 199, 202 | mpjaodan 810 |
1
|
| Colors of variables: wff set class |
| This proof depends on syntax axioms:
wi 4
wa 104
wb 105 wo 720 w3a 1009 wceq 1402 wcel 2209 class class class wbr 4131
cfv 5380
(class class class)co 6088 cc 8184 cr 8185 cc0 8186 c1 8187 caddc 8189 cmul 8191 clt 8367 cle 8368 cmin 8505 cdiv 9011 cn 9314 c2 9365 cn0 9575 cz 9656 cuz 9938 crp 10072 cfz 10429 cfa 11186 cbc 11208 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-coll 4248 ax-sep 4251 ax-nul 4261 ax-pow 4313 ax-pr 4348 ax-un 4580 ax-setind 4686 ax-iinf 4737 ax-cnex 8277 ax-resscn 8278 ax-1cn 8279 ax-1re 8280 ax-icn 8281 ax-addcl 8282 ax-addrcl 8283 ax-mulcl 8284 ax-mulrcl 8285 ax-addcom 8286 ax-mulcom 8287 ax-addass 8288 ax-mulass 8289 ax-distr 8290 ax-i2m1 8291 ax-0lt1 8292 ax-1rid 8293 ax-0id 8294 ax-rnegex 8295 ax-precex 8296 ax-cnre 8297 ax-pre-ltirr 8298 ax-pre-ltwlin 8299 ax-pre-lttrn 8300 ax-pre-apti 8301 ax-pre-ltadd 8302 ax-pre-mulgt0 8303 ax-pre-mulext 8304 |
| This proof depends on definitions: df-bi 117 df-dc 847 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-nel 2516 df-ral 2533 df-rex 2534 df-reu 2535 df-rmo 2536 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-if 3639 df-pw 3690 df-sn 3715 df-pr 3716 df-op 3718 df-uni 3936 df-int 3971 df-iun 4014 df-br 4132 df-opab 4194 df-mpt 4195 df-tr 4232 df-id 4440 df-po 4443 df-iso 4444 df-iord 4513 df-on 4515 df-ilim 4516 df-suc 4518 df-iom 4740 df-xp 4782 df-rel 4783 df-cnv 4784 df-co 4785 df-dm 4786 df-rn 4787 df-res 4788 df-ima 4789 df-iota 5340 df-fun 5382 df-fn 5383 df-f 5384 df-f1 5385 df-fo 5386 df-f1o 5387 df-fv 5388 df-riota 6041 df-ov 6091 df-oprab 6092 df-mpo 6093 df-1st 6378 df-2nd 6379 df-recs 6580 df-frec 6666 df-pnf 8369 df-mnf 8370 df-xr 8371 df-ltxr 8372 df-le 8373 df-sub 8507 df-neg 8508 df-reap 8912 df-ap 8919 df-div 9012 df-inn 9315 df-2 9373 df-n0 9576 df-z 9657 df-uz 9939 df-q 10037 df-rp 10073 df-fz 10430 df-seqfrec 10907 df-fac 11187 df-bc 11209 |
| This theorem is used by: bcmax 16317 |
| Copyright terms: Public domain | W3C validator |