Step | Hyp | Ref
| Expression |
1 | | reelznn0nn 41318 |
. 2
โข (๐ด โ โค โ (๐ด โ โ0 โจ
(๐ด โ โ โง (0
โโ ๐ด) โ โ))) |
2 | | reelznn0nn 41318 |
. 2
โข (๐ต โ โค โ (๐ต โ โ0 โจ
(๐ต โ โ โง (0
โโ ๐ต) โ โ))) |
3 | | nn0mulcom 41323 |
. . 3
โข ((๐ด โ โ0
โง ๐ต โ
โ0) โ (๐ด ยท ๐ต) = (๐ต ยท ๐ด)) |
4 | | zmulcomlem 41324 |
. . 3
โข (((๐ด โ โ โง (0
โโ ๐ด) โ โ) โง ๐ต โ โ0) โ (๐ด ยท ๐ต) = (๐ต ยท ๐ด)) |
5 | | zmulcomlem 41324 |
. . . . 5
โข (((๐ต โ โ โง (0
โโ ๐ต) โ โ) โง ๐ด โ โ0) โ (๐ต ยท ๐ด) = (๐ด ยท ๐ต)) |
6 | 5 | eqcomd 2738 |
. . . 4
โข (((๐ต โ โ โง (0
โโ ๐ต) โ โ) โง ๐ด โ โ0) โ (๐ด ยท ๐ต) = (๐ต ยท ๐ด)) |
7 | 6 | ancoms 459 |
. . 3
โข ((๐ด โ โ0
โง (๐ต โ โ
โง (0 โโ ๐ต) โ โ)) โ (๐ด ยท ๐ต) = (๐ต ยท ๐ด)) |
8 | | nnmulcom 41183 |
. . . . . . . . 9
โข (((0
โโ ๐ด) โ โ โง (0
โโ ๐ต) โ โ) โ ((0
โโ ๐ด) ยท (0 โโ
๐ต)) = ((0
โโ ๐ต) ยท (0 โโ
๐ด))) |
9 | 8 | ad2ant2l 744 |
. . . . . . . 8
โข (((๐ด โ โ โง (0
โโ ๐ด) โ โ) โง (๐ต โ โ โง (0
โโ ๐ต) โ โ)) โ ((0
โโ ๐ด) ยท (0 โโ
๐ต)) = ((0
โโ ๐ต) ยท (0 โโ
๐ด))) |
10 | 9 | oveq2d 7421 |
. . . . . . 7
โข (((๐ด โ โ โง (0
โโ ๐ด) โ โ) โง (๐ต โ โ โง (0
โโ ๐ต) โ โ)) โ (0
โโ ((0 โโ ๐ด) ยท (0 โโ
๐ต))) = (0
โโ ((0 โโ ๐ต) ยท (0 โโ
๐ด)))) |
11 | | rernegcl 41240 |
. . . . . . . . 9
โข (๐ด โ โ โ (0
โโ ๐ด) โ โ) |
12 | 11 | ad2antrr 724 |
. . . . . . . 8
โข (((๐ด โ โ โง (0
โโ ๐ด) โ โ) โง (๐ต โ โ โง (0
โโ ๐ต) โ โ)) โ (0
โโ ๐ด) โ โ) |
13 | | simprr 771 |
. . . . . . . 8
โข (((๐ด โ โ โง (0
โโ ๐ด) โ โ) โง (๐ต โ โ โง (0
โโ ๐ต) โ โ)) โ (0
โโ ๐ต) โ โ) |
14 | 12, 13 | renegmulnnass 41322 |
. . . . . . 7
โข (((๐ด โ โ โง (0
โโ ๐ด) โ โ) โง (๐ต โ โ โง (0
โโ ๐ต) โ โ)) โ ((0
โโ (0 โโ ๐ด)) ยท (0 โโ
๐ต)) = (0
โโ ((0 โโ ๐ด) ยท (0 โโ
๐ต)))) |
15 | | rernegcl 41240 |
. . . . . . . . 9
โข (๐ต โ โ โ (0
โโ ๐ต) โ โ) |
16 | 15 | ad2antrl 726 |
. . . . . . . 8
โข (((๐ด โ โ โง (0
โโ ๐ด) โ โ) โง (๐ต โ โ โง (0
โโ ๐ต) โ โ)) โ (0
โโ ๐ต) โ โ) |
17 | | simplr 767 |
. . . . . . . 8
โข (((๐ด โ โ โง (0
โโ ๐ด) โ โ) โง (๐ต โ โ โง (0
โโ ๐ต) โ โ)) โ (0
โโ ๐ด) โ โ) |
18 | 16, 17 | renegmulnnass 41322 |
. . . . . . 7
โข (((๐ด โ โ โง (0
โโ ๐ด) โ โ) โง (๐ต โ โ โง (0
โโ ๐ต) โ โ)) โ ((0
โโ (0 โโ ๐ต)) ยท (0 โโ
๐ด)) = (0
โโ ((0 โโ ๐ต) ยท (0 โโ
๐ด)))) |
19 | 10, 14, 18 | 3eqtr4d 2782 |
. . . . . 6
โข (((๐ด โ โ โง (0
โโ ๐ด) โ โ) โง (๐ต โ โ โง (0
โโ ๐ต) โ โ)) โ ((0
โโ (0 โโ ๐ด)) ยท (0 โโ
๐ต)) = ((0
โโ (0 โโ ๐ต)) ยท (0 โโ
๐ด))) |
20 | 19 | oveq2d 7421 |
. . . . 5
โข (((๐ด โ โ โง (0
โโ ๐ด) โ โ) โง (๐ต โ โ โง (0
โโ ๐ต) โ โ)) โ (0
โโ ((0 โโ (0
โโ ๐ด)) ยท (0 โโ
๐ต))) = (0
โโ ((0 โโ (0
โโ ๐ต)) ยท (0 โโ
๐ด)))) |
21 | | rernegcl 41240 |
. . . . . . . 8
โข ((0
โโ ๐ด) โ โ โ (0
โโ (0 โโ ๐ด)) โ โ) |
22 | 11, 21 | syl 17 |
. . . . . . 7
โข (๐ด โ โ โ (0
โโ (0 โโ ๐ด)) โ โ) |
23 | 22 | ad2antrr 724 |
. . . . . 6
โข (((๐ด โ โ โง (0
โโ ๐ด) โ โ) โง (๐ต โ โ โง (0
โโ ๐ต) โ โ)) โ (0
โโ (0 โโ ๐ด)) โ โ) |
24 | 23, 16 | remulneg2d 41283 |
. . . . 5
โข (((๐ด โ โ โง (0
โโ ๐ด) โ โ) โง (๐ต โ โ โง (0
โโ ๐ต) โ โ)) โ ((0
โโ (0 โโ ๐ด)) ยท (0 โโ (0
โโ ๐ต))) = (0 โโ ((0
โโ (0 โโ ๐ด)) ยท (0 โโ
๐ต)))) |
25 | | rernegcl 41240 |
. . . . . . . 8
โข ((0
โโ ๐ต) โ โ โ (0
โโ (0 โโ ๐ต)) โ โ) |
26 | 15, 25 | syl 17 |
. . . . . . 7
โข (๐ต โ โ โ (0
โโ (0 โโ ๐ต)) โ โ) |
27 | 26 | ad2antrl 726 |
. . . . . 6
โข (((๐ด โ โ โง (0
โโ ๐ด) โ โ) โง (๐ต โ โ โง (0
โโ ๐ต) โ โ)) โ (0
โโ (0 โโ ๐ต)) โ โ) |
28 | 27, 12 | remulneg2d 41283 |
. . . . 5
โข (((๐ด โ โ โง (0
โโ ๐ด) โ โ) โง (๐ต โ โ โง (0
โโ ๐ต) โ โ)) โ ((0
โโ (0 โโ ๐ต)) ยท (0 โโ (0
โโ ๐ด))) = (0 โโ ((0
โโ (0 โโ ๐ต)) ยท (0 โโ
๐ด)))) |
29 | 20, 24, 28 | 3eqtr4d 2782 |
. . . 4
โข (((๐ด โ โ โง (0
โโ ๐ด) โ โ) โง (๐ต โ โ โง (0
โโ ๐ต) โ โ)) โ ((0
โโ (0 โโ ๐ด)) ยท (0 โโ (0
โโ ๐ต))) = ((0 โโ (0
โโ ๐ต)) ยท (0 โโ (0
โโ ๐ด)))) |
30 | | renegneg 41280 |
. . . . . 6
โข (๐ด โ โ โ (0
โโ (0 โโ ๐ด)) = ๐ด) |
31 | 30 | ad2antrr 724 |
. . . . 5
โข (((๐ด โ โ โง (0
โโ ๐ด) โ โ) โง (๐ต โ โ โง (0
โโ ๐ต) โ โ)) โ (0
โโ (0 โโ ๐ด)) = ๐ด) |
32 | | renegneg 41280 |
. . . . . 6
โข (๐ต โ โ โ (0
โโ (0 โโ ๐ต)) = ๐ต) |
33 | 32 | ad2antrl 726 |
. . . . 5
โข (((๐ด โ โ โง (0
โโ ๐ด) โ โ) โง (๐ต โ โ โง (0
โโ ๐ต) โ โ)) โ (0
โโ (0 โโ ๐ต)) = ๐ต) |
34 | 31, 33 | oveq12d 7423 |
. . . 4
โข (((๐ด โ โ โง (0
โโ ๐ด) โ โ) โง (๐ต โ โ โง (0
โโ ๐ต) โ โ)) โ ((0
โโ (0 โโ ๐ด)) ยท (0 โโ (0
โโ ๐ต))) = (๐ด ยท ๐ต)) |
35 | 33, 31 | oveq12d 7423 |
. . . 4
โข (((๐ด โ โ โง (0
โโ ๐ด) โ โ) โง (๐ต โ โ โง (0
โโ ๐ต) โ โ)) โ ((0
โโ (0 โโ ๐ต)) ยท (0 โโ (0
โโ ๐ด))) = (๐ต ยท ๐ด)) |
36 | 29, 34, 35 | 3eqtr3d 2780 |
. . 3
โข (((๐ด โ โ โง (0
โโ ๐ด) โ โ) โง (๐ต โ โ โง (0
โโ ๐ต) โ โ)) โ (๐ด ยท ๐ต) = (๐ต ยท ๐ด)) |
37 | 3, 4, 7, 36 | ccase 1036 |
. 2
โข (((๐ด โ โ0 โจ
(๐ด โ โ โง (0
โโ ๐ด) โ โ)) โง (๐ต โ โ0 โจ (๐ต โ โ โง (0
โโ ๐ต) โ โ))) โ (๐ด ยท ๐ต) = (๐ต ยท ๐ด)) |
38 | 1, 2, 37 | syl2anb 598 |
1
โข ((๐ด โ โค โง ๐ต โ โค) โ (๐ด ยท ๐ต) = (๐ต ยท ๐ด)) |