Step | Hyp | Ref
| Expression |
1 | | elfzel1 13503 |
. . . . . 6
โข (๐พ โ (0...๐) โ 0 โ โค) |
2 | | elfzel2 13502 |
. . . . . 6
โข (๐พ โ (0...๐) โ ๐ โ โค) |
3 | | elfzelz 13504 |
. . . . . 6
โข (๐พ โ (0...๐) โ ๐พ โ โค) |
4 | | 1zzd 12594 |
. . . . . 6
โข (๐พ โ (0...๐) โ 1 โ โค) |
5 | | fzaddel 13538 |
. . . . . 6
โข (((0
โ โค โง ๐
โ โค) โง (๐พ
โ โค โง 1 โ โค)) โ (๐พ โ (0...๐) โ (๐พ + 1) โ ((0 + 1)...(๐ + 1)))) |
6 | 1, 2, 3, 4, 5 | syl22anc 836 |
. . . . 5
โข (๐พ โ (0...๐) โ (๐พ โ (0...๐) โ (๐พ + 1) โ ((0 + 1)...(๐ + 1)))) |
7 | 6 | ibi 267 |
. . . 4
โข (๐พ โ (0...๐) โ (๐พ + 1) โ ((0 + 1)...(๐ + 1))) |
8 | | 1e0p1 12720 |
. . . . 5
โข 1 = (0 +
1) |
9 | 8 | oveq1i 7414 |
. . . 4
โข
(1...(๐ + 1)) = ((0
+ 1)...(๐ +
1)) |
10 | 7, 9 | eleqtrrdi 2838 |
. . 3
โข (๐พ โ (0...๐) โ (๐พ + 1) โ (1...(๐ + 1))) |
11 | | bcm1k 14278 |
. . 3
โข ((๐พ + 1) โ (1...(๐ + 1)) โ ((๐ + 1)C(๐พ + 1)) = (((๐ + 1)C((๐พ + 1) โ 1)) ยท (((๐ + 1) โ ((๐พ + 1) โ 1)) / (๐พ + 1)))) |
12 | 10, 11 | syl 17 |
. 2
โข (๐พ โ (0...๐) โ ((๐ + 1)C(๐พ + 1)) = (((๐ + 1)C((๐พ + 1) โ 1)) ยท (((๐ + 1) โ ((๐พ + 1) โ 1)) / (๐พ + 1)))) |
13 | 3 | zcnd 12668 |
. . . . . . 7
โข (๐พ โ (0...๐) โ ๐พ โ โ) |
14 | | ax-1cn 11167 |
. . . . . . 7
โข 1 โ
โ |
15 | | pncan 11467 |
. . . . . . 7
โข ((๐พ โ โ โง 1 โ
โ) โ ((๐พ + 1)
โ 1) = ๐พ) |
16 | 13, 14, 15 | sylancl 585 |
. . . . . 6
โข (๐พ โ (0...๐) โ ((๐พ + 1) โ 1) = ๐พ) |
17 | 16 | oveq2d 7420 |
. . . . 5
โข (๐พ โ (0...๐) โ ((๐ + 1)C((๐พ + 1) โ 1)) = ((๐ + 1)C๐พ)) |
18 | | bcp1n 14279 |
. . . . 5
โข (๐พ โ (0...๐) โ ((๐ + 1)C๐พ) = ((๐C๐พ) ยท ((๐ + 1) / ((๐ + 1) โ ๐พ)))) |
19 | 17, 18 | eqtrd 2766 |
. . . 4
โข (๐พ โ (0...๐) โ ((๐ + 1)C((๐พ + 1) โ 1)) = ((๐C๐พ) ยท ((๐ + 1) / ((๐ + 1) โ ๐พ)))) |
20 | 16 | oveq2d 7420 |
. . . . 5
โข (๐พ โ (0...๐) โ ((๐ + 1) โ ((๐พ + 1) โ 1)) = ((๐ + 1) โ ๐พ)) |
21 | 20 | oveq1d 7419 |
. . . 4
โข (๐พ โ (0...๐) โ (((๐ + 1) โ ((๐พ + 1) โ 1)) / (๐พ + 1)) = (((๐ + 1) โ ๐พ) / (๐พ + 1))) |
22 | 19, 21 | oveq12d 7422 |
. . 3
โข (๐พ โ (0...๐) โ (((๐ + 1)C((๐พ + 1) โ 1)) ยท (((๐ + 1) โ ((๐พ + 1) โ 1)) / (๐พ + 1))) = (((๐C๐พ) ยท ((๐ + 1) / ((๐ + 1) โ ๐พ))) ยท (((๐ + 1) โ ๐พ) / (๐พ + 1)))) |
23 | | bcrpcl 14271 |
. . . . . 6
โข (๐พ โ (0...๐) โ (๐C๐พ) โ
โ+) |
24 | 23 | rpcnd 13021 |
. . . . 5
โข (๐พ โ (0...๐) โ (๐C๐พ) โ โ) |
25 | 2 | peano2zd 12670 |
. . . . . . . 8
โข (๐พ โ (0...๐) โ (๐ + 1) โ โค) |
26 | 25 | zred 12667 |
. . . . . . 7
โข (๐พ โ (0...๐) โ (๐ + 1) โ โ) |
27 | 3 | zred 12667 |
. . . . . . . . 9
โข (๐พ โ (0...๐) โ ๐พ โ โ) |
28 | 2 | zred 12667 |
. . . . . . . . 9
โข (๐พ โ (0...๐) โ ๐ โ โ) |
29 | | elfzle2 13508 |
. . . . . . . . 9
โข (๐พ โ (0...๐) โ ๐พ โค ๐) |
30 | 28 | ltp1d 12145 |
. . . . . . . . 9
โข (๐พ โ (0...๐) โ ๐ < (๐ + 1)) |
31 | 27, 28, 26, 29, 30 | lelttrd 11373 |
. . . . . . . 8
โข (๐พ โ (0...๐) โ ๐พ < (๐ + 1)) |
32 | | znnsub 12609 |
. . . . . . . . 9
โข ((๐พ โ โค โง (๐ + 1) โ โค) โ
(๐พ < (๐ + 1) โ ((๐ + 1) โ ๐พ) โ โ)) |
33 | 3, 25, 32 | syl2anc 583 |
. . . . . . . 8
โข (๐พ โ (0...๐) โ (๐พ < (๐ + 1) โ ((๐ + 1) โ ๐พ) โ โ)) |
34 | 31, 33 | mpbid 231 |
. . . . . . 7
โข (๐พ โ (0...๐) โ ((๐ + 1) โ ๐พ) โ โ) |
35 | 26, 34 | nndivred 12267 |
. . . . . 6
โข (๐พ โ (0...๐) โ ((๐ + 1) / ((๐ + 1) โ ๐พ)) โ โ) |
36 | 35 | recnd 11243 |
. . . . 5
โข (๐พ โ (0...๐) โ ((๐ + 1) / ((๐ + 1) โ ๐พ)) โ โ) |
37 | 34 | nnred 12228 |
. . . . . . 7
โข (๐พ โ (0...๐) โ ((๐ + 1) โ ๐พ) โ โ) |
38 | | elfznn0 13597 |
. . . . . . . 8
โข (๐พ โ (0...๐) โ ๐พ โ
โ0) |
39 | | nn0p1nn 12512 |
. . . . . . . 8
โข (๐พ โ โ0
โ (๐พ + 1) โ
โ) |
40 | 38, 39 | syl 17 |
. . . . . . 7
โข (๐พ โ (0...๐) โ (๐พ + 1) โ โ) |
41 | 37, 40 | nndivred 12267 |
. . . . . 6
โข (๐พ โ (0...๐) โ (((๐ + 1) โ ๐พ) / (๐พ + 1)) โ โ) |
42 | 41 | recnd 11243 |
. . . . 5
โข (๐พ โ (0...๐) โ (((๐ + 1) โ ๐พ) / (๐พ + 1)) โ โ) |
43 | 24, 36, 42 | mulassd 11238 |
. . . 4
โข (๐พ โ (0...๐) โ (((๐C๐พ) ยท ((๐ + 1) / ((๐ + 1) โ ๐พ))) ยท (((๐ + 1) โ ๐พ) / (๐พ + 1))) = ((๐C๐พ) ยท (((๐ + 1) / ((๐ + 1) โ ๐พ)) ยท (((๐ + 1) โ ๐พ) / (๐พ + 1))))) |
44 | 25 | zcnd 12668 |
. . . . . 6
โข (๐พ โ (0...๐) โ (๐ + 1) โ โ) |
45 | 34 | nncnd 12229 |
. . . . . 6
โข (๐พ โ (0...๐) โ ((๐ + 1) โ ๐พ) โ โ) |
46 | 40 | nncnd 12229 |
. . . . . 6
โข (๐พ โ (0...๐) โ (๐พ + 1) โ โ) |
47 | 34 | nnne0d 12263 |
. . . . . 6
โข (๐พ โ (0...๐) โ ((๐ + 1) โ ๐พ) โ 0) |
48 | 40 | nnne0d 12263 |
. . . . . 6
โข (๐พ โ (0...๐) โ (๐พ + 1) โ 0) |
49 | 44, 45, 46, 47, 48 | dmdcan2d 12021 |
. . . . 5
โข (๐พ โ (0...๐) โ (((๐ + 1) / ((๐ + 1) โ ๐พ)) ยท (((๐ + 1) โ ๐พ) / (๐พ + 1))) = ((๐ + 1) / (๐พ + 1))) |
50 | 49 | oveq2d 7420 |
. . . 4
โข (๐พ โ (0...๐) โ ((๐C๐พ) ยท (((๐ + 1) / ((๐ + 1) โ ๐พ)) ยท (((๐ + 1) โ ๐พ) / (๐พ + 1)))) = ((๐C๐พ) ยท ((๐ + 1) / (๐พ + 1)))) |
51 | 43, 50 | eqtrd 2766 |
. . 3
โข (๐พ โ (0...๐) โ (((๐C๐พ) ยท ((๐ + 1) / ((๐ + 1) โ ๐พ))) ยท (((๐ + 1) โ ๐พ) / (๐พ + 1))) = ((๐C๐พ) ยท ((๐ + 1) / (๐พ + 1)))) |
52 | 22, 51 | eqtrd 2766 |
. 2
โข (๐พ โ (0...๐) โ (((๐ + 1)C((๐พ + 1) โ 1)) ยท (((๐ + 1) โ ((๐พ + 1) โ 1)) / (๐พ + 1))) = ((๐C๐พ) ยท ((๐ + 1) / (๐พ + 1)))) |
53 | 12, 52 | eqtrd 2766 |
1
โข (๐พ โ (0...๐) โ ((๐ + 1)C(๐พ + 1)) = ((๐C๐พ) ยท ((๐ + 1) / (๐พ + 1)))) |