Step | Hyp | Ref
| Expression |
1 | | fveq2 6846 |
. . . . 5
โข (๐ = 1 โ (seq1( + , (โ
ร {๐ด}))โ๐) = (seq1( + , (โ ร
{๐ด}))โ1)) |
2 | | oveq1 7368 |
. . . . 5
โข (๐ = 1 โ (๐ ยท ๐ด) = (1 ยท ๐ด)) |
3 | 1, 2 | eqeq12d 2749 |
. . . 4
โข (๐ = 1 โ ((seq1( + , (โ
ร {๐ด}))โ๐) = (๐ ยท ๐ด) โ (seq1( + , (โ ร {๐ด}))โ1) = (1 ยท ๐ด))) |
4 | 3 | imbi2d 341 |
. . 3
โข (๐ = 1 โ ((๐ด โ โ โ (seq1( + , (โ
ร {๐ด}))โ๐) = (๐ ยท ๐ด)) โ (๐ด โ โ โ (seq1( + , (โ
ร {๐ด}))โ1) = (1
ยท ๐ด)))) |
5 | | fveq2 6846 |
. . . . 5
โข (๐ = ๐ โ (seq1( + , (โ ร {๐ด}))โ๐) = (seq1( + , (โ ร {๐ด}))โ๐)) |
6 | | oveq1 7368 |
. . . . 5
โข (๐ = ๐ โ (๐ ยท ๐ด) = (๐ ยท ๐ด)) |
7 | 5, 6 | eqeq12d 2749 |
. . . 4
โข (๐ = ๐ โ ((seq1( + , (โ ร {๐ด}))โ๐) = (๐ ยท ๐ด) โ (seq1( + , (โ ร {๐ด}))โ๐) = (๐ ยท ๐ด))) |
8 | 7 | imbi2d 341 |
. . 3
โข (๐ = ๐ โ ((๐ด โ โ โ (seq1( + , (โ
ร {๐ด}))โ๐) = (๐ ยท ๐ด)) โ (๐ด โ โ โ (seq1( + , (โ
ร {๐ด}))โ๐) = (๐ ยท ๐ด)))) |
9 | | fveq2 6846 |
. . . . 5
โข (๐ = (๐ + 1) โ (seq1( + , (โ ร
{๐ด}))โ๐) = (seq1( + , (โ ร
{๐ด}))โ(๐ + 1))) |
10 | | oveq1 7368 |
. . . . 5
โข (๐ = (๐ + 1) โ (๐ ยท ๐ด) = ((๐ + 1) ยท ๐ด)) |
11 | 9, 10 | eqeq12d 2749 |
. . . 4
โข (๐ = (๐ + 1) โ ((seq1( + , (โ ร
{๐ด}))โ๐) = (๐ ยท ๐ด) โ (seq1( + , (โ ร {๐ด}))โ(๐ + 1)) = ((๐ + 1) ยท ๐ด))) |
12 | 11 | imbi2d 341 |
. . 3
โข (๐ = (๐ + 1) โ ((๐ด โ โ โ (seq1( + , (โ
ร {๐ด}))โ๐) = (๐ ยท ๐ด)) โ (๐ด โ โ โ (seq1( + , (โ
ร {๐ด}))โ(๐ + 1)) = ((๐ + 1) ยท ๐ด)))) |
13 | | fveq2 6846 |
. . . . 5
โข (๐ = ๐ โ (seq1( + , (โ ร {๐ด}))โ๐) = (seq1( + , (โ ร {๐ด}))โ๐)) |
14 | | oveq1 7368 |
. . . . 5
โข (๐ = ๐ โ (๐ ยท ๐ด) = (๐ ยท ๐ด)) |
15 | 13, 14 | eqeq12d 2749 |
. . . 4
โข (๐ = ๐ โ ((seq1( + , (โ ร {๐ด}))โ๐) = (๐ ยท ๐ด) โ (seq1( + , (โ ร {๐ด}))โ๐) = (๐ ยท ๐ด))) |
16 | 15 | imbi2d 341 |
. . 3
โข (๐ = ๐ โ ((๐ด โ โ โ (seq1( + , (โ
ร {๐ด}))โ๐) = (๐ ยท ๐ด)) โ (๐ด โ โ โ (seq1( + , (โ
ร {๐ด}))โ๐) = (๐ ยท ๐ด)))) |
17 | | 1z 12541 |
. . . 4
โข 1 โ
โค |
18 | | 1nn 12172 |
. . . . . 6
โข 1 โ
โ |
19 | | fvconst2g 7155 |
. . . . . 6
โข ((๐ด โ โ โง 1 โ
โ) โ ((โ ร {๐ด})โ1) = ๐ด) |
20 | 18, 19 | mpan2 690 |
. . . . 5
โข (๐ด โ โ โ ((โ
ร {๐ด})โ1) =
๐ด) |
21 | | mulid2 11162 |
. . . . 5
โข (๐ด โ โ โ (1
ยท ๐ด) = ๐ด) |
22 | 20, 21 | eqtr4d 2776 |
. . . 4
โข (๐ด โ โ โ ((โ
ร {๐ด})โ1) = (1
ยท ๐ด)) |
23 | 17, 22 | seq1i 13929 |
. . 3
โข (๐ด โ โ โ (seq1( +
, (โ ร {๐ด}))โ1) = (1 ยท ๐ด)) |
24 | | oveq1 7368 |
. . . . . 6
โข ((seq1( +
, (โ ร {๐ด}))โ๐) = (๐ ยท ๐ด) โ ((seq1( + , (โ ร {๐ด}))โ๐) + ๐ด) = ((๐ ยท ๐ด) + ๐ด)) |
25 | | seqp1 13930 |
. . . . . . . . . 10
โข (๐ โ
(โคโฅโ1) โ (seq1( + , (โ ร {๐ด}))โ(๐ + 1)) = ((seq1( + , (โ ร {๐ด}))โ๐) + ((โ ร {๐ด})โ(๐ + 1)))) |
26 | | nnuz 12814 |
. . . . . . . . . 10
โข โ =
(โคโฅโ1) |
27 | 25, 26 | eleq2s 2852 |
. . . . . . . . 9
โข (๐ โ โ โ (seq1( +
, (โ ร {๐ด}))โ(๐ + 1)) = ((seq1( + , (โ ร {๐ด}))โ๐) + ((โ ร {๐ด})โ(๐ + 1)))) |
28 | 27 | adantl 483 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ โ) โ (seq1( +
, (โ ร {๐ด}))โ(๐ + 1)) = ((seq1( + , (โ ร {๐ด}))โ๐) + ((โ ร {๐ด})โ(๐ + 1)))) |
29 | | peano2nn 12173 |
. . . . . . . . . 10
โข (๐ โ โ โ (๐ + 1) โ
โ) |
30 | | fvconst2g 7155 |
. . . . . . . . . 10
โข ((๐ด โ โ โง (๐ + 1) โ โ) โ
((โ ร {๐ด})โ(๐ + 1)) = ๐ด) |
31 | 29, 30 | sylan2 594 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ โ) โ
((โ ร {๐ด})โ(๐ + 1)) = ๐ด) |
32 | 31 | oveq2d 7377 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ โ) โ ((seq1(
+ , (โ ร {๐ด}))โ๐) + ((โ ร {๐ด})โ(๐ + 1))) = ((seq1( + , (โ ร {๐ด}))โ๐) + ๐ด)) |
33 | 28, 32 | eqtrd 2773 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ) โ (seq1( +
, (โ ร {๐ด}))โ(๐ + 1)) = ((seq1( + , (โ ร {๐ด}))โ๐) + ๐ด)) |
34 | | nncn 12169 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โ) |
35 | | id 22 |
. . . . . . . . 9
โข (๐ด โ โ โ ๐ด โ
โ) |
36 | | ax-1cn 11117 |
. . . . . . . . . 10
โข 1 โ
โ |
37 | | adddir 11154 |
. . . . . . . . . 10
โข ((๐ โ โ โง 1 โ
โ โง ๐ด โ
โ) โ ((๐ + 1)
ยท ๐ด) = ((๐ ยท ๐ด) + (1 ยท ๐ด))) |
38 | 36, 37 | mp3an2 1450 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ด โ โ) โ ((๐ + 1) ยท ๐ด) = ((๐ ยท ๐ด) + (1 ยท ๐ด))) |
39 | 34, 35, 38 | syl2anr 598 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ โ) โ ((๐ + 1) ยท ๐ด) = ((๐ ยท ๐ด) + (1 ยท ๐ด))) |
40 | 21 | adantr 482 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ โ) โ (1
ยท ๐ด) = ๐ด) |
41 | 40 | oveq2d 7377 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ โ) โ ((๐ ยท ๐ด) + (1 ยท ๐ด)) = ((๐ ยท ๐ด) + ๐ด)) |
42 | 39, 41 | eqtrd 2773 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ) โ ((๐ + 1) ยท ๐ด) = ((๐ ยท ๐ด) + ๐ด)) |
43 | 33, 42 | eqeq12d 2749 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โ) โ ((seq1(
+ , (โ ร {๐ด}))โ(๐ + 1)) = ((๐ + 1) ยท ๐ด) โ ((seq1( + , (โ ร {๐ด}))โ๐) + ๐ด) = ((๐ ยท ๐ด) + ๐ด))) |
44 | 24, 43 | imbitrrid 245 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ โ) โ ((seq1(
+ , (โ ร {๐ด}))โ๐) = (๐ ยท ๐ด) โ (seq1( + , (โ ร {๐ด}))โ(๐ + 1)) = ((๐ + 1) ยท ๐ด))) |
45 | 44 | expcom 415 |
. . . 4
โข (๐ โ โ โ (๐ด โ โ โ ((seq1( +
, (โ ร {๐ด}))โ๐) = (๐ ยท ๐ด) โ (seq1( + , (โ ร {๐ด}))โ(๐ + 1)) = ((๐ + 1) ยท ๐ด)))) |
46 | 45 | a2d 29 |
. . 3
โข (๐ โ โ โ ((๐ด โ โ โ (seq1( +
, (โ ร {๐ด}))โ๐) = (๐ ยท ๐ด)) โ (๐ด โ โ โ (seq1( + , (โ
ร {๐ด}))โ(๐ + 1)) = ((๐ + 1) ยท ๐ด)))) |
47 | 4, 8, 12, 16, 23, 46 | nnind 12179 |
. 2
โข (๐ โ โ โ (๐ด โ โ โ (seq1( +
, (โ ร {๐ด}))โ๐) = (๐ ยท ๐ด))) |
48 | 47 | impcom 409 |
1
โข ((๐ด โ โ โง ๐ โ โ) โ (seq1( +
, (โ ร {๐ด}))โ๐) = (๐ ยท ๐ด)) |