Step | Hyp | Ref
| Expression |
1 | | 2cnd 12238 |
. . . . . . . 8
โข (๐ โ 2 โ
โ) |
2 | | 2np3bcnp1.1 |
. . . . . . . . 9
โข (๐ โ ๐ โ
โ0) |
3 | 2 | nn0cnd 12482 |
. . . . . . . 8
โข (๐ โ ๐ โ โ) |
4 | | 1cnd 11157 |
. . . . . . . 8
โข (๐ โ 1 โ
โ) |
5 | 1, 3, 4 | adddid 11186 |
. . . . . . 7
โข (๐ โ (2 ยท (๐ + 1)) = ((2 ยท ๐) + (2 ยท
1))) |
6 | | 2t1e2 12323 |
. . . . . . . 8
โข (2
ยท 1) = 2 |
7 | 6 | oveq2i 7373 |
. . . . . . 7
โข ((2
ยท ๐) + (2 ยท
1)) = ((2 ยท ๐) +
2) |
8 | 5, 7 | eqtrdi 2793 |
. . . . . 6
โข (๐ โ (2 ยท (๐ + 1)) = ((2 ยท ๐) + 2)) |
9 | 8 | oveq1d 7377 |
. . . . 5
โข (๐ โ ((2 ยท (๐ + 1)) + 1) = (((2 ยท
๐) + 2) +
1)) |
10 | 1, 3 | mulcld 11182 |
. . . . . 6
โข (๐ โ (2 ยท ๐) โ
โ) |
11 | 10, 1, 4 | addassd 11184 |
. . . . 5
โข (๐ โ (((2 ยท ๐) + 2) + 1) = ((2 ยท ๐) + (2 + 1))) |
12 | 9, 11 | eqtrd 2777 |
. . . 4
โข (๐ โ ((2 ยท (๐ + 1)) + 1) = ((2 ยท ๐) + (2 + 1))) |
13 | | 2p1e3 12302 |
. . . . . 6
โข (2 + 1) =
3 |
14 | 13 | a1i 11 |
. . . . 5
โข (๐ โ (2 + 1) =
3) |
15 | 14 | oveq2d 7378 |
. . . 4
โข (๐ โ ((2 ยท ๐) + (2 + 1)) = ((2 ยท
๐) + 3)) |
16 | 12, 15 | eqtrd 2777 |
. . 3
โข (๐ โ ((2 ยท (๐ + 1)) + 1) = ((2 ยท ๐) + 3)) |
17 | 16 | oveq1d 7377 |
. 2
โข (๐ โ (((2 ยท (๐ + 1)) + 1)C(๐ + 1)) = (((2 ยท ๐) + 3)C(๐ + 1))) |
18 | | 0zd 12518 |
. . . . 5
โข (๐ โ 0 โ
โค) |
19 | | 2z 12542 |
. . . . . . . 8
โข 2 โ
โค |
20 | 19 | a1i 11 |
. . . . . . 7
โข (๐ โ 2 โ
โค) |
21 | 2 | nn0zd 12532 |
. . . . . . 7
โข (๐ โ ๐ โ โค) |
22 | 20, 21 | zmulcld 12620 |
. . . . . 6
โข (๐ โ (2 ยท ๐) โ
โค) |
23 | | 3z 12543 |
. . . . . . 7
โข 3 โ
โค |
24 | 23 | a1i 11 |
. . . . . 6
โข (๐ โ 3 โ
โค) |
25 | 22, 24 | zaddcld 12618 |
. . . . 5
โข (๐ โ ((2 ยท ๐) + 3) โ
โค) |
26 | 21 | peano2zd 12617 |
. . . . 5
โข (๐ โ (๐ + 1) โ โค) |
27 | 2 | nn0red 12481 |
. . . . . 6
โข (๐ โ ๐ โ โ) |
28 | | 1red 11163 |
. . . . . 6
โข (๐ โ 1 โ
โ) |
29 | 2 | nn0ge0d 12483 |
. . . . . 6
โข (๐ โ 0 โค ๐) |
30 | | 0le1 11685 |
. . . . . . 7
โข 0 โค
1 |
31 | 30 | a1i 11 |
. . . . . 6
โข (๐ โ 0 โค 1) |
32 | 27, 28, 29, 31 | addge0d 11738 |
. . . . 5
โข (๐ โ 0 โค (๐ + 1)) |
33 | | 2re 12234 |
. . . . . . . 8
โข 2 โ
โ |
34 | 33 | a1i 11 |
. . . . . . 7
โข (๐ โ 2 โ
โ) |
35 | 34, 27 | remulcld 11192 |
. . . . . 6
โข (๐ โ (2 ยท ๐) โ
โ) |
36 | | 3re 12240 |
. . . . . . 7
โข 3 โ
โ |
37 | 36 | a1i 11 |
. . . . . 6
โข (๐ โ 3 โ
โ) |
38 | | 1le2 12369 |
. . . . . . . 8
โข 1 โค
2 |
39 | 38 | a1i 11 |
. . . . . . 7
โข (๐ โ 1 โค 2) |
40 | 27, 34, 29, 39 | lemulge12d 12100 |
. . . . . 6
โข (๐ โ ๐ โค (2 ยท ๐)) |
41 | | 1le3 12372 |
. . . . . . 7
โข 1 โค
3 |
42 | 41 | a1i 11 |
. . . . . 6
โข (๐ โ 1 โค 3) |
43 | 27, 28, 35, 37, 40, 42 | le2addd 11781 |
. . . . 5
โข (๐ โ (๐ + 1) โค ((2 ยท ๐) + 3)) |
44 | 18, 25, 26, 32, 43 | elfzd 13439 |
. . . 4
โข (๐ โ (๐ + 1) โ (0...((2 ยท ๐) + 3))) |
45 | | bcval2 14212 |
. . . 4
โข ((๐ + 1) โ (0...((2 ยท
๐) + 3)) โ (((2
ยท ๐) + 3)C(๐ + 1)) = ((!โ((2 ยท
๐) + 3)) / ((!โ(((2
ยท ๐) + 3) โ
(๐ + 1))) ยท
(!โ(๐ +
1))))) |
46 | 44, 45 | syl 17 |
. . 3
โข (๐ โ (((2 ยท ๐) + 3)C(๐ + 1)) = ((!โ((2 ยท ๐) + 3)) / ((!โ(((2
ยท ๐) + 3) โ
(๐ + 1))) ยท
(!โ(๐ +
1))))) |
47 | 37 | recnd 11190 |
. . . . . . . . 9
โข (๐ โ 3 โ
โ) |
48 | 10, 47, 3, 4 | addsub4d 11566 |
. . . . . . . 8
โข (๐ โ (((2 ยท ๐) + 3) โ (๐ + 1)) = (((2 ยท ๐) โ ๐) + (3 โ 1))) |
49 | | 2txmxeqx 12300 |
. . . . . . . . . 10
โข (๐ โ โ โ ((2
ยท ๐) โ ๐) = ๐) |
50 | 3, 49 | syl 17 |
. . . . . . . . 9
โข (๐ โ ((2 ยท ๐) โ ๐) = ๐) |
51 | | 3m1e2 12288 |
. . . . . . . . . 10
โข (3
โ 1) = 2 |
52 | 51 | a1i 11 |
. . . . . . . . 9
โข (๐ โ (3 โ 1) =
2) |
53 | 50, 52 | oveq12d 7380 |
. . . . . . . 8
โข (๐ โ (((2 ยท ๐) โ ๐) + (3 โ 1)) = (๐ + 2)) |
54 | 48, 53 | eqtrd 2777 |
. . . . . . 7
โข (๐ โ (((2 ยท ๐) + 3) โ (๐ + 1)) = (๐ + 2)) |
55 | 54 | fveq2d 6851 |
. . . . . 6
โข (๐ โ (!โ(((2 ยท
๐) + 3) โ (๐ + 1))) = (!โ(๐ + 2))) |
56 | 55 | oveq1d 7377 |
. . . . 5
โข (๐ โ ((!โ(((2 ยท
๐) + 3) โ (๐ + 1))) ยท (!โ(๐ + 1))) = ((!โ(๐ + 2)) ยท (!โ(๐ + 1)))) |
57 | 56 | oveq2d 7378 |
. . . 4
โข (๐ โ ((!โ((2 ยท
๐) + 3)) / ((!โ(((2
ยท ๐) + 3) โ
(๐ + 1))) ยท
(!โ(๐ + 1)))) =
((!โ((2 ยท ๐) +
3)) / ((!โ(๐ + 2))
ยท (!โ(๐ +
1))))) |
58 | | 2nn0 12437 |
. . . . . . . . . . 11
โข 2 โ
โ0 |
59 | 58 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ 2 โ
โ0) |
60 | 2, 59 | nn0addcld 12484 |
. . . . . . . . 9
โข (๐ โ (๐ + 2) โ
โ0) |
61 | 60 | faccld 14191 |
. . . . . . . 8
โข (๐ โ (!โ(๐ + 2)) โ
โ) |
62 | 61 | nncnd 12176 |
. . . . . . 7
โข (๐ โ (!โ(๐ + 2)) โ
โ) |
63 | | 1nn0 12436 |
. . . . . . . . . . 11
โข 1 โ
โ0 |
64 | 63 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ 1 โ
โ0) |
65 | 2, 64 | nn0addcld 12484 |
. . . . . . . . 9
โข (๐ โ (๐ + 1) โ
โ0) |
66 | 65 | faccld 14191 |
. . . . . . . 8
โข (๐ โ (!โ(๐ + 1)) โ
โ) |
67 | 66 | nncnd 12176 |
. . . . . . 7
โข (๐ โ (!โ(๐ + 1)) โ
โ) |
68 | 62, 67 | mulcomd 11183 |
. . . . . 6
โข (๐ โ ((!โ(๐ + 2)) ยท (!โ(๐ + 1))) = ((!โ(๐ + 1)) ยท (!โ(๐ + 2)))) |
69 | 68 | oveq2d 7378 |
. . . . 5
โข (๐ โ ((!โ((2 ยท
๐) + 3)) / ((!โ(๐ + 2)) ยท (!โ(๐ + 1)))) = ((!โ((2
ยท ๐) + 3)) /
((!โ(๐ + 1)) ยท
(!โ(๐ +
2))))) |
70 | 10, 4, 1 | addassd 11184 |
. . . . . . . . . . . 12
โข (๐ โ (((2 ยท ๐) + 1) + 2) = ((2 ยท ๐) + (1 + 2))) |
71 | | 1p2e3 12303 |
. . . . . . . . . . . . 13
โข (1 + 2) =
3 |
72 | 71 | oveq2i 7373 |
. . . . . . . . . . . 12
โข ((2
ยท ๐) + (1 + 2)) =
((2 ยท ๐) +
3) |
73 | 70, 72 | eqtrdi 2793 |
. . . . . . . . . . 11
โข (๐ โ (((2 ยท ๐) + 1) + 2) = ((2 ยท ๐) + 3)) |
74 | 73 | fveq2d 6851 |
. . . . . . . . . 10
โข (๐ โ (!โ(((2 ยท
๐) + 1) + 2)) =
(!โ((2 ยท ๐) +
3))) |
75 | 74 | eqcomd 2743 |
. . . . . . . . 9
โข (๐ โ (!โ((2 ยท
๐) + 3)) = (!โ(((2
ยท ๐) + 1) +
2))) |
76 | 59, 2 | nn0mulcld 12485 |
. . . . . . . . . . 11
โข (๐ โ (2 ยท ๐) โ
โ0) |
77 | 76, 64 | nn0addcld 12484 |
. . . . . . . . . 10
โข (๐ โ ((2 ยท ๐) + 1) โ
โ0) |
78 | | facp2 40580 |
. . . . . . . . . 10
โข (((2
ยท ๐) + 1) โ
โ0 โ (!โ(((2 ยท ๐) + 1) + 2)) = ((!โ((2 ยท ๐) + 1)) ยท ((((2 ยท
๐) + 1) + 1) ยท (((2
ยท ๐) + 1) +
2)))) |
79 | 77, 78 | syl 17 |
. . . . . . . . 9
โข (๐ โ (!โ(((2 ยท
๐) + 1) + 2)) =
((!โ((2 ยท ๐) +
1)) ยท ((((2 ยท ๐) + 1) + 1) ยท (((2 ยท ๐) + 1) + 2)))) |
80 | 75, 79 | eqtrd 2777 |
. . . . . . . 8
โข (๐ โ (!โ((2 ยท
๐) + 3)) = ((!โ((2
ยท ๐) + 1)) ยท
((((2 ยท ๐) + 1) + 1)
ยท (((2 ยท ๐) +
1) + 2)))) |
81 | 10, 4, 4 | addassd 11184 |
. . . . . . . . . . 11
โข (๐ โ (((2 ยท ๐) + 1) + 1) = ((2 ยท ๐) + (1 + 1))) |
82 | | 1p1e2 12285 |
. . . . . . . . . . . . 13
โข (1 + 1) =
2 |
83 | 82 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ (1 + 1) =
2) |
84 | 83 | oveq2d 7378 |
. . . . . . . . . . 11
โข (๐ โ ((2 ยท ๐) + (1 + 1)) = ((2 ยท
๐) + 2)) |
85 | 81, 84 | eqtrd 2777 |
. . . . . . . . . 10
โข (๐ โ (((2 ยท ๐) + 1) + 1) = ((2 ยท ๐) + 2)) |
86 | 71 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ (1 + 2) =
3) |
87 | 86 | oveq2d 7378 |
. . . . . . . . . . 11
โข (๐ โ ((2 ยท ๐) + (1 + 2)) = ((2 ยท
๐) + 3)) |
88 | 70, 87 | eqtrd 2777 |
. . . . . . . . . 10
โข (๐ โ (((2 ยท ๐) + 1) + 2) = ((2 ยท ๐) + 3)) |
89 | 85, 88 | oveq12d 7380 |
. . . . . . . . 9
โข (๐ โ ((((2 ยท ๐) + 1) + 1) ยท (((2
ยท ๐) + 1) + 2)) =
(((2 ยท ๐) + 2)
ยท ((2 ยท ๐) +
3))) |
90 | 89 | oveq2d 7378 |
. . . . . . . 8
โข (๐ โ ((!โ((2 ยท
๐) + 1)) ยท ((((2
ยท ๐) + 1) + 1)
ยท (((2 ยท ๐) +
1) + 2))) = ((!โ((2 ยท ๐) + 1)) ยท (((2 ยท ๐) + 2) ยท ((2 ยท
๐) + 3)))) |
91 | 80, 90 | eqtrd 2777 |
. . . . . . 7
โข (๐ โ (!โ((2 ยท
๐) + 3)) = ((!โ((2
ยท ๐) + 1)) ยท
(((2 ยท ๐) + 2)
ยท ((2 ยท ๐) +
3)))) |
92 | 91 | oveq1d 7377 |
. . . . . 6
โข (๐ โ ((!โ((2 ยท
๐) + 3)) / ((!โ(๐ + 1)) ยท (!โ(๐ + 2)))) = (((!โ((2
ยท ๐) + 1)) ยท
(((2 ยท ๐) + 2)
ยท ((2 ยท ๐) +
3))) / ((!โ(๐ + 1))
ยท (!โ(๐ +
2))))) |
93 | | facp2 40580 |
. . . . . . . . . 10
โข (๐ โ โ0
โ (!โ(๐ + 2)) =
((!โ๐) ยท
((๐ + 1) ยท (๐ + 2)))) |
94 | 2, 93 | syl 17 |
. . . . . . . . 9
โข (๐ โ (!โ(๐ + 2)) = ((!โ๐) ยท ((๐ + 1) ยท (๐ + 2)))) |
95 | 94 | oveq2d 7378 |
. . . . . . . 8
โข (๐ โ ((!โ(๐ + 1)) ยท (!โ(๐ + 2))) = ((!โ(๐ + 1)) ยท ((!โ๐) ยท ((๐ + 1) ยท (๐ + 2))))) |
96 | 95 | oveq2d 7378 |
. . . . . . 7
โข (๐ โ (((!โ((2 ยท
๐) + 1)) ยท (((2
ยท ๐) + 2) ยท
((2 ยท ๐) + 3))) /
((!โ(๐ + 1)) ยท
(!โ(๐ + 2)))) =
(((!โ((2 ยท ๐)
+ 1)) ยท (((2 ยท ๐) + 2) ยท ((2 ยท ๐) + 3))) / ((!โ(๐ + 1)) ยท ((!โ๐) ยท ((๐ + 1) ยท (๐ + 2)))))) |
97 | 2 | faccld 14191 |
. . . . . . . . . . . 12
โข (๐ โ (!โ๐) โ โ) |
98 | 97 | nncnd 12176 |
. . . . . . . . . . 11
โข (๐ โ (!โ๐) โ โ) |
99 | 3, 4 | addcld 11181 |
. . . . . . . . . . . 12
โข (๐ โ (๐ + 1) โ โ) |
100 | 3, 1 | addcld 11181 |
. . . . . . . . . . . 12
โข (๐ โ (๐ + 2) โ โ) |
101 | 99, 100 | mulcld 11182 |
. . . . . . . . . . 11
โข (๐ โ ((๐ + 1) ยท (๐ + 2)) โ โ) |
102 | 67, 98, 101 | mulassd 11185 |
. . . . . . . . . 10
โข (๐ โ (((!โ(๐ + 1)) ยท (!โ๐)) ยท ((๐ + 1) ยท (๐ + 2))) = ((!โ(๐ + 1)) ยท ((!โ๐) ยท ((๐ + 1) ยท (๐ + 2))))) |
103 | 102 | eqcomd 2743 |
. . . . . . . . 9
โข (๐ โ ((!โ(๐ + 1)) ยท ((!โ๐) ยท ((๐ + 1) ยท (๐ + 2)))) = (((!โ(๐ + 1)) ยท (!โ๐)) ยท ((๐ + 1) ยท (๐ + 2)))) |
104 | 103 | oveq2d 7378 |
. . . . . . . 8
โข (๐ โ (((!โ((2 ยท
๐) + 1)) ยท (((2
ยท ๐) + 2) ยท
((2 ยท ๐) + 3))) /
((!โ(๐ + 1)) ยท
((!โ๐) ยท
((๐ + 1) ยท (๐ + 2))))) = (((!โ((2
ยท ๐) + 1)) ยท
(((2 ยท ๐) + 2)
ยท ((2 ยท ๐) +
3))) / (((!โ(๐ + 1))
ยท (!โ๐))
ยท ((๐ + 1) ยท
(๐ +
2))))) |
105 | 77 | faccld 14191 |
. . . . . . . . . . . 12
โข (๐ โ (!โ((2 ยท
๐) + 1)) โ
โ) |
106 | 105 | nncnd 12176 |
. . . . . . . . . . 11
โข (๐ โ (!โ((2 ยท
๐) + 1)) โ
โ) |
107 | 67, 98 | mulcld 11182 |
. . . . . . . . . . 11
โข (๐ โ ((!โ(๐ + 1)) ยท (!โ๐)) โ
โ) |
108 | 10, 1 | addcld 11181 |
. . . . . . . . . . . 12
โข (๐ โ ((2 ยท ๐) + 2) โ
โ) |
109 | 10, 47 | addcld 11181 |
. . . . . . . . . . . 12
โข (๐ โ ((2 ยท ๐) + 3) โ
โ) |
110 | 108, 109 | mulcld 11182 |
. . . . . . . . . . 11
โข (๐ โ (((2 ยท ๐) + 2) ยท ((2 ยท
๐) + 3)) โ
โ) |
111 | 66 | nnne0d 12210 |
. . . . . . . . . . . 12
โข (๐ โ (!โ(๐ + 1)) โ 0) |
112 | 97 | nnne0d 12210 |
. . . . . . . . . . . 12
โข (๐ โ (!โ๐) โ 0) |
113 | 67, 98, 111, 112 | mulne0d 11814 |
. . . . . . . . . . 11
โข (๐ โ ((!โ(๐ + 1)) ยท (!โ๐)) โ 0) |
114 | | 0red 11165 |
. . . . . . . . . . . . . 14
โข (๐ โ 0 โ
โ) |
115 | 27, 28 | readdcld 11191 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ + 1) โ โ) |
116 | 27 | ltp1d 12092 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ < (๐ + 1)) |
117 | 114, 27, 115, 29, 116 | lelttrd 11320 |
. . . . . . . . . . . . . 14
โข (๐ โ 0 < (๐ + 1)) |
118 | 114, 117 | ltned 11298 |
. . . . . . . . . . . . 13
โข (๐ โ 0 โ (๐ + 1)) |
119 | 118 | necomd 3000 |
. . . . . . . . . . . 12
โข (๐ โ (๐ + 1) โ 0) |
120 | 27, 34 | readdcld 11191 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ + 2) โ โ) |
121 | | 2rp 12927 |
. . . . . . . . . . . . . . . . 17
โข 2 โ
โ+ |
122 | 121 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 2 โ
โ+) |
123 | 27, 122 | ltaddrpd 12997 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ < (๐ + 2)) |
124 | 114, 27, 120, 29, 123 | lelttrd 11320 |
. . . . . . . . . . . . . 14
โข (๐ โ 0 < (๐ + 2)) |
125 | 114, 124 | ltned 11298 |
. . . . . . . . . . . . 13
โข (๐ โ 0 โ (๐ + 2)) |
126 | 125 | necomd 3000 |
. . . . . . . . . . . 12
โข (๐ โ (๐ + 2) โ 0) |
127 | 99, 100, 119, 126 | mulne0d 11814 |
. . . . . . . . . . 11
โข (๐ โ ((๐ + 1) ยท (๐ + 2)) โ 0) |
128 | 106, 107,
110, 101, 113, 127 | divmuldivd 11979 |
. . . . . . . . . 10
โข (๐ โ (((!โ((2 ยท
๐) + 1)) / ((!โ(๐ + 1)) ยท (!โ๐))) ยท ((((2 ยท
๐) + 2) ยท ((2
ยท ๐) + 3)) / ((๐ + 1) ยท (๐ + 2)))) = (((!โ((2
ยท ๐) + 1)) ยท
(((2 ยท ๐) + 2)
ยท ((2 ยท ๐) +
3))) / (((!โ(๐ + 1))
ยท (!โ๐))
ยท ((๐ + 1) ยท
(๐ +
2))))) |
129 | 128 | eqcomd 2743 |
. . . . . . . . 9
โข (๐ โ (((!โ((2 ยท
๐) + 1)) ยท (((2
ยท ๐) + 2) ยท
((2 ยท ๐) + 3))) /
(((!โ(๐ + 1))
ยท (!โ๐))
ยท ((๐ + 1) ยท
(๐ + 2)))) = (((!โ((2
ยท ๐) + 1)) /
((!โ(๐ + 1)) ยท
(!โ๐))) ยท
((((2 ยท ๐) + 2)
ยท ((2 ยท ๐) +
3)) / ((๐ + 1) ยท
(๐ +
2))))) |
130 | 22 | peano2zd 12617 |
. . . . . . . . . . . . . 14
โข (๐ โ ((2 ยท ๐) + 1) โ
โค) |
131 | 35, 28 | readdcld 11191 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((2 ยท ๐) + 1) โ
โ) |
132 | 35 | lep1d 12093 |
. . . . . . . . . . . . . . 15
โข (๐ โ (2 ยท ๐) โค ((2 ยท ๐) + 1)) |
133 | 27, 35, 131, 40, 132 | letrd 11319 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ โค ((2 ยท ๐) + 1)) |
134 | 18, 130, 21, 29, 133 | elfzd 13439 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ (0...((2 ยท ๐) + 1))) |
135 | | bcval2 14212 |
. . . . . . . . . . . . 13
โข (๐ โ (0...((2 ยท ๐) + 1)) โ (((2 ยท
๐) + 1)C๐) = ((!โ((2 ยท ๐) + 1)) / ((!โ(((2 ยท ๐) + 1) โ ๐)) ยท (!โ๐)))) |
136 | 134, 135 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ (((2 ยท ๐) + 1)C๐) = ((!โ((2 ยท ๐) + 1)) / ((!โ(((2 ยท ๐) + 1) โ ๐)) ยท (!โ๐)))) |
137 | 10, 4, 3 | addsubd 11540 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (((2 ยท ๐) + 1) โ ๐) = (((2 ยท ๐) โ ๐) + 1)) |
138 | 50 | oveq1d 7377 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (((2 ยท ๐) โ ๐) + 1) = (๐ + 1)) |
139 | 137, 138 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
โข (๐ โ (((2 ยท ๐) + 1) โ ๐) = (๐ + 1)) |
140 | 139 | fveq2d 6851 |
. . . . . . . . . . . . . 14
โข (๐ โ (!โ(((2 ยท
๐) + 1) โ ๐)) = (!โ(๐ + 1))) |
141 | 140 | oveq1d 7377 |
. . . . . . . . . . . . 13
โข (๐ โ ((!โ(((2 ยท
๐) + 1) โ ๐)) ยท (!โ๐)) = ((!โ(๐ + 1)) ยท (!โ๐))) |
142 | 141 | oveq2d 7378 |
. . . . . . . . . . . 12
โข (๐ โ ((!โ((2 ยท
๐) + 1)) / ((!โ(((2
ยท ๐) + 1) โ
๐)) ยท (!โ๐))) = ((!โ((2 ยท
๐) + 1)) / ((!โ(๐ + 1)) ยท (!โ๐)))) |
143 | 136, 142 | eqtrd 2777 |
. . . . . . . . . . 11
โข (๐ โ (((2 ยท ๐) + 1)C๐) = ((!โ((2 ยท ๐) + 1)) / ((!โ(๐ + 1)) ยท (!โ๐)))) |
144 | 143 | eqcomd 2743 |
. . . . . . . . . 10
โข (๐ โ ((!โ((2 ยท
๐) + 1)) / ((!โ(๐ + 1)) ยท (!โ๐))) = (((2 ยท ๐) + 1)C๐)) |
145 | 108, 99, 109, 100, 119, 126 | divmuldivd 11979 |
. . . . . . . . . . . 12
โข (๐ โ ((((2 ยท ๐) + 2) / (๐ + 1)) ยท (((2 ยท ๐) + 3) / (๐ + 2))) = ((((2 ยท ๐) + 2) ยท ((2 ยท ๐) + 3)) / ((๐ + 1) ยท (๐ + 2)))) |
146 | 145 | eqcomd 2743 |
. . . . . . . . . . 11
โข (๐ โ ((((2 ยท ๐) + 2) ยท ((2 ยท
๐) + 3)) / ((๐ + 1) ยท (๐ + 2))) = ((((2 ยท ๐) + 2) / (๐ + 1)) ยท (((2 ยท ๐) + 3) / (๐ + 2)))) |
147 | 8 | eqcomd 2743 |
. . . . . . . . . . . . . 14
โข (๐ โ ((2 ยท ๐) + 2) = (2 ยท (๐ + 1))) |
148 | 147 | oveq1d 7377 |
. . . . . . . . . . . . 13
โข (๐ โ (((2 ยท ๐) + 2) / (๐ + 1)) = ((2 ยท (๐ + 1)) / (๐ + 1))) |
149 | 1, 99, 119 | divcan4d 11944 |
. . . . . . . . . . . . 13
โข (๐ โ ((2 ยท (๐ + 1)) / (๐ + 1)) = 2) |
150 | 148, 149 | eqtrd 2777 |
. . . . . . . . . . . 12
โข (๐ โ (((2 ยท ๐) + 2) / (๐ + 1)) = 2) |
151 | | eqidd 2738 |
. . . . . . . . . . . 12
โข (๐ โ (((2 ยท ๐) + 3) / (๐ + 2)) = (((2 ยท ๐) + 3) / (๐ + 2))) |
152 | 150, 151 | oveq12d 7380 |
. . . . . . . . . . 11
โข (๐ โ ((((2 ยท ๐) + 2) / (๐ + 1)) ยท (((2 ยท ๐) + 3) / (๐ + 2))) = (2 ยท (((2 ยท ๐) + 3) / (๐ + 2)))) |
153 | 146, 152 | eqtrd 2777 |
. . . . . . . . . 10
โข (๐ โ ((((2 ยท ๐) + 2) ยท ((2 ยท
๐) + 3)) / ((๐ + 1) ยท (๐ + 2))) = (2 ยท (((2
ยท ๐) + 3) / (๐ + 2)))) |
154 | 144, 153 | oveq12d 7380 |
. . . . . . . . 9
โข (๐ โ (((!โ((2 ยท
๐) + 1)) / ((!โ(๐ + 1)) ยท (!โ๐))) ยท ((((2 ยท
๐) + 2) ยท ((2
ยท ๐) + 3)) / ((๐ + 1) ยท (๐ + 2)))) = ((((2 ยท ๐) + 1)C๐) ยท (2 ยท (((2 ยท ๐) + 3) / (๐ + 2))))) |
155 | 129, 154 | eqtrd 2777 |
. . . . . . . 8
โข (๐ โ (((!โ((2 ยท
๐) + 1)) ยท (((2
ยท ๐) + 2) ยท
((2 ยท ๐) + 3))) /
(((!โ(๐ + 1))
ยท (!โ๐))
ยท ((๐ + 1) ยท
(๐ + 2)))) = ((((2 ยท
๐) + 1)C๐) ยท (2 ยท (((2 ยท ๐) + 3) / (๐ + 2))))) |
156 | 104, 155 | eqtrd 2777 |
. . . . . . 7
โข (๐ โ (((!โ((2 ยท
๐) + 1)) ยท (((2
ยท ๐) + 2) ยท
((2 ยท ๐) + 3))) /
((!โ(๐ + 1)) ยท
((!โ๐) ยท
((๐ + 1) ยท (๐ + 2))))) = ((((2 ยท ๐) + 1)C๐) ยท (2 ยท (((2 ยท ๐) + 3) / (๐ + 2))))) |
157 | 96, 156 | eqtrd 2777 |
. . . . . 6
โข (๐ โ (((!โ((2 ยท
๐) + 1)) ยท (((2
ยท ๐) + 2) ยท
((2 ยท ๐) + 3))) /
((!โ(๐ + 1)) ยท
(!โ(๐ + 2)))) = ((((2
ยท ๐) + 1)C๐) ยท (2 ยท (((2
ยท ๐) + 3) / (๐ + 2))))) |
158 | 92, 157 | eqtrd 2777 |
. . . . 5
โข (๐ โ ((!โ((2 ยท
๐) + 3)) / ((!โ(๐ + 1)) ยท (!โ(๐ + 2)))) = ((((2 ยท ๐) + 1)C๐) ยท (2 ยท (((2 ยท ๐) + 3) / (๐ + 2))))) |
159 | 69, 158 | eqtrd 2777 |
. . . 4
โข (๐ โ ((!โ((2 ยท
๐) + 3)) / ((!โ(๐ + 2)) ยท (!โ(๐ + 1)))) = ((((2 ยท ๐) + 1)C๐) ยท (2 ยท (((2 ยท ๐) + 3) / (๐ + 2))))) |
160 | 57, 159 | eqtrd 2777 |
. . 3
โข (๐ โ ((!โ((2 ยท
๐) + 3)) / ((!โ(((2
ยท ๐) + 3) โ
(๐ + 1))) ยท
(!โ(๐ + 1)))) = ((((2
ยท ๐) + 1)C๐) ยท (2 ยท (((2
ยท ๐) + 3) / (๐ + 2))))) |
161 | 46, 160 | eqtrd 2777 |
. 2
โข (๐ โ (((2 ยท ๐) + 3)C(๐ + 1)) = ((((2 ยท ๐) + 1)C๐) ยท (2 ยท (((2 ยท ๐) + 3) / (๐ + 2))))) |
162 | 17, 161 | eqtrd 2777 |
1
โข (๐ โ (((2 ยท (๐ + 1)) + 1)C(๐ + 1)) = ((((2 ยท ๐) + 1)C๐) ยท (2 ยท (((2 ยท ๐) + 3) / (๐ + 2))))) |