Step | Hyp | Ref
| Expression |
1 | | recl 15002 |
. . . . . . 7
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
2 | 1 | adantr 482 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ๐ด) โ
โ) |
3 | 2 | recnd 11190 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ๐ด) โ
โ) |
4 | | ax-icn 11117 |
. . . . . 6
โข i โ
โ |
5 | | imcl 15003 |
. . . . . . . 8
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
6 | 5 | adantr 482 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ๐ด) โ
โ) |
7 | 6 | recnd 11190 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ๐ด) โ
โ) |
8 | | mulcl 11142 |
. . . . . 6
โข ((i
โ โ โง (โโ๐ด) โ โ) โ (i ยท
(โโ๐ด)) โ
โ) |
9 | 4, 7, 8 | sylancr 588 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ (i
ยท (โโ๐ด))
โ โ) |
10 | | recl 15002 |
. . . . . . 7
โข (๐ต โ โ โ
(โโ๐ต) โ
โ) |
11 | 10 | adantl 483 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ๐ต) โ
โ) |
12 | 11 | recnd 11190 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ๐ต) โ
โ) |
13 | | imcl 15003 |
. . . . . . . 8
โข (๐ต โ โ โ
(โโ๐ต) โ
โ) |
14 | 13 | adantl 483 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ๐ต) โ
โ) |
15 | 14 | recnd 11190 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ๐ต) โ
โ) |
16 | | mulcl 11142 |
. . . . . 6
โข ((i
โ โ โง (โโ๐ต) โ โ) โ (i ยท
(โโ๐ต)) โ
โ) |
17 | 4, 15, 16 | sylancr 588 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ (i
ยท (โโ๐ต))
โ โ) |
18 | 3, 9, 12, 17 | add4d 11390 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ
(((โโ๐ด) + (i
ยท (โโ๐ด))) + ((โโ๐ต) + (i ยท (โโ๐ต)))) = (((โโ๐ด) + (โโ๐ต)) + ((i ยท
(โโ๐ด)) + (i
ยท (โโ๐ต))))) |
19 | | replim 15008 |
. . . . 5
โข (๐ด โ โ โ ๐ด = ((โโ๐ด) + (i ยท
(โโ๐ด)))) |
20 | | replim 15008 |
. . . . 5
โข (๐ต โ โ โ ๐ต = ((โโ๐ต) + (i ยท
(โโ๐ต)))) |
21 | 19, 20 | oveqan12d 7381 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด + ๐ต) = (((โโ๐ด) + (i ยท (โโ๐ด))) + ((โโ๐ต) + (i ยท
(โโ๐ต))))) |
22 | 4 | a1i 11 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ i โ
โ) |
23 | 22, 7, 15 | adddid 11186 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ (i
ยท ((โโ๐ด)
+ (โโ๐ต))) = ((i
ยท (โโ๐ด))
+ (i ยท (โโ๐ต)))) |
24 | 23 | oveq2d 7378 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ
(((โโ๐ด) +
(โโ๐ต)) + (i
ยท ((โโ๐ด)
+ (โโ๐ต)))) =
(((โโ๐ด) +
(โโ๐ต)) + ((i
ยท (โโ๐ด))
+ (i ยท (โโ๐ต))))) |
25 | 18, 21, 24 | 3eqtr4d 2787 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด + ๐ต) = (((โโ๐ด) + (โโ๐ต)) + (i ยท ((โโ๐ด) + (โโ๐ต))))) |
26 | 25 | fveq2d 6851 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ(๐ด + ๐ต)) =
(โโ(((โโ๐ด) + (โโ๐ต)) + (i ยท ((โโ๐ด) + (โโ๐ต)))))) |
27 | | readdcl 11141 |
. . . 4
โข
(((โโ๐ด)
โ โ โง (โโ๐ต) โ โ) โ
((โโ๐ด) +
(โโ๐ต)) โ
โ) |
28 | 1, 10, 27 | syl2an 597 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ๐ด) +
(โโ๐ต)) โ
โ) |
29 | | readdcl 11141 |
. . . 4
โข
(((โโ๐ด)
โ โ โง (โโ๐ต) โ โ) โ
((โโ๐ด) +
(โโ๐ต)) โ
โ) |
30 | 5, 13, 29 | syl2an 597 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ๐ด) +
(โโ๐ต)) โ
โ) |
31 | | crim 15007 |
. . 3
โข
((((โโ๐ด)
+ (โโ๐ต)) โ
โ โง ((โโ๐ด) + (โโ๐ต)) โ โ) โ
(โโ(((โโ๐ด) + (โโ๐ต)) + (i ยท ((โโ๐ด) + (โโ๐ต))))) = ((โโ๐ด) + (โโ๐ต))) |
32 | 28, 30, 31 | syl2anc 585 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ(((โโ๐ด) + (โโ๐ต)) + (i ยท ((โโ๐ด) + (โโ๐ต))))) = ((โโ๐ด) + (โโ๐ต))) |
33 | 26, 32 | eqtrd 2777 |
1
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ(๐ด + ๐ต)) = ((โโ๐ด) + (โโ๐ต))) |