Step | Hyp | Ref
| Expression |
1 | | oveq2 7420 |
. . . . . . 7
โข (๐ = 0 โ (๐ ยท ๐) = (๐ ยท 0)) |
2 | 1 | oveq2d 7428 |
. . . . . 6
โข (๐ = 0 โ (๐ดโ(๐ ยท ๐)) = (๐ดโ(๐ ยท 0))) |
3 | | oveq2 7420 |
. . . . . 6
โข (๐ = 0 โ ((๐ดโ๐)โ๐) = ((๐ดโ๐)โ0)) |
4 | 2, 3 | eqeq12d 2747 |
. . . . 5
โข (๐ = 0 โ ((๐ดโ(๐ ยท ๐)) = ((๐ดโ๐)โ๐) โ (๐ดโ(๐ ยท 0)) = ((๐ดโ๐)โ0))) |
5 | 4 | imbi2d 340 |
. . . 4
โข (๐ = 0 โ (((๐ด โ โ โง ๐ โ โ0) โ (๐ดโ(๐ ยท ๐)) = ((๐ดโ๐)โ๐)) โ ((๐ด โ โ โง ๐ โ โ0) โ (๐ดโ(๐ ยท 0)) = ((๐ดโ๐)โ0)))) |
6 | | oveq2 7420 |
. . . . . . 7
โข (๐ = ๐ โ (๐ ยท ๐) = (๐ ยท ๐)) |
7 | 6 | oveq2d 7428 |
. . . . . 6
โข (๐ = ๐ โ (๐ดโ(๐ ยท ๐)) = (๐ดโ(๐ ยท ๐))) |
8 | | oveq2 7420 |
. . . . . 6
โข (๐ = ๐ โ ((๐ดโ๐)โ๐) = ((๐ดโ๐)โ๐)) |
9 | 7, 8 | eqeq12d 2747 |
. . . . 5
โข (๐ = ๐ โ ((๐ดโ(๐ ยท ๐)) = ((๐ดโ๐)โ๐) โ (๐ดโ(๐ ยท ๐)) = ((๐ดโ๐)โ๐))) |
10 | 9 | imbi2d 340 |
. . . 4
โข (๐ = ๐ โ (((๐ด โ โ โง ๐ โ โ0) โ (๐ดโ(๐ ยท ๐)) = ((๐ดโ๐)โ๐)) โ ((๐ด โ โ โง ๐ โ โ0) โ (๐ดโ(๐ ยท ๐)) = ((๐ดโ๐)โ๐)))) |
11 | | oveq2 7420 |
. . . . . . 7
โข (๐ = (๐ + 1) โ (๐ ยท ๐) = (๐ ยท (๐ + 1))) |
12 | 11 | oveq2d 7428 |
. . . . . 6
โข (๐ = (๐ + 1) โ (๐ดโ(๐ ยท ๐)) = (๐ดโ(๐ ยท (๐ + 1)))) |
13 | | oveq2 7420 |
. . . . . 6
โข (๐ = (๐ + 1) โ ((๐ดโ๐)โ๐) = ((๐ดโ๐)โ(๐ + 1))) |
14 | 12, 13 | eqeq12d 2747 |
. . . . 5
โข (๐ = (๐ + 1) โ ((๐ดโ(๐ ยท ๐)) = ((๐ดโ๐)โ๐) โ (๐ดโ(๐ ยท (๐ + 1))) = ((๐ดโ๐)โ(๐ + 1)))) |
15 | 14 | imbi2d 340 |
. . . 4
โข (๐ = (๐ + 1) โ (((๐ด โ โ โง ๐ โ โ0) โ (๐ดโ(๐ ยท ๐)) = ((๐ดโ๐)โ๐)) โ ((๐ด โ โ โง ๐ โ โ0) โ (๐ดโ(๐ ยท (๐ + 1))) = ((๐ดโ๐)โ(๐ + 1))))) |
16 | | oveq2 7420 |
. . . . . . 7
โข (๐ = ๐ โ (๐ ยท ๐) = (๐ ยท ๐)) |
17 | 16 | oveq2d 7428 |
. . . . . 6
โข (๐ = ๐ โ (๐ดโ(๐ ยท ๐)) = (๐ดโ(๐ ยท ๐))) |
18 | | oveq2 7420 |
. . . . . 6
โข (๐ = ๐ โ ((๐ดโ๐)โ๐) = ((๐ดโ๐)โ๐)) |
19 | 17, 18 | eqeq12d 2747 |
. . . . 5
โข (๐ = ๐ โ ((๐ดโ(๐ ยท ๐)) = ((๐ดโ๐)โ๐) โ (๐ดโ(๐ ยท ๐)) = ((๐ดโ๐)โ๐))) |
20 | 19 | imbi2d 340 |
. . . 4
โข (๐ = ๐ โ (((๐ด โ โ โง ๐ โ โ0) โ (๐ดโ(๐ ยท ๐)) = ((๐ดโ๐)โ๐)) โ ((๐ด โ โ โง ๐ โ โ0) โ (๐ดโ(๐ ยท ๐)) = ((๐ดโ๐)โ๐)))) |
21 | | nn0cn 12489 |
. . . . . . . 8
โข (๐ โ โ0
โ ๐ โ
โ) |
22 | 21 | mul01d 11420 |
. . . . . . 7
โข (๐ โ โ0
โ (๐ ยท 0) =
0) |
23 | 22 | oveq2d 7428 |
. . . . . 6
โข (๐ โ โ0
โ (๐ดโ(๐ ยท 0)) = (๐ดโ0)) |
24 | | exp0 14038 |
. . . . . 6
โข (๐ด โ โ โ (๐ดโ0) = 1) |
25 | 23, 24 | sylan9eqr 2793 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ(๐ ยท 0)) =
1) |
26 | | expcl 14052 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ๐) โ
โ) |
27 | | exp0 14038 |
. . . . . 6
โข ((๐ดโ๐) โ โ โ ((๐ดโ๐)โ0) = 1) |
28 | 26, 27 | syl 17 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ โ0)
โ ((๐ดโ๐)โ0) = 1) |
29 | 25, 28 | eqtr4d 2774 |
. . . 4
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ(๐ ยท 0)) = ((๐ดโ๐)โ0)) |
30 | | oveq1 7419 |
. . . . . . 7
โข ((๐ดโ(๐ ยท ๐)) = ((๐ดโ๐)โ๐) โ ((๐ดโ(๐ ยท ๐)) ยท (๐ดโ๐)) = (((๐ดโ๐)โ๐) ยท (๐ดโ๐))) |
31 | | nn0cn 12489 |
. . . . . . . . . . . 12
โข (๐ โ โ0
โ ๐ โ
โ) |
32 | | ax-1cn 11174 |
. . . . . . . . . . . . . 14
โข 1 โ
โ |
33 | | adddi 11205 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐ โ โ โง 1 โ
โ) โ (๐ ยท
(๐ + 1)) = ((๐ ยท ๐) + (๐ ยท 1))) |
34 | 32, 33 | mp3an3 1449 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท (๐ + 1)) = ((๐ ยท ๐) + (๐ ยท 1))) |
35 | | mulrid 11219 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ (๐ ยท 1) = ๐) |
36 | 35 | adantr 480 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท 1) = ๐) |
37 | 36 | oveq2d 7428 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ โ) โ ((๐ ยท ๐) + (๐ ยท 1)) = ((๐ ยท ๐) + ๐)) |
38 | 34, 37 | eqtrd 2771 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท (๐ + 1)) = ((๐ ยท ๐) + ๐)) |
39 | 21, 31, 38 | syl2an 595 |
. . . . . . . . . . 11
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐ ยท (๐ + 1)) = ((๐ ยท ๐) + ๐)) |
40 | 39 | adantll 711 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ โ
โ0) โ (๐ ยท (๐ + 1)) = ((๐ ยท ๐) + ๐)) |
41 | 40 | oveq2d 7428 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ โ
โ0) โ (๐ดโ(๐ ยท (๐ + 1))) = (๐ดโ((๐ ยท ๐) + ๐))) |
42 | | simpll 764 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ โ
โ0) โ ๐ด โ โ) |
43 | | nn0mulcl 12515 |
. . . . . . . . . . 11
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐ ยท ๐) โ
โ0) |
44 | 43 | adantll 711 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ โ
โ0) โ (๐ ยท ๐) โ
โ0) |
45 | | simplr 766 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ โ
โ0) โ ๐ โ
โ0) |
46 | | expadd 14077 |
. . . . . . . . . 10
โข ((๐ด โ โ โง (๐ ยท ๐) โ โ0 โง ๐ โ โ0)
โ (๐ดโ((๐ ยท ๐) + ๐)) = ((๐ดโ(๐ ยท ๐)) ยท (๐ดโ๐))) |
47 | 42, 44, 45, 46 | syl3anc 1370 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ โ
โ0) โ (๐ดโ((๐ ยท ๐) + ๐)) = ((๐ดโ(๐ ยท ๐)) ยท (๐ดโ๐))) |
48 | 41, 47 | eqtrd 2771 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ โ
โ0) โ (๐ดโ(๐ ยท (๐ + 1))) = ((๐ดโ(๐ ยท ๐)) ยท (๐ดโ๐))) |
49 | | expp1 14041 |
. . . . . . . . 9
โข (((๐ดโ๐) โ โ โง ๐ โ โ0) โ ((๐ดโ๐)โ(๐ + 1)) = (((๐ดโ๐)โ๐) ยท (๐ดโ๐))) |
50 | 26, 49 | sylan 579 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ โ
โ0) โ ((๐ดโ๐)โ(๐ + 1)) = (((๐ดโ๐)โ๐) ยท (๐ดโ๐))) |
51 | 48, 50 | eqeq12d 2747 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ โ
โ0) โ ((๐ดโ(๐ ยท (๐ + 1))) = ((๐ดโ๐)โ(๐ + 1)) โ ((๐ดโ(๐ ยท ๐)) ยท (๐ดโ๐)) = (((๐ดโ๐)โ๐) ยท (๐ดโ๐)))) |
52 | 30, 51 | imbitrrid 245 |
. . . . . 6
โข (((๐ด โ โ โง ๐ โ โ0)
โง ๐ โ
โ0) โ ((๐ดโ(๐ ยท ๐)) = ((๐ดโ๐)โ๐) โ (๐ดโ(๐ ยท (๐ + 1))) = ((๐ดโ๐)โ(๐ + 1)))) |
53 | 52 | expcom 413 |
. . . . 5
โข (๐ โ โ0
โ ((๐ด โ โ
โง ๐ โ
โ0) โ ((๐ดโ(๐ ยท ๐)) = ((๐ดโ๐)โ๐) โ (๐ดโ(๐ ยท (๐ + 1))) = ((๐ดโ๐)โ(๐ + 1))))) |
54 | 53 | a2d 29 |
. . . 4
โข (๐ โ โ0
โ (((๐ด โ โ
โง ๐ โ
โ0) โ (๐ดโ(๐ ยท ๐)) = ((๐ดโ๐)โ๐)) โ ((๐ด โ โ โง ๐ โ โ0) โ (๐ดโ(๐ ยท (๐ + 1))) = ((๐ดโ๐)โ(๐ + 1))))) |
55 | 5, 10, 15, 20, 29, 54 | nn0ind 12664 |
. . 3
โข (๐ โ โ0
โ ((๐ด โ โ
โง ๐ โ
โ0) โ (๐ดโ(๐ ยท ๐)) = ((๐ดโ๐)โ๐))) |
56 | 55 | expdcom 414 |
. 2
โข (๐ด โ โ โ (๐ โ โ0
โ (๐ โ
โ0 โ (๐ดโ(๐ ยท ๐)) = ((๐ดโ๐)โ๐)))) |
57 | 56 | 3imp 1110 |
1
โข ((๐ด โ โ โง ๐ โ โ0
โง ๐ โ
โ0) โ (๐ดโ(๐ ยท ๐)) = ((๐ดโ๐)โ๐)) |