Step | Hyp | Ref
| Expression |
1 | | oveq2 7370 |
. . . 4
โข (๐ = 0 โ (๐ดโ๐) = (๐ดโ0)) |
2 | 1 | fveq2d 6851 |
. . 3
โข (๐ = 0 โ
(โโ(๐ดโ๐)) = (โโ(๐ดโ0))) |
3 | | oveq2 7370 |
. . 3
โข (๐ = 0 โ
((โโ๐ด)โ๐) = ((โโ๐ด)โ0)) |
4 | 2, 3 | eqeq12d 2753 |
. 2
โข (๐ = 0 โ
((โโ(๐ดโ๐)) = ((โโ๐ด)โ๐) โ (โโ(๐ดโ0)) = ((โโ๐ด)โ0))) |
5 | | oveq2 7370 |
. . . 4
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
6 | 5 | fveq2d 6851 |
. . 3
โข (๐ = ๐ โ (โโ(๐ดโ๐)) = (โโ(๐ดโ๐))) |
7 | | oveq2 7370 |
. . 3
โข (๐ = ๐ โ ((โโ๐ด)โ๐) = ((โโ๐ด)โ๐)) |
8 | 6, 7 | eqeq12d 2753 |
. 2
โข (๐ = ๐ โ ((โโ(๐ดโ๐)) = ((โโ๐ด)โ๐) โ (โโ(๐ดโ๐)) = ((โโ๐ด)โ๐))) |
9 | | oveq2 7370 |
. . . 4
โข (๐ = (๐ + 1) โ (๐ดโ๐) = (๐ดโ(๐ + 1))) |
10 | 9 | fveq2d 6851 |
. . 3
โข (๐ = (๐ + 1) โ (โโ(๐ดโ๐)) = (โโ(๐ดโ(๐ + 1)))) |
11 | | oveq2 7370 |
. . 3
โข (๐ = (๐ + 1) โ ((โโ๐ด)โ๐) = ((โโ๐ด)โ(๐ + 1))) |
12 | 10, 11 | eqeq12d 2753 |
. 2
โข (๐ = (๐ + 1) โ ((โโ(๐ดโ๐)) = ((โโ๐ด)โ๐) โ (โโ(๐ดโ(๐ + 1))) = ((โโ๐ด)โ(๐ + 1)))) |
13 | | oveq2 7370 |
. . . 4
โข (๐ = ๐ โ (๐ดโ๐) = (๐ดโ๐)) |
14 | 13 | fveq2d 6851 |
. . 3
โข (๐ = ๐ โ (โโ(๐ดโ๐)) = (โโ(๐ดโ๐))) |
15 | | oveq2 7370 |
. . 3
โข (๐ = ๐ โ ((โโ๐ด)โ๐) = ((โโ๐ด)โ๐)) |
16 | 14, 15 | eqeq12d 2753 |
. 2
โข (๐ = ๐ โ ((โโ(๐ดโ๐)) = ((โโ๐ด)โ๐) โ (โโ(๐ดโ๐)) = ((โโ๐ด)โ๐))) |
17 | | exp0 13978 |
. . . 4
โข (๐ด โ โ โ (๐ดโ0) = 1) |
18 | 17 | fveq2d 6851 |
. . 3
โข (๐ด โ โ โ
(โโ(๐ดโ0))
= (โโ1)) |
19 | | cjcl 14997 |
. . . 4
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
20 | | exp0 13978 |
. . . . 5
โข
((โโ๐ด)
โ โ โ ((โโ๐ด)โ0) = 1) |
21 | | 1re 11162 |
. . . . . 6
โข 1 โ
โ |
22 | | cjre 15031 |
. . . . . 6
โข (1 โ
โ โ (โโ1) = 1) |
23 | 21, 22 | ax-mp 5 |
. . . . 5
โข
(โโ1) = 1 |
24 | 20, 23 | eqtr4di 2795 |
. . . 4
โข
((โโ๐ด)
โ โ โ ((โโ๐ด)โ0) =
(โโ1)) |
25 | 19, 24 | syl 17 |
. . 3
โข (๐ด โ โ โ
((โโ๐ด)โ0)
= (โโ1)) |
26 | 18, 25 | eqtr4d 2780 |
. 2
โข (๐ด โ โ โ
(โโ(๐ดโ0))
= ((โโ๐ด)โ0)) |
27 | | expp1 13981 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ(๐ + 1)) = ((๐ดโ๐) ยท ๐ด)) |
28 | 27 | fveq2d 6851 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ โ0)
โ (โโ(๐ดโ(๐ + 1))) = (โโ((๐ดโ๐) ยท ๐ด))) |
29 | | expcl 13992 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ๐) โ
โ) |
30 | | simpl 484 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โ0)
โ ๐ด โ
โ) |
31 | | cjmul 15034 |
. . . . . 6
โข (((๐ดโ๐) โ โ โง ๐ด โ โ) โ
(โโ((๐ดโ๐) ยท ๐ด)) = ((โโ(๐ดโ๐)) ยท (โโ๐ด))) |
32 | 29, 30, 31 | syl2anc 585 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ โ0)
โ (โโ((๐ดโ๐) ยท ๐ด)) = ((โโ(๐ดโ๐)) ยท (โโ๐ด))) |
33 | 28, 32 | eqtrd 2777 |
. . . 4
โข ((๐ด โ โ โง ๐ โ โ0)
โ (โโ(๐ดโ(๐ + 1))) = ((โโ(๐ดโ๐)) ยท (โโ๐ด))) |
34 | 33 | adantr 482 |
. . 3
โข (((๐ด โ โ โง ๐ โ โ0)
โง (โโ(๐ดโ๐)) = ((โโ๐ด)โ๐)) โ (โโ(๐ดโ(๐ + 1))) = ((โโ(๐ดโ๐)) ยท (โโ๐ด))) |
35 | | oveq1 7369 |
. . . 4
โข
((โโ(๐ดโ๐)) = ((โโ๐ด)โ๐) โ ((โโ(๐ดโ๐)) ยท (โโ๐ด)) = (((โโ๐ด)โ๐) ยท (โโ๐ด))) |
36 | | expp1 13981 |
. . . . . 6
โข
(((โโ๐ด)
โ โ โง ๐
โ โ0) โ ((โโ๐ด)โ(๐ + 1)) = (((โโ๐ด)โ๐) ยท (โโ๐ด))) |
37 | 19, 36 | sylan 581 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ โ0)
โ ((โโ๐ด)โ(๐ + 1)) = (((โโ๐ด)โ๐) ยท (โโ๐ด))) |
38 | 37 | eqcomd 2743 |
. . . 4
โข ((๐ด โ โ โง ๐ โ โ0)
โ (((โโ๐ด)โ๐) ยท (โโ๐ด)) = ((โโ๐ด)โ(๐ + 1))) |
39 | 35, 38 | sylan9eqr 2799 |
. . 3
โข (((๐ด โ โ โง ๐ โ โ0)
โง (โโ(๐ดโ๐)) = ((โโ๐ด)โ๐)) โ ((โโ(๐ดโ๐)) ยท (โโ๐ด)) = ((โโ๐ด)โ(๐ + 1))) |
40 | 34, 39 | eqtrd 2777 |
. 2
โข (((๐ด โ โ โง ๐ โ โ0)
โง (โโ(๐ดโ๐)) = ((โโ๐ด)โ๐)) โ (โโ(๐ดโ(๐ + 1))) = ((โโ๐ด)โ(๐ + 1))) |
41 | 4, 8, 12, 16, 26, 40 | nn0indd 12607 |
1
โข ((๐ด โ โ โง ๐ โ โ0)
โ (โโ(๐ดโ๐)) = ((โโ๐ด)โ๐)) |