Step | Hyp | Ref
| Expression |
1 | | rereb 15069 |
. . 3
โข (๐ด โ โ โ (๐ด โ โ โ
(โโ๐ด) = ๐ด)) |
2 | 1 | 3ad2ant1 1130 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ (๐ด โ โ โ
(โโ๐ด) = ๐ด)) |
3 | | recl 15059 |
. . . . 5
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
4 | 3 | recnd 11241 |
. . . 4
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
5 | 4 | 3ad2ant1 1130 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ
(โโ๐ด) โ
โ) |
6 | | simp1 1133 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ ๐ด โ
โ) |
7 | | recn 11197 |
. . . . 5
โข (๐ต โ โ โ ๐ต โ
โ) |
8 | 7 | anim1i 614 |
. . . 4
โข ((๐ต โ โ โง ๐ต โ 0) โ (๐ต โ โ โง ๐ต โ 0)) |
9 | 8 | 3adant1 1127 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ (๐ต โ โ โง ๐ต โ 0)) |
10 | | mulcan 11850 |
. . 3
โข
(((โโ๐ด)
โ โ โง ๐ด
โ โ โง (๐ต
โ โ โง ๐ต โ
0)) โ ((๐ต ยท
(โโ๐ด)) = (๐ต ยท ๐ด) โ (โโ๐ด) = ๐ด)) |
11 | 5, 6, 9, 10 | syl3anc 1368 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ ((๐ต ยท (โโ๐ด)) = (๐ต ยท ๐ด) โ (โโ๐ด) = ๐ด)) |
12 | 7 | adantr 480 |
. . . . . . . . . 10
โข ((๐ต โ โ โง ๐ด โ โ) โ ๐ต โ
โ) |
13 | 4 | adantl 481 |
. . . . . . . . . 10
โข ((๐ต โ โ โง ๐ด โ โ) โ
(โโ๐ด) โ
โ) |
14 | | ax-icn 11166 |
. . . . . . . . . . . 12
โข i โ
โ |
15 | | imcl 15060 |
. . . . . . . . . . . . 13
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
16 | 15 | recnd 11241 |
. . . . . . . . . . . 12
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
17 | | mulcl 11191 |
. . . . . . . . . . . 12
โข ((i
โ โ โง (โโ๐ด) โ โ) โ (i ยท
(โโ๐ด)) โ
โ) |
18 | 14, 16, 17 | sylancr 586 |
. . . . . . . . . . 11
โข (๐ด โ โ โ (i
ยท (โโ๐ด))
โ โ) |
19 | 18 | adantl 481 |
. . . . . . . . . 10
โข ((๐ต โ โ โง ๐ด โ โ) โ (i
ยท (โโ๐ด))
โ โ) |
20 | 12, 13, 19 | adddid 11237 |
. . . . . . . . 9
โข ((๐ต โ โ โง ๐ด โ โ) โ (๐ต ยท ((โโ๐ด) + (i ยท
(โโ๐ด)))) =
((๐ต ยท
(โโ๐ด)) + (๐ต ยท (i ยท
(โโ๐ด))))) |
21 | | replim 15065 |
. . . . . . . . . . 11
โข (๐ด โ โ โ ๐ด = ((โโ๐ด) + (i ยท
(โโ๐ด)))) |
22 | 21 | adantl 481 |
. . . . . . . . . 10
โข ((๐ต โ โ โง ๐ด โ โ) โ ๐ด = ((โโ๐ด) + (i ยท
(โโ๐ด)))) |
23 | 22 | oveq2d 7418 |
. . . . . . . . 9
โข ((๐ต โ โ โง ๐ด โ โ) โ (๐ต ยท ๐ด) = (๐ต ยท ((โโ๐ด) + (i ยท (โโ๐ด))))) |
24 | | mul12 11378 |
. . . . . . . . . . 11
โข ((i
โ โ โง ๐ต
โ โ โง (โโ๐ด) โ โ) โ (i ยท (๐ต ยท (โโ๐ด))) = (๐ต ยท (i ยท (โโ๐ด)))) |
25 | 14, 7, 16, 24 | mp3an3an 1463 |
. . . . . . . . . 10
โข ((๐ต โ โ โง ๐ด โ โ) โ (i
ยท (๐ต ยท
(โโ๐ด))) =
(๐ต ยท (i ยท
(โโ๐ด)))) |
26 | 25 | oveq2d 7418 |
. . . . . . . . 9
โข ((๐ต โ โ โง ๐ด โ โ) โ ((๐ต ยท (โโ๐ด)) + (i ยท (๐ต ยท (โโ๐ด)))) = ((๐ต ยท (โโ๐ด)) + (๐ต ยท (i ยท (โโ๐ด))))) |
27 | 20, 23, 26 | 3eqtr4d 2774 |
. . . . . . . 8
โข ((๐ต โ โ โง ๐ด โ โ) โ (๐ต ยท ๐ด) = ((๐ต ยท (โโ๐ด)) + (i ยท (๐ต ยท (โโ๐ด))))) |
28 | 27 | fveq2d 6886 |
. . . . . . 7
โข ((๐ต โ โ โง ๐ด โ โ) โ
(โโ(๐ต ยท
๐ด)) = (โโ((๐ต ยท (โโ๐ด)) + (i ยท (๐ต ยท (โโ๐ด)))))) |
29 | | remulcl 11192 |
. . . . . . . . 9
โข ((๐ต โ โ โง
(โโ๐ด) โ
โ) โ (๐ต ยท
(โโ๐ด)) โ
โ) |
30 | 3, 29 | sylan2 592 |
. . . . . . . 8
โข ((๐ต โ โ โง ๐ด โ โ) โ (๐ต ยท (โโ๐ด)) โ
โ) |
31 | | remulcl 11192 |
. . . . . . . . 9
โข ((๐ต โ โ โง
(โโ๐ด) โ
โ) โ (๐ต ยท
(โโ๐ด)) โ
โ) |
32 | 15, 31 | sylan2 592 |
. . . . . . . 8
โข ((๐ต โ โ โง ๐ด โ โ) โ (๐ต ยท (โโ๐ด)) โ
โ) |
33 | | crre 15063 |
. . . . . . . 8
โข (((๐ต ยท (โโ๐ด)) โ โ โง (๐ต ยท (โโ๐ด)) โ โ) โ
(โโ((๐ต ยท
(โโ๐ด)) + (i
ยท (๐ต ยท
(โโ๐ด))))) =
(๐ต ยท
(โโ๐ด))) |
34 | 30, 32, 33 | syl2anc 583 |
. . . . . . 7
โข ((๐ต โ โ โง ๐ด โ โ) โ
(โโ((๐ต ยท
(โโ๐ด)) + (i
ยท (๐ต ยท
(โโ๐ด))))) =
(๐ต ยท
(โโ๐ด))) |
35 | 28, 34 | eqtr2d 2765 |
. . . . . 6
โข ((๐ต โ โ โง ๐ด โ โ) โ (๐ต ยท (โโ๐ด)) = (โโ(๐ต ยท ๐ด))) |
36 | 35 | eqeq1d 2726 |
. . . . 5
โข ((๐ต โ โ โง ๐ด โ โ) โ ((๐ต ยท (โโ๐ด)) = (๐ต ยท ๐ด) โ (โโ(๐ต ยท ๐ด)) = (๐ต ยท ๐ด))) |
37 | | mulcl 11191 |
. . . . . . 7
โข ((๐ต โ โ โง ๐ด โ โ) โ (๐ต ยท ๐ด) โ โ) |
38 | 7, 37 | sylan 579 |
. . . . . 6
โข ((๐ต โ โ โง ๐ด โ โ) โ (๐ต ยท ๐ด) โ โ) |
39 | | rereb 15069 |
. . . . . 6
โข ((๐ต ยท ๐ด) โ โ โ ((๐ต ยท ๐ด) โ โ โ (โโ(๐ต ยท ๐ด)) = (๐ต ยท ๐ด))) |
40 | 38, 39 | syl 17 |
. . . . 5
โข ((๐ต โ โ โง ๐ด โ โ) โ ((๐ต ยท ๐ด) โ โ โ (โโ(๐ต ยท ๐ด)) = (๐ต ยท ๐ด))) |
41 | 36, 40 | bitr4d 282 |
. . . 4
โข ((๐ต โ โ โง ๐ด โ โ) โ ((๐ต ยท (โโ๐ด)) = (๐ต ยท ๐ด) โ (๐ต ยท ๐ด) โ โ)) |
42 | 41 | ancoms 458 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ต ยท (โโ๐ด)) = (๐ต ยท ๐ด) โ (๐ต ยท ๐ด) โ โ)) |
43 | 42 | 3adant3 1129 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ ((๐ต ยท (โโ๐ด)) = (๐ต ยท ๐ด) โ (๐ต ยท ๐ด) โ โ)) |
44 | 2, 11, 43 | 3bitr2d 307 |
1
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ (๐ด โ โ โ (๐ต ยท ๐ด) โ โ)) |