Step | Hyp | Ref
| Expression |
1 | | cjval 14994 |
. 2
โข (๐ด โ โ โ
(โโ๐ด) =
(โฉ๐ฅ โ
โ ((๐ด + ๐ฅ) โ โ โง (i
ยท (๐ด โ ๐ฅ)) โ
โ))) |
2 | | replim 15008 |
. . . . . 6
โข (๐ด โ โ โ ๐ด = ((โโ๐ด) + (i ยท
(โโ๐ด)))) |
3 | 2 | oveq1d 7377 |
. . . . 5
โข (๐ด โ โ โ (๐ด + ((โโ๐ด) โ (i ยท
(โโ๐ด)))) =
(((โโ๐ด) + (i
ยท (โโ๐ด))) + ((โโ๐ด) โ (i ยท (โโ๐ด))))) |
4 | | recl 15002 |
. . . . . . 7
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
5 | 4 | recnd 11190 |
. . . . . 6
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
6 | | ax-icn 11117 |
. . . . . . 7
โข i โ
โ |
7 | | imcl 15003 |
. . . . . . . 8
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
8 | 7 | recnd 11190 |
. . . . . . 7
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
9 | | mulcl 11142 |
. . . . . . 7
โข ((i
โ โ โง (โโ๐ด) โ โ) โ (i ยท
(โโ๐ด)) โ
โ) |
10 | 6, 8, 9 | sylancr 588 |
. . . . . 6
โข (๐ด โ โ โ (i
ยท (โโ๐ด))
โ โ) |
11 | 5, 10, 5 | ppncand 11559 |
. . . . 5
โข (๐ด โ โ โ
(((โโ๐ด) + (i
ยท (โโ๐ด))) + ((โโ๐ด) โ (i ยท (โโ๐ด)))) = ((โโ๐ด) + (โโ๐ด))) |
12 | 3, 11 | eqtrd 2777 |
. . . 4
โข (๐ด โ โ โ (๐ด + ((โโ๐ด) โ (i ยท
(โโ๐ด)))) =
((โโ๐ด) +
(โโ๐ด))) |
13 | 4, 4 | readdcld 11191 |
. . . 4
โข (๐ด โ โ โ
((โโ๐ด) +
(โโ๐ด)) โ
โ) |
14 | 12, 13 | eqeltrd 2838 |
. . 3
โข (๐ด โ โ โ (๐ด + ((โโ๐ด) โ (i ยท
(โโ๐ด)))) โ
โ) |
15 | 5, 10, 10 | pnncand 11558 |
. . . . . . 7
โข (๐ด โ โ โ
(((โโ๐ด) + (i
ยท (โโ๐ด))) โ ((โโ๐ด) โ (i ยท (โโ๐ด)))) = ((i ยท
(โโ๐ด)) + (i
ยท (โโ๐ด)))) |
16 | 2 | oveq1d 7377 |
. . . . . . 7
โข (๐ด โ โ โ (๐ด โ ((โโ๐ด) โ (i ยท
(โโ๐ด)))) =
(((โโ๐ด) + (i
ยท (โโ๐ด))) โ ((โโ๐ด) โ (i ยท (โโ๐ด))))) |
17 | 6 | a1i 11 |
. . . . . . . 8
โข (๐ด โ โ โ i โ
โ) |
18 | 17, 8, 8 | adddid 11186 |
. . . . . . 7
โข (๐ด โ โ โ (i
ยท ((โโ๐ด)
+ (โโ๐ด))) = ((i
ยท (โโ๐ด))
+ (i ยท (โโ๐ด)))) |
19 | 15, 16, 18 | 3eqtr4d 2787 |
. . . . . 6
โข (๐ด โ โ โ (๐ด โ ((โโ๐ด) โ (i ยท
(โโ๐ด)))) = (i
ยท ((โโ๐ด)
+ (โโ๐ด)))) |
20 | 19 | oveq2d 7378 |
. . . . 5
โข (๐ด โ โ โ (i
ยท (๐ด โ
((โโ๐ด) โ
(i ยท (โโ๐ด))))) = (i ยท (i ยท
((โโ๐ด) +
(โโ๐ด))))) |
21 | 7, 7 | readdcld 11191 |
. . . . . . 7
โข (๐ด โ โ โ
((โโ๐ด) +
(โโ๐ด)) โ
โ) |
22 | 21 | recnd 11190 |
. . . . . 6
โข (๐ด โ โ โ
((โโ๐ด) +
(โโ๐ด)) โ
โ) |
23 | | mulass 11146 |
. . . . . 6
โข ((i
โ โ โง i โ โ โง ((โโ๐ด) + (โโ๐ด)) โ โ) โ ((i ยท i)
ยท ((โโ๐ด)
+ (โโ๐ด))) = (i
ยท (i ยท ((โโ๐ด) + (โโ๐ด))))) |
24 | 6, 6, 22, 23 | mp3an12i 1466 |
. . . . 5
โข (๐ด โ โ โ ((i
ยท i) ยท ((โโ๐ด) + (โโ๐ด))) = (i ยท (i ยท
((โโ๐ด) +
(โโ๐ด))))) |
25 | 20, 24 | eqtr4d 2780 |
. . . 4
โข (๐ด โ โ โ (i
ยท (๐ด โ
((โโ๐ด) โ
(i ยท (โโ๐ด))))) = ((i ยท i) ยท
((โโ๐ด) +
(โโ๐ด)))) |
26 | | ixi 11791 |
. . . . . 6
โข (i
ยท i) = -1 |
27 | | neg1rr 12275 |
. . . . . 6
โข -1 โ
โ |
28 | 26, 27 | eqeltri 2834 |
. . . . 5
โข (i
ยท i) โ โ |
29 | | remulcl 11143 |
. . . . 5
โข (((i
ยท i) โ โ โง ((โโ๐ด) + (โโ๐ด)) โ โ) โ ((i ยท i)
ยท ((โโ๐ด)
+ (โโ๐ด)))
โ โ) |
30 | 28, 21, 29 | sylancr 588 |
. . . 4
โข (๐ด โ โ โ ((i
ยท i) ยท ((โโ๐ด) + (โโ๐ด))) โ โ) |
31 | 25, 30 | eqeltrd 2838 |
. . 3
โข (๐ด โ โ โ (i
ยท (๐ด โ
((โโ๐ด) โ
(i ยท (โโ๐ด))))) โ โ) |
32 | 5, 10 | subcld 11519 |
. . . 4
โข (๐ด โ โ โ
((โโ๐ด) โ
(i ยท (โโ๐ด))) โ โ) |
33 | | cju 12156 |
. . . 4
โข (๐ด โ โ โ
โ!๐ฅ โ โ
((๐ด + ๐ฅ) โ โ โง (i ยท (๐ด โ ๐ฅ)) โ โ)) |
34 | | oveq2 7370 |
. . . . . . 7
โข (๐ฅ = ((โโ๐ด) โ (i ยท
(โโ๐ด))) โ
(๐ด + ๐ฅ) = (๐ด + ((โโ๐ด) โ (i ยท (โโ๐ด))))) |
35 | 34 | eleq1d 2823 |
. . . . . 6
โข (๐ฅ = ((โโ๐ด) โ (i ยท
(โโ๐ด))) โ
((๐ด + ๐ฅ) โ โ โ (๐ด + ((โโ๐ด) โ (i ยท (โโ๐ด)))) โ
โ)) |
36 | | oveq2 7370 |
. . . . . . . 8
โข (๐ฅ = ((โโ๐ด) โ (i ยท
(โโ๐ด))) โ
(๐ด โ ๐ฅ) = (๐ด โ ((โโ๐ด) โ (i ยท (โโ๐ด))))) |
37 | 36 | oveq2d 7378 |
. . . . . . 7
โข (๐ฅ = ((โโ๐ด) โ (i ยท
(โโ๐ด))) โ
(i ยท (๐ด โ
๐ฅ)) = (i ยท (๐ด โ ((โโ๐ด) โ (i ยท
(โโ๐ด)))))) |
38 | 37 | eleq1d 2823 |
. . . . . 6
โข (๐ฅ = ((โโ๐ด) โ (i ยท
(โโ๐ด))) โ
((i ยท (๐ด โ
๐ฅ)) โ โ โ
(i ยท (๐ด โ
((โโ๐ด) โ
(i ยท (โโ๐ด))))) โ โ)) |
39 | 35, 38 | anbi12d 632 |
. . . . 5
โข (๐ฅ = ((โโ๐ด) โ (i ยท
(โโ๐ด))) โ
(((๐ด + ๐ฅ) โ โ โง (i ยท (๐ด โ ๐ฅ)) โ โ) โ ((๐ด + ((โโ๐ด) โ (i ยท (โโ๐ด)))) โ โ โง (i
ยท (๐ด โ
((โโ๐ด) โ
(i ยท (โโ๐ด))))) โ โ))) |
40 | 39 | riota2 7344 |
. . . 4
โข
((((โโ๐ด)
โ (i ยท (โโ๐ด))) โ โ โง โ!๐ฅ โ โ ((๐ด + ๐ฅ) โ โ โง (i ยท (๐ด โ ๐ฅ)) โ โ)) โ (((๐ด + ((โโ๐ด) โ (i ยท
(โโ๐ด)))) โ
โ โง (i ยท (๐ด โ ((โโ๐ด) โ (i ยท (โโ๐ด))))) โ โ) โ
(โฉ๐ฅ โ
โ ((๐ด + ๐ฅ) โ โ โง (i
ยท (๐ด โ ๐ฅ)) โ โ)) =
((โโ๐ด) โ
(i ยท (โโ๐ด))))) |
41 | 32, 33, 40 | syl2anc 585 |
. . 3
โข (๐ด โ โ โ (((๐ด + ((โโ๐ด) โ (i ยท
(โโ๐ด)))) โ
โ โง (i ยท (๐ด โ ((โโ๐ด) โ (i ยท (โโ๐ด))))) โ โ) โ
(โฉ๐ฅ โ
โ ((๐ด + ๐ฅ) โ โ โง (i
ยท (๐ด โ ๐ฅ)) โ โ)) =
((โโ๐ด) โ
(i ยท (โโ๐ด))))) |
42 | 14, 31, 41 | mpbi2and 711 |
. 2
โข (๐ด โ โ โ
(โฉ๐ฅ โ
โ ((๐ด + ๐ฅ) โ โ โง (i
ยท (๐ด โ ๐ฅ)) โ โ)) =
((โโ๐ด) โ
(i ยท (โโ๐ด)))) |
43 | 1, 42 | eqtrd 2777 |
1
โข (๐ด โ โ โ
(โโ๐ด) =
((โโ๐ด) โ
(i ยท (โโ๐ด)))) |