Step | Hyp | Ref
| Expression |
1 | | elnn0 9177 |
. 2
โข (๐ โ โ0
โ (๐ โ โ
โจ ๐ =
0)) |
2 | | simpr 110 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ) โ ๐ โ
โ) |
3 | | elnnuz 9563 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
(โคโฅโ1)) |
4 | 2, 3 | sylib 122 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โ) โ ๐ โ
(โคโฅโ1)) |
5 | | simpll 527 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ โ โ) โง ๐ฅ โ
(โคโฅโ1)) โ ๐ด โ โ) |
6 | | elnnuz 9563 |
. . . . . . . . 9
โข (๐ฅ โ โ โ ๐ฅ โ
(โคโฅโ1)) |
7 | | fvconst2g 5730 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ฅ โ โ) โ
((โ ร {๐ด})โ๐ฅ) = ๐ด) |
8 | 7 | eleq1d 2246 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ฅ โ โ) โ
(((โ ร {๐ด})โ๐ฅ) โ โ โ ๐ด โ โ)) |
9 | 6, 8 | sylan2br 288 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ฅ โ
(โคโฅโ1)) โ (((โ ร {๐ด})โ๐ฅ) โ โ โ ๐ด โ โ)) |
10 | 9 | adantlr 477 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ โ โ) โง ๐ฅ โ
(โคโฅโ1)) โ (((โ ร {๐ด})โ๐ฅ) โ โ โ ๐ด โ โ)) |
11 | 5, 10 | mpbird 167 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ โ) โง ๐ฅ โ
(โคโฅโ1)) โ ((โ ร {๐ด})โ๐ฅ) โ โ) |
12 | | mulcl 7937 |
. . . . . . 7
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐ฅ ยท ๐ฆ) โ โ) |
13 | 12 | adantl 277 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ โ) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (๐ฅ ยท ๐ฆ) โ โ) |
14 | 4, 11, 13 | seq3p1 10461 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ โ) โ (seq1(
ยท , (โ ร {๐ด}))โ(๐ + 1)) = ((seq1( ยท , (โ ร
{๐ด}))โ๐) ยท ((โ ร
{๐ด})โ(๐ + 1)))) |
15 | | peano2nn 8930 |
. . . . . . 7
โข (๐ โ โ โ (๐ + 1) โ
โ) |
16 | | fvconst2g 5730 |
. . . . . . 7
โข ((๐ด โ โ โง (๐ + 1) โ โ) โ
((โ ร {๐ด})โ(๐ + 1)) = ๐ด) |
17 | 15, 16 | sylan2 286 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โ) โ
((โ ร {๐ด})โ(๐ + 1)) = ๐ด) |
18 | 17 | oveq2d 5890 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ โ) โ ((seq1(
ยท , (โ ร {๐ด}))โ๐) ยท ((โ ร {๐ด})โ(๐ + 1))) = ((seq1( ยท , (โ
ร {๐ด}))โ๐) ยท ๐ด)) |
19 | 14, 18 | eqtrd 2210 |
. . . 4
โข ((๐ด โ โ โง ๐ โ โ) โ (seq1(
ยท , (โ ร {๐ด}))โ(๐ + 1)) = ((seq1( ยท , (โ ร
{๐ด}))โ๐) ยท ๐ด)) |
20 | | expnnval 10522 |
. . . . 5
โข ((๐ด โ โ โง (๐ + 1) โ โ) โ
(๐ดโ(๐ + 1)) = (seq1( ยท , (โ ร
{๐ด}))โ(๐ + 1))) |
21 | 15, 20 | sylan2 286 |
. . . 4
โข ((๐ด โ โ โง ๐ โ โ) โ (๐ดโ(๐ + 1)) = (seq1( ยท , (โ ร
{๐ด}))โ(๐ + 1))) |
22 | | expnnval 10522 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ โ) โ (๐ดโ๐) = (seq1( ยท , (โ ร
{๐ด}))โ๐)) |
23 | 22 | oveq1d 5889 |
. . . 4
โข ((๐ด โ โ โง ๐ โ โ) โ ((๐ดโ๐) ยท ๐ด) = ((seq1( ยท , (โ ร
{๐ด}))โ๐) ยท ๐ด)) |
24 | 19, 21, 23 | 3eqtr4d 2220 |
. . 3
โข ((๐ด โ โ โง ๐ โ โ) โ (๐ดโ(๐ + 1)) = ((๐ดโ๐) ยท ๐ด)) |
25 | | exp1 10525 |
. . . . . 6
โข (๐ด โ โ โ (๐ดโ1) = ๐ด) |
26 | | mullid 7954 |
. . . . . 6
โข (๐ด โ โ โ (1
ยท ๐ด) = ๐ด) |
27 | 25, 26 | eqtr4d 2213 |
. . . . 5
โข (๐ด โ โ โ (๐ดโ1) = (1 ยท ๐ด)) |
28 | 27 | adantr 276 |
. . . 4
โข ((๐ด โ โ โง ๐ = 0) โ (๐ดโ1) = (1 ยท ๐ด)) |
29 | | simpr 110 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ = 0) โ ๐ = 0) |
30 | 29 | oveq1d 5889 |
. . . . . 6
โข ((๐ด โ โ โง ๐ = 0) โ (๐ + 1) = (0 + 1)) |
31 | | 0p1e1 9032 |
. . . . . 6
โข (0 + 1) =
1 |
32 | 30, 31 | eqtrdi 2226 |
. . . . 5
โข ((๐ด โ โ โง ๐ = 0) โ (๐ + 1) = 1) |
33 | 32 | oveq2d 5890 |
. . . 4
โข ((๐ด โ โ โง ๐ = 0) โ (๐ดโ(๐ + 1)) = (๐ดโ1)) |
34 | | oveq2 5882 |
. . . . . 6
โข (๐ = 0 โ (๐ดโ๐) = (๐ดโ0)) |
35 | | exp0 10523 |
. . . . . 6
โข (๐ด โ โ โ (๐ดโ0) = 1) |
36 | 34, 35 | sylan9eqr 2232 |
. . . . 5
โข ((๐ด โ โ โง ๐ = 0) โ (๐ดโ๐) = 1) |
37 | 36 | oveq1d 5889 |
. . . 4
โข ((๐ด โ โ โง ๐ = 0) โ ((๐ดโ๐) ยท ๐ด) = (1 ยท ๐ด)) |
38 | 28, 33, 37 | 3eqtr4d 2220 |
. . 3
โข ((๐ด โ โ โง ๐ = 0) โ (๐ดโ(๐ + 1)) = ((๐ดโ๐) ยท ๐ด)) |
39 | 24, 38 | jaodan 797 |
. 2
โข ((๐ด โ โ โง (๐ โ โ โจ ๐ = 0)) โ (๐ดโ(๐ + 1)) = ((๐ดโ๐) ยท ๐ด)) |
40 | 1, 39 | sylan2b 287 |
1
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ(๐ + 1)) = ((๐ดโ๐) ยท ๐ด)) |