Step | Hyp | Ref
| Expression |
1 | | oveq2 5882 |
. . . . . . 7
โข (๐ = 0 โ (๐ ยท ๐) = (๐ ยท 0)) |
2 | 1 | oveq2d 5890 |
. . . . . 6
โข (๐ = 0 โ (๐ดโ(๐ ยท ๐)) = (๐ดโ(๐ ยท 0))) |
3 | | oveq2 5882 |
. . . . . 6
โข (๐ = 0 โ ((๐ดโ๐)โ๐) = ((๐ดโ๐)โ0)) |
4 | 2, 3 | eqeq12d 2192 |
. . . . 5
โข (๐ = 0 โ ((๐ดโ(๐ ยท ๐)) = ((๐ดโ๐)โ๐) โ (๐ดโ(๐ ยท 0)) = ((๐ดโ๐)โ0))) |
5 | 4 | imbi2d 230 |
. . . 4
โข (๐ = 0 โ (((๐ด โ โ โง ๐ โ โ0) โ (๐ดโ(๐ ยท ๐)) = ((๐ดโ๐)โ๐)) โ ((๐ด โ โ โง ๐ โ โ0) โ (๐ดโ(๐ ยท 0)) = ((๐ดโ๐)โ0)))) |
6 | | oveq2 5882 |
. . . . . . 7
โข (๐ = ๐ โ (๐ ยท ๐) = (๐ ยท ๐)) |
7 | 6 | oveq2d 5890 |
. . . . . 6
โข (๐ = ๐ โ (๐ดโ(๐ ยท ๐)) = (๐ดโ(๐ ยท ๐))) |
8 | | oveq2 5882 |
. . . . . 6
โข (๐ = ๐ โ ((๐ดโ๐)โ๐) = ((๐ดโ๐)โ๐)) |
9 | 7, 8 | eqeq12d 2192 |
. . . . 5
โข (๐ = ๐ โ ((๐ดโ(๐ ยท ๐)) = ((๐ดโ๐)โ๐) โ (๐ดโ(๐ ยท ๐)) = ((๐ดโ๐)โ๐))) |
10 | 9 | imbi2d 230 |
. . . 4
โข (๐ = ๐ โ (((๐ด โ โ โง ๐ โ โ0) โ (๐ดโ(๐ ยท ๐)) = ((๐ดโ๐)โ๐)) โ ((๐ด โ โ โง ๐ โ โ0) โ (๐ดโ(๐ ยท ๐)) = ((๐ดโ๐)โ๐)))) |
11 | | oveq2 5882 |
. . . . . . 7
โข (๐ = (๐ + 1) โ (๐ ยท ๐) = (๐ ยท (๐ + 1))) |
12 | 11 | oveq2d 5890 |
. . . . . 6
โข (๐ = (๐ + 1) โ (๐ดโ(๐ ยท ๐)) = (๐ดโ(๐ ยท (๐ + 1)))) |
13 | | oveq2 5882 |
. . . . . 6
โข (๐ = (๐ + 1) โ ((๐ดโ๐)โ๐) = ((๐ดโ๐)โ(๐ + 1))) |
14 | 12, 13 | eqeq12d 2192 |
. . . . 5
โข (๐ = (๐ + 1) โ ((๐ดโ(๐ ยท ๐)) = ((๐ดโ๐)โ๐) โ (๐ดโ(๐ ยท (๐ + 1))) = ((๐ดโ๐)โ(๐ + 1)))) |
15 | 14 | imbi2d 230 |
. . . 4
โข (๐ = (๐ + 1) โ (((๐ด โ โ โง ๐ โ โ0) โ (๐ดโ(๐ ยท ๐)) = ((๐ดโ๐)โ๐)) โ ((๐ด โ โ โง ๐ โ โ0) โ (๐ดโ(๐ ยท (๐ + 1))) = ((๐ดโ๐)โ(๐ + 1))))) |
16 | | oveq2 5882 |
. . . . . . 7
โข (๐ = ๐ โ (๐ ยท ๐) = (๐ ยท ๐)) |
17 | 16 | oveq2d 5890 |
. . . . . 6
โข (๐ = ๐ โ (๐ดโ(๐ ยท ๐)) = (๐ดโ(๐ ยท ๐))) |
18 | | oveq2 5882 |
. . . . . 6
โข (๐ = ๐ โ ((๐ดโ๐)โ๐) = ((๐ดโ๐)โ๐)) |
19 | 17, 18 | eqeq12d 2192 |
. . . . 5
โข (๐ = ๐ โ ((๐ดโ(๐ ยท ๐)) = ((๐ดโ๐)โ๐) โ (๐ดโ(๐ ยท ๐)) = ((๐ดโ๐)โ๐))) |
20 | 19 | imbi2d 230 |
. . . 4
โข (๐ = ๐ โ (((๐ด โ โ โง ๐ โ โ0) โ (๐ดโ(๐ ยท ๐)) = ((๐ดโ๐)โ๐)) โ ((๐ด โ โ โง ๐ โ โ0) โ (๐ดโ(๐ ยท ๐)) = ((๐ดโ๐)โ๐)))) |
21 | | nn0cn 9185 |
. . . . . . . 8
โข (๐ โ โ0
โ ๐ โ
โ) |
22 | 21 | mul01d 8349 |
. . . . . . 7
โข (๐ โ โ0
โ (๐ ยท 0) =
0) |
23 | 22 | oveq2d 5890 |
. . . . . 6
โข (๐ โ โ0
โ (๐ดโ(๐ ยท 0)) = (๐ดโ0)) |
24 | | exp0 10523 |
. . . . . 6
โข (๐ด โ โ โ (๐ดโ0) = 1) |
25 | 23, 24 | sylan9eqr 2232 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ(๐ ยท 0)) =
1) |
26 | | expcl 10537 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ๐) โ
โ) |
27 | | exp0 10523 |
. . . . . 6
โข ((๐ดโ๐) โ โ โ ((๐ดโ๐)โ0) = 1) |
28 | 26, 27 | syl 14 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ โ0)
โ ((๐ดโ๐)โ0) = 1) |
29 | 25, 28 | eqtr4d 2213 |
. . . 4
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ(๐ ยท 0)) = ((๐ดโ๐)โ0)) |
30 | | oveq1 5881 |
. . . . . . 7
โข ((๐ดโ(๐ ยท ๐)) = ((๐ดโ๐)โ๐) โ ((๐ดโ(๐ ยท ๐)) ยท (๐ดโ๐)) = (((๐ดโ๐)โ๐) ยท (๐ดโ๐))) |
31 | | nn0cn 9185 |
. . . . . . . . . . . 12
โข (๐ โ โ0
โ ๐ โ
โ) |
32 | | ax-1cn 7903 |
. . . . . . . . . . . . . 14
โข 1 โ
โ |
33 | | adddi 7942 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐ โ โ โง 1 โ
โ) โ (๐ ยท
(๐ + 1)) = ((๐ ยท ๐) + (๐ ยท 1))) |
34 | 32, 33 | mp3an3 1326 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท (๐ + 1)) = ((๐ ยท ๐) + (๐ ยท 1))) |
35 | | mulrid 7953 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ (๐ ยท 1) = ๐) |
36 | 35 | adantr 276 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท 1) = ๐) |
37 | 36 | oveq2d 5890 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ ยท ๐) + (๐ ยท 1)) = ((๐ ยท ๐) + ๐)) |
38 | 34, 37 | eqtrd 2210 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท (๐ + 1)) = ((๐ ยท ๐) + ๐)) |
39 | 21, 31, 38 | syl2an 289 |
. . . . . . . . . . 11
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐ ยท (๐ + 1)) = ((๐ ยท ๐) + ๐)) |
40 | 39 | adantll 476 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ โ
โ0) โ (๐ ยท (๐ + 1)) = ((๐ ยท ๐) + ๐)) |
41 | 40 | oveq2d 5890 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ โ
โ0) โ (๐ดโ(๐ ยท (๐ + 1))) = (๐ดโ((๐ ยท ๐) + ๐))) |
42 | | simpll 527 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ โ
โ0) โ ๐ด โ โ) |
43 | | nn0mulcl 9211 |
. . . . . . . . . . 11
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐ ยท ๐) โ
โ0) |
44 | 43 | adantll 476 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ โ
โ0) โ (๐ ยท ๐) โ
โ0) |
45 | | simplr 528 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ โ
โ0) โ ๐ โ
โ0) |
46 | | expadd 10561 |
. . . . . . . . . 10
โข ((๐ด โ โ โง (๐ ยท ๐) โ โ0 โง ๐ โ โ0)
โ (๐ดโ((๐ ยท ๐) + ๐)) = ((๐ดโ(๐ ยท ๐)) ยท (๐ดโ๐))) |
47 | 42, 44, 45, 46 | syl3anc 1238 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ โ
โ0) โ (๐ดโ((๐ ยท ๐) + ๐)) = ((๐ดโ(๐ ยท ๐)) ยท (๐ดโ๐))) |
48 | 41, 47 | eqtrd 2210 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ โ
โ0) โ (๐ดโ(๐ ยท (๐ + 1))) = ((๐ดโ(๐ ยท ๐)) ยท (๐ดโ๐))) |
49 | | expp1 10526 |
. . . . . . . . 9
โข (((๐ดโ๐) โ โ โง ๐ โ โ0) โ ((๐ดโ๐)โ(๐ + 1)) = (((๐ดโ๐)โ๐) ยท (๐ดโ๐))) |
50 | 26, 49 | sylan 283 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ โ
โ0) โ ((๐ดโ๐)โ(๐ + 1)) = (((๐ดโ๐)โ๐) ยท (๐ดโ๐))) |
51 | 48, 50 | eqeq12d 2192 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ โ
โ0) โ ((๐ดโ(๐ ยท (๐ + 1))) = ((๐ดโ๐)โ(๐ + 1)) โ ((๐ดโ(๐ ยท ๐)) ยท (๐ดโ๐)) = (((๐ดโ๐)โ๐) ยท (๐ดโ๐)))) |
52 | 30, 51 | imbitrrid 156 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ โ
โ0) โ ((๐ดโ(๐ ยท ๐)) = ((๐ดโ๐)โ๐) โ (๐ดโ(๐ ยท (๐ + 1))) = ((๐ดโ๐)โ(๐ + 1)))) |
53 | 52 | expcom 116 |
. . . . 5
โข (๐ โ โ0
โ ((๐ด โ โ
โง ๐ โ
โ0) โ ((๐ดโ(๐ ยท ๐)) = ((๐ดโ๐)โ๐) โ (๐ดโ(๐ ยท (๐ + 1))) = ((๐ดโ๐)โ(๐ + 1))))) |
54 | 53 | a2d 26 |
. . . 4
โข (๐ โ โ0
โ (((๐ด โ โ
โง ๐ โ
โ0) โ (๐ดโ(๐ ยท ๐)) = ((๐ดโ๐)โ๐)) โ ((๐ด โ โ โง ๐ โ โ0) โ (๐ดโ(๐ ยท (๐ + 1))) = ((๐ดโ๐)โ(๐ + 1))))) |
55 | 5, 10, 15, 20, 29, 54 | nn0ind 9366 |
. . 3
โข (๐ โ โ0
โ ((๐ด โ โ
โง ๐ โ
โ0) โ (๐ดโ(๐ ยท ๐)) = ((๐ดโ๐)โ๐))) |
56 | 55 | expdcom 1442 |
. 2
โข (๐ด โ โ โ (๐ โ โ0
โ (๐ โ
โ0 โ (๐ดโ(๐ ยท ๐)) = ((๐ดโ๐)โ๐)))) |
57 | 56 | 3imp 1193 |
1
โข ((๐ด โ โ โง ๐ โ โ0
โง ๐ โ
โ0) โ (๐ดโ(๐ ยท ๐)) = ((๐ดโ๐)โ๐)) |