Step | Hyp | Ref
| Expression |
1 | | rereb 10871 |
. . 3
โข (๐ด โ โ โ (๐ด โ โ โ
(โโ๐ด) = ๐ด)) |
2 | 1 | 3ad2ant1 1018 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต # 0) โ (๐ด โ โ โ (โโ๐ด) = ๐ด)) |
3 | | recl 10861 |
. . . . 5
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
4 | 3 | recnd 7985 |
. . . 4
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
5 | 4 | 3ad2ant1 1018 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต # 0) โ (โโ๐ด) โ
โ) |
6 | | simp1 997 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต # 0) โ ๐ด โ โ) |
7 | | recn 7943 |
. . . . 5
โข (๐ต โ โ โ ๐ต โ
โ) |
8 | 7 | anim1i 340 |
. . . 4
โข ((๐ต โ โ โง ๐ต # 0) โ (๐ต โ โ โง ๐ต # 0)) |
9 | 8 | 3adant1 1015 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต # 0) โ (๐ต โ โ โง ๐ต # 0)) |
10 | | mulcanap 8621 |
. . 3
โข
(((โโ๐ด)
โ โ โง ๐ด
โ โ โง (๐ต
โ โ โง ๐ต #
0)) โ ((๐ต ยท
(โโ๐ด)) = (๐ต ยท ๐ด) โ (โโ๐ด) = ๐ด)) |
11 | 5, 6, 9, 10 | syl3anc 1238 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต # 0) โ ((๐ต ยท (โโ๐ด)) = (๐ต ยท ๐ด) โ (โโ๐ด) = ๐ด)) |
12 | 7 | adantr 276 |
. . . . . . . . . 10
โข ((๐ต โ โ โง ๐ด โ โ) โ ๐ต โ
โ) |
13 | 4 | adantl 277 |
. . . . . . . . . 10
โข ((๐ต โ โ โง ๐ด โ โ) โ
(โโ๐ด) โ
โ) |
14 | | ax-icn 7905 |
. . . . . . . . . . . 12
โข i โ
โ |
15 | | imcl 10862 |
. . . . . . . . . . . . 13
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
16 | 15 | recnd 7985 |
. . . . . . . . . . . 12
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
17 | | mulcl 7937 |
. . . . . . . . . . . 12
โข ((i
โ โ โง (โโ๐ด) โ โ) โ (i ยท
(โโ๐ด)) โ
โ) |
18 | 14, 16, 17 | sylancr 414 |
. . . . . . . . . . 11
โข (๐ด โ โ โ (i
ยท (โโ๐ด))
โ โ) |
19 | 18 | adantl 277 |
. . . . . . . . . 10
โข ((๐ต โ โ โง ๐ด โ โ) โ (i
ยท (โโ๐ด))
โ โ) |
20 | 12, 13, 19 | adddid 7981 |
. . . . . . . . 9
โข ((๐ต โ โ โง ๐ด โ โ) โ (๐ต ยท ((โโ๐ด) + (i ยท
(โโ๐ด)))) =
((๐ต ยท
(โโ๐ด)) + (๐ต ยท (i ยท
(โโ๐ด))))) |
21 | | replim 10867 |
. . . . . . . . . . 11
โข (๐ด โ โ โ ๐ด = ((โโ๐ด) + (i ยท
(โโ๐ด)))) |
22 | 21 | adantl 277 |
. . . . . . . . . 10
โข ((๐ต โ โ โง ๐ด โ โ) โ ๐ด = ((โโ๐ด) + (i ยท
(โโ๐ด)))) |
23 | 22 | oveq2d 5890 |
. . . . . . . . 9
โข ((๐ต โ โ โง ๐ด โ โ) โ (๐ต ยท ๐ด) = (๐ต ยท ((โโ๐ด) + (i ยท (โโ๐ด))))) |
24 | | mul12 8085 |
. . . . . . . . . . . 12
โข ((i
โ โ โง ๐ต
โ โ โง (โโ๐ด) โ โ) โ (i ยท (๐ต ยท (โโ๐ด))) = (๐ต ยท (i ยท (โโ๐ด)))) |
25 | 14, 24 | mp3an1 1324 |
. . . . . . . . . . 11
โข ((๐ต โ โ โง
(โโ๐ด) โ
โ) โ (i ยท (๐ต ยท (โโ๐ด))) = (๐ต ยท (i ยท (โโ๐ด)))) |
26 | 7, 16, 25 | syl2an 289 |
. . . . . . . . . 10
โข ((๐ต โ โ โง ๐ด โ โ) โ (i
ยท (๐ต ยท
(โโ๐ด))) =
(๐ต ยท (i ยท
(โโ๐ด)))) |
27 | 26 | oveq2d 5890 |
. . . . . . . . 9
โข ((๐ต โ โ โง ๐ด โ โ) โ ((๐ต ยท (โโ๐ด)) + (i ยท (๐ต ยท (โโ๐ด)))) = ((๐ต ยท (โโ๐ด)) + (๐ต ยท (i ยท (โโ๐ด))))) |
28 | 20, 23, 27 | 3eqtr4d 2220 |
. . . . . . . 8
โข ((๐ต โ โ โง ๐ด โ โ) โ (๐ต ยท ๐ด) = ((๐ต ยท (โโ๐ด)) + (i ยท (๐ต ยท (โโ๐ด))))) |
29 | 28 | fveq2d 5519 |
. . . . . . 7
โข ((๐ต โ โ โง ๐ด โ โ) โ
(โโ(๐ต ยท
๐ด)) = (โโ((๐ต ยท (โโ๐ด)) + (i ยท (๐ต ยท (โโ๐ด)))))) |
30 | | remulcl 7938 |
. . . . . . . . 9
โข ((๐ต โ โ โง
(โโ๐ด) โ
โ) โ (๐ต ยท
(โโ๐ด)) โ
โ) |
31 | 3, 30 | sylan2 286 |
. . . . . . . 8
โข ((๐ต โ โ โง ๐ด โ โ) โ (๐ต ยท (โโ๐ด)) โ
โ) |
32 | | remulcl 7938 |
. . . . . . . . 9
โข ((๐ต โ โ โง
(โโ๐ด) โ
โ) โ (๐ต ยท
(โโ๐ด)) โ
โ) |
33 | 15, 32 | sylan2 286 |
. . . . . . . 8
โข ((๐ต โ โ โง ๐ด โ โ) โ (๐ต ยท (โโ๐ด)) โ
โ) |
34 | | crre 10865 |
. . . . . . . 8
โข (((๐ต ยท (โโ๐ด)) โ โ โง (๐ต ยท (โโ๐ด)) โ โ) โ
(โโ((๐ต ยท
(โโ๐ด)) + (i
ยท (๐ต ยท
(โโ๐ด))))) =
(๐ต ยท
(โโ๐ด))) |
35 | 31, 33, 34 | syl2anc 411 |
. . . . . . 7
โข ((๐ต โ โ โง ๐ด โ โ) โ
(โโ((๐ต ยท
(โโ๐ด)) + (i
ยท (๐ต ยท
(โโ๐ด))))) =
(๐ต ยท
(โโ๐ด))) |
36 | 29, 35 | eqtr2d 2211 |
. . . . . 6
โข ((๐ต โ โ โง ๐ด โ โ) โ (๐ต ยท (โโ๐ด)) = (โโ(๐ต ยท ๐ด))) |
37 | 36 | eqeq1d 2186 |
. . . . 5
โข ((๐ต โ โ โง ๐ด โ โ) โ ((๐ต ยท (โโ๐ด)) = (๐ต ยท ๐ด) โ (โโ(๐ต ยท ๐ด)) = (๐ต ยท ๐ด))) |
38 | | mulcl 7937 |
. . . . . . 7
โข ((๐ต โ โ โง ๐ด โ โ) โ (๐ต ยท ๐ด) โ โ) |
39 | 7, 38 | sylan 283 |
. . . . . 6
โข ((๐ต โ โ โง ๐ด โ โ) โ (๐ต ยท ๐ด) โ โ) |
40 | | rereb 10871 |
. . . . . 6
โข ((๐ต ยท ๐ด) โ โ โ ((๐ต ยท ๐ด) โ โ โ (โโ(๐ต ยท ๐ด)) = (๐ต ยท ๐ด))) |
41 | 39, 40 | syl 14 |
. . . . 5
โข ((๐ต โ โ โง ๐ด โ โ) โ ((๐ต ยท ๐ด) โ โ โ (โโ(๐ต ยท ๐ด)) = (๐ต ยท ๐ด))) |
42 | 37, 41 | bitr4d 191 |
. . . 4
โข ((๐ต โ โ โง ๐ด โ โ) โ ((๐ต ยท (โโ๐ด)) = (๐ต ยท ๐ด) โ (๐ต ยท ๐ด) โ โ)) |
43 | 42 | ancoms 268 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ต ยท (โโ๐ด)) = (๐ต ยท ๐ด) โ (๐ต ยท ๐ด) โ โ)) |
44 | 43 | 3adant3 1017 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต # 0) โ ((๐ต ยท (โโ๐ด)) = (๐ต ยท ๐ด) โ (๐ต ยท ๐ด) โ โ)) |
45 | 2, 11, 44 | 3bitr2d 216 |
1
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต # 0) โ (๐ด โ โ โ (๐ต ยท ๐ด) โ โ)) |