Step | Hyp | Ref
| Expression |
1 | | elnn0 12456 |
. 2
โข (๐ต โ โ0
โ (๐ต โ โ
โจ ๐ต =
0)) |
2 | | renegneg 41066 |
. . . . . 6
โข (๐ด โ โ โ (0
โโ (0 โโ ๐ด)) = ๐ด) |
3 | 2 | oveq1d 7408 |
. . . . 5
โข (๐ด โ โ โ ((0
โโ (0 โโ ๐ด)) ยท ๐ต) = (๐ด ยท ๐ต)) |
4 | 3 | ad2antrr 724 |
. . . 4
โข (((๐ด โ โ โง (0
โโ ๐ด) โ โ) โง ๐ต โ โ) โ ((0
โโ (0 โโ ๐ด)) ยท ๐ต) = (๐ด ยท ๐ต)) |
5 | | rernegcl 41026 |
. . . . . . 7
โข (๐ด โ โ โ (0
โโ ๐ด) โ โ) |
6 | 5 | ad2antrr 724 |
. . . . . 6
โข (((๐ด โ โ โง (0
โโ ๐ด) โ โ) โง ๐ต โ โ) โ (0
โโ ๐ด) โ โ) |
7 | | simpr 485 |
. . . . . 6
โข (((๐ด โ โ โง (0
โโ ๐ด) โ โ) โง ๐ต โ โ) โ ๐ต โ โ) |
8 | 6, 7 | renegmulnnass 41108 |
. . . . 5
โข (((๐ด โ โ โง (0
โโ ๐ด) โ โ) โง ๐ต โ โ) โ ((0
โโ (0 โโ ๐ด)) ยท ๐ต) = (0 โโ ((0
โโ ๐ด) ยท ๐ต))) |
9 | | nnmulcom 40974 |
. . . . . . . 8
โข (((0
โโ ๐ด) โ โ โง ๐ต โ โ) โ ((0
โโ ๐ด) ยท ๐ต) = (๐ต ยท (0 โโ ๐ด))) |
10 | 9 | adantll 712 |
. . . . . . 7
โข (((๐ด โ โ โง (0
โโ ๐ด) โ โ) โง ๐ต โ โ) โ ((0
โโ ๐ด) ยท ๐ต) = (๐ต ยท (0 โโ ๐ด))) |
11 | 10 | oveq2d 7409 |
. . . . . 6
โข (((๐ด โ โ โง (0
โโ ๐ด) โ โ) โง ๐ต โ โ) โ (0
โโ ((0 โโ ๐ด) ยท ๐ต)) = (0 โโ (๐ต ยท (0
โโ ๐ด)))) |
12 | | nnre 12201 |
. . . . . . . . 9
โข (๐ต โ โ โ ๐ต โ
โ) |
13 | 12 | adantl 482 |
. . . . . . . 8
โข (((๐ด โ โ โง (0
โโ ๐ด) โ โ) โง ๐ต โ โ) โ ๐ต โ โ) |
14 | | 0red 11199 |
. . . . . . . 8
โข (((๐ด โ โ โง (0
โโ ๐ด) โ โ) โง ๐ต โ โ) โ 0 โ
โ) |
15 | | resubdi 41051 |
. . . . . . . 8
โข ((๐ต โ โ โง 0 โ
โ โง (0 โโ ๐ด) โ โ) โ (๐ต ยท (0 โโ (0
โโ ๐ด))) = ((๐ต ยท 0) โโ
(๐ต ยท (0
โโ ๐ด)))) |
16 | 13, 14, 6, 15 | syl3anc 1371 |
. . . . . . 7
โข (((๐ด โ โ โง (0
โโ ๐ด) โ โ) โง ๐ต โ โ) โ (๐ต ยท (0 โโ (0
โโ ๐ด))) = ((๐ต ยท 0) โโ
(๐ต ยท (0
โโ ๐ด)))) |
17 | | remul01 41062 |
. . . . . . . . . 10
โข (๐ต โ โ โ (๐ต ยท 0) =
0) |
18 | 12, 17 | syl 17 |
. . . . . . . . 9
โข (๐ต โ โ โ (๐ต ยท 0) =
0) |
19 | 18 | adantl 482 |
. . . . . . . 8
โข (((๐ด โ โ โง (0
โโ ๐ด) โ โ) โง ๐ต โ โ) โ (๐ต ยท 0) = 0) |
20 | 19 | oveq1d 7408 |
. . . . . . 7
โข (((๐ด โ โ โง (0
โโ ๐ด) โ โ) โง ๐ต โ โ) โ ((๐ต ยท 0) โโ
(๐ต ยท (0
โโ ๐ด))) = (0 โโ (๐ต ยท (0
โโ ๐ด)))) |
21 | 16, 20 | eqtrd 2771 |
. . . . . 6
โข (((๐ด โ โ โง (0
โโ ๐ด) โ โ) โง ๐ต โ โ) โ (๐ต ยท (0 โโ (0
โโ ๐ด))) = (0 โโ (๐ต ยท (0
โโ ๐ด)))) |
22 | 2 | ad2antrr 724 |
. . . . . . 7
โข (((๐ด โ โ โง (0
โโ ๐ด) โ โ) โง ๐ต โ โ) โ (0
โโ (0 โโ ๐ด)) = ๐ด) |
23 | 22 | oveq2d 7409 |
. . . . . 6
โข (((๐ด โ โ โง (0
โโ ๐ด) โ โ) โง ๐ต โ โ) โ (๐ต ยท (0 โโ (0
โโ ๐ด))) = (๐ต ยท ๐ด)) |
24 | 11, 21, 23 | 3eqtr2d 2777 |
. . . . 5
โข (((๐ด โ โ โง (0
โโ ๐ด) โ โ) โง ๐ต โ โ) โ (0
โโ ((0 โโ ๐ด) ยท ๐ต)) = (๐ต ยท ๐ด)) |
25 | 8, 4, 24 | 3eqtr3d 2779 |
. . . 4
โข (((๐ด โ โ โง (0
โโ ๐ด) โ โ) โง ๐ต โ โ) โ (๐ด ยท ๐ต) = (๐ต ยท ๐ด)) |
26 | 4, 4, 25 | 3eqtr3d 2779 |
. . 3
โข (((๐ด โ โ โง (0
โโ ๐ด) โ โ) โง ๐ต โ โ) โ (๐ด ยท ๐ต) = (๐ต ยท ๐ด)) |
27 | | remul01 41062 |
. . . . . . 7
โข (๐ด โ โ โ (๐ด ยท 0) =
0) |
28 | | remul02 41060 |
. . . . . . 7
โข (๐ด โ โ โ (0
ยท ๐ด) =
0) |
29 | 27, 28 | eqtr4d 2774 |
. . . . . 6
โข (๐ด โ โ โ (๐ด ยท 0) = (0 ยท ๐ด)) |
30 | 29 | adantr 481 |
. . . . 5
โข ((๐ด โ โ โง (0
โโ ๐ด) โ โ) โ (๐ด ยท 0) = (0 ยท ๐ด)) |
31 | | oveq2 7401 |
. . . . . 6
โข (๐ต = 0 โ (๐ด ยท ๐ต) = (๐ด ยท 0)) |
32 | | oveq1 7400 |
. . . . . 6
โข (๐ต = 0 โ (๐ต ยท ๐ด) = (0 ยท ๐ด)) |
33 | 31, 32 | eqeq12d 2747 |
. . . . 5
โข (๐ต = 0 โ ((๐ด ยท ๐ต) = (๐ต ยท ๐ด) โ (๐ด ยท 0) = (0 ยท ๐ด))) |
34 | 30, 33 | syl5ibrcom 246 |
. . . 4
โข ((๐ด โ โ โง (0
โโ ๐ด) โ โ) โ (๐ต = 0 โ (๐ด ยท ๐ต) = (๐ต ยท ๐ด))) |
35 | 34 | imp 407 |
. . 3
โข (((๐ด โ โ โง (0
โโ ๐ด) โ โ) โง ๐ต = 0) โ (๐ด ยท ๐ต) = (๐ต ยท ๐ด)) |
36 | 26, 35 | jaodan 956 |
. 2
โข (((๐ด โ โ โง (0
โโ ๐ด) โ โ) โง (๐ต โ โ โจ ๐ต = 0)) โ (๐ด ยท ๐ต) = (๐ต ยท ๐ด)) |
37 | 1, 36 | sylan2b 594 |
1
โข (((๐ด โ โ โง (0
โโ ๐ด) โ โ) โง ๐ต โ โ0) โ (๐ด ยท ๐ต) = (๐ต ยท ๐ด)) |