Step | Hyp | Ref
| Expression |
1 | | 2nn 12231 |
. . 3
โข 2 โ
โ |
2 | | bcval5 14224 |
. . 3
โข ((๐ โ โ0
โง 2 โ โ) โ (๐C2) = ((seq((๐ โ 2) + 1)( ยท , I )โ๐) /
(!โ2))) |
3 | 1, 2 | mpan2 690 |
. 2
โข (๐ โ โ0
โ (๐C2) = ((seq((๐ โ 2) + 1)( ยท , I
)โ๐) /
(!โ2))) |
4 | | 2m1e1 12284 |
. . . . . . . 8
โข (2
โ 1) = 1 |
5 | 4 | oveq2i 7369 |
. . . . . . 7
โข ((๐ โ 2) + (2 โ 1)) =
((๐ โ 2) +
1) |
6 | | nn0cn 12428 |
. . . . . . . 8
โข (๐ โ โ0
โ ๐ โ
โ) |
7 | | 2cn 12233 |
. . . . . . . . 9
โข 2 โ
โ |
8 | | ax-1cn 11114 |
. . . . . . . . 9
โข 1 โ
โ |
9 | | npncan 11427 |
. . . . . . . . 9
โข ((๐ โ โ โง 2 โ
โ โง 1 โ โ) โ ((๐ โ 2) + (2 โ 1)) = (๐ โ 1)) |
10 | 7, 8, 9 | mp3an23 1454 |
. . . . . . . 8
โข (๐ โ โ โ ((๐ โ 2) + (2 โ 1)) =
(๐ โ
1)) |
11 | 6, 10 | syl 17 |
. . . . . . 7
โข (๐ โ โ0
โ ((๐ โ 2) + (2
โ 1)) = (๐ โ
1)) |
12 | 5, 11 | eqtr3id 2787 |
. . . . . 6
โข (๐ โ โ0
โ ((๐ โ 2) + 1)
= (๐ โ
1)) |
13 | 12 | seqeq1d 13918 |
. . . . 5
โข (๐ โ โ0
โ seq((๐ โ 2) +
1)( ยท , I ) = seq(๐
โ 1)( ยท , I )) |
14 | 13 | fveq1d 6845 |
. . . 4
โข (๐ โ โ0
โ (seq((๐ โ 2) +
1)( ยท , I )โ๐)
= (seq(๐ โ 1)(
ยท , I )โ๐)) |
15 | | nn0z 12529 |
. . . . . . . 8
โข (๐ โ โ0
โ ๐ โ
โค) |
16 | | peano2zm 12551 |
. . . . . . . 8
โข (๐ โ โค โ (๐ โ 1) โ
โค) |
17 | 15, 16 | syl 17 |
. . . . . . 7
โข (๐ โ โ0
โ (๐ โ 1) โ
โค) |
18 | | uzid 12783 |
. . . . . . . . 9
โข (๐ โ โค โ ๐ โ
(โคโฅโ๐)) |
19 | 15, 18 | syl 17 |
. . . . . . . 8
โข (๐ โ โ0
โ ๐ โ
(โคโฅโ๐)) |
20 | | npcan 11415 |
. . . . . . . . . 10
โข ((๐ โ โ โง 1 โ
โ) โ ((๐ โ
1) + 1) = ๐) |
21 | 6, 8, 20 | sylancl 587 |
. . . . . . . . 9
โข (๐ โ โ0
โ ((๐ โ 1) + 1)
= ๐) |
22 | 21 | fveq2d 6847 |
. . . . . . . 8
โข (๐ โ โ0
โ (โคโฅโ((๐ โ 1) + 1)) =
(โคโฅโ๐)) |
23 | 19, 22 | eleqtrrd 2837 |
. . . . . . 7
โข (๐ โ โ0
โ ๐ โ
(โคโฅโ((๐ โ 1) + 1))) |
24 | | seqm1 13931 |
. . . . . . 7
โข (((๐ โ 1) โ โค โง
๐ โ
(โคโฅโ((๐ โ 1) + 1))) โ (seq(๐ โ 1)( ยท , I
)โ๐) = ((seq(๐ โ 1)( ยท , I
)โ(๐ โ 1))
ยท ( I โ๐))) |
25 | 17, 23, 24 | syl2anc 585 |
. . . . . 6
โข (๐ โ โ0
โ (seq(๐ โ 1)(
ยท , I )โ๐) =
((seq(๐ โ 1)(
ยท , I )โ(๐
โ 1)) ยท ( I โ๐))) |
26 | | seq1 13925 |
. . . . . . . . 9
โข ((๐ โ 1) โ โค
โ (seq(๐ โ 1)(
ยท , I )โ(๐
โ 1)) = ( I โ(๐
โ 1))) |
27 | 17, 26 | syl 17 |
. . . . . . . 8
โข (๐ โ โ0
โ (seq(๐ โ 1)(
ยท , I )โ(๐
โ 1)) = ( I โ(๐
โ 1))) |
28 | | fvi 6918 |
. . . . . . . . 9
โข ((๐ โ 1) โ โค
โ ( I โ(๐
โ 1)) = (๐ โ
1)) |
29 | 17, 28 | syl 17 |
. . . . . . . 8
โข (๐ โ โ0
โ ( I โ(๐
โ 1)) = (๐ โ
1)) |
30 | 27, 29 | eqtrd 2773 |
. . . . . . 7
โข (๐ โ โ0
โ (seq(๐ โ 1)(
ยท , I )โ(๐
โ 1)) = (๐ โ
1)) |
31 | | fvi 6918 |
. . . . . . 7
โข (๐ โ โ0
โ ( I โ๐) =
๐) |
32 | 30, 31 | oveq12d 7376 |
. . . . . 6
โข (๐ โ โ0
โ ((seq(๐ โ 1)(
ยท , I )โ(๐
โ 1)) ยท ( I โ๐)) = ((๐ โ 1) ยท ๐)) |
33 | 25, 32 | eqtrd 2773 |
. . . . 5
โข (๐ โ โ0
โ (seq(๐ โ 1)(
ยท , I )โ๐) =
((๐ โ 1) ยท
๐)) |
34 | | subcl 11405 |
. . . . . . 7
โข ((๐ โ โ โง 1 โ
โ) โ (๐ โ
1) โ โ) |
35 | 6, 8, 34 | sylancl 587 |
. . . . . 6
โข (๐ โ โ0
โ (๐ โ 1) โ
โ) |
36 | 35, 6 | mulcomd 11181 |
. . . . 5
โข (๐ โ โ0
โ ((๐ โ 1)
ยท ๐) = (๐ ยท (๐ โ 1))) |
37 | 33, 36 | eqtrd 2773 |
. . . 4
โข (๐ โ โ0
โ (seq(๐ โ 1)(
ยท , I )โ๐) =
(๐ ยท (๐ โ 1))) |
38 | 14, 37 | eqtrd 2773 |
. . 3
โข (๐ โ โ0
โ (seq((๐ โ 2) +
1)( ยท , I )โ๐)
= (๐ ยท (๐ โ 1))) |
39 | | fac2 14185 |
. . . 4
โข
(!โ2) = 2 |
40 | 39 | a1i 11 |
. . 3
โข (๐ โ โ0
โ (!โ2) = 2) |
41 | 38, 40 | oveq12d 7376 |
. 2
โข (๐ โ โ0
โ ((seq((๐ โ 2)
+ 1)( ยท , I )โ๐) / (!โ2)) = ((๐ ยท (๐ โ 1)) / 2)) |
42 | 3, 41 | eqtrd 2773 |
1
โข (๐ โ โ0
โ (๐C2) = ((๐ ยท (๐ โ 1)) / 2)) |