Step | Hyp | Ref
| Expression |
1 | | imcl 15003 |
. . . 4
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
2 | 1 | recnd 11190 |
. . 3
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
3 | | 2mulicn 12383 |
. . . 4
โข (2
ยท i) โ โ |
4 | | 2muline0 12384 |
. . . 4
โข (2
ยท i) โ 0 |
5 | | divcan4 11847 |
. . . 4
โข
(((โโ๐ด)
โ โ โง (2 ยท i) โ โ โง (2 ยท i) โ 0)
โ (((โโ๐ด)
ยท (2 ยท i)) / (2 ยท i)) = (โโ๐ด)) |
6 | 3, 4, 5 | mp3an23 1454 |
. . 3
โข
((โโ๐ด)
โ โ โ (((โโ๐ด) ยท (2 ยท i)) / (2 ยท i))
= (โโ๐ด)) |
7 | 2, 6 | syl 17 |
. 2
โข (๐ด โ โ โ
(((โโ๐ด)
ยท (2 ยท i)) / (2 ยท i)) = (โโ๐ด)) |
8 | | recl 15002 |
. . . . . . 7
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
9 | 8 | recnd 11190 |
. . . . . 6
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
10 | | ax-icn 11117 |
. . . . . . 7
โข i โ
โ |
11 | | mulcl 11142 |
. . . . . . 7
โข ((i
โ โ โง (โโ๐ด) โ โ) โ (i ยท
(โโ๐ด)) โ
โ) |
12 | 10, 2, 11 | sylancr 588 |
. . . . . 6
โข (๐ด โ โ โ (i
ยท (โโ๐ด))
โ โ) |
13 | 9, 12 | addcld 11181 |
. . . . 5
โข (๐ด โ โ โ
((โโ๐ด) + (i
ยท (โโ๐ด))) โ โ) |
14 | 13, 9, 12 | subsubd 11547 |
. . . 4
โข (๐ด โ โ โ
(((โโ๐ด) + (i
ยท (โโ๐ด))) โ ((โโ๐ด) โ (i ยท (โโ๐ด)))) = ((((โโ๐ด) + (i ยท
(โโ๐ด))) โ
(โโ๐ด)) + (i
ยท (โโ๐ด)))) |
15 | | replim 15008 |
. . . . 5
โข (๐ด โ โ โ ๐ด = ((โโ๐ด) + (i ยท
(โโ๐ด)))) |
16 | | remim 15009 |
. . . . 5
โข (๐ด โ โ โ
(โโ๐ด) =
((โโ๐ด) โ
(i ยท (โโ๐ด)))) |
17 | 15, 16 | oveq12d 7380 |
. . . 4
โข (๐ด โ โ โ (๐ด โ (โโ๐ด)) = (((โโ๐ด) + (i ยท
(โโ๐ด))) โ
((โโ๐ด) โ
(i ยท (โโ๐ด))))) |
18 | 12 | 2timesd 12403 |
. . . . 5
โข (๐ด โ โ โ (2
ยท (i ยท (โโ๐ด))) = ((i ยท (โโ๐ด)) + (i ยท
(โโ๐ด)))) |
19 | | mulcom 11144 |
. . . . . . . 8
โข
(((โโ๐ด)
โ โ โง (2 ยท i) โ โ) โ
((โโ๐ด) ยท
(2 ยท i)) = ((2 ยท i) ยท (โโ๐ด))) |
20 | 3, 19 | mpan2 690 |
. . . . . . 7
โข
((โโ๐ด)
โ โ โ ((โโ๐ด) ยท (2 ยท i)) = ((2 ยท i)
ยท (โโ๐ด))) |
21 | | 2cn 12235 |
. . . . . . . 8
โข 2 โ
โ |
22 | | mulass 11146 |
. . . . . . . 8
โข ((2
โ โ โง i โ โ โง (โโ๐ด) โ โ) โ ((2 ยท i)
ยท (โโ๐ด))
= (2 ยท (i ยท (โโ๐ด)))) |
23 | 21, 10, 22 | mp3an12 1452 |
. . . . . . 7
โข
((โโ๐ด)
โ โ โ ((2 ยท i) ยท (โโ๐ด)) = (2 ยท (i ยท
(โโ๐ด)))) |
24 | 20, 23 | eqtrd 2777 |
. . . . . 6
โข
((โโ๐ด)
โ โ โ ((โโ๐ด) ยท (2 ยท i)) = (2 ยท (i
ยท (โโ๐ด)))) |
25 | 2, 24 | syl 17 |
. . . . 5
โข (๐ด โ โ โ
((โโ๐ด) ยท
(2 ยท i)) = (2 ยท (i ยท (โโ๐ด)))) |
26 | 9, 12 | pncan2d 11521 |
. . . . . 6
โข (๐ด โ โ โ
(((โโ๐ด) + (i
ยท (โโ๐ด))) โ (โโ๐ด)) = (i ยท (โโ๐ด))) |
27 | 26 | oveq1d 7377 |
. . . . 5
โข (๐ด โ โ โ
((((โโ๐ด) + (i
ยท (โโ๐ด))) โ (โโ๐ด)) + (i ยท (โโ๐ด))) = ((i ยท
(โโ๐ด)) + (i
ยท (โโ๐ด)))) |
28 | 18, 25, 27 | 3eqtr4d 2787 |
. . . 4
โข (๐ด โ โ โ
((โโ๐ด) ยท
(2 ยท i)) = ((((โโ๐ด) + (i ยท (โโ๐ด))) โ (โโ๐ด)) + (i ยท
(โโ๐ด)))) |
29 | 14, 17, 28 | 3eqtr4rd 2788 |
. . 3
โข (๐ด โ โ โ
((โโ๐ด) ยท
(2 ยท i)) = (๐ด
โ (โโ๐ด))) |
30 | 29 | oveq1d 7377 |
. 2
โข (๐ด โ โ โ
(((โโ๐ด)
ยท (2 ยท i)) / (2 ยท i)) = ((๐ด โ (โโ๐ด)) / (2 ยท i))) |
31 | 7, 30 | eqtr3d 2779 |
1
โข (๐ด โ โ โ
(โโ๐ด) = ((๐ด โ (โโ๐ด)) / (2 ยท
i))) |