Step | Hyp | Ref
| Expression |
1 | | oveq2 7413 |
. . . . 5
โข (๐ฅ = 0 โ (1...๐ฅ) = (1...0)) |
2 | 1 | sumeq1d 15653 |
. . . 4
โข (๐ฅ = 0 โ ฮฃ๐ โ (1...๐ฅ)ฮฃ๐ โ (1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) = ฮฃ๐ โ (1...0)ฮฃ๐ โ (1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1))) |
3 | 1 | sumeq1d 15653 |
. . . . . 6
โข (๐ฅ = 0 โ ฮฃ๐ โ (1...๐ฅ)๐ = ฮฃ๐ โ (1...0)๐) |
4 | 3 | oveq2d 7421 |
. . . . 5
โข (๐ฅ = 0 โ (1...ฮฃ๐ โ (1...๐ฅ)๐) = (1...ฮฃ๐ โ (1...0)๐)) |
5 | 4 | sumeq1d 15653 |
. . . 4
โข (๐ฅ = 0 โ ฮฃ๐ โ (1...ฮฃ๐ โ (1...๐ฅ)๐)((2 ยท ๐) โ 1) = ฮฃ๐ โ (1...ฮฃ๐ โ (1...0)๐)((2 ยท ๐) โ 1)) |
6 | 2, 5 | eqeq12d 2742 |
. . 3
โข (๐ฅ = 0 โ (ฮฃ๐ โ (1...๐ฅ)ฮฃ๐ โ (1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) = ฮฃ๐ โ (1...ฮฃ๐ โ (1...๐ฅ)๐)((2 ยท ๐) โ 1) โ ฮฃ๐ โ (1...0)ฮฃ๐ โ (1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) = ฮฃ๐ โ (1...ฮฃ๐ โ (1...0)๐)((2 ยท ๐) โ 1))) |
7 | | oveq2 7413 |
. . . . 5
โข (๐ฅ = ๐ฆ โ (1...๐ฅ) = (1...๐ฆ)) |
8 | 7 | sumeq1d 15653 |
. . . 4
โข (๐ฅ = ๐ฆ โ ฮฃ๐ โ (1...๐ฅ)ฮฃ๐ โ (1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) = ฮฃ๐ โ (1...๐ฆ)ฮฃ๐ โ (1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1))) |
9 | 7 | sumeq1d 15653 |
. . . . . 6
โข (๐ฅ = ๐ฆ โ ฮฃ๐ โ (1...๐ฅ)๐ = ฮฃ๐ โ (1...๐ฆ)๐) |
10 | 9 | oveq2d 7421 |
. . . . 5
โข (๐ฅ = ๐ฆ โ (1...ฮฃ๐ โ (1...๐ฅ)๐) = (1...ฮฃ๐ โ (1...๐ฆ)๐)) |
11 | 10 | sumeq1d 15653 |
. . . 4
โข (๐ฅ = ๐ฆ โ ฮฃ๐ โ (1...ฮฃ๐ โ (1...๐ฅ)๐)((2 ยท ๐) โ 1) = ฮฃ๐ โ (1...ฮฃ๐ โ (1...๐ฆ)๐)((2 ยท ๐) โ 1)) |
12 | 8, 11 | eqeq12d 2742 |
. . 3
โข (๐ฅ = ๐ฆ โ (ฮฃ๐ โ (1...๐ฅ)ฮฃ๐ โ (1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) = ฮฃ๐ โ (1...ฮฃ๐ โ (1...๐ฅ)๐)((2 ยท ๐) โ 1) โ ฮฃ๐ โ (1...๐ฆ)ฮฃ๐ โ (1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) = ฮฃ๐ โ (1...ฮฃ๐ โ (1...๐ฆ)๐)((2 ยท ๐) โ 1))) |
13 | | oveq2 7413 |
. . . . 5
โข (๐ฅ = (๐ฆ + 1) โ (1...๐ฅ) = (1...(๐ฆ + 1))) |
14 | 13 | sumeq1d 15653 |
. . . 4
โข (๐ฅ = (๐ฆ + 1) โ ฮฃ๐ โ (1...๐ฅ)ฮฃ๐ โ (1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) = ฮฃ๐ โ (1...(๐ฆ + 1))ฮฃ๐ โ (1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1))) |
15 | 13 | sumeq1d 15653 |
. . . . . 6
โข (๐ฅ = (๐ฆ + 1) โ ฮฃ๐ โ (1...๐ฅ)๐ = ฮฃ๐ โ (1...(๐ฆ + 1))๐) |
16 | 15 | oveq2d 7421 |
. . . . 5
โข (๐ฅ = (๐ฆ + 1) โ (1...ฮฃ๐ โ (1...๐ฅ)๐) = (1...ฮฃ๐ โ (1...(๐ฆ + 1))๐)) |
17 | 16 | sumeq1d 15653 |
. . . 4
โข (๐ฅ = (๐ฆ + 1) โ ฮฃ๐ โ (1...ฮฃ๐ โ (1...๐ฅ)๐)((2 ยท ๐) โ 1) = ฮฃ๐ โ (1...ฮฃ๐ โ (1...(๐ฆ + 1))๐)((2 ยท ๐) โ 1)) |
18 | 14, 17 | eqeq12d 2742 |
. . 3
โข (๐ฅ = (๐ฆ + 1) โ (ฮฃ๐ โ (1...๐ฅ)ฮฃ๐ โ (1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) = ฮฃ๐ โ (1...ฮฃ๐ โ (1...๐ฅ)๐)((2 ยท ๐) โ 1) โ ฮฃ๐ โ (1...(๐ฆ + 1))ฮฃ๐ โ (1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) = ฮฃ๐ โ (1...ฮฃ๐ โ (1...(๐ฆ + 1))๐)((2 ยท ๐) โ 1))) |
19 | | oveq2 7413 |
. . . . 5
โข (๐ฅ = ๐ โ (1...๐ฅ) = (1...๐)) |
20 | 19 | sumeq1d 15653 |
. . . 4
โข (๐ฅ = ๐ โ ฮฃ๐ โ (1...๐ฅ)ฮฃ๐ โ (1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) = ฮฃ๐ โ (1...๐)ฮฃ๐ โ (1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1))) |
21 | 19 | sumeq1d 15653 |
. . . . . 6
โข (๐ฅ = ๐ โ ฮฃ๐ โ (1...๐ฅ)๐ = ฮฃ๐ โ (1...๐)๐) |
22 | 21 | oveq2d 7421 |
. . . . 5
โข (๐ฅ = ๐ โ (1...ฮฃ๐ โ (1...๐ฅ)๐) = (1...ฮฃ๐ โ (1...๐)๐)) |
23 | 22 | sumeq1d 15653 |
. . . 4
โข (๐ฅ = ๐ โ ฮฃ๐ โ (1...ฮฃ๐ โ (1...๐ฅ)๐)((2 ยท ๐) โ 1) = ฮฃ๐ โ (1...ฮฃ๐ โ (1...๐)๐)((2 ยท ๐) โ 1)) |
24 | 20, 23 | eqeq12d 2742 |
. . 3
โข (๐ฅ = ๐ โ (ฮฃ๐ โ (1...๐ฅ)ฮฃ๐ โ (1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) = ฮฃ๐ โ (1...ฮฃ๐ โ (1...๐ฅ)๐)((2 ยท ๐) โ 1) โ ฮฃ๐ โ (1...๐)ฮฃ๐ โ (1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) = ฮฃ๐ โ (1...ฮฃ๐ โ (1...๐)๐)((2 ยท ๐) โ 1))) |
25 | | sum0 15673 |
. . . . 5
โข
ฮฃ๐ โ
โ
ฮฃ๐ โ
(1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) =
0 |
26 | | sum0 15673 |
. . . . 5
โข
ฮฃ๐ โ
โ
((2 ยท ๐)
โ 1) = 0 |
27 | 25, 26 | eqtr4i 2757 |
. . . 4
โข
ฮฃ๐ โ
โ
ฮฃ๐ โ
(1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) = ฮฃ๐ โ โ
((2 ยท
๐) โ
1) |
28 | | fz10 13528 |
. . . . 5
โข (1...0) =
โ
|
29 | 28 | sumeq1i 15650 |
. . . 4
โข
ฮฃ๐ โ
(1...0)ฮฃ๐ โ
(1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) = ฮฃ๐ โ โ
ฮฃ๐ โ (1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) |
30 | 28 | sumeq1i 15650 |
. . . . . . . 8
โข
ฮฃ๐ โ
(1...0)๐ = ฮฃ๐ โ โ
๐ |
31 | | sum0 15673 |
. . . . . . . 8
โข
ฮฃ๐ โ
โ
๐ =
0 |
32 | 30, 31 | eqtri 2754 |
. . . . . . 7
โข
ฮฃ๐ โ
(1...0)๐ =
0 |
33 | 32 | oveq2i 7416 |
. . . . . 6
โข
(1...ฮฃ๐ โ
(1...0)๐) =
(1...0) |
34 | 33, 28 | eqtri 2754 |
. . . . 5
โข
(1...ฮฃ๐ โ
(1...0)๐) =
โ
|
35 | 34 | sumeq1i 15650 |
. . . 4
โข
ฮฃ๐ โ
(1...ฮฃ๐ โ
(1...0)๐)((2 ยท ๐) โ 1) = ฮฃ๐ โ โ
((2 ยท
๐) โ
1) |
36 | 27, 29, 35 | 3eqtr4i 2764 |
. . 3
โข
ฮฃ๐ โ
(1...0)ฮฃ๐ โ
(1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) = ฮฃ๐ โ (1...ฮฃ๐ โ (1...0)๐)((2 ยท ๐) โ 1) |
37 | | simpr 484 |
. . . . . 6
โข ((๐ฆ โ โ0
โง ฮฃ๐ โ
(1...๐ฆ)ฮฃ๐ โ (1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) = ฮฃ๐ โ (1...ฮฃ๐ โ (1...๐ฆ)๐)((2 ยท ๐) โ 1)) โ ฮฃ๐ โ (1...๐ฆ)ฮฃ๐ โ (1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) = ฮฃ๐ โ (1...ฮฃ๐ โ (1...๐ฆ)๐)((2 ยท ๐) โ 1)) |
38 | | fzfid 13944 |
. . . . . . . . . . 11
โข (๐ฆ โ โ0
โ (1...๐ฆ) โ
Fin) |
39 | | elfznn 13536 |
. . . . . . . . . . . . 13
โข (๐ โ (1...๐ฆ) โ ๐ โ โ) |
40 | 39 | adantl 481 |
. . . . . . . . . . . 12
โข ((๐ฆ โ โ0
โง ๐ โ (1...๐ฆ)) โ ๐ โ โ) |
41 | 40 | nnnn0d 12536 |
. . . . . . . . . . 11
โข ((๐ฆ โ โ0
โง ๐ โ (1...๐ฆ)) โ ๐ โ โ0) |
42 | 38, 41 | fsumnn0cl 15688 |
. . . . . . . . . 10
โข (๐ฆ โ โ0
โ ฮฃ๐ โ
(1...๐ฆ)๐ โ โ0) |
43 | 42 | nn0zd 12588 |
. . . . . . . . 9
โข (๐ฆ โ โ0
โ ฮฃ๐ โ
(1...๐ฆ)๐ โ โค) |
44 | | nn0p1nn 12515 |
. . . . . . . . . . 11
โข
(ฮฃ๐ โ
(1...๐ฆ)๐ โ โ0 โ
(ฮฃ๐ โ (1...๐ฆ)๐ + 1) โ โ) |
45 | 42, 44 | syl 17 |
. . . . . . . . . 10
โข (๐ฆ โ โ0
โ (ฮฃ๐ โ
(1...๐ฆ)๐ + 1) โ โ) |
46 | 45 | nnzd 12589 |
. . . . . . . . 9
โข (๐ฆ โ โ0
โ (ฮฃ๐ โ
(1...๐ฆ)๐ + 1) โ โค) |
47 | | peano2nn0 12516 |
. . . . . . . . . . 11
โข (๐ฆ โ โ0
โ (๐ฆ + 1) โ
โ0) |
48 | 47 | nn0zd 12588 |
. . . . . . . . . 10
โข (๐ฆ โ โ0
โ (๐ฆ + 1) โ
โค) |
49 | 43, 48 | zaddcld 12674 |
. . . . . . . . 9
โข (๐ฆ โ โ0
โ (ฮฃ๐ โ
(1...๐ฆ)๐ + (๐ฆ + 1)) โ โค) |
50 | | 2cnd 12294 |
. . . . . . . . . . 11
โข ((๐ฆ โ โ0
โง ๐ โ
((ฮฃ๐ โ
(1...๐ฆ)๐ + 1)...(ฮฃ๐ โ (1...๐ฆ)๐ + (๐ฆ + 1)))) โ 2 โ
โ) |
51 | | elfzelz 13507 |
. . . . . . . . . . . . 13
โข (๐ โ ((ฮฃ๐ โ (1...๐ฆ)๐ + 1)...(ฮฃ๐ โ (1...๐ฆ)๐ + (๐ฆ + 1))) โ ๐ โ โค) |
52 | 51 | zcnd 12671 |
. . . . . . . . . . . 12
โข (๐ โ ((ฮฃ๐ โ (1...๐ฆ)๐ + 1)...(ฮฃ๐ โ (1...๐ฆ)๐ + (๐ฆ + 1))) โ ๐ โ โ) |
53 | 52 | adantl 481 |
. . . . . . . . . . 11
โข ((๐ฆ โ โ0
โง ๐ โ
((ฮฃ๐ โ
(1...๐ฆ)๐ + 1)...(ฮฃ๐ โ (1...๐ฆ)๐ + (๐ฆ + 1)))) โ ๐ โ โ) |
54 | 50, 53 | mulcld 11238 |
. . . . . . . . . 10
โข ((๐ฆ โ โ0
โง ๐ โ
((ฮฃ๐ โ
(1...๐ฆ)๐ + 1)...(ฮฃ๐ โ (1...๐ฆ)๐ + (๐ฆ + 1)))) โ (2 ยท ๐) โ
โ) |
55 | | 1cnd 11213 |
. . . . . . . . . 10
โข ((๐ฆ โ โ0
โง ๐ โ
((ฮฃ๐ โ
(1...๐ฆ)๐ + 1)...(ฮฃ๐ โ (1...๐ฆ)๐ + (๐ฆ + 1)))) โ 1 โ
โ) |
56 | 54, 55 | subcld 11575 |
. . . . . . . . 9
โข ((๐ฆ โ โ0
โง ๐ โ
((ฮฃ๐ โ
(1...๐ฆ)๐ + 1)...(ฮฃ๐ โ (1...๐ฆ)๐ + (๐ฆ + 1)))) โ ((2 ยท ๐) โ 1) โ
โ) |
57 | | oveq2 7413 |
. . . . . . . . . 10
โข (๐ = (๐ + ฮฃ๐ โ (1...๐ฆ)๐) โ (2 ยท ๐) = (2 ยท (๐ + ฮฃ๐ โ (1...๐ฆ)๐))) |
58 | 57 | oveq1d 7420 |
. . . . . . . . 9
โข (๐ = (๐ + ฮฃ๐ โ (1...๐ฆ)๐) โ ((2 ยท ๐) โ 1) = ((2 ยท (๐ + ฮฃ๐ โ (1...๐ฆ)๐)) โ 1)) |
59 | 43, 46, 49, 56, 58 | fsumshftm 15733 |
. . . . . . . 8
โข (๐ฆ โ โ0
โ ฮฃ๐ โ
((ฮฃ๐ โ
(1...๐ฆ)๐ + 1)...(ฮฃ๐ โ (1...๐ฆ)๐ + (๐ฆ + 1)))((2 ยท ๐) โ 1) = ฮฃ๐ โ (((ฮฃ๐ โ (1...๐ฆ)๐ + 1) โ ฮฃ๐ โ (1...๐ฆ)๐)...((ฮฃ๐ โ (1...๐ฆ)๐ + (๐ฆ + 1)) โ ฮฃ๐ โ (1...๐ฆ)๐))((2 ยท (๐ + ฮฃ๐ โ (1...๐ฆ)๐)) โ 1)) |
60 | | elfzelz 13507 |
. . . . . . . . . . . . . . 15
โข (๐ โ (1...๐ฆ) โ ๐ โ โค) |
61 | 60 | adantl 481 |
. . . . . . . . . . . . . 14
โข ((๐ฆ โ โ0
โง ๐ โ (1...๐ฆ)) โ ๐ โ โค) |
62 | 61 | zred 12670 |
. . . . . . . . . . . . 13
โข ((๐ฆ โ โ0
โง ๐ โ (1...๐ฆ)) โ ๐ โ โ) |
63 | 38, 62 | fsumrecl 15686 |
. . . . . . . . . . . 12
โข (๐ฆ โ โ0
โ ฮฃ๐ โ
(1...๐ฆ)๐ โ โ) |
64 | 63 | recnd 11246 |
. . . . . . . . . . 11
โข (๐ฆ โ โ0
โ ฮฃ๐ โ
(1...๐ฆ)๐ โ โ) |
65 | | 1cnd 11213 |
. . . . . . . . . . 11
โข (๐ฆ โ โ0
โ 1 โ โ) |
66 | 64, 65 | pncan2d 11577 |
. . . . . . . . . 10
โข (๐ฆ โ โ0
โ ((ฮฃ๐ โ
(1...๐ฆ)๐ + 1) โ ฮฃ๐ โ (1...๐ฆ)๐) = 1) |
67 | 47 | nn0cnd 12538 |
. . . . . . . . . . 11
โข (๐ฆ โ โ0
โ (๐ฆ + 1) โ
โ) |
68 | 64, 67 | pncan2d 11577 |
. . . . . . . . . 10
โข (๐ฆ โ โ0
โ ((ฮฃ๐ โ
(1...๐ฆ)๐ + (๐ฆ + 1)) โ ฮฃ๐ โ (1...๐ฆ)๐) = (๐ฆ + 1)) |
69 | 66, 68 | oveq12d 7423 |
. . . . . . . . 9
โข (๐ฆ โ โ0
โ (((ฮฃ๐ โ
(1...๐ฆ)๐ + 1) โ ฮฃ๐ โ (1...๐ฆ)๐)...((ฮฃ๐ โ (1...๐ฆ)๐ + (๐ฆ + 1)) โ ฮฃ๐ โ (1...๐ฆ)๐)) = (1...(๐ฆ + 1))) |
70 | | elfzelz 13507 |
. . . . . . . . . . 11
โข (๐ โ (((ฮฃ๐ โ (1...๐ฆ)๐ + 1) โ ฮฃ๐ โ (1...๐ฆ)๐)...((ฮฃ๐ โ (1...๐ฆ)๐ + (๐ฆ + 1)) โ ฮฃ๐ โ (1...๐ฆ)๐)) โ ๐ โ โค) |
71 | 70 | zcnd 12671 |
. . . . . . . . . 10
โข (๐ โ (((ฮฃ๐ โ (1...๐ฆ)๐ + 1) โ ฮฃ๐ โ (1...๐ฆ)๐)...((ฮฃ๐ โ (1...๐ฆ)๐ + (๐ฆ + 1)) โ ฮฃ๐ โ (1...๐ฆ)๐)) โ ๐ โ โ) |
72 | | 2cnd 12294 |
. . . . . . . . . . . . 13
โข ((๐ฆ โ โ0
โง ๐ โ โ)
โ 2 โ โ) |
73 | | simpr 484 |
. . . . . . . . . . . . 13
โข ((๐ฆ โ โ0
โง ๐ โ โ)
โ ๐ โ
โ) |
74 | 64 | adantr 480 |
. . . . . . . . . . . . 13
โข ((๐ฆ โ โ0
โง ๐ โ โ)
โ ฮฃ๐ โ
(1...๐ฆ)๐ โ โ) |
75 | 72, 73, 74 | adddid 11242 |
. . . . . . . . . . . 12
โข ((๐ฆ โ โ0
โง ๐ โ โ)
โ (2 ยท (๐ +
ฮฃ๐ โ (1...๐ฆ)๐)) = ((2 ยท ๐) + (2 ยท ฮฃ๐ โ (1...๐ฆ)๐))) |
76 | 75 | oveq1d 7420 |
. . . . . . . . . . 11
โข ((๐ฆ โ โ0
โง ๐ โ โ)
โ ((2 ยท (๐ +
ฮฃ๐ โ (1...๐ฆ)๐)) โ 1) = (((2 ยท ๐) + (2 ยท ฮฃ๐ โ (1...๐ฆ)๐)) โ 1)) |
77 | 72, 73 | mulcld 11238 |
. . . . . . . . . . . 12
โข ((๐ฆ โ โ0
โง ๐ โ โ)
โ (2 ยท ๐)
โ โ) |
78 | 72, 74 | mulcld 11238 |
. . . . . . . . . . . 12
โข ((๐ฆ โ โ0
โง ๐ โ โ)
โ (2 ยท ฮฃ๐
โ (1...๐ฆ)๐) โ
โ) |
79 | | 1cnd 11213 |
. . . . . . . . . . . 12
โข ((๐ฆ โ โ0
โง ๐ โ โ)
โ 1 โ โ) |
80 | 77, 78, 79 | addsubassd 11595 |
. . . . . . . . . . 11
โข ((๐ฆ โ โ0
โง ๐ โ โ)
โ (((2 ยท ๐) +
(2 ยท ฮฃ๐ โ
(1...๐ฆ)๐)) โ 1) = ((2 ยท ๐) + ((2 ยท ฮฃ๐ โ (1...๐ฆ)๐) โ 1))) |
81 | 77, 78, 79 | addsub12d 11598 |
. . . . . . . . . . . 12
โข ((๐ฆ โ โ0
โง ๐ โ โ)
โ ((2 ยท ๐) +
((2 ยท ฮฃ๐
โ (1...๐ฆ)๐) โ 1)) = ((2 ยท
ฮฃ๐ โ (1...๐ฆ)๐) + ((2 ยท ๐) โ 1))) |
82 | | arisum 15812 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ โ โ0
โ ฮฃ๐ โ
(1...๐ฆ)๐ = (((๐ฆโ2) + ๐ฆ) / 2)) |
83 | 82 | oveq2d 7421 |
. . . . . . . . . . . . . . 15
โข (๐ฆ โ โ0
โ (2 ยท ฮฃ๐
โ (1...๐ฆ)๐) = (2 ยท (((๐ฆโ2) + ๐ฆ) / 2))) |
84 | | nn0cn 12486 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฆ โ โ0
โ ๐ฆ โ
โ) |
85 | 84 | sqcld 14114 |
. . . . . . . . . . . . . . . . 17
โข (๐ฆ โ โ0
โ (๐ฆโ2) โ
โ) |
86 | 85, 84 | addcld 11237 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ โ โ0
โ ((๐ฆโ2) + ๐ฆ) โ
โ) |
87 | | 2cnd 12294 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ โ โ0
โ 2 โ โ) |
88 | | 2ne0 12320 |
. . . . . . . . . . . . . . . . 17
โข 2 โ
0 |
89 | 88 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ โ โ0
โ 2 โ 0) |
90 | 86, 87, 89 | divcan2d 11996 |
. . . . . . . . . . . . . . 15
โข (๐ฆ โ โ0
โ (2 ยท (((๐ฆโ2) + ๐ฆ) / 2)) = ((๐ฆโ2) + ๐ฆ)) |
91 | | binom21 14187 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฆ โ โ โ ((๐ฆ + 1)โ2) = (((๐ฆโ2) + (2 ยท ๐ฆ)) + 1)) |
92 | 84, 91 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข (๐ฆ โ โ0
โ ((๐ฆ + 1)โ2) =
(((๐ฆโ2) + (2 ยท
๐ฆ)) + 1)) |
93 | 92 | oveq1d 7420 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ โ โ0
โ (((๐ฆ + 1)โ2)
โ (๐ฆ + 1)) =
((((๐ฆโ2) + (2 ยท
๐ฆ)) + 1) โ (๐ฆ + 1))) |
94 | 87, 84 | mulcld 11238 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฆ โ โ0
โ (2 ยท ๐ฆ)
โ โ) |
95 | 85, 94 | addcld 11237 |
. . . . . . . . . . . . . . . . 17
โข (๐ฆ โ โ0
โ ((๐ฆโ2) + (2
ยท ๐ฆ)) โ
โ) |
96 | 95, 84, 65 | pnpcan2d 11613 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ โ โ0
โ ((((๐ฆโ2) + (2
ยท ๐ฆ)) + 1) โ
(๐ฆ + 1)) = (((๐ฆโ2) + (2 ยท ๐ฆ)) โ ๐ฆ)) |
97 | 85, 94, 84 | addsubassd 11595 |
. . . . . . . . . . . . . . . . 17
โข (๐ฆ โ โ0
โ (((๐ฆโ2) + (2
ยท ๐ฆ)) โ ๐ฆ) = ((๐ฆโ2) + ((2 ยท ๐ฆ) โ ๐ฆ))) |
98 | 84 | 2timesd 12459 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฆ โ โ0
โ (2 ยท ๐ฆ) =
(๐ฆ + ๐ฆ)) |
99 | 84, 84, 98 | mvrladdd 11631 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฆ โ โ0
โ ((2 ยท ๐ฆ)
โ ๐ฆ) = ๐ฆ) |
100 | 99 | oveq2d 7421 |
. . . . . . . . . . . . . . . . 17
โข (๐ฆ โ โ0
โ ((๐ฆโ2) + ((2
ยท ๐ฆ) โ ๐ฆ)) = ((๐ฆโ2) + ๐ฆ)) |
101 | 97, 100 | eqtrd 2766 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ โ โ0
โ (((๐ฆโ2) + (2
ยท ๐ฆ)) โ ๐ฆ) = ((๐ฆโ2) + ๐ฆ)) |
102 | 93, 96, 101 | 3eqtrrd 2771 |
. . . . . . . . . . . . . . 15
โข (๐ฆ โ โ0
โ ((๐ฆโ2) + ๐ฆ) = (((๐ฆ + 1)โ2) โ (๐ฆ + 1))) |
103 | 83, 90, 102 | 3eqtrd 2770 |
. . . . . . . . . . . . . 14
โข (๐ฆ โ โ0
โ (2 ยท ฮฃ๐
โ (1...๐ฆ)๐) = (((๐ฆ + 1)โ2) โ (๐ฆ + 1))) |
104 | 103 | adantr 480 |
. . . . . . . . . . . . 13
โข ((๐ฆ โ โ0
โง ๐ โ โ)
โ (2 ยท ฮฃ๐
โ (1...๐ฆ)๐) = (((๐ฆ + 1)โ2) โ (๐ฆ + 1))) |
105 | 104 | oveq1d 7420 |
. . . . . . . . . . . 12
โข ((๐ฆ โ โ0
โง ๐ โ โ)
โ ((2 ยท ฮฃ๐ โ (1...๐ฆ)๐) + ((2 ยท ๐) โ 1)) = ((((๐ฆ + 1)โ2) โ (๐ฆ + 1)) + ((2 ยท ๐) โ 1))) |
106 | 81, 105 | eqtrd 2766 |
. . . . . . . . . . 11
โข ((๐ฆ โ โ0
โง ๐ โ โ)
โ ((2 ยท ๐) +
((2 ยท ฮฃ๐
โ (1...๐ฆ)๐) โ 1)) = ((((๐ฆ + 1)โ2) โ (๐ฆ + 1)) + ((2 ยท ๐) โ 1))) |
107 | 76, 80, 106 | 3eqtrd 2770 |
. . . . . . . . . 10
โข ((๐ฆ โ โ0
โง ๐ โ โ)
โ ((2 ยท (๐ +
ฮฃ๐ โ (1...๐ฆ)๐)) โ 1) = ((((๐ฆ + 1)โ2) โ (๐ฆ + 1)) + ((2 ยท ๐) โ 1))) |
108 | 71, 107 | sylan2 592 |
. . . . . . . . 9
โข ((๐ฆ โ โ0
โง ๐ โ
(((ฮฃ๐ โ
(1...๐ฆ)๐ + 1) โ ฮฃ๐ โ (1...๐ฆ)๐)...((ฮฃ๐ โ (1...๐ฆ)๐ + (๐ฆ + 1)) โ ฮฃ๐ โ (1...๐ฆ)๐))) โ ((2 ยท (๐ + ฮฃ๐ โ (1...๐ฆ)๐)) โ 1) = ((((๐ฆ + 1)โ2) โ (๐ฆ + 1)) + ((2 ยท ๐) โ 1))) |
109 | 69, 108 | sumeq12dv 15658 |
. . . . . . . 8
โข (๐ฆ โ โ0
โ ฮฃ๐ โ
(((ฮฃ๐ โ
(1...๐ฆ)๐ + 1) โ ฮฃ๐ โ (1...๐ฆ)๐)...((ฮฃ๐ โ (1...๐ฆ)๐ + (๐ฆ + 1)) โ ฮฃ๐ โ (1...๐ฆ)๐))((2 ยท (๐ + ฮฃ๐ โ (1...๐ฆ)๐)) โ 1) = ฮฃ๐ โ (1...(๐ฆ + 1))((((๐ฆ + 1)โ2) โ (๐ฆ + 1)) + ((2 ยท ๐) โ 1))) |
110 | 59, 109 | eqtr2d 2767 |
. . . . . . 7
โข (๐ฆ โ โ0
โ ฮฃ๐ โ
(1...(๐ฆ + 1))((((๐ฆ + 1)โ2) โ (๐ฆ + 1)) + ((2 ยท ๐) โ 1)) = ฮฃ๐ โ ((ฮฃ๐ โ (1...๐ฆ)๐ + 1)...(ฮฃ๐ โ (1...๐ฆ)๐ + (๐ฆ + 1)))((2 ยท ๐) โ 1)) |
111 | 110 | adantr 480 |
. . . . . 6
โข ((๐ฆ โ โ0
โง ฮฃ๐ โ
(1...๐ฆ)ฮฃ๐ โ (1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) = ฮฃ๐ โ (1...ฮฃ๐ โ (1...๐ฆ)๐)((2 ยท ๐) โ 1)) โ ฮฃ๐ โ (1...(๐ฆ + 1))((((๐ฆ + 1)โ2) โ (๐ฆ + 1)) + ((2 ยท ๐) โ 1)) = ฮฃ๐ โ ((ฮฃ๐ โ (1...๐ฆ)๐ + 1)...(ฮฃ๐ โ (1...๐ฆ)๐ + (๐ฆ + 1)))((2 ยท ๐) โ 1)) |
112 | 37, 111 | oveq12d 7423 |
. . . . 5
โข ((๐ฆ โ โ0
โง ฮฃ๐ โ
(1...๐ฆ)ฮฃ๐ โ (1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) = ฮฃ๐ โ (1...ฮฃ๐ โ (1...๐ฆ)๐)((2 ยท ๐) โ 1)) โ (ฮฃ๐ โ (1...๐ฆ)ฮฃ๐ โ (1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) + ฮฃ๐ โ (1...(๐ฆ + 1))((((๐ฆ + 1)โ2) โ (๐ฆ + 1)) + ((2 ยท ๐) โ 1))) = (ฮฃ๐ โ (1...ฮฃ๐ โ (1...๐ฆ)๐)((2 ยท ๐) โ 1) + ฮฃ๐ โ ((ฮฃ๐ โ (1...๐ฆ)๐ + 1)...(ฮฃ๐ โ (1...๐ฆ)๐ + (๐ฆ + 1)))((2 ยท ๐) โ 1))) |
113 | | id 22 |
. . . . . . 7
โข (๐ฆ โ โ0
โ ๐ฆ โ
โ0) |
114 | | fzfid 13944 |
. . . . . . . 8
โข ((๐ฆ โ โ0
โง ๐ โ (1...(๐ฆ + 1))) โ (1...๐) โ Fin) |
115 | | elfzelz 13507 |
. . . . . . . . . . . . 13
โข (๐ โ (1...(๐ฆ + 1)) โ ๐ โ โค) |
116 | 115 | zcnd 12671 |
. . . . . . . . . . . 12
โข (๐ โ (1...(๐ฆ + 1)) โ ๐ โ โ) |
117 | 116 | sqcld 14114 |
. . . . . . . . . . 11
โข (๐ โ (1...(๐ฆ + 1)) โ (๐โ2) โ โ) |
118 | 117, 116 | subcld 11575 |
. . . . . . . . . 10
โข (๐ โ (1...(๐ฆ + 1)) โ ((๐โ2) โ ๐) โ โ) |
119 | | 2cnd 12294 |
. . . . . . . . . . . 12
โข (๐ โ (1...๐) โ 2 โ โ) |
120 | | elfzelz 13507 |
. . . . . . . . . . . . 13
โข (๐ โ (1...๐) โ ๐ โ โค) |
121 | 120 | zcnd 12671 |
. . . . . . . . . . . 12
โข (๐ โ (1...๐) โ ๐ โ โ) |
122 | 119, 121 | mulcld 11238 |
. . . . . . . . . . 11
โข (๐ โ (1...๐) โ (2 ยท ๐) โ โ) |
123 | | 1cnd 11213 |
. . . . . . . . . . 11
โข (๐ โ (1...๐) โ 1 โ โ) |
124 | 122, 123 | subcld 11575 |
. . . . . . . . . 10
โข (๐ โ (1...๐) โ ((2 ยท ๐) โ 1) โ โ) |
125 | | addcl 11194 |
. . . . . . . . . 10
โข ((((๐โ2) โ ๐) โ โ โง ((2
ยท ๐) โ 1)
โ โ) โ (((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) โ
โ) |
126 | 118, 124,
125 | syl2an 595 |
. . . . . . . . 9
โข ((๐ โ (1...(๐ฆ + 1)) โง ๐ โ (1...๐)) โ (((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) โ
โ) |
127 | 126 | adantll 711 |
. . . . . . . 8
โข (((๐ฆ โ โ0
โง ๐ โ (1...(๐ฆ + 1))) โง ๐ โ (1...๐)) โ (((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) โ
โ) |
128 | 114, 127 | fsumcl 15685 |
. . . . . . 7
โข ((๐ฆ โ โ0
โง ๐ โ (1...(๐ฆ + 1))) โ ฮฃ๐ โ (1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) โ
โ) |
129 | | oveq2 7413 |
. . . . . . . 8
โข (๐ = (๐ฆ + 1) โ (1...๐) = (1...(๐ฆ + 1))) |
130 | | oveq1 7412 |
. . . . . . . . . . 11
โข (๐ = (๐ฆ + 1) โ (๐โ2) = ((๐ฆ + 1)โ2)) |
131 | | id 22 |
. . . . . . . . . . 11
โข (๐ = (๐ฆ + 1) โ ๐ = (๐ฆ + 1)) |
132 | 130, 131 | oveq12d 7423 |
. . . . . . . . . 10
โข (๐ = (๐ฆ + 1) โ ((๐โ2) โ ๐) = (((๐ฆ + 1)โ2) โ (๐ฆ + 1))) |
133 | 132 | oveq1d 7420 |
. . . . . . . . 9
โข (๐ = (๐ฆ + 1) โ (((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) = ((((๐ฆ + 1)โ2) โ (๐ฆ + 1)) + ((2 ยท ๐) โ 1))) |
134 | 133 | adantr 480 |
. . . . . . . 8
โข ((๐ = (๐ฆ + 1) โง ๐ โ (1...๐)) โ (((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) = ((((๐ฆ + 1)โ2) โ (๐ฆ + 1)) + ((2 ยท ๐) โ 1))) |
135 | 129, 134 | sumeq12dv 15658 |
. . . . . . 7
โข (๐ = (๐ฆ + 1) โ ฮฃ๐ โ (1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) = ฮฃ๐ โ (1...(๐ฆ + 1))((((๐ฆ + 1)โ2) โ (๐ฆ + 1)) + ((2 ยท ๐) โ 1))) |
136 | 113, 128,
135 | fz1sump1 41763 |
. . . . . 6
โข (๐ฆ โ โ0
โ ฮฃ๐ โ
(1...(๐ฆ + 1))ฮฃ๐ โ (1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) = (ฮฃ๐ โ (1...๐ฆ)ฮฃ๐ โ (1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) + ฮฃ๐ โ (1...(๐ฆ + 1))((((๐ฆ + 1)โ2) โ (๐ฆ + 1)) + ((2 ยท ๐) โ 1)))) |
137 | 136 | adantr 480 |
. . . . 5
โข ((๐ฆ โ โ0
โง ฮฃ๐ โ
(1...๐ฆ)ฮฃ๐ โ (1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) = ฮฃ๐ โ (1...ฮฃ๐ โ (1...๐ฆ)๐)((2 ยท ๐) โ 1)) โ ฮฃ๐ โ (1...(๐ฆ + 1))ฮฃ๐ โ (1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) = (ฮฃ๐ โ (1...๐ฆ)ฮฃ๐ โ (1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) + ฮฃ๐ โ (1...(๐ฆ + 1))((((๐ฆ + 1)โ2) โ (๐ฆ + 1)) + ((2 ยท ๐) โ 1)))) |
138 | 116 | adantl 481 |
. . . . . . . . . 10
โข ((๐ฆ โ โ0
โง ๐ โ (1...(๐ฆ + 1))) โ ๐ โ
โ) |
139 | 113, 138,
131 | fz1sump1 41763 |
. . . . . . . . 9
โข (๐ฆ โ โ0
โ ฮฃ๐ โ
(1...(๐ฆ + 1))๐ = (ฮฃ๐ โ (1...๐ฆ)๐ + (๐ฆ + 1))) |
140 | 139 | adantr 480 |
. . . . . . . 8
โข ((๐ฆ โ โ0
โง ฮฃ๐ โ
(1...๐ฆ)ฮฃ๐ โ (1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) = ฮฃ๐ โ (1...ฮฃ๐ โ (1...๐ฆ)๐)((2 ยท ๐) โ 1)) โ ฮฃ๐ โ (1...(๐ฆ + 1))๐ = (ฮฃ๐ โ (1...๐ฆ)๐ + (๐ฆ + 1))) |
141 | 140 | oveq2d 7421 |
. . . . . . 7
โข ((๐ฆ โ โ0
โง ฮฃ๐ โ
(1...๐ฆ)ฮฃ๐ โ (1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) = ฮฃ๐ โ (1...ฮฃ๐ โ (1...๐ฆ)๐)((2 ยท ๐) โ 1)) โ (1...ฮฃ๐ โ (1...(๐ฆ + 1))๐) = (1...(ฮฃ๐ โ (1...๐ฆ)๐ + (๐ฆ + 1)))) |
142 | 141 | sumeq1d 15653 |
. . . . . 6
โข ((๐ฆ โ โ0
โง ฮฃ๐ โ
(1...๐ฆ)ฮฃ๐ โ (1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) = ฮฃ๐ โ (1...ฮฃ๐ โ (1...๐ฆ)๐)((2 ยท ๐) โ 1)) โ ฮฃ๐ โ (1...ฮฃ๐ โ (1...(๐ฆ + 1))๐)((2 ยท ๐) โ 1) = ฮฃ๐ โ (1...(ฮฃ๐ โ (1...๐ฆ)๐ + (๐ฆ + 1)))((2 ยท ๐) โ 1)) |
143 | 63 | ltp1d 12148 |
. . . . . . . . 9
โข (๐ฆ โ โ0
โ ฮฃ๐ โ
(1...๐ฆ)๐ < (ฮฃ๐ โ (1...๐ฆ)๐ + 1)) |
144 | | fzdisj 13534 |
. . . . . . . . 9
โข
(ฮฃ๐ โ
(1...๐ฆ)๐ < (ฮฃ๐ โ (1...๐ฆ)๐ + 1) โ ((1...ฮฃ๐ โ (1...๐ฆ)๐) โฉ ((ฮฃ๐ โ (1...๐ฆ)๐ + 1)...(ฮฃ๐ โ (1...๐ฆ)๐ + (๐ฆ + 1)))) = โ
) |
145 | 143, 144 | syl 17 |
. . . . . . . 8
โข (๐ฆ โ โ0
โ ((1...ฮฃ๐
โ (1...๐ฆ)๐) โฉ ((ฮฃ๐ โ (1...๐ฆ)๐ + 1)...(ฮฃ๐ โ (1...๐ฆ)๐ + (๐ฆ + 1)))) = โ
) |
146 | | nnuz 12869 |
. . . . . . . . . 10
โข โ =
(โคโฅโ1) |
147 | 45, 146 | eleqtrdi 2837 |
. . . . . . . . 9
โข (๐ฆ โ โ0
โ (ฮฃ๐ โ
(1...๐ฆ)๐ + 1) โ
(โคโฅโ1)) |
148 | 43 | uzidd 12842 |
. . . . . . . . . 10
โข (๐ฆ โ โ0
โ ฮฃ๐ โ
(1...๐ฆ)๐ โ
(โคโฅโฮฃ๐ โ (1...๐ฆ)๐)) |
149 | | uzaddcl 12892 |
. . . . . . . . . 10
โข
((ฮฃ๐ โ
(1...๐ฆ)๐ โ
(โคโฅโฮฃ๐ โ (1...๐ฆ)๐) โง (๐ฆ + 1) โ โ0) โ
(ฮฃ๐ โ (1...๐ฆ)๐ + (๐ฆ + 1)) โ
(โคโฅโฮฃ๐ โ (1...๐ฆ)๐)) |
150 | 148, 47, 149 | syl2anc 583 |
. . . . . . . . 9
โข (๐ฆ โ โ0
โ (ฮฃ๐ โ
(1...๐ฆ)๐ + (๐ฆ + 1)) โ
(โคโฅโฮฃ๐ โ (1...๐ฆ)๐)) |
151 | | fzsplit2 13532 |
. . . . . . . . 9
โข
(((ฮฃ๐ โ
(1...๐ฆ)๐ + 1) โ (โคโฅโ1)
โง (ฮฃ๐ โ
(1...๐ฆ)๐ + (๐ฆ + 1)) โ
(โคโฅโฮฃ๐ โ (1...๐ฆ)๐)) โ (1...(ฮฃ๐ โ (1...๐ฆ)๐ + (๐ฆ + 1))) = ((1...ฮฃ๐ โ (1...๐ฆ)๐) โช ((ฮฃ๐ โ (1...๐ฆ)๐ + 1)...(ฮฃ๐ โ (1...๐ฆ)๐ + (๐ฆ + 1))))) |
152 | 147, 150,
151 | syl2anc 583 |
. . . . . . . 8
โข (๐ฆ โ โ0
โ (1...(ฮฃ๐
โ (1...๐ฆ)๐ + (๐ฆ + 1))) = ((1...ฮฃ๐ โ (1...๐ฆ)๐) โช ((ฮฃ๐ โ (1...๐ฆ)๐ + 1)...(ฮฃ๐ โ (1...๐ฆ)๐ + (๐ฆ + 1))))) |
153 | | fzfid 13944 |
. . . . . . . 8
โข (๐ฆ โ โ0
โ (1...(ฮฃ๐
โ (1...๐ฆ)๐ + (๐ฆ + 1))) โ Fin) |
154 | | 2cnd 12294 |
. . . . . . . . . 10
โข ((๐ฆ โ โ0
โง ๐ โ
(1...(ฮฃ๐ โ
(1...๐ฆ)๐ + (๐ฆ + 1)))) โ 2 โ
โ) |
155 | | elfzelz 13507 |
. . . . . . . . . . . 12
โข (๐ โ (1...(ฮฃ๐ โ (1...๐ฆ)๐ + (๐ฆ + 1))) โ ๐ โ โค) |
156 | 155 | zcnd 12671 |
. . . . . . . . . . 11
โข (๐ โ (1...(ฮฃ๐ โ (1...๐ฆ)๐ + (๐ฆ + 1))) โ ๐ โ โ) |
157 | 156 | adantl 481 |
. . . . . . . . . 10
โข ((๐ฆ โ โ0
โง ๐ โ
(1...(ฮฃ๐ โ
(1...๐ฆ)๐ + (๐ฆ + 1)))) โ ๐ โ โ) |
158 | 154, 157 | mulcld 11238 |
. . . . . . . . 9
โข ((๐ฆ โ โ0
โง ๐ โ
(1...(ฮฃ๐ โ
(1...๐ฆ)๐ + (๐ฆ + 1)))) โ (2 ยท ๐) โ
โ) |
159 | | 1cnd 11213 |
. . . . . . . . 9
โข ((๐ฆ โ โ0
โง ๐ โ
(1...(ฮฃ๐ โ
(1...๐ฆ)๐ + (๐ฆ + 1)))) โ 1 โ
โ) |
160 | 158, 159 | subcld 11575 |
. . . . . . . 8
โข ((๐ฆ โ โ0
โง ๐ โ
(1...(ฮฃ๐ โ
(1...๐ฆ)๐ + (๐ฆ + 1)))) โ ((2 ยท ๐) โ 1) โ
โ) |
161 | 145, 152,
153, 160 | fsumsplit 15693 |
. . . . . . 7
โข (๐ฆ โ โ0
โ ฮฃ๐ โ
(1...(ฮฃ๐ โ
(1...๐ฆ)๐ + (๐ฆ + 1)))((2 ยท ๐) โ 1) = (ฮฃ๐ โ (1...ฮฃ๐ โ (1...๐ฆ)๐)((2 ยท ๐) โ 1) + ฮฃ๐ โ ((ฮฃ๐ โ (1...๐ฆ)๐ + 1)...(ฮฃ๐ โ (1...๐ฆ)๐ + (๐ฆ + 1)))((2 ยท ๐) โ 1))) |
162 | 161 | adantr 480 |
. . . . . 6
โข ((๐ฆ โ โ0
โง ฮฃ๐ โ
(1...๐ฆ)ฮฃ๐ โ (1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) = ฮฃ๐ โ (1...ฮฃ๐ โ (1...๐ฆ)๐)((2 ยท ๐) โ 1)) โ ฮฃ๐ โ (1...(ฮฃ๐ โ (1...๐ฆ)๐ + (๐ฆ + 1)))((2 ยท ๐) โ 1) = (ฮฃ๐ โ (1...ฮฃ๐ โ (1...๐ฆ)๐)((2 ยท ๐) โ 1) + ฮฃ๐ โ ((ฮฃ๐ โ (1...๐ฆ)๐ + 1)...(ฮฃ๐ โ (1...๐ฆ)๐ + (๐ฆ + 1)))((2 ยท ๐) โ 1))) |
163 | 142, 162 | eqtrd 2766 |
. . . . 5
โข ((๐ฆ โ โ0
โง ฮฃ๐ โ
(1...๐ฆ)ฮฃ๐ โ (1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) = ฮฃ๐ โ (1...ฮฃ๐ โ (1...๐ฆ)๐)((2 ยท ๐) โ 1)) โ ฮฃ๐ โ (1...ฮฃ๐ โ (1...(๐ฆ + 1))๐)((2 ยท ๐) โ 1) = (ฮฃ๐ โ (1...ฮฃ๐ โ (1...๐ฆ)๐)((2 ยท ๐) โ 1) + ฮฃ๐ โ ((ฮฃ๐ โ (1...๐ฆ)๐ + 1)...(ฮฃ๐ โ (1...๐ฆ)๐ + (๐ฆ + 1)))((2 ยท ๐) โ 1))) |
164 | 112, 137,
163 | 3eqtr4d 2776 |
. . . 4
โข ((๐ฆ โ โ0
โง ฮฃ๐ โ
(1...๐ฆ)ฮฃ๐ โ (1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) = ฮฃ๐ โ (1...ฮฃ๐ โ (1...๐ฆ)๐)((2 ยท ๐) โ 1)) โ ฮฃ๐ โ (1...(๐ฆ + 1))ฮฃ๐ โ (1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) = ฮฃ๐ โ (1...ฮฃ๐ โ (1...(๐ฆ + 1))๐)((2 ยท ๐) โ 1)) |
165 | 164 | ex 412 |
. . 3
โข (๐ฆ โ โ0
โ (ฮฃ๐ โ
(1...๐ฆ)ฮฃ๐ โ (1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) = ฮฃ๐ โ (1...ฮฃ๐ โ (1...๐ฆ)๐)((2 ยท ๐) โ 1) โ ฮฃ๐ โ (1...(๐ฆ + 1))ฮฃ๐ โ (1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) = ฮฃ๐ โ (1...ฮฃ๐ โ (1...(๐ฆ + 1))๐)((2 ยท ๐) โ 1))) |
166 | 6, 12, 18, 24, 36, 165 | nn0ind 12661 |
. 2
โข (๐ โ โ0
โ ฮฃ๐ โ
(1...๐)ฮฃ๐ โ (1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) = ฮฃ๐ โ (1...ฮฃ๐ โ (1...๐)๐)((2 ยท ๐) โ 1)) |
167 | | fz1ssnn 13538 |
. . . . . . 7
โข
(1...๐) โ
โ |
168 | | nnssnn0 12479 |
. . . . . . 7
โข โ
โ โ0 |
169 | 167, 168 | sstri 3986 |
. . . . . 6
โข
(1...๐) โ
โ0 |
170 | 169 | a1i 11 |
. . . . 5
โข (๐ โ โ0
โ (1...๐) โ
โ0) |
171 | 170 | sselda 3977 |
. . . 4
โข ((๐ โ โ0
โง ๐ โ (1...๐)) โ ๐ โ โ0) |
172 | | nicomachus 41765 |
. . . 4
โข (๐ โ โ0
โ ฮฃ๐ โ
(1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) = (๐โ3)) |
173 | 171, 172 | syl 17 |
. . 3
โข ((๐ โ โ0
โง ๐ โ (1...๐)) โ ฮฃ๐ โ (1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) = (๐โ3)) |
174 | 173 | sumeq2dv 15655 |
. 2
โข (๐ โ โ0
โ ฮฃ๐ โ
(1...๐)ฮฃ๐ โ (1...๐)(((๐โ2) โ ๐) + ((2 ยท ๐) โ 1)) = ฮฃ๐ โ (1...๐)(๐โ3)) |
175 | | fzfid 13944 |
. . . 4
โข (๐ โ โ0
โ (1...๐) โ
Fin) |
176 | 175, 171 | fsumnn0cl 15688 |
. . 3
โข (๐ โ โ0
โ ฮฃ๐ โ
(1...๐)๐ โ โ0) |
177 | | oddnumth 41764 |
. . 3
โข
(ฮฃ๐ โ
(1...๐)๐ โ โ0 โ
ฮฃ๐ โ
(1...ฮฃ๐ โ
(1...๐)๐)((2 ยท ๐) โ 1) = (ฮฃ๐ โ (1...๐)๐โ2)) |
178 | 176, 177 | syl 17 |
. 2
โข (๐ โ โ0
โ ฮฃ๐ โ
(1...ฮฃ๐ โ
(1...๐)๐)((2 ยท ๐) โ 1) = (ฮฃ๐ โ (1...๐)๐โ2)) |
179 | 166, 174,
178 | 3eqtr3d 2774 |
1
โข (๐ โ โ0
โ ฮฃ๐ โ
(1...๐)(๐โ3) = (ฮฃ๐ โ (1...๐)๐โ2)) |