This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bcval4

Description: Value of the binomial coefficient, N choose K , outside of its standard domain. Remark in Gleason p. 295. (Contributed by NM, 14-Jul-2005) (Revised by Mario Carneiro, 7-Nov-2013)

Ref Expression
Assertion bcval4 
|- ( ( N e. NN0 /\ K e. ZZ /\ ( K < 0 \/ N < K ) ) -> ( N _C K ) = 0 )

Proof

Step Hyp Ref Expression
1 elfzle1 
 |-  ( K e. ( 0 ... N ) -> 0 <_ K )
2 0re 
 |-  0 e. RR
3 elfzelz 
 |-  ( K e. ( 0 ... N ) -> K e. ZZ )
4 3 zred 
 |-  ( K e. ( 0 ... N ) -> K e. RR )
5 lenlt 
 |-  ( ( 0 e. RR /\ K e. RR ) -> ( 0 <_ K <-> -. K < 0 ) )
6 2 4 5 sylancr 
 |-  ( K e. ( 0 ... N ) -> ( 0 <_ K <-> -. K < 0 ) )
7 1 6 mpbid 
 |-  ( K e. ( 0 ... N ) -> -. K < 0 )
8 7 adantl 
 |-  ( ( N e. NN0 /\ K e. ( 0 ... N ) ) -> -. K < 0 )
9 elfzle2 
 |-  ( K e. ( 0 ... N ) -> K <_ N )
10 9 adantl 
 |-  ( ( N e. NN0 /\ K e. ( 0 ... N ) ) -> K <_ N )
11 nn0re 
 |-  ( N e. NN0 -> N e. RR )
12 lenlt 
 |-  ( ( K e. RR /\ N e. RR ) -> ( K <_ N <-> -. N < K ) )
13 4 11 12 syl2anr 
 |-  ( ( N e. NN0 /\ K e. ( 0 ... N ) ) -> ( K <_ N <-> -. N < K ) )
14 10 13 mpbid 
 |-  ( ( N e. NN0 /\ K e. ( 0 ... N ) ) -> -. N < K )
15 ioran 
 |-  ( -. ( K < 0 \/ N < K ) <-> ( -. K < 0 /\ -. N < K ) )
16 8 14 15 sylanbrc 
 |-  ( ( N e. NN0 /\ K e. ( 0 ... N ) ) -> -. ( K < 0 \/ N < K ) )
17 16 ex 
 |-  ( N e. NN0 -> ( K e. ( 0 ... N ) -> -. ( K < 0 \/ N < K ) ) )
18 17 adantr 
 |-  ( ( N e. NN0 /\ K e. ZZ ) -> ( K e. ( 0 ... N ) -> -. ( K < 0 \/ N < K ) ) )
19 18 con2d 
 |-  ( ( N e. NN0 /\ K e. ZZ ) -> ( ( K < 0 \/ N < K ) -> -. K e. ( 0 ... N ) ) )
20 19 3impia 
 |-  ( ( N e. NN0 /\ K e. ZZ /\ ( K < 0 \/ N < K ) ) -> -. K e. ( 0 ... N ) )
21 bcval3 
 |-  ( ( N e. NN0 /\ K e. ZZ /\ -. K e. ( 0 ... N ) ) -> ( N _C K ) = 0 )
22 20 21 syld3an3 
 |-  ( ( N e. NN0 /\ K e. ZZ /\ ( K < 0 \/ N < K ) ) -> ( N _C K ) = 0 )