HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem bcpasc2t 6968
Description: Pascal's rule for the binomial coefficient. Equation 2 of [Gleason] p. 295.
Assertion
Ref Expression
bcpasc2t |- ((N e. NN /\ K e. NN /\ K <_ N) -> ((N C. K) + (N C. (K - 1))) = ((N + 1) C. K))
Proof of Theorem bcpasc2t
StepHypRef Expression
1 opreq1 3974 . . . 4 |- (N = if((N e. NN /\ K e. NN /\ K <_ N), N, 1) -> (N C. K) = (if((N e. NN /\ K e. NN /\ K <_ N), N, 1) C. K))
2 opreq1 3974 . . . 4 |- (N = if((N e. NN /\ K e. NN /\ K <_ N), N, 1) -> (N C. (K - 1)) = (if((N e. NN /\ K e. NN /\ K <_ N), N, 1) C. (K - 1)))
31, 2opreq12d 3984 . . 3 |- (N = if((N e. NN /\ K e. NN /\ K <_ N), N, 1) -> ((N C. K) + (N C. (K - 1))) = ((if((N e. NN /\ K e. NN /\ K <_ N), N, 1) C. K) + (if((N e. NN /\ K e. NN /\ K <_ N), N, 1) C. (K - 1))))
4 opreq1 3974 . . . 4 |- (N = if((N e. NN /\ K e. NN /\ K <_ N), N, 1) -> (N + 1) = (if((N e. NN /\ K e. NN /\ K <_ N), N, 1) + 1))
54opreq1d 3981 . . 3 |- (N = if((N e. NN /\ K e. NN /\ K <_ N), N, 1) -> ((N + 1) C. K) = ((if((N e. NN /\ K e. NN /\ K <_ N), N, 1) + 1) C. K))
63, 5eqeq12d 1492 . 2 |- (N = if((N e. NN /\ K e. NN /\ K <_ N), N, 1) -> (((N C. K) + (N C. (K - 1))) = ((N + 1) C. K) <-> ((if((N e. NN /\ K e. NN /\ K <_ N), N, 1) C. K) + (if((N e. NN /\ K e. NN /\ K <_ N), N, 1) C. (K - 1))) = ((if((N e. NN /\ K e. NN /\ K <_ N), N, 1) + 1) C. K)))
7 opreq2 3975 . . . 4 |- (K = if((N e. NN /\ K e. NN /\ K <_ N), K, 1) -> (if((N e. NN /\ K e. NN /\ K <_ N), N, 1) C. K) = (if((N e. NN /\ K e. NN /\ K <_ N), N, 1) C. if((N e. NN /\ K e. NN /\ K <_ N), K, 1)))
8 opreq1 3974 . . . . 5 |- (K = if((N e. NN /\ K e. NN /\ K <_ N), K, 1) -> (K - 1) = (if((N e. NN /\ K e. NN /\ K <_ N), K, 1) - 1))
98opreq2d 3982 . . . 4 |- (K = if((N e. NN /\ K e. NN /\ K <_ N), K, 1) -> (if((N e. NN /\ K e. NN /\ K <_ N), N, 1) C. (K - 1)) = (if((N e. NN /\ K e. NN /\ K <_ N), N, 1) C. (if((N e. NN /\ K e. NN /\ K <_ N), K, 1) - 1)))
107, 9opreq12d 3984 . . 3 |- (K = if((N e. NN /\ K e. NN /\ K <_ N), K, 1) -> ((if((N e. NN /\ K e. NN /\ K <_ N), N, 1) C. K) + (if((N e. NN /\ K e. NN /\ K <_ N), N, 1) C. (K - 1))) = ((if((N e. NN /\ K e. NN /\ K <_ N), N, 1) C. if((N e. NN /\ K e. NN /\ K <_ N), K, 1)) + (if((N e. NN /\ K e. NN /\ K <_ N), N, 1) C. (if((N e. NN /\ K e. NN /\ K <_ N), K, 1) - 1))))
11 opreq2 3975 . . 3 |- (K = if((N e. NN /\ K e. NN /\ K <_ N), K, 1) -> ((if((N e. NN /\ K e. NN /\ K <_ N), N, 1) + 1) C. K) = ((if((N e. NN /\ K e. NN /\ K <_ N), N, 1) + 1) C. if((N e. NN /\ K e. NN /\ K <_ N), K, 1)))
1210, 11eqeq12d 1492 . 2 |- (K = if((N e. NN /\ K e. NN /\ K <_ N), K, 1) -> (((if((N e. NN /\ K e. NN /\ K <_ N), N, 1) C. K) + (if((N e. NN /\ K e. NN /\ K <_ N), N, 1) C. (K - 1))) = ((if((N e. NN /\ K e. NN /\ K <_ N), N, 1) + 1) C. K) <-> ((if((N e. NN /\ K e. NN /\ K <_ N), N, 1) C. if((N e. NN /\ K e. NN /\ K <_ N), K, 1)) + (if((N e. NN /\ K e. NN /\ K <_ N), N, 1) C. (if((N e. NN /\ K e. NN /\ K <_ N), K, 1) - 1))) = ((if((N e. NN /\ K e. NN /\ K <_ N), N, 1) + 1) C. if((N e. NN /\ K e. NN /\ K <_ N), K, 1))))
13 eleq1 1537 . . . . . 6 |- (N = if((N e. NN /\ K e. NN /\ K <_ N), N, 1) -> (N e. NN <-> if((N e. NN /\ K e. NN /\ K <_ N), N, 1) e. NN))
14 breq2 2628 . . . . . 6 |- (N = if((N e. NN /\ K e. NN /\ K <_ N), N, 1) -> (K <_ N <-> K <_ if((N e. NN /\ K e. NN /\ K <_ N), N, 1)))
1513, 143anbi13d 897 . . . . 5 |- (N = if((N e. NN /\ K e. NN /\ K <_ N), N, 1) -> ((N e. NN /\ K e. NN /\ K <_ N) <-> (if((N e. NN /\ K e. NN /\ K <_ N), N, 1) e. NN /\ K e. NN /\ K <_ if((N e. NN /\ K e. NN /\ K <_ N), N, 1))))
16 eleq1 1537 . . . . . 6 |- (K = if((N e. NN /\ K e. NN /\ K <_ N), K, 1) -> (K e. NN <-> if((N e. NN /\ K e. NN /\ K <_ N), K, 1) e. NN))
17 breq1 2627 . . . . . 6 |- (K = if((N e. NN /\ K e. NN /\ K <_ N), K, 1) -> (K <_ if((N e. NN /\ K e. NN /\ K <_ N), N, 1) <-> if((N e. NN /\ K e. NN /\ K <_ N), K, 1) <_ if((N e. NN /\ K e. NN /\ K <_ N), N, 1)))
1816, 173anbi23d 898 . . . . 5 |- (K = if((N e. NN /\ K e. NN /\ K <_ N), K, 1) -> ((if((N e. NN /\ K e. NN /\ K <_ N), N, 1) e. NN /\ K e. NN /\ K <_ if((N e. NN /\ K e. NN /\ K <_ N), N, 1)) <-> (if((N e. NN /\ K e. NN /\ K <_ N), N, 1) e. NN /\ if((N e. NN /\ K e. NN /\ K <_ N), K, 1) e. NN /\ if((N e. NN /\ K e. NN /\ K <_ N), K, 1) <_ if((N e. NN /\ K e. NN /\ K <_ N), N, 1))))
19 eleq1 1537 . . . . . 6 |- (1 = if((N e. NN /\ K e. NN /\ K <_ N), N, 1) -> (1 e. NN <-> if((N e. NN /\ K e. NN /\ K <_ N), N, 1) e. NN))
20 breq2 2628 . . . . . 6 |- (1 = if((N e. NN /\ K e. NN /\ K <_ N), N, 1) -> (1 <_ 1 <-> 1 <_ if((N e. NN /\ K e. NN /\ K <_ N), N, 1)))
2119, 203anbi13d 897 . . . . 5 |- (1 = if((N e. NN /\ K e. NN /\ K <_ N), N, 1) -> ((1 e. NN /\ 1 e. NN /\ 1 <_ 1) <-> (if((N e. NN /\ K e. NN /\ K <_ N), N, 1) e. NN /\ 1 e. NN /\ 1 <_ if((N e. NN /\ K e. NN /\ K <_ N), N, 1))))
22 eleq1 1537 . . . . . 6 |- (1 = if((N e. NN /\ K e. NN /\ K <_ N), K, 1) -> (1 e. NN <-> if((N e. NN /\ K e. NN /\ K <_ N), K, 1) e. NN))
23 breq1 2627 . . . . . 6 |- (1 = if((N e. NN /\ K e. NN /\ K <_ N), K, 1) -> (1 <_ if((N e. NN /\ K e. NN /\ K <_ N), N, 1) <-> if((N e. NN /\ K e. NN /\ K <_ N), K, 1) <_ if((N e. NN /\ K e. NN /\ K <_ N), N, 1)))
2422, 233anbi23d