Step | Hyp | Ref
| Expression |
1 | | renegmulnnass.n |
. 2
โข (๐ โ ๐ โ โ) |
2 | | oveq2 7422 |
. . . 4
โข (๐ฅ = 1 โ ((0
โโ ๐ด) ยท ๐ฅ) = ((0 โโ ๐ด) ยท 1)) |
3 | | oveq2 7422 |
. . . . 5
โข (๐ฅ = 1 โ (๐ด ยท ๐ฅ) = (๐ด ยท 1)) |
4 | 3 | oveq2d 7430 |
. . . 4
โข (๐ฅ = 1 โ (0
โโ (๐ด ยท ๐ฅ)) = (0 โโ (๐ด ยท 1))) |
5 | 2, 4 | eqeq12d 2743 |
. . 3
โข (๐ฅ = 1 โ (((0
โโ ๐ด) ยท ๐ฅ) = (0 โโ (๐ด ยท ๐ฅ)) โ ((0 โโ ๐ด) ยท 1) = (0
โโ (๐ด ยท 1)))) |
6 | | oveq2 7422 |
. . . 4
โข (๐ฅ = ๐ฆ โ ((0 โโ ๐ด) ยท ๐ฅ) = ((0 โโ ๐ด) ยท ๐ฆ)) |
7 | | oveq2 7422 |
. . . . 5
โข (๐ฅ = ๐ฆ โ (๐ด ยท ๐ฅ) = (๐ด ยท ๐ฆ)) |
8 | 7 | oveq2d 7430 |
. . . 4
โข (๐ฅ = ๐ฆ โ (0 โโ (๐ด ยท ๐ฅ)) = (0 โโ (๐ด ยท ๐ฆ))) |
9 | 6, 8 | eqeq12d 2743 |
. . 3
โข (๐ฅ = ๐ฆ โ (((0 โโ ๐ด) ยท ๐ฅ) = (0 โโ (๐ด ยท ๐ฅ)) โ ((0 โโ ๐ด) ยท ๐ฆ) = (0 โโ (๐ด ยท ๐ฆ)))) |
10 | | oveq2 7422 |
. . . 4
โข (๐ฅ = (๐ฆ + 1) โ ((0 โโ
๐ด) ยท ๐ฅ) = ((0
โโ ๐ด) ยท (๐ฆ + 1))) |
11 | | oveq2 7422 |
. . . . 5
โข (๐ฅ = (๐ฆ + 1) โ (๐ด ยท ๐ฅ) = (๐ด ยท (๐ฆ + 1))) |
12 | 11 | oveq2d 7430 |
. . . 4
โข (๐ฅ = (๐ฆ + 1) โ (0 โโ
(๐ด ยท ๐ฅ)) = (0
โโ (๐ด ยท (๐ฆ + 1)))) |
13 | 10, 12 | eqeq12d 2743 |
. . 3
โข (๐ฅ = (๐ฆ + 1) โ (((0 โโ
๐ด) ยท ๐ฅ) = (0 โโ
(๐ด ยท ๐ฅ)) โ ((0
โโ ๐ด) ยท (๐ฆ + 1)) = (0 โโ (๐ด ยท (๐ฆ + 1))))) |
14 | | oveq2 7422 |
. . . 4
โข (๐ฅ = ๐ โ ((0 โโ ๐ด) ยท ๐ฅ) = ((0 โโ ๐ด) ยท ๐)) |
15 | | oveq2 7422 |
. . . . 5
โข (๐ฅ = ๐ โ (๐ด ยท ๐ฅ) = (๐ด ยท ๐)) |
16 | 15 | oveq2d 7430 |
. . . 4
โข (๐ฅ = ๐ โ (0 โโ (๐ด ยท ๐ฅ)) = (0 โโ (๐ด ยท ๐))) |
17 | 14, 16 | eqeq12d 2743 |
. . 3
โข (๐ฅ = ๐ โ (((0 โโ ๐ด) ยท ๐ฅ) = (0 โโ (๐ด ยท ๐ฅ)) โ ((0 โโ ๐ด) ยท ๐) = (0 โโ (๐ด ยท ๐)))) |
18 | | renegmulnnass.a |
. . . . . 6
โข (๐ โ ๐ด โ โ) |
19 | | rernegcl 41848 |
. . . . . 6
โข (๐ด โ โ โ (0
โโ ๐ด) โ โ) |
20 | 18, 19 | syl 17 |
. . . . 5
โข (๐ โ (0
โโ ๐ด) โ โ) |
21 | | ax-1rid 11200 |
. . . . 5
โข ((0
โโ ๐ด) โ โ โ ((0
โโ ๐ด) ยท 1) = (0 โโ
๐ด)) |
22 | 20, 21 | syl 17 |
. . . 4
โข (๐ โ ((0
โโ ๐ด) ยท 1) = (0 โโ
๐ด)) |
23 | | ax-1rid 11200 |
. . . . . 6
โข (๐ด โ โ โ (๐ด ยท 1) = ๐ด) |
24 | 18, 23 | syl 17 |
. . . . 5
โข (๐ โ (๐ด ยท 1) = ๐ด) |
25 | 24 | oveq2d 7430 |
. . . 4
โข (๐ โ (0
โโ (๐ด ยท 1)) = (0 โโ
๐ด)) |
26 | 22, 25 | eqtr4d 2770 |
. . 3
โข (๐ โ ((0
โโ ๐ด) ยท 1) = (0 โโ
(๐ด ยท
1))) |
27 | | simpr 484 |
. . . . . . 7
โข (((๐ โง ๐ฆ โ โ) โง ((0
โโ ๐ด) ยท ๐ฆ) = (0 โโ (๐ด ยท ๐ฆ))) โ ((0 โโ
๐ด) ยท ๐ฆ) = (0 โโ
(๐ด ยท ๐ฆ))) |
28 | 27 | oveq2d 7430 |
. . . . . 6
โข (((๐ โง ๐ฆ โ โ) โง ((0
โโ ๐ด) ยท ๐ฆ) = (0 โโ (๐ด ยท ๐ฆ))) โ ((0 โโ
๐ด) + ((0
โโ ๐ด) ยท ๐ฆ)) = ((0 โโ ๐ด) + (0 โโ
(๐ด ยท ๐ฆ)))) |
29 | | 0red 11239 |
. . . . . . . 8
โข (((๐ โง ๐ฆ โ โ) โง ((0
โโ ๐ด) ยท ๐ฆ) = (0 โโ (๐ด ยท ๐ฆ))) โ 0 โ โ) |
30 | 18 | ad2antrr 725 |
. . . . . . . . . 10
โข (((๐ โง ๐ฆ โ โ) โง ((0
โโ ๐ด) ยท ๐ฆ) = (0 โโ (๐ด ยท ๐ฆ))) โ ๐ด โ โ) |
31 | | nnre 12241 |
. . . . . . . . . . 11
โข (๐ฆ โ โ โ ๐ฆ โ
โ) |
32 | 31 | ad2antlr 726 |
. . . . . . . . . 10
โข (((๐ โง ๐ฆ โ โ) โง ((0
โโ ๐ด) ยท ๐ฆ) = (0 โโ (๐ด ยท ๐ฆ))) โ ๐ฆ โ โ) |
33 | 30, 32 | remulcld 11266 |
. . . . . . . . 9
โข (((๐ โง ๐ฆ โ โ) โง ((0
โโ ๐ด) ยท ๐ฆ) = (0 โโ (๐ด ยท ๐ฆ))) โ (๐ด ยท ๐ฆ) โ โ) |
34 | | rernegcl 41848 |
. . . . . . . . 9
โข ((๐ด ยท ๐ฆ) โ โ โ (0
โโ (๐ด ยท ๐ฆ)) โ โ) |
35 | 33, 34 | syl 17 |
. . . . . . . 8
โข (((๐ โง ๐ฆ โ โ) โง ((0
โโ ๐ด) ยท ๐ฆ) = (0 โโ (๐ด ยท ๐ฆ))) โ (0 โโ
(๐ด ยท ๐ฆ)) โ
โ) |
36 | | readdsub 41861 |
. . . . . . . 8
โข ((0
โ โ โง (0 โโ (๐ด ยท ๐ฆ)) โ โ โง ๐ด โ โ) โ ((0 + (0
โโ (๐ด ยท ๐ฆ))) โโ ๐ด) = ((0
โโ ๐ด) + (0 โโ (๐ด ยท ๐ฆ)))) |
37 | 29, 35, 30, 36 | syl3anc 1369 |
. . . . . . 7
โข (((๐ โง ๐ฆ โ โ) โง ((0
โโ ๐ด) ยท ๐ฆ) = (0 โโ (๐ด ยท ๐ฆ))) โ ((0 + (0 โโ
(๐ด ยท ๐ฆ))) โโ
๐ด) = ((0
โโ ๐ด) + (0 โโ (๐ด ยท ๐ฆ)))) |
38 | | readdlid 41880 |
. . . . . . . . 9
โข ((0
โโ (๐ด ยท ๐ฆ)) โ โ โ (0 + (0
โโ (๐ด ยท ๐ฆ))) = (0 โโ (๐ด ยท ๐ฆ))) |
39 | 35, 38 | syl 17 |
. . . . . . . 8
โข (((๐ โง ๐ฆ โ โ) โง ((0
โโ ๐ด) ยท ๐ฆ) = (0 โโ (๐ด ยท ๐ฆ))) โ (0 + (0 โโ
(๐ด ยท ๐ฆ))) = (0
โโ (๐ด ยท ๐ฆ))) |
40 | 39 | oveq1d 7429 |
. . . . . . 7
โข (((๐ โง ๐ฆ โ โ) โง ((0
โโ ๐ด) ยท ๐ฆ) = (0 โโ (๐ด ยท ๐ฆ))) โ ((0 + (0 โโ
(๐ด ยท ๐ฆ))) โโ
๐ด) = ((0
โโ (๐ด ยท ๐ฆ)) โโ ๐ด)) |
41 | 37, 40 | eqtr3d 2769 |
. . . . . 6
โข (((๐ โง ๐ฆ โ โ) โง ((0
โโ ๐ด) ยท ๐ฆ) = (0 โโ (๐ด ยท ๐ฆ))) โ ((0 โโ
๐ด) + (0
โโ (๐ด ยท ๐ฆ))) = ((0 โโ (๐ด ยท ๐ฆ)) โโ ๐ด)) |
42 | | resubsub4 41866 |
. . . . . . 7
โข ((0
โ โ โง (๐ด
ยท ๐ฆ) โ โ
โง ๐ด โ โ)
โ ((0 โโ (๐ด ยท ๐ฆ)) โโ ๐ด) = (0 โโ
((๐ด ยท ๐ฆ) + ๐ด))) |
43 | 29, 33, 30, 42 | syl3anc 1369 |
. . . . . 6
โข (((๐ โง ๐ฆ โ โ) โง ((0
โโ ๐ด) ยท ๐ฆ) = (0 โโ (๐ด ยท ๐ฆ))) โ ((0 โโ
(๐ด ยท ๐ฆ)) โโ
๐ด) = (0
โโ ((๐ด ยท ๐ฆ) + ๐ด))) |
44 | 28, 41, 43 | 3eqtrd 2771 |
. . . . 5
โข (((๐ โง ๐ฆ โ โ) โง ((0
โโ ๐ด) ยท ๐ฆ) = (0 โโ (๐ด ยท ๐ฆ))) โ ((0 โโ
๐ด) + ((0
โโ ๐ด) ยท ๐ฆ)) = (0 โโ ((๐ด ยท ๐ฆ) + ๐ด))) |
45 | 22 | oveq1d 7429 |
. . . . . 6
โข (๐ โ (((0
โโ ๐ด) ยท 1) + ((0
โโ ๐ด) ยท ๐ฆ)) = ((0 โโ ๐ด) + ((0
โโ ๐ด) ยท ๐ฆ))) |
46 | 45 | ad2antrr 725 |
. . . . 5
โข (((๐ โง ๐ฆ โ โ) โง ((0
โโ ๐ด) ยท ๐ฆ) = (0 โโ (๐ด ยท ๐ฆ))) โ (((0 โโ
๐ด) ยท 1) + ((0
โโ ๐ด) ยท ๐ฆ)) = ((0 โโ ๐ด) + ((0
โโ ๐ด) ยท ๐ฆ))) |
47 | 24 | oveq2d 7430 |
. . . . . . 7
โข (๐ โ ((๐ด ยท ๐ฆ) + (๐ด ยท 1)) = ((๐ด ยท ๐ฆ) + ๐ด)) |
48 | 47 | oveq2d 7430 |
. . . . . 6
โข (๐ โ (0
โโ ((๐ด ยท ๐ฆ) + (๐ด ยท 1))) = (0
โโ ((๐ด ยท ๐ฆ) + ๐ด))) |
49 | 48 | ad2antrr 725 |
. . . . 5
โข (((๐ โง ๐ฆ โ โ) โง ((0
โโ ๐ด) ยท ๐ฆ) = (0 โโ (๐ด ยท ๐ฆ))) โ (0 โโ
((๐ด ยท ๐ฆ) + (๐ด ยท 1))) = (0
โโ ((๐ด ยท ๐ฆ) + ๐ด))) |
50 | 44, 46, 49 | 3eqtr4d 2777 |
. . . 4
โข (((๐ โง ๐ฆ โ โ) โง ((0
โโ ๐ด) ยท ๐ฆ) = (0 โโ (๐ด ยท ๐ฆ))) โ (((0 โโ
๐ด) ยท 1) + ((0
โโ ๐ด) ยท ๐ฆ)) = (0 โโ ((๐ด ยท ๐ฆ) + (๐ด ยท 1)))) |
51 | | nnadd1com 41764 |
. . . . . . 7
โข (๐ฆ โ โ โ (๐ฆ + 1) = (1 + ๐ฆ)) |
52 | 51 | oveq2d 7430 |
. . . . . 6
โข (๐ฆ โ โ โ ((0
โโ ๐ด) ยท (๐ฆ + 1)) = ((0 โโ ๐ด) ยท (1 + ๐ฆ))) |
53 | 52 | ad2antlr 726 |
. . . . 5
โข (((๐ โง ๐ฆ โ โ) โง ((0
โโ ๐ด) ยท ๐ฆ) = (0 โโ (๐ด ยท ๐ฆ))) โ ((0 โโ
๐ด) ยท (๐ฆ + 1)) = ((0
โโ ๐ด) ยท (1 + ๐ฆ))) |
54 | 20 | recnd 11264 |
. . . . . . 7
โข (๐ โ (0
โโ ๐ด) โ โ) |
55 | 54 | ad2antrr 725 |
. . . . . 6
โข (((๐ โง ๐ฆ โ โ) โง ((0
โโ ๐ด) ยท ๐ฆ) = (0 โโ (๐ด ยท ๐ฆ))) โ (0 โโ ๐ด) โ
โ) |
56 | | 1cnd 11231 |
. . . . . 6
โข (((๐ โง ๐ฆ โ โ) โง ((0
โโ ๐ด) ยท ๐ฆ) = (0 โโ (๐ด ยท ๐ฆ))) โ 1 โ โ) |
57 | | nncn 12242 |
. . . . . . 7
โข (๐ฆ โ โ โ ๐ฆ โ
โ) |
58 | 57 | ad2antlr 726 |
. . . . . 6
โข (((๐ โง ๐ฆ โ โ) โง ((0
โโ ๐ด) ยท ๐ฆ) = (0 โโ (๐ด ยท ๐ฆ))) โ ๐ฆ โ โ) |
59 | 55, 56, 58 | adddid 11260 |
. . . . 5
โข (((๐ โง ๐ฆ โ โ) โง ((0
โโ ๐ด) ยท ๐ฆ) = (0 โโ (๐ด ยท ๐ฆ))) โ ((0 โโ
๐ด) ยท (1 + ๐ฆ)) = (((0
โโ ๐ด) ยท 1) + ((0
โโ ๐ด) ยท ๐ฆ))) |
60 | 53, 59 | eqtrd 2767 |
. . . 4
โข (((๐ โง ๐ฆ โ โ) โง ((0
โโ ๐ด) ยท ๐ฆ) = (0 โโ (๐ด ยท ๐ฆ))) โ ((0 โโ
๐ด) ยท (๐ฆ + 1)) = (((0
โโ ๐ด) ยท 1) + ((0
โโ ๐ด) ยท ๐ฆ))) |
61 | 18 | recnd 11264 |
. . . . . . 7
โข (๐ โ ๐ด โ โ) |
62 | 61 | ad2antrr 725 |
. . . . . 6
โข (((๐ โง ๐ฆ โ โ) โง ((0
โโ ๐ด) ยท ๐ฆ) = (0 โโ (๐ด ยท ๐ฆ))) โ ๐ด โ โ) |
63 | 62, 58, 56 | adddid 11260 |
. . . . 5
โข (((๐ โง ๐ฆ โ โ) โง ((0
โโ ๐ด) ยท ๐ฆ) = (0 โโ (๐ด ยท ๐ฆ))) โ (๐ด ยท (๐ฆ + 1)) = ((๐ด ยท ๐ฆ) + (๐ด ยท 1))) |
64 | 63 | oveq2d 7430 |
. . . 4
โข (((๐ โง ๐ฆ โ โ) โง ((0
โโ ๐ด) ยท ๐ฆ) = (0 โโ (๐ด ยท ๐ฆ))) โ (0 โโ
(๐ด ยท (๐ฆ + 1))) = (0
โโ ((๐ด ยท ๐ฆ) + (๐ด ยท 1)))) |
65 | 50, 60, 64 | 3eqtr4d 2777 |
. . 3
โข (((๐ โง ๐ฆ โ โ) โง ((0
โโ ๐ด) ยท ๐ฆ) = (0 โโ (๐ด ยท ๐ฆ))) โ ((0 โโ
๐ด) ยท (๐ฆ + 1)) = (0
โโ (๐ด ยท (๐ฆ + 1)))) |
66 | 5, 9, 13, 17, 26, 65 | nnindd 12254 |
. 2
โข ((๐ โง ๐ โ โ) โ ((0
โโ ๐ด) ยท ๐) = (0 โโ (๐ด ยท ๐))) |
67 | 1, 66 | mpdan 686 |
1
โข (๐ โ ((0
โโ ๐ด) ยท ๐) = (0 โโ (๐ด ยท ๐))) |