Step | Hyp | Ref
| Expression |
1 | | rereb 15012 |
. . 3
โข (๐ด โ โ โ (๐ด โ โ โ
(โโ๐ด) = ๐ด)) |
2 | 1 | 3ad2ant1 1134 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ (๐ด โ โ โ
(โโ๐ด) = ๐ด)) |
3 | | recl 15002 |
. . . . 5
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
4 | 3 | recnd 11190 |
. . . 4
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
5 | 4 | 3ad2ant1 1134 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ
(โโ๐ด) โ
โ) |
6 | | simp1 1137 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ ๐ด โ
โ) |
7 | | recn 11148 |
. . . . 5
โข (๐ต โ โ โ ๐ต โ
โ) |
8 | 7 | anim1i 616 |
. . . 4
โข ((๐ต โ โ โง ๐ต โ 0) โ (๐ต โ โ โง ๐ต โ 0)) |
9 | 8 | 3adant1 1131 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ (๐ต โ โ โง ๐ต โ 0)) |
10 | | mulcan 11799 |
. . 3
โข
(((โโ๐ด)
โ โ โง ๐ด
โ โ โง (๐ต
โ โ โง ๐ต โ
0)) โ ((๐ต ยท
(โโ๐ด)) = (๐ต ยท ๐ด) โ (โโ๐ด) = ๐ด)) |
11 | 5, 6, 9, 10 | syl3anc 1372 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ ((๐ต ยท (โโ๐ด)) = (๐ต ยท ๐ด) โ (โโ๐ด) = ๐ด)) |
12 | 7 | adantr 482 |
. . . . . . . . . 10
โข ((๐ต โ โ โง ๐ด โ โ) โ ๐ต โ
โ) |
13 | 4 | adantl 483 |
. . . . . . . . . 10
โข ((๐ต โ โ โง ๐ด โ โ) โ
(โโ๐ด) โ
โ) |
14 | | ax-icn 11117 |
. . . . . . . . . . . 12
โข i โ
โ |
15 | | imcl 15003 |
. . . . . . . . . . . . 13
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
16 | 15 | recnd 11190 |
. . . . . . . . . . . 12
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
17 | | mulcl 11142 |
. . . . . . . . . . . 12
โข ((i
โ โ โง (โโ๐ด) โ โ) โ (i ยท
(โโ๐ด)) โ
โ) |
18 | 14, 16, 17 | sylancr 588 |
. . . . . . . . . . 11
โข (๐ด โ โ โ (i
ยท (โโ๐ด))
โ โ) |
19 | 18 | adantl 483 |
. . . . . . . . . 10
โข ((๐ต โ โ โง ๐ด โ โ) โ (i
ยท (โโ๐ด))
โ โ) |
20 | 12, 13, 19 | adddid 11186 |
. . . . . . . . 9
โข ((๐ต โ โ โง ๐ด โ โ) โ (๐ต ยท ((โโ๐ด) + (i ยท
(โโ๐ด)))) =
((๐ต ยท
(โโ๐ด)) + (๐ต ยท (i ยท
(โโ๐ด))))) |
21 | | replim 15008 |
. . . . . . . . . . 11
โข (๐ด โ โ โ ๐ด = ((โโ๐ด) + (i ยท
(โโ๐ด)))) |
22 | 21 | adantl 483 |
. . . . . . . . . 10
โข ((๐ต โ โ โง ๐ด โ โ) โ ๐ด = ((โโ๐ด) + (i ยท
(โโ๐ด)))) |
23 | 22 | oveq2d 7378 |
. . . . . . . . 9
โข ((๐ต โ โ โง ๐ด โ โ) โ (๐ต ยท ๐ด) = (๐ต ยท ((โโ๐ด) + (i ยท (โโ๐ด))))) |
24 | | mul12 11327 |
. . . . . . . . . . 11
โข ((i
โ โ โง ๐ต
โ โ โง (โโ๐ด) โ โ) โ (i ยท (๐ต ยท (โโ๐ด))) = (๐ต ยท (i ยท (โโ๐ด)))) |
25 | 14, 7, 16, 24 | mp3an3an 1468 |
. . . . . . . . . 10
โข ((๐ต โ โ โง ๐ด โ โ) โ (i
ยท (๐ต ยท
(โโ๐ด))) =
(๐ต ยท (i ยท
(โโ๐ด)))) |
26 | 25 | oveq2d 7378 |
. . . . . . . . 9
โข ((๐ต โ โ โง ๐ด โ โ) โ ((๐ต ยท (โโ๐ด)) + (i ยท (๐ต ยท (โโ๐ด)))) = ((๐ต ยท (โโ๐ด)) + (๐ต ยท (i ยท (โโ๐ด))))) |
27 | 20, 23, 26 | 3eqtr4d 2787 |
. . . . . . . 8
โข ((๐ต โ โ โง ๐ด โ โ) โ (๐ต ยท ๐ด) = ((๐ต ยท (โโ๐ด)) + (i ยท (๐ต ยท (โโ๐ด))))) |
28 | 27 | fveq2d 6851 |
. . . . . . 7
โข ((๐ต โ โ โง ๐ด โ โ) โ
(โโ(๐ต ยท
๐ด)) = (โโ((๐ต ยท (โโ๐ด)) + (i ยท (๐ต ยท (โโ๐ด)))))) |
29 | | remulcl 11143 |
. . . . . . . . 9
โข ((๐ต โ โ โง
(โโ๐ด) โ
โ) โ (๐ต ยท
(โโ๐ด)) โ
โ) |
30 | 3, 29 | sylan2 594 |
. . . . . . . 8
โข ((๐ต โ โ โง ๐ด โ โ) โ (๐ต ยท (โโ๐ด)) โ
โ) |
31 | | remulcl 11143 |
. . . . . . . . 9
โข ((๐ต โ โ โง
(โโ๐ด) โ
โ) โ (๐ต ยท
(โโ๐ด)) โ
โ) |
32 | 15, 31 | sylan2 594 |
. . . . . . . 8
โข ((๐ต โ โ โง ๐ด โ โ) โ (๐ต ยท (โโ๐ด)) โ
โ) |
33 | | crre 15006 |
. . . . . . . 8
โข (((๐ต ยท (โโ๐ด)) โ โ โง (๐ต ยท (โโ๐ด)) โ โ) โ
(โโ((๐ต ยท
(โโ๐ด)) + (i
ยท (๐ต ยท
(โโ๐ด))))) =
(๐ต ยท
(โโ๐ด))) |
34 | 30, 32, 33 | syl2anc 585 |
. . . . . . 7
โข ((๐ต โ โ โง ๐ด โ โ) โ
(โโ((๐ต ยท
(โโ๐ด)) + (i
ยท (๐ต ยท
(โโ๐ด))))) =
(๐ต ยท
(โโ๐ด))) |
35 | 28, 34 | eqtr2d 2778 |
. . . . . 6
โข ((๐ต โ โ โง ๐ด โ โ) โ (๐ต ยท (โโ๐ด)) = (โโ(๐ต ยท ๐ด))) |
36 | 35 | eqeq1d 2739 |
. . . . 5
โข ((๐ต โ โ โง ๐ด โ โ) โ ((๐ต ยท (โโ๐ด)) = (๐ต ยท ๐ด) โ (โโ(๐ต ยท ๐ด)) = (๐ต ยท ๐ด))) |
37 | | mulcl 11142 |
. . . . . . 7
โข ((๐ต โ โ โง ๐ด โ โ) โ (๐ต ยท ๐ด) โ โ) |
38 | 7, 37 | sylan 581 |
. . . . . 6
โข ((๐ต โ โ โง ๐ด โ โ) โ (๐ต ยท ๐ด) โ โ) |
39 | | rereb 15012 |
. . . . . 6
โข ((๐ต ยท ๐ด) โ โ โ ((๐ต ยท ๐ด) โ โ โ (โโ(๐ต ยท ๐ด)) = (๐ต ยท ๐ด))) |
40 | 38, 39 | syl 17 |
. . . . 5
โข ((๐ต โ โ โง ๐ด โ โ) โ ((๐ต ยท ๐ด) โ โ โ (โโ(๐ต ยท ๐ด)) = (๐ต ยท ๐ด))) |
41 | 36, 40 | bitr4d 282 |
. . . 4
โข ((๐ต โ โ โง ๐ด โ โ) โ ((๐ต ยท (โโ๐ด)) = (๐ต ยท ๐ด) โ (๐ต ยท ๐ด) โ โ)) |
42 | 41 | ancoms 460 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ต ยท (โโ๐ด)) = (๐ต ยท ๐ด) โ (๐ต ยท ๐ด) โ โ)) |
43 | 42 | 3adant3 1133 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ ((๐ต ยท (โโ๐ด)) = (๐ต ยท ๐ด) โ (๐ต ยท ๐ด) โ โ)) |
44 | 2, 11, 43 | 3bitr2d 307 |
1
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ (๐ด โ โ โ (๐ต ยท ๐ด) โ โ)) |