Step | Hyp | Ref
| Expression |
1 | | 2nn 9079 |
. . 3
โข 2 โ
โ |
2 | | bcval5 10742 |
. . 3
โข ((๐ โ โ0
โง 2 โ โ) โ (๐C2) = ((seq((๐ โ 2) + 1)( ยท , I )โ๐) /
(!โ2))) |
3 | 1, 2 | mpan2 425 |
. 2
โข (๐ โ โ0
โ (๐C2) = ((seq((๐ โ 2) + 1)( ยท , I
)โ๐) /
(!โ2))) |
4 | | 2m1e1 9036 |
. . . . . . . 8
โข (2
โ 1) = 1 |
5 | 4 | oveq2i 5885 |
. . . . . . 7
โข ((๐ โ 2) + (2 โ 1)) =
((๐ โ 2) +
1) |
6 | | nn0cn 9185 |
. . . . . . . 8
โข (๐ โ โ0
โ ๐ โ
โ) |
7 | | 2cn 8989 |
. . . . . . . . 9
โข 2 โ
โ |
8 | | ax-1cn 7903 |
. . . . . . . . 9
โข 1 โ
โ |
9 | | npncan 8177 |
. . . . . . . . 9
โข ((๐ โ โ โง 2 โ
โ โง 1 โ โ) โ ((๐ โ 2) + (2 โ 1)) = (๐ โ 1)) |
10 | 7, 8, 9 | mp3an23 1329 |
. . . . . . . 8
โข (๐ โ โ โ ((๐ โ 2) + (2 โ 1)) =
(๐ โ
1)) |
11 | 6, 10 | syl 14 |
. . . . . . 7
โข (๐ โ โ0
โ ((๐ โ 2) + (2
โ 1)) = (๐ โ
1)) |
12 | 5, 11 | eqtr3id 2224 |
. . . . . 6
โข (๐ โ โ0
โ ((๐ โ 2) + 1)
= (๐ โ
1)) |
13 | 12 | seqeq1d 10450 |
. . . . 5
โข (๐ โ โ0
โ seq((๐ โ 2) +
1)( ยท , I ) = seq(๐
โ 1)( ยท , I )) |
14 | 13 | fveq1d 5517 |
. . . 4
โข (๐ โ โ0
โ (seq((๐ โ 2) +
1)( ยท , I )โ๐)
= (seq(๐ โ 1)(
ยท , I )โ๐)) |
15 | | nn0z 9272 |
. . . . . . . 8
โข (๐ โ โ0
โ ๐ โ
โค) |
16 | | peano2zm 9290 |
. . . . . . . 8
โข (๐ โ โค โ (๐ โ 1) โ
โค) |
17 | 15, 16 | syl 14 |
. . . . . . 7
โข (๐ โ โ0
โ (๐ โ 1) โ
โค) |
18 | | uzid 9541 |
. . . . . . . . 9
โข (๐ โ โค โ ๐ โ
(โคโฅโ๐)) |
19 | 15, 18 | syl 14 |
. . . . . . . 8
โข (๐ โ โ0
โ ๐ โ
(โคโฅโ๐)) |
20 | | npcan 8165 |
. . . . . . . . . 10
โข ((๐ โ โ โง 1 โ
โ) โ ((๐ โ
1) + 1) = ๐) |
21 | 6, 8, 20 | sylancl 413 |
. . . . . . . . 9
โข (๐ โ โ0
โ ((๐ โ 1) + 1)
= ๐) |
22 | 21 | fveq2d 5519 |
. . . . . . . 8
โข (๐ โ โ0
โ (โคโฅโ((๐ โ 1) + 1)) =
(โคโฅโ๐)) |
23 | 19, 22 | eleqtrrd 2257 |
. . . . . . 7
โข (๐ โ โ0
โ ๐ โ
(โคโฅโ((๐ โ 1) + 1))) |
24 | | eluzelcn 9538 |
. . . . . . . . 9
โข (๐ฅ โ
(โคโฅโ(๐ โ 1)) โ ๐ฅ โ โ) |
25 | 24 | adantl 277 |
. . . . . . . 8
โข ((๐ โ โ0
โง ๐ฅ โ
(โคโฅโ(๐ โ 1))) โ ๐ฅ โ โ) |
26 | | fvi 5573 |
. . . . . . . . . 10
โข (๐ฅ โ โ โ ( I
โ๐ฅ) = ๐ฅ) |
27 | 26 | eleq1d 2246 |
. . . . . . . . 9
โข (๐ฅ โ โ โ (( I
โ๐ฅ) โ โ
โ ๐ฅ โ
โ)) |
28 | 27 | ibir 177 |
. . . . . . . 8
โข (๐ฅ โ โ โ ( I
โ๐ฅ) โ
โ) |
29 | 25, 28 | syl 14 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ฅ โ
(โคโฅโ(๐ โ 1))) โ ( I โ๐ฅ) โ
โ) |
30 | | mulcl 7937 |
. . . . . . . 8
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐ฅ ยท ๐ฆ) โ โ) |
31 | 30 | adantl 277 |
. . . . . . 7
โข ((๐ โ โ0
โง (๐ฅ โ โ
โง ๐ฆ โ โ))
โ (๐ฅ ยท ๐ฆ) โ
โ) |
32 | 17, 23, 29, 31 | seq3m1 10467 |
. . . . . 6
โข (๐ โ โ0
โ (seq(๐ โ 1)(
ยท , I )โ๐) =
((seq(๐ โ 1)(
ยท , I )โ(๐
โ 1)) ยท ( I โ๐))) |
33 | 17, 29, 31 | seq3-1 10459 |
. . . . . . . 8
โข (๐ โ โ0
โ (seq(๐ โ 1)(
ยท , I )โ(๐
โ 1)) = ( I โ(๐
โ 1))) |
34 | | fvi 5573 |
. . . . . . . . 9
โข ((๐ โ 1) โ โค
โ ( I โ(๐
โ 1)) = (๐ โ
1)) |
35 | 17, 34 | syl 14 |
. . . . . . . 8
โข (๐ โ โ0
โ ( I โ(๐
โ 1)) = (๐ โ
1)) |
36 | 33, 35 | eqtrd 2210 |
. . . . . . 7
โข (๐ โ โ0
โ (seq(๐ โ 1)(
ยท , I )โ(๐
โ 1)) = (๐ โ
1)) |
37 | | fvi 5573 |
. . . . . . 7
โข (๐ โ โ0
โ ( I โ๐) =
๐) |
38 | 36, 37 | oveq12d 5892 |
. . . . . 6
โข (๐ โ โ0
โ ((seq(๐ โ 1)(
ยท , I )โ(๐
โ 1)) ยท ( I โ๐)) = ((๐ โ 1) ยท ๐)) |
39 | 32, 38 | eqtrd 2210 |
. . . . 5
โข (๐ โ โ0
โ (seq(๐ โ 1)(
ยท , I )โ๐) =
((๐ โ 1) ยท
๐)) |
40 | | subcl 8155 |
. . . . . . 7
โข ((๐ โ โ โง 1 โ
โ) โ (๐ โ
1) โ โ) |
41 | 6, 8, 40 | sylancl 413 |
. . . . . 6
โข (๐ โ โ0
โ (๐ โ 1) โ
โ) |
42 | 41, 6 | mulcomd 7978 |
. . . . 5
โข (๐ โ โ0
โ ((๐ โ 1)
ยท ๐) = (๐ ยท (๐ โ 1))) |
43 | 39, 42 | eqtrd 2210 |
. . . 4
โข (๐ โ โ0
โ (seq(๐ โ 1)(
ยท , I )โ๐) =
(๐ ยท (๐ โ 1))) |
44 | 14, 43 | eqtrd 2210 |
. . 3
โข (๐ โ โ0
โ (seq((๐ โ 2) +
1)( ยท , I )โ๐)
= (๐ ยท (๐ โ 1))) |
45 | | fac2 10710 |
. . . 4
โข
(!โ2) = 2 |
46 | 45 | a1i 9 |
. . 3
โข (๐ โ โ0
โ (!โ2) = 2) |
47 | 44, 46 | oveq12d 5892 |
. 2
โข (๐ โ โ0
โ ((seq((๐ โ 2)
+ 1)( ยท , I )โ๐) / (!โ2)) = ((๐ ยท (๐ โ 1)) / 2)) |
48 | 3, 47 | eqtrd 2210 |
1
โข (๐ โ โ0
โ (๐C2) = ((๐ ยท (๐ โ 1)) / 2)) |