Step | Hyp | Ref
| Expression |
1 | | 2t1e2 12323 |
. . . . . . 7
โข (2
ยท 1) = 2 |
2 | | df-2 12223 |
. . . . . . 7
โข 2 = (1 +
1) |
3 | 1, 2 | eqtri 2765 |
. . . . . 6
โข (2
ยท 1) = (1 + 1) |
4 | 3 | oveq2i 7373 |
. . . . 5
โข ((2
ยท ๐) + (2 ยท
1)) = ((2 ยท ๐) + (1
+ 1)) |
5 | | nn0cn 12430 |
. . . . . 6
โข (๐ โ โ0
โ ๐ โ
โ) |
6 | | 2cn 12235 |
. . . . . . 7
โข 2 โ
โ |
7 | | ax-1cn 11116 |
. . . . . . 7
โข 1 โ
โ |
8 | | adddi 11147 |
. . . . . . 7
โข ((2
โ โ โง ๐
โ โ โง 1 โ โ) โ (2 ยท (๐ + 1)) = ((2 ยท ๐) + (2 ยท 1))) |
9 | 6, 7, 8 | mp3an13 1453 |
. . . . . 6
โข (๐ โ โ โ (2
ยท (๐ + 1)) = ((2
ยท ๐) + (2 ยท
1))) |
10 | 5, 9 | syl 17 |
. . . . 5
โข (๐ โ โ0
โ (2 ยท (๐ + 1))
= ((2 ยท ๐) + (2
ยท 1))) |
11 | | 2nn0 12437 |
. . . . . . . 8
โข 2 โ
โ0 |
12 | | nn0mulcl 12456 |
. . . . . . . 8
โข ((2
โ โ0 โง ๐ โ โ0) โ (2
ยท ๐) โ
โ0) |
13 | 11, 12 | mpan 689 |
. . . . . . 7
โข (๐ โ โ0
โ (2 ยท ๐)
โ โ0) |
14 | 13 | nn0cnd 12482 |
. . . . . 6
โข (๐ โ โ0
โ (2 ยท ๐)
โ โ) |
15 | | addass 11145 |
. . . . . . 7
โข (((2
ยท ๐) โ โ
โง 1 โ โ โง 1 โ โ) โ (((2 ยท ๐) + 1) + 1) = ((2 ยท ๐) + (1 + 1))) |
16 | 7, 7, 15 | mp3an23 1454 |
. . . . . 6
โข ((2
ยท ๐) โ โ
โ (((2 ยท ๐) +
1) + 1) = ((2 ยท ๐) +
(1 + 1))) |
17 | 14, 16 | syl 17 |
. . . . 5
โข (๐ โ โ0
โ (((2 ยท ๐) +
1) + 1) = ((2 ยท ๐) +
(1 + 1))) |
18 | 4, 10, 17 | 3eqtr4a 2803 |
. . . 4
โข (๐ โ โ0
โ (2 ยท (๐ + 1))
= (((2 ยท ๐) + 1) +
1)) |
19 | 18 | oveq1d 7377 |
. . 3
โข (๐ โ โ0
โ ((2 ยท (๐ +
1))C(๐ + 1)) = ((((2
ยท ๐) + 1) +
1)C(๐ +
1))) |
20 | | peano2nn0 12460 |
. . . . 5
โข ((2
ยท ๐) โ
โ0 โ ((2 ยท ๐) + 1) โ
โ0) |
21 | 13, 20 | syl 17 |
. . . 4
โข (๐ โ โ0
โ ((2 ยท ๐) + 1)
โ โ0) |
22 | | nn0p1nn 12459 |
. . . . 5
โข (๐ โ โ0
โ (๐ + 1) โ
โ) |
23 | 22 | nnzd 12533 |
. . . 4
โข (๐ โ โ0
โ (๐ + 1) โ
โค) |
24 | | bcpasc 14228 |
. . . 4
โข ((((2
ยท ๐) + 1) โ
โ0 โง (๐ + 1) โ โค) โ ((((2 ยท
๐) + 1)C(๐ + 1)) + (((2 ยท ๐) + 1)C((๐ + 1) โ 1))) = ((((2 ยท ๐) + 1) + 1)C(๐ + 1))) |
25 | 21, 23, 24 | syl2anc 585 |
. . 3
โข (๐ โ โ0
โ ((((2 ยท ๐) +
1)C(๐ + 1)) + (((2 ยท
๐) + 1)C((๐ + 1) โ 1))) = ((((2 ยท ๐) + 1) + 1)C(๐ + 1))) |
26 | 19, 25 | eqtr4d 2780 |
. 2
โข (๐ โ โ0
โ ((2 ยท (๐ +
1))C(๐ + 1)) = ((((2
ยท ๐) + 1)C(๐ + 1)) + (((2 ยท ๐) + 1)C((๐ + 1) โ 1)))) |
27 | | nn0z 12531 |
. . . . . . 7
โข (๐ โ โ0
โ ๐ โ
โค) |
28 | | bccl 14229 |
. . . . . . 7
โข (((2
ยท ๐) โ
โ0 โง ๐
โ โค) โ ((2 ยท ๐)C๐) โ
โ0) |
29 | 13, 27, 28 | syl2anc 585 |
. . . . . 6
โข (๐ โ โ0
โ ((2 ยท ๐)C๐) โ
โ0) |
30 | 29 | nn0cnd 12482 |
. . . . 5
โข (๐ โ โ0
โ ((2 ยท ๐)C๐) โ โ) |
31 | | 2cnd 12238 |
. . . . 5
โข (๐ โ โ0
โ 2 โ โ) |
32 | 21 | nn0red 12481 |
. . . . . . 7
โข (๐ โ โ0
โ ((2 ยท ๐) + 1)
โ โ) |
33 | 32, 22 | nndivred 12214 |
. . . . . 6
โข (๐ โ โ0
โ (((2 ยท ๐) +
1) / (๐ + 1)) โ
โ) |
34 | 33 | recnd 11190 |
. . . . 5
โข (๐ โ โ0
โ (((2 ยท ๐) +
1) / (๐ + 1)) โ
โ) |
35 | 30, 31, 34 | mul12d 11371 |
. . . 4
โข (๐ โ โ0
โ (((2 ยท ๐)C๐) ยท (2 ยท (((2 ยท ๐) + 1) / (๐ + 1)))) = (2 ยท (((2 ยท ๐)C๐) ยท (((2 ยท ๐) + 1) / (๐ + 1))))) |
36 | | 1cnd 11157 |
. . . . . . . . . 10
โข (๐ โ โ0
โ 1 โ โ) |
37 | 14, 36, 5 | addsubd 11540 |
. . . . . . . . 9
โข (๐ โ โ0
โ (((2 ยท ๐) +
1) โ ๐) = (((2
ยท ๐) โ ๐) + 1)) |
38 | 5 | 2timesd 12403 |
. . . . . . . . . . 11
โข (๐ โ โ0
โ (2 ยท ๐) =
(๐ + ๐)) |
39 | 5, 5, 38 | mvrladdd 11575 |
. . . . . . . . . 10
โข (๐ โ โ0
โ ((2 ยท ๐)
โ ๐) = ๐) |
40 | 39 | oveq1d 7377 |
. . . . . . . . 9
โข (๐ โ โ0
โ (((2 ยท ๐)
โ ๐) + 1) = (๐ + 1)) |
41 | 37, 40 | eqtr2d 2778 |
. . . . . . . 8
โข (๐ โ โ0
โ (๐ + 1) = (((2
ยท ๐) + 1) โ
๐)) |
42 | 41 | oveq2d 7378 |
. . . . . . 7
โข (๐ โ โ0
โ (((2 ยท ๐) +
1) / (๐ + 1)) = (((2
ยท ๐) + 1) / (((2
ยท ๐) + 1) โ
๐))) |
43 | 42 | oveq2d 7378 |
. . . . . 6
โข (๐ โ โ0
โ (((2 ยท ๐)C๐) ยท (((2 ยท ๐) + 1) / (๐ + 1))) = (((2 ยท ๐)C๐) ยท (((2 ยท ๐) + 1) / (((2 ยท ๐) + 1) โ ๐)))) |
44 | | fzctr 13560 |
. . . . . . 7
โข (๐ โ โ0
โ ๐ โ (0...(2
ยท ๐))) |
45 | | bcp1n 14223 |
. . . . . . 7
โข (๐ โ (0...(2 ยท ๐)) โ (((2 ยท ๐) + 1)C๐) = (((2 ยท ๐)C๐) ยท (((2 ยท ๐) + 1) / (((2 ยท ๐) + 1) โ ๐)))) |
46 | 44, 45 | syl 17 |
. . . . . 6
โข (๐ โ โ0
โ (((2 ยท ๐) +
1)C๐) = (((2 ยท ๐)C๐) ยท (((2 ยท ๐) + 1) / (((2 ยท ๐) + 1) โ ๐)))) |
47 | 43, 46 | eqtr4d 2780 |
. . . . 5
โข (๐ โ โ0
โ (((2 ยท ๐)C๐) ยท (((2 ยท ๐) + 1) / (๐ + 1))) = (((2 ยท ๐) + 1)C๐)) |
48 | 47 | oveq2d 7378 |
. . . 4
โข (๐ โ โ0
โ (2 ยท (((2 ยท ๐)C๐) ยท (((2 ยท ๐) + 1) / (๐ + 1)))) = (2 ยท (((2 ยท ๐) + 1)C๐))) |
49 | 35, 48 | eqtrd 2777 |
. . 3
โข (๐ โ โ0
โ (((2 ยท ๐)C๐) ยท (2 ยท (((2 ยท ๐) + 1) / (๐ + 1)))) = (2 ยท (((2 ยท ๐) + 1)C๐))) |
50 | | bccmpl 14216 |
. . . . . . 7
โข ((((2
ยท ๐) + 1) โ
โ0 โง (๐ + 1) โ โค) โ (((2 ยท
๐) + 1)C(๐ + 1)) = (((2 ยท ๐) + 1)C(((2 ยท ๐) + 1) โ (๐ + 1)))) |
51 | 21, 23, 50 | syl2anc 585 |
. . . . . 6
โข (๐ โ โ0
โ (((2 ยท ๐) +
1)C(๐ + 1)) = (((2 ยท
๐) + 1)C(((2 ยท ๐) + 1) โ (๐ + 1)))) |
52 | 22 | nncnd 12176 |
. . . . . . . 8
โข (๐ โ โ0
โ (๐ + 1) โ
โ) |
53 | 38 | oveq1d 7377 |
. . . . . . . . 9
โข (๐ โ โ0
โ ((2 ยท ๐) + 1)
= ((๐ + ๐) + 1)) |
54 | 5, 5, 36 | addassd 11184 |
. . . . . . . . 9
โข (๐ โ โ0
โ ((๐ + ๐) + 1) = (๐ + (๐ + 1))) |
55 | 53, 54 | eqtrd 2777 |
. . . . . . . 8
โข (๐ โ โ0
โ ((2 ยท ๐) + 1)
= (๐ + (๐ + 1))) |
56 | 5, 52, 55 | mvrraddd 11574 |
. . . . . . 7
โข (๐ โ โ0
โ (((2 ยท ๐) +
1) โ (๐ + 1)) = ๐) |
57 | 56 | oveq2d 7378 |
. . . . . 6
โข (๐ โ โ0
โ (((2 ยท ๐) +
1)C(((2 ยท ๐) + 1)
โ (๐ + 1))) = (((2
ยท ๐) + 1)C๐)) |
58 | 51, 57 | eqtrd 2777 |
. . . . 5
โข (๐ โ โ0
โ (((2 ยท ๐) +
1)C(๐ + 1)) = (((2 ยท
๐) + 1)C๐)) |
59 | | pncan 11414 |
. . . . . . 7
โข ((๐ โ โ โง 1 โ
โ) โ ((๐ + 1)
โ 1) = ๐) |
60 | 5, 7, 59 | sylancl 587 |
. . . . . 6
โข (๐ โ โ0
โ ((๐ + 1) โ 1)
= ๐) |
61 | 60 | oveq2d 7378 |
. . . . 5
โข (๐ โ โ0
โ (((2 ยท ๐) +
1)C((๐ + 1) โ 1)) =
(((2 ยท ๐) + 1)C๐)) |
62 | 58, 61 | oveq12d 7380 |
. . . 4
โข (๐ โ โ0
โ ((((2 ยท ๐) +
1)C(๐ + 1)) + (((2 ยท
๐) + 1)C((๐ + 1) โ 1))) = ((((2 ยท ๐) + 1)C๐) + (((2 ยท ๐) + 1)C๐))) |
63 | | bccl 14229 |
. . . . . . 7
โข ((((2
ยท ๐) + 1) โ
โ0 โง ๐
โ โค) โ (((2 ยท ๐) + 1)C๐) โ
โ0) |
64 | 21, 27, 63 | syl2anc 585 |
. . . . . 6
โข (๐ โ โ0
โ (((2 ยท ๐) +
1)C๐) โ
โ0) |
65 | 64 | nn0cnd 12482 |
. . . . 5
โข (๐ โ โ0
โ (((2 ยท ๐) +
1)C๐) โ
โ) |
66 | 65 | 2timesd 12403 |
. . . 4
โข (๐ โ โ0
โ (2 ยท (((2 ยท ๐) + 1)C๐)) = ((((2 ยท ๐) + 1)C๐) + (((2 ยท ๐) + 1)C๐))) |
67 | 62, 66 | eqtr4d 2780 |
. . 3
โข (๐ โ โ0
โ ((((2 ยท ๐) +
1)C(๐ + 1)) + (((2 ยท
๐) + 1)C((๐ + 1) โ 1))) = (2 ยท (((2
ยท ๐) + 1)C๐))) |
68 | 49, 67 | eqtr4d 2780 |
. 2
โข (๐ โ โ0
โ (((2 ยท ๐)C๐) ยท (2 ยท (((2 ยท ๐) + 1) / (๐ + 1)))) = ((((2 ยท ๐) + 1)C(๐ + 1)) + (((2 ยท ๐) + 1)C((๐ + 1) โ 1)))) |
69 | 26, 68 | eqtr4d 2780 |
1
โข (๐ โ โ0
โ ((2 ยท (๐ +
1))C(๐ + 1)) = (((2
ยท ๐)C๐) ยท (2 ยท (((2
ยท ๐) + 1) / (๐ + 1))))) |