Step | Hyp | Ref
| Expression |
1 | | 0zd 12518 |
. . . . . . . . . . . 12
โข (๐ โ 0 โ
โค) |
2 | | 2z 12542 |
. . . . . . . . . . . . . . 15
โข 2 โ
โค |
3 | 2 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ 2 โ
โค) |
4 | | lcmineqlem18.1 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ โ โ) |
5 | 4 | nnzd 12533 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ โ โค) |
6 | 3, 5 | zmulcld 12620 |
. . . . . . . . . . . . 13
โข (๐ โ (2 ยท ๐) โ
โค) |
7 | 6 | peano2zd 12617 |
. . . . . . . . . . . 12
โข (๐ โ ((2 ยท ๐) + 1) โ
โค) |
8 | 5 | peano2zd 12617 |
. . . . . . . . . . . 12
โข (๐ โ (๐ + 1) โ โค) |
9 | 4 | nnred 12175 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ โ) |
10 | | 1red 11163 |
. . . . . . . . . . . . 13
โข (๐ โ 1 โ
โ) |
11 | 4 | nnnn0d 12480 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ โ
โ0) |
12 | 11 | nn0ge0d 12483 |
. . . . . . . . . . . . 13
โข (๐ โ 0 โค ๐) |
13 | | 0le1 11685 |
. . . . . . . . . . . . . 14
โข 0 โค
1 |
14 | 13 | a1i 11 |
. . . . . . . . . . . . 13
โข (๐ โ 0 โค 1) |
15 | 9, 10, 12, 14 | addge0d 11738 |
. . . . . . . . . . . 12
โข (๐ โ 0 โค (๐ + 1)) |
16 | 9, 10 | readdcld 11191 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ + 1) โ โ) |
17 | 16, 9 | addge01d 11750 |
. . . . . . . . . . . . . 14
โข (๐ โ (0 โค ๐ โ (๐ + 1) โค ((๐ + 1) + ๐))) |
18 | 12, 17 | mpbid 231 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ + 1) โค ((๐ + 1) + ๐)) |
19 | 9 | recnd 11190 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ โ โ) |
20 | | 1cnd 11157 |
. . . . . . . . . . . . . . 15
โข (๐ โ 1 โ
โ) |
21 | 19, 20, 19 | add32d 11389 |
. . . . . . . . . . . . . 14
โข (๐ โ ((๐ + 1) + ๐) = ((๐ + ๐) + 1)) |
22 | 19 | 2timesd 12403 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (2 ยท ๐) = (๐ + ๐)) |
23 | 22 | oveq1d 7377 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((2 ยท ๐) + 1) = ((๐ + ๐) + 1)) |
24 | 23 | eqcomd 2743 |
. . . . . . . . . . . . . 14
โข (๐ โ ((๐ + ๐) + 1) = ((2 ยท ๐) + 1)) |
25 | 21, 24 | eqtrd 2777 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ + 1) + ๐) = ((2 ยท ๐) + 1)) |
26 | 18, 25 | breqtrd 5136 |
. . . . . . . . . . . 12
โข (๐ โ (๐ + 1) โค ((2 ยท ๐) + 1)) |
27 | 1, 7, 8, 15, 26 | elfzd 13439 |
. . . . . . . . . . 11
โข (๐ โ (๐ + 1) โ (0...((2 ยท ๐) + 1))) |
28 | | bcval2 14212 |
. . . . . . . . . . 11
โข ((๐ + 1) โ (0...((2 ยท
๐) + 1)) โ (((2
ยท ๐) + 1)C(๐ + 1)) = ((!โ((2 ยท
๐) + 1)) / ((!โ(((2
ยท ๐) + 1) โ
(๐ + 1))) ยท
(!โ(๐ +
1))))) |
29 | 27, 28 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (((2 ยท ๐) + 1)C(๐ + 1)) = ((!โ((2 ยท ๐) + 1)) / ((!โ(((2
ยท ๐) + 1) โ
(๐ + 1))) ยท
(!โ(๐ +
1))))) |
30 | 6 | zcnd 12615 |
. . . . . . . . . . . . . . 15
โข (๐ โ (2 ยท ๐) โ
โ) |
31 | 30, 20, 19, 20 | addsub4d 11566 |
. . . . . . . . . . . . . 14
โข (๐ โ (((2 ยท ๐) + 1) โ (๐ + 1)) = (((2 ยท ๐) โ ๐) + (1 โ 1))) |
32 | 22 | oveq1d 7377 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((2 ยท ๐) โ ๐) = ((๐ + ๐) โ ๐)) |
33 | 19, 19 | pncand 11520 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((๐ + ๐) โ ๐) = ๐) |
34 | 32, 33 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ((2 ยท ๐) โ ๐) = ๐) |
35 | | 1m1e0 12232 |
. . . . . . . . . . . . . . . . 17
โข (1
โ 1) = 0 |
36 | 35 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (1 โ 1) =
0) |
37 | 34, 36 | oveq12d 7380 |
. . . . . . . . . . . . . . 15
โข (๐ โ (((2 ยท ๐) โ ๐) + (1 โ 1)) = (๐ + 0)) |
38 | 19 | addid1d 11362 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ + 0) = ๐) |
39 | 37, 38 | eqtrd 2777 |
. . . . . . . . . . . . . 14
โข (๐ โ (((2 ยท ๐) โ ๐) + (1 โ 1)) = ๐) |
40 | 31, 39 | eqtrd 2777 |
. . . . . . . . . . . . 13
โข (๐ โ (((2 ยท ๐) + 1) โ (๐ + 1)) = ๐) |
41 | 40 | fveq2d 6851 |
. . . . . . . . . . . 12
โข (๐ โ (!โ(((2 ยท
๐) + 1) โ (๐ + 1))) = (!โ๐)) |
42 | 41 | oveq1d 7377 |
. . . . . . . . . . 11
โข (๐ โ ((!โ(((2 ยท
๐) + 1) โ (๐ + 1))) ยท (!โ(๐ + 1))) = ((!โ๐) ยท (!โ(๐ + 1)))) |
43 | 42 | oveq2d 7378 |
. . . . . . . . . 10
โข (๐ โ ((!โ((2 ยท
๐) + 1)) / ((!โ(((2
ยท ๐) + 1) โ
(๐ + 1))) ยท
(!โ(๐ + 1)))) =
((!โ((2 ยท ๐) +
1)) / ((!โ๐) ยท
(!โ(๐ +
1))))) |
44 | 29, 43 | eqtrd 2777 |
. . . . . . . . 9
โข (๐ โ (((2 ยท ๐) + 1)C(๐ + 1)) = ((!โ((2 ยท ๐) + 1)) / ((!โ๐) ยท (!โ(๐ + 1))))) |
45 | | faccl 14190 |
. . . . . . . . . . . . . 14
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
46 | 11, 45 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ (!โ๐) โ โ) |
47 | 46 | nncnd 12176 |
. . . . . . . . . . . 12
โข (๐ โ (!โ๐) โ โ) |
48 | | 1nn0 12436 |
. . . . . . . . . . . . . . . 16
โข 1 โ
โ0 |
49 | 48 | a1i 11 |
. . . . . . . . . . . . . . 15
โข (๐ โ 1 โ
โ0) |
50 | 11, 49 | nn0addcld 12484 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ + 1) โ
โ0) |
51 | | faccl 14190 |
. . . . . . . . . . . . . 14
โข ((๐ + 1) โ โ0
โ (!โ(๐ + 1))
โ โ) |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ (!โ(๐ + 1)) โ
โ) |
53 | 52 | nncnd 12176 |
. . . . . . . . . . . 12
โข (๐ โ (!โ(๐ + 1)) โ
โ) |
54 | 47, 53 | mulcomd 11183 |
. . . . . . . . . . 11
โข (๐ โ ((!โ๐) ยท (!โ(๐ + 1))) = ((!โ(๐ + 1)) ยท (!โ๐))) |
55 | | facp1 14185 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ0
โ (!โ(๐ + 1)) =
((!โ๐) ยท
(๐ + 1))) |
56 | 11, 55 | syl 17 |
. . . . . . . . . . . . . 14
โข (๐ โ (!โ(๐ + 1)) = ((!โ๐) ยท (๐ + 1))) |
57 | 19, 20 | addcld 11181 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ + 1) โ โ) |
58 | 47, 57 | mulcomd 11183 |
. . . . . . . . . . . . . 14
โข (๐ โ ((!โ๐) ยท (๐ + 1)) = ((๐ + 1) ยท (!โ๐))) |
59 | 56, 58 | eqtrd 2777 |
. . . . . . . . . . . . 13
โข (๐ โ (!โ(๐ + 1)) = ((๐ + 1) ยท (!โ๐))) |
60 | 59 | oveq1d 7377 |
. . . . . . . . . . . 12
โข (๐ โ ((!โ(๐ + 1)) ยท (!โ๐)) = (((๐ + 1) ยท (!โ๐)) ยท (!โ๐))) |
61 | 57, 47, 47 | mulassd 11185 |
. . . . . . . . . . . 12
โข (๐ โ (((๐ + 1) ยท (!โ๐)) ยท (!โ๐)) = ((๐ + 1) ยท ((!โ๐) ยท (!โ๐)))) |
62 | 60, 61 | eqtrd 2777 |
. . . . . . . . . . 11
โข (๐ โ ((!โ(๐ + 1)) ยท (!โ๐)) = ((๐ + 1) ยท ((!โ๐) ยท (!โ๐)))) |
63 | 54, 62 | eqtrd 2777 |
. . . . . . . . . 10
โข (๐ โ ((!โ๐) ยท (!โ(๐ + 1))) = ((๐ + 1) ยท ((!โ๐) ยท (!โ๐)))) |
64 | 63 | oveq2d 7378 |
. . . . . . . . 9
โข (๐ โ ((!โ((2 ยท
๐) + 1)) / ((!โ๐) ยท (!โ(๐ + 1)))) = ((!โ((2
ยท ๐) + 1)) / ((๐ + 1) ยท ((!โ๐) ยท (!โ๐))))) |
65 | 44, 64 | eqtrd 2777 |
. . . . . . . 8
โข (๐ โ (((2 ยท ๐) + 1)C(๐ + 1)) = ((!โ((2 ยท ๐) + 1)) / ((๐ + 1) ยท ((!โ๐) ยท (!โ๐))))) |
66 | | 2nn0 12437 |
. . . . . . . . . . . . 13
โข 2 โ
โ0 |
67 | 66 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ 2 โ
โ0) |
68 | 67, 11 | nn0mulcld 12485 |
. . . . . . . . . . 11
โข (๐ โ (2 ยท ๐) โ
โ0) |
69 | | facp1 14185 |
. . . . . . . . . . 11
โข ((2
ยท ๐) โ
โ0 โ (!โ((2 ยท ๐) + 1)) = ((!โ(2 ยท ๐)) ยท ((2 ยท ๐) + 1))) |
70 | 68, 69 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (!โ((2 ยท
๐) + 1)) = ((!โ(2
ยท ๐)) ยท ((2
ยท ๐) +
1))) |
71 | | faccl 14190 |
. . . . . . . . . . . . 13
โข ((2
ยท ๐) โ
โ0 โ (!โ(2 ยท ๐)) โ โ) |
72 | 68, 71 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ (!โ(2 ยท ๐)) โ
โ) |
73 | 72 | nncnd 12176 |
. . . . . . . . . . 11
โข (๐ โ (!โ(2 ยท ๐)) โ
โ) |
74 | 30, 20 | addcld 11181 |
. . . . . . . . . . 11
โข (๐ โ ((2 ยท ๐) + 1) โ
โ) |
75 | 73, 74 | mulcomd 11183 |
. . . . . . . . . 10
โข (๐ โ ((!โ(2 ยท
๐)) ยท ((2 ยท
๐) + 1)) = (((2 ยท
๐) + 1) ยท
(!โ(2 ยท ๐)))) |
76 | 70, 75 | eqtrd 2777 |
. . . . . . . . 9
โข (๐ โ (!โ((2 ยท
๐) + 1)) = (((2 ยท
๐) + 1) ยท
(!โ(2 ยท ๐)))) |
77 | 76 | oveq1d 7377 |
. . . . . . . 8
โข (๐ โ ((!โ((2 ยท
๐) + 1)) / ((๐ + 1) ยท ((!โ๐) ยท (!โ๐)))) = ((((2 ยท ๐) + 1) ยท (!โ(2
ยท ๐))) / ((๐ + 1) ยท ((!โ๐) ยท (!โ๐))))) |
78 | 65, 77 | eqtrd 2777 |
. . . . . . 7
โข (๐ โ (((2 ยท ๐) + 1)C(๐ + 1)) = ((((2 ยท ๐) + 1) ยท (!โ(2 ยท ๐))) / ((๐ + 1) ยท ((!โ๐) ยท (!โ๐))))) |
79 | 78 | oveq2d 7378 |
. . . . . 6
โข (๐ โ ((๐ + 1) ยท (((2 ยท ๐) + 1)C(๐ + 1))) = ((๐ + 1) ยท ((((2 ยท ๐) + 1) ยท (!โ(2
ยท ๐))) / ((๐ + 1) ยท ((!โ๐) ยท (!โ๐)))))) |
80 | 74, 73 | mulcld 11182 |
. . . . . . . 8
โข (๐ โ (((2 ยท ๐) + 1) ยท (!โ(2
ยท ๐))) โ
โ) |
81 | 47, 47 | mulcld 11182 |
. . . . . . . . 9
โข (๐ โ ((!โ๐) ยท (!โ๐)) โ
โ) |
82 | 57, 81 | mulcld 11182 |
. . . . . . . 8
โข (๐ โ ((๐ + 1) ยท ((!โ๐) ยท (!โ๐))) โ โ) |
83 | 4 | peano2nnd 12177 |
. . . . . . . . . 10
โข (๐ โ (๐ + 1) โ โ) |
84 | 83 | nnne0d 12210 |
. . . . . . . . 9
โข (๐ โ (๐ + 1) โ 0) |
85 | 46 | nnne0d 12210 |
. . . . . . . . . 10
โข (๐ โ (!โ๐) โ 0) |
86 | 47, 47, 85, 85 | mulne0d 11814 |
. . . . . . . . 9
โข (๐ โ ((!โ๐) ยท (!โ๐)) โ 0) |
87 | 57, 81, 84, 86 | mulne0d 11814 |
. . . . . . . 8
โข (๐ โ ((๐ + 1) ยท ((!โ๐) ยท (!โ๐))) โ 0) |
88 | 57, 80, 82, 87 | divassd 11973 |
. . . . . . 7
โข (๐ โ (((๐ + 1) ยท (((2 ยท ๐) + 1) ยท (!โ(2
ยท ๐)))) / ((๐ + 1) ยท ((!โ๐) ยท (!โ๐)))) = ((๐ + 1) ยท ((((2 ยท ๐) + 1) ยท (!โ(2
ยท ๐))) / ((๐ + 1) ยท ((!โ๐) ยท (!โ๐)))))) |
89 | 88 | eqcomd 2743 |
. . . . . 6
โข (๐ โ ((๐ + 1) ยท ((((2 ยท ๐) + 1) ยท (!โ(2
ยท ๐))) / ((๐ + 1) ยท ((!โ๐) ยท (!โ๐))))) = (((๐ + 1) ยท (((2 ยท ๐) + 1) ยท (!โ(2
ยท ๐)))) / ((๐ + 1) ยท ((!โ๐) ยท (!โ๐))))) |
90 | 79, 89 | eqtrd 2777 |
. . . . 5
โข (๐ โ ((๐ + 1) ยท (((2 ยท ๐) + 1)C(๐ + 1))) = (((๐ + 1) ยท (((2 ยท ๐) + 1) ยท (!โ(2
ยท ๐)))) / ((๐ + 1) ยท ((!โ๐) ยท (!โ๐))))) |
91 | 57, 57, 80, 81, 84, 86 | divmuldivd 11979 |
. . . . . 6
โข (๐ โ (((๐ + 1) / (๐ + 1)) ยท ((((2 ยท ๐) + 1) ยท (!โ(2
ยท ๐))) /
((!โ๐) ยท
(!โ๐)))) = (((๐ + 1) ยท (((2 ยท
๐) + 1) ยท
(!โ(2 ยท ๐))))
/ ((๐ + 1) ยท
((!โ๐) ยท
(!โ๐))))) |
92 | 91 | eqcomd 2743 |
. . . . 5
โข (๐ โ (((๐ + 1) ยท (((2 ยท ๐) + 1) ยท (!โ(2
ยท ๐)))) / ((๐ + 1) ยท ((!โ๐) ยท (!โ๐)))) = (((๐ + 1) / (๐ + 1)) ยท ((((2 ยท ๐) + 1) ยท (!โ(2
ยท ๐))) /
((!โ๐) ยท
(!โ๐))))) |
93 | 90, 92 | eqtrd 2777 |
. . . 4
โข (๐ โ ((๐ + 1) ยท (((2 ยท ๐) + 1)C(๐ + 1))) = (((๐ + 1) / (๐ + 1)) ยท ((((2 ยท ๐) + 1) ยท (!โ(2
ยท ๐))) /
((!โ๐) ยท
(!โ๐))))) |
94 | 57, 84 | dividd 11936 |
. . . . . 6
โข (๐ โ ((๐ + 1) / (๐ + 1)) = 1) |
95 | 94 | oveq1d 7377 |
. . . . 5
โข (๐ โ (((๐ + 1) / (๐ + 1)) ยท ((((2 ยท ๐) + 1) ยท (!โ(2
ยท ๐))) /
((!โ๐) ยท
(!โ๐)))) = (1
ยท ((((2 ยท ๐)
+ 1) ยท (!โ(2 ยท ๐))) / ((!โ๐) ยท (!โ๐))))) |
96 | 80, 81, 86 | divcld 11938 |
. . . . . 6
โข (๐ โ ((((2 ยท ๐) + 1) ยท (!โ(2
ยท ๐))) /
((!โ๐) ยท
(!โ๐))) โ
โ) |
97 | 96 | mulid2d 11180 |
. . . . 5
โข (๐ โ (1 ยท ((((2 ยท
๐) + 1) ยท
(!โ(2 ยท ๐))) /
((!โ๐) ยท
(!โ๐)))) = ((((2
ยท ๐) + 1) ยท
(!โ(2 ยท ๐))) /
((!โ๐) ยท
(!โ๐)))) |
98 | 95, 97 | eqtrd 2777 |
. . . 4
โข (๐ โ (((๐ + 1) / (๐ + 1)) ยท ((((2 ยท ๐) + 1) ยท (!โ(2
ยท ๐))) /
((!โ๐) ยท
(!โ๐)))) = ((((2
ยท ๐) + 1) ยท
(!โ(2 ยท ๐))) /
((!โ๐) ยท
(!โ๐)))) |
99 | 93, 98 | eqtrd 2777 |
. . 3
โข (๐ โ ((๐ + 1) ยท (((2 ยท ๐) + 1)C(๐ + 1))) = ((((2 ยท ๐) + 1) ยท (!โ(2 ยท ๐))) / ((!โ๐) ยท (!โ๐)))) |
100 | 74, 73, 81, 86 | divassd 11973 |
. . 3
โข (๐ โ ((((2 ยท ๐) + 1) ยท (!โ(2
ยท ๐))) /
((!โ๐) ยท
(!โ๐))) = (((2
ยท ๐) + 1) ยท
((!โ(2 ยท ๐)) /
((!โ๐) ยท
(!โ๐))))) |
101 | 99, 100 | eqtrd 2777 |
. 2
โข (๐ โ ((๐ + 1) ยท (((2 ยท ๐) + 1)C(๐ + 1))) = (((2 ยท ๐) + 1) ยท ((!โ(2 ยท ๐)) / ((!โ๐) ยท (!โ๐))))) |
102 | 9, 9 | addge01d 11750 |
. . . . . . . . 9
โข (๐ โ (0 โค ๐ โ ๐ โค (๐ + ๐))) |
103 | 22 | breq2d 5122 |
. . . . . . . . 9
โข (๐ โ (๐ โค (2 ยท ๐) โ ๐ โค (๐ + ๐))) |
104 | 102, 103 | bitr4d 282 |
. . . . . . . 8
โข (๐ โ (0 โค ๐ โ ๐ โค (2 ยท ๐))) |
105 | 12, 104 | mpbid 231 |
. . . . . . 7
โข (๐ โ ๐ โค (2 ยท ๐)) |
106 | 1, 6, 5, 12, 105 | elfzd 13439 |
. . . . . 6
โข (๐ โ ๐ โ (0...(2 ยท ๐))) |
107 | | bcval2 14212 |
. . . . . 6
โข (๐ โ (0...(2 ยท ๐)) โ ((2 ยท ๐)C๐) = ((!โ(2 ยท ๐)) / ((!โ((2 ยท ๐) โ ๐)) ยท (!โ๐)))) |
108 | 106, 107 | syl 17 |
. . . . 5
โข (๐ โ ((2 ยท ๐)C๐) = ((!โ(2 ยท ๐)) / ((!โ((2 ยท ๐) โ ๐)) ยท (!โ๐)))) |
109 | 34 | fveq2d 6851 |
. . . . . . 7
โข (๐ โ (!โ((2 ยท
๐) โ ๐)) = (!โ๐)) |
110 | 109 | oveq1d 7377 |
. . . . . 6
โข (๐ โ ((!โ((2 ยท
๐) โ ๐)) ยท (!โ๐)) = ((!โ๐) ยท (!โ๐))) |
111 | 110 | oveq2d 7378 |
. . . . 5
โข (๐ โ ((!โ(2 ยท
๐)) / ((!โ((2
ยท ๐) โ ๐)) ยท (!โ๐))) = ((!โ(2 ยท
๐)) / ((!โ๐) ยท (!โ๐)))) |
112 | 108, 111 | eqtrd 2777 |
. . . 4
โข (๐ โ ((2 ยท ๐)C๐) = ((!โ(2 ยท ๐)) / ((!โ๐) ยท (!โ๐)))) |
113 | 112 | oveq2d 7378 |
. . 3
โข (๐ โ (((2 ยท ๐) + 1) ยท ((2 ยท
๐)C๐)) = (((2 ยท ๐) + 1) ยท ((!โ(2 ยท ๐)) / ((!โ๐) ยท (!โ๐))))) |
114 | 113 | eqcomd 2743 |
. 2
โข (๐ โ (((2 ยท ๐) + 1) ยท ((!โ(2
ยท ๐)) /
((!โ๐) ยท
(!โ๐)))) = (((2
ยท ๐) + 1) ยท
((2 ยท ๐)C๐))) |
115 | 101, 114 | eqtrd 2777 |
1
โข (๐ โ ((๐ + 1) ยท (((2 ยท ๐) + 1)C(๐ + 1))) = (((2 ยท ๐) + 1) ยท ((2 ยท ๐)C๐))) |