Step | Hyp | Ref
| Expression |
1 | | oveq2 7413 |
. . . 4
โข (๐ = 0 โ (๐ดโ๐) = (๐ดโ0)) |
2 | 1 | fveq2d 6892 |
. . 3
โข (๐ = 0 โ (absโ(๐ดโ๐)) = (absโ(๐ดโ0))) |
3 | | oveq2 7413 |
. . 3
โข (๐ = 0 โ ((absโ๐ด)โ๐) = ((absโ๐ด)โ0)) |
4 | 2, 3 | eqeq12d 2748 |
. 2
โข (๐ = 0 โ ((absโ(๐ดโ๐)) = ((absโ๐ด)โ๐) โ (absโ(๐ดโ0)) = ((absโ๐ด)โ0))) |
5 | | oveq2 7413 |
. . . 4
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
6 | 5 | fveq2d 6892 |
. . 3
โข (๐ = ๐ โ (absโ(๐ดโ๐)) = (absโ(๐ดโ๐))) |
7 | | oveq2 7413 |
. . 3
โข (๐ = ๐ โ ((absโ๐ด)โ๐) = ((absโ๐ด)โ๐)) |
8 | 6, 7 | eqeq12d 2748 |
. 2
โข (๐ = ๐ โ ((absโ(๐ดโ๐)) = ((absโ๐ด)โ๐) โ (absโ(๐ดโ๐)) = ((absโ๐ด)โ๐))) |
9 | | oveq2 7413 |
. . . 4
โข (๐ = (๐ + 1) โ (๐ดโ๐) = (๐ดโ(๐ + 1))) |
10 | 9 | fveq2d 6892 |
. . 3
โข (๐ = (๐ + 1) โ (absโ(๐ดโ๐)) = (absโ(๐ดโ(๐ + 1)))) |
11 | | oveq2 7413 |
. . 3
โข (๐ = (๐ + 1) โ ((absโ๐ด)โ๐) = ((absโ๐ด)โ(๐ + 1))) |
12 | 10, 11 | eqeq12d 2748 |
. 2
โข (๐ = (๐ + 1) โ ((absโ(๐ดโ๐)) = ((absโ๐ด)โ๐) โ (absโ(๐ดโ(๐ + 1))) = ((absโ๐ด)โ(๐ + 1)))) |
13 | | oveq2 7413 |
. . . 4
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
14 | 13 | fveq2d 6892 |
. . 3
โข (๐ = ๐ โ (absโ(๐ดโ๐)) = (absโ(๐ดโ๐))) |
15 | | oveq2 7413 |
. . 3
โข (๐ = ๐ โ ((absโ๐ด)โ๐) = ((absโ๐ด)โ๐)) |
16 | 14, 15 | eqeq12d 2748 |
. 2
โข (๐ = ๐ โ ((absโ(๐ดโ๐)) = ((absโ๐ด)โ๐) โ (absโ(๐ดโ๐)) = ((absโ๐ด)โ๐))) |
17 | | abs1 15240 |
. . 3
โข
(absโ1) = 1 |
18 | | exp0 14027 |
. . . 4
โข (๐ด โ โ โ (๐ดโ0) = 1) |
19 | 18 | fveq2d 6892 |
. . 3
โข (๐ด โ โ โ
(absโ(๐ดโ0)) =
(absโ1)) |
20 | | abscl 15221 |
. . . . 5
โข (๐ด โ โ โ
(absโ๐ด) โ
โ) |
21 | 20 | recnd 11238 |
. . . 4
โข (๐ด โ โ โ
(absโ๐ด) โ
โ) |
22 | 21 | exp0d 14101 |
. . 3
โข (๐ด โ โ โ
((absโ๐ด)โ0) =
1) |
23 | 17, 19, 22 | 3eqtr4a 2798 |
. 2
โข (๐ด โ โ โ
(absโ(๐ดโ0)) =
((absโ๐ด)โ0)) |
24 | | oveq1 7412 |
. . . 4
โข
((absโ(๐ดโ๐)) = ((absโ๐ด)โ๐) โ ((absโ(๐ดโ๐)) ยท (absโ๐ด)) = (((absโ๐ด)โ๐) ยท (absโ๐ด))) |
25 | 24 | adantl 482 |
. . 3
โข (((๐ด โ โ โง ๐ โ โ0)
โง (absโ(๐ดโ๐)) = ((absโ๐ด)โ๐)) โ ((absโ(๐ดโ๐)) ยท (absโ๐ด)) = (((absโ๐ด)โ๐) ยท (absโ๐ด))) |
26 | | expp1 14030 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ(๐ + 1)) = ((๐ดโ๐) ยท ๐ด)) |
27 | 26 | fveq2d 6892 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ โ0)
โ (absโ(๐ดโ(๐ + 1))) = (absโ((๐ดโ๐) ยท ๐ด))) |
28 | | expcl 14041 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ๐) โ
โ) |
29 | | simpl 483 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โ0)
โ ๐ด โ
โ) |
30 | | absmul 15237 |
. . . . . 6
โข (((๐ดโ๐) โ โ โง ๐ด โ โ) โ (absโ((๐ดโ๐) ยท ๐ด)) = ((absโ(๐ดโ๐)) ยท (absโ๐ด))) |
31 | 28, 29, 30 | syl2anc 584 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ โ0)
โ (absโ((๐ดโ๐) ยท ๐ด)) = ((absโ(๐ดโ๐)) ยท (absโ๐ด))) |
32 | 27, 31 | eqtrd 2772 |
. . . 4
โข ((๐ด โ โ โง ๐ โ โ0)
โ (absโ(๐ดโ(๐ + 1))) = ((absโ(๐ดโ๐)) ยท (absโ๐ด))) |
33 | 32 | adantr 481 |
. . 3
โข (((๐ด โ โ โง ๐ โ โ0)
โง (absโ(๐ดโ๐)) = ((absโ๐ด)โ๐)) โ (absโ(๐ดโ(๐ + 1))) = ((absโ(๐ดโ๐)) ยท (absโ๐ด))) |
34 | | expp1 14030 |
. . . . 5
โข
(((absโ๐ด)
โ โ โง ๐
โ โ0) โ ((absโ๐ด)โ(๐ + 1)) = (((absโ๐ด)โ๐) ยท (absโ๐ด))) |
35 | 21, 34 | sylan 580 |
. . . 4
โข ((๐ด โ โ โง ๐ โ โ0)
โ ((absโ๐ด)โ(๐ + 1)) = (((absโ๐ด)โ๐) ยท (absโ๐ด))) |
36 | 35 | adantr 481 |
. . 3
โข (((๐ด โ โ โง ๐ โ โ0)
โง (absโ(๐ดโ๐)) = ((absโ๐ด)โ๐)) โ ((absโ๐ด)โ(๐ + 1)) = (((absโ๐ด)โ๐) ยท (absโ๐ด))) |
37 | 25, 33, 36 | 3eqtr4d 2782 |
. 2
โข (((๐ด โ โ โง ๐ โ โ0)
โง (absโ(๐ดโ๐)) = ((absโ๐ด)โ๐)) โ (absโ(๐ดโ(๐ + 1))) = ((absโ๐ด)โ(๐ + 1))) |
38 | 4, 8, 12, 16, 23, 37 | nn0indd 12655 |
1
โข ((๐ด โ โ โง ๐ โ โ0)
โ (absโ(๐ดโ๐)) = ((absโ๐ด)โ๐)) |