Step | Hyp | Ref
| Expression |
1 | | lnophmlem.2 |
. . . . . 6
โข ๐ต โ โ |
2 | | lnophmlem.1 |
. . . . . . 7
โข ๐ด โ โ |
3 | | lnophmlem.3 |
. . . . . . . . 9
โข ๐ โ LinOp |
4 | 3 | lnopfi 30960 |
. . . . . . . 8
โข ๐: โโถ
โ |
5 | 4 | ffvelcdmi 7038 |
. . . . . . 7
โข (๐ด โ โ โ (๐โ๐ด) โ โ) |
6 | 2, 5 | ax-mp 5 |
. . . . . 6
โข (๐โ๐ด) โ โ |
7 | 4 | ffvelcdmi 7038 |
. . . . . . 7
โข (๐ต โ โ โ (๐โ๐ต) โ โ) |
8 | 1, 7 | ax-mp 5 |
. . . . . 6
โข (๐โ๐ต) โ โ |
9 | 1, 6, 2, 8 | polid2i 30148 |
. . . . 5
โข (๐ต
ยทih (๐โ๐ด)) = (((((๐ต +โ ๐ด) ยทih
((๐โ๐ต) +โ (๐โ๐ด))) โ ((๐ต โโ ๐ด)
ยทih ((๐โ๐ต) โโ (๐โ๐ด)))) + (i ยท (((๐ต +โ (i
ยทโ ๐ด)) ยทih
((๐โ๐ต) +โ (i
ยทโ (๐โ๐ด)))) โ ((๐ต โโ (i
ยทโ ๐ด)) ยทih
((๐โ๐ต) โโ (i
ยทโ (๐โ๐ด))))))) / 4) |
10 | 1, 2 | hvcomi 30010 |
. . . . . . . . 9
โข (๐ต +โ ๐ด) = (๐ด +โ ๐ต) |
11 | 8, 6 | hvcomi 30010 |
. . . . . . . . . 10
โข ((๐โ๐ต) +โ (๐โ๐ด)) = ((๐โ๐ด) +โ (๐โ๐ต)) |
12 | 3 | lnopaddi 30962 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐โ(๐ด +โ ๐ต)) = ((๐โ๐ด) +โ (๐โ๐ต))) |
13 | 2, 1, 12 | mp2an 691 |
. . . . . . . . . 10
โข (๐โ(๐ด +โ ๐ต)) = ((๐โ๐ด) +โ (๐โ๐ต)) |
14 | 11, 13 | eqtr4i 2764 |
. . . . . . . . 9
โข ((๐โ๐ต) +โ (๐โ๐ด)) = (๐โ(๐ด +โ ๐ต)) |
15 | 10, 14 | oveq12i 7373 |
. . . . . . . 8
โข ((๐ต +โ ๐ด)
ยทih ((๐โ๐ต) +โ (๐โ๐ด))) = ((๐ด +โ ๐ต) ยทih (๐โ(๐ด +โ ๐ต))) |
16 | 1, 2, 8, 6 | hisubcomi 30095 |
. . . . . . . . 9
โข ((๐ต โโ
๐ด)
ยทih ((๐โ๐ต) โโ (๐โ๐ด))) = ((๐ด โโ ๐ต)
ยทih ((๐โ๐ด) โโ (๐โ๐ต))) |
17 | 3 | lnopsubi 30965 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐โ(๐ด โโ ๐ต)) = ((๐โ๐ด) โโ (๐โ๐ต))) |
18 | 2, 1, 17 | mp2an 691 |
. . . . . . . . . 10
โข (๐โ(๐ด โโ ๐ต)) = ((๐โ๐ด) โโ (๐โ๐ต)) |
19 | 18 | oveq2i 7372 |
. . . . . . . . 9
โข ((๐ด โโ
๐ต)
ยทih (๐โ(๐ด โโ ๐ต))) = ((๐ด โโ ๐ต)
ยทih ((๐โ๐ด) โโ (๐โ๐ต))) |
20 | 16, 19 | eqtr4i 2764 |
. . . . . . . 8
โข ((๐ต โโ
๐ด)
ยทih ((๐โ๐ต) โโ (๐โ๐ด))) = ((๐ด โโ ๐ต)
ยทih (๐โ(๐ด โโ ๐ต))) |
21 | 15, 20 | oveq12i 7373 |
. . . . . . 7
โข (((๐ต +โ ๐ด)
ยทih ((๐โ๐ต) +โ (๐โ๐ด))) โ ((๐ต โโ ๐ด)
ยทih ((๐โ๐ต) โโ (๐โ๐ด)))) = (((๐ด +โ ๐ต) ยทih (๐โ(๐ด +โ ๐ต))) โ ((๐ด โโ ๐ต)
ยทih (๐โ(๐ด โโ ๐ต)))) |
22 | | ax-icn 11118 |
. . . . . . . . . . 11
โข i โ
โ |
23 | 22, 1 | hvmulcli 30005 |
. . . . . . . . . . . 12
โข (i
ยทโ ๐ต) โ โ |
24 | 2, 23 | hvsubcli 30012 |
. . . . . . . . . . 11
โข (๐ด โโ (i
ยทโ ๐ต)) โ โ |
25 | 4 | ffvelcdmi 7038 |
. . . . . . . . . . . 12
โข ((๐ด โโ (i
ยทโ ๐ต)) โ โ โ (๐โ(๐ด โโ (i
ยทโ ๐ต))) โ โ) |
26 | 24, 25 | ax-mp 5 |
. . . . . . . . . . 11
โข (๐โ(๐ด โโ (i
ยทโ ๐ต))) โ โ |
27 | 22, 22, 24, 26 | his35i 30080 |
. . . . . . . . . 10
โข ((i
ยทโ (๐ด โโ (i
ยทโ ๐ต))) ยทih (i
ยทโ (๐โ(๐ด โโ (i
ยทโ ๐ต))))) = ((i ยท (โโi))
ยท ((๐ด
โโ (i ยทโ ๐ต))
ยทih (๐โ(๐ด โโ (i
ยทโ ๐ต))))) |
28 | 22, 2, 23 | hvsubdistr1i 30043 |
. . . . . . . . . . . 12
โข (i
ยทโ (๐ด โโ (i
ยทโ ๐ต))) = ((i ยทโ
๐ด)
โโ (i ยทโ (i
ยทโ ๐ต))) |
29 | 22, 2 | hvmulcli 30005 |
. . . . . . . . . . . . . 14
โข (i
ยทโ ๐ด) โ โ |
30 | 22, 23 | hvmulcli 30005 |
. . . . . . . . . . . . . 14
โข (i
ยทโ (i ยทโ ๐ต)) โ
โ |
31 | 29, 30 | hvsubvali 30011 |
. . . . . . . . . . . . 13
โข ((i
ยทโ ๐ด) โโ (i
ยทโ (i ยทโ ๐ต))) = ((i
ยทโ ๐ด) +โ (-1
ยทโ (i ยทโ (i
ยทโ ๐ต)))) |
32 | 22, 22, 1 | hvmulassi 30037 |
. . . . . . . . . . . . . . . 16
โข ((i
ยท i) ยทโ ๐ต) = (i ยทโ (i
ยทโ ๐ต)) |
33 | 32 | oveq2i 7372 |
. . . . . . . . . . . . . . 15
โข (-1
ยทโ ((i ยท i)
ยทโ ๐ต)) = (-1 ยทโ
(i ยทโ (i ยทโ
๐ต))) |
34 | | ixi 11792 |
. . . . . . . . . . . . . . . . . . 19
โข (i
ยท i) = -1 |
35 | 34 | oveq2i 7372 |
. . . . . . . . . . . . . . . . . 18
โข (-1
ยท (i ยท i)) = (-1 ยท -1) |
36 | | ax-1cn 11117 |
. . . . . . . . . . . . . . . . . . 19
โข 1 โ
โ |
37 | 36, 36 | mul2negi 11611 |
. . . . . . . . . . . . . . . . . 18
โข (-1
ยท -1) = (1 ยท 1) |
38 | | 1t1e1 12323 |
. . . . . . . . . . . . . . . . . 18
โข (1
ยท 1) = 1 |
39 | 35, 37, 38 | 3eqtri 2765 |
. . . . . . . . . . . . . . . . 17
โข (-1
ยท (i ยท i)) = 1 |
40 | 39 | oveq1i 7371 |
. . . . . . . . . . . . . . . 16
โข ((-1
ยท (i ยท i)) ยทโ ๐ต) = (1 ยทโ
๐ต) |
41 | | neg1cn 12275 |
. . . . . . . . . . . . . . . . 17
โข -1 โ
โ |
42 | 22, 22 | mulcli 11170 |
. . . . . . . . . . . . . . . . 17
โข (i
ยท i) โ โ |
43 | 41, 42, 1 | hvmulassi 30037 |
. . . . . . . . . . . . . . . 16
โข ((-1
ยท (i ยท i)) ยทโ ๐ต) = (-1 ยทโ
((i ยท i) ยทโ ๐ต)) |
44 | | ax-hvmulid 29997 |
. . . . . . . . . . . . . . . . 17
โข (๐ต โ โ โ (1
ยทโ ๐ต) = ๐ต) |
45 | 1, 44 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
โข (1
ยทโ ๐ต) = ๐ต |
46 | 40, 43, 45 | 3eqtr3i 2769 |
. . . . . . . . . . . . . . 15
โข (-1
ยทโ ((i ยท i)
ยทโ ๐ต)) = ๐ต |
47 | 33, 46 | eqtr3i 2763 |
. . . . . . . . . . . . . 14
โข (-1
ยทโ (i ยทโ (i
ยทโ ๐ต))) = ๐ต |
48 | 47 | oveq2i 7372 |
. . . . . . . . . . . . 13
โข ((i
ยทโ ๐ด) +โ (-1
ยทโ (i ยทโ (i
ยทโ ๐ต)))) = ((i
ยทโ ๐ด) +โ ๐ต) |
49 | 31, 48 | eqtri 2761 |
. . . . . . . . . . . 12
โข ((i
ยทโ ๐ด) โโ (i
ยทโ (i ยทโ ๐ต))) = ((i
ยทโ ๐ด) +โ ๐ต) |
50 | 29, 1 | hvcomi 30010 |
. . . . . . . . . . . 12
โข ((i
ยทโ ๐ด) +โ ๐ต) = (๐ต +โ (i
ยทโ ๐ด)) |
51 | 28, 49, 50 | 3eqtri 2765 |
. . . . . . . . . . 11
โข (i
ยทโ (๐ด โโ (i
ยทโ ๐ต))) = (๐ต +โ (i
ยทโ ๐ด)) |
52 | 51 | fveq2i 6849 |
. . . . . . . . . . . 12
โข (๐โ(i
ยทโ (๐ด โโ (i
ยทโ ๐ต)))) = (๐โ(๐ต +โ (i
ยทโ ๐ด))) |
53 | 3 | lnopmuli 30963 |
. . . . . . . . . . . . 13
โข ((i
โ โ โง (๐ด
โโ (i ยทโ ๐ต)) โ โ) โ (๐โ(i
ยทโ (๐ด โโ (i
ยทโ ๐ต)))) = (i ยทโ
(๐โ(๐ด โโ (i
ยทโ ๐ต))))) |
54 | 22, 24, 53 | mp2an 691 |
. . . . . . . . . . . 12
โข (๐โ(i
ยทโ (๐ด โโ (i
ยทโ ๐ต)))) = (i ยทโ
(๐โ(๐ด โโ (i
ยทโ ๐ต)))) |
55 | 3 | lnopaddmuli 30964 |
. . . . . . . . . . . . 13
โข ((i
โ โ โง ๐ต
โ โ โง ๐ด
โ โ) โ (๐โ(๐ต +โ (i
ยทโ ๐ด))) = ((๐โ๐ต) +โ (i
ยทโ (๐โ๐ด)))) |
56 | 22, 1, 2, 55 | mp3an 1462 |
. . . . . . . . . . . 12
โข (๐โ(๐ต +โ (i
ยทโ ๐ด))) = ((๐โ๐ต) +โ (i
ยทโ (๐โ๐ด))) |
57 | 52, 54, 56 | 3eqtr3i 2769 |
. . . . . . . . . . 11
โข (i
ยทโ (๐โ(๐ด โโ (i
ยทโ ๐ต)))) = ((๐โ๐ต) +โ (i
ยทโ (๐โ๐ด))) |
58 | 51, 57 | oveq12i 7373 |
. . . . . . . . . 10
โข ((i
ยทโ (๐ด โโ (i
ยทโ ๐ต))) ยทih (i
ยทโ (๐โ(๐ด โโ (i
ยทโ ๐ต))))) = ((๐ต +โ (i
ยทโ ๐ด)) ยทih
((๐โ๐ต) +โ (i
ยทโ (๐โ๐ด)))) |
59 | | cji 15053 |
. . . . . . . . . . . . . 14
โข
(โโi) = -i |
60 | 59 | oveq2i 7372 |
. . . . . . . . . . . . 13
โข (i
ยท (โโi)) = (i ยท -i) |
61 | 22, 22 | mulneg2i 11610 |
. . . . . . . . . . . . 13
โข (i
ยท -i) = -(i ยท i) |
62 | 34 | negeqi 11402 |
. . . . . . . . . . . . . 14
โข -(i
ยท i) = --1 |
63 | | negneg1e1 12279 |
. . . . . . . . . . . . . 14
โข --1 =
1 |
64 | 62, 63 | eqtri 2761 |
. . . . . . . . . . . . 13
โข -(i
ยท i) = 1 |
65 | 60, 61, 64 | 3eqtri 2765 |
. . . . . . . . . . . 12
โข (i
ยท (โโi)) = 1 |
66 | 65 | oveq1i 7371 |
. . . . . . . . . . 11
โข ((i
ยท (โโi)) ยท ((๐ด โโ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด โโ (i
ยทโ ๐ต))))) = (1 ยท ((๐ด โโ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด โโ (i
ยทโ ๐ต))))) |
67 | | lnophmlem.4 |
. . . . . . . . . . . . . 14
โข
โ๐ฅ โ
โ (๐ฅ
ยทih (๐โ๐ฅ)) โ โ |
68 | 24, 2, 3, 67 | lnophmlem1 31007 |
. . . . . . . . . . . . 13
โข ((๐ด โโ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด โโ (i
ยทโ ๐ต)))) โ โ |
69 | 68 | recni 11177 |
. . . . . . . . . . . 12
โข ((๐ด โโ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด โโ (i
ยทโ ๐ต)))) โ โ |
70 | 69 | mulid2i 11168 |
. . . . . . . . . . 11
โข (1
ยท ((๐ด
โโ (i ยทโ ๐ต))
ยทih (๐โ(๐ด โโ (i
ยทโ ๐ต))))) = ((๐ด โโ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด โโ (i
ยทโ ๐ต)))) |
71 | 66, 70 | eqtri 2761 |
. . . . . . . . . 10
โข ((i
ยท (โโi)) ยท ((๐ด โโ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด โโ (i
ยทโ ๐ต))))) = ((๐ด โโ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด โโ (i
ยทโ ๐ต)))) |
72 | 27, 58, 71 | 3eqtr3i 2769 |
. . . . . . . . 9
โข ((๐ต +โ (i
ยทโ ๐ด)) ยทih
((๐โ๐ต) +โ (i
ยทโ (๐โ๐ด)))) = ((๐ด โโ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด โโ (i
ยทโ ๐ต)))) |
73 | 22, 6 | hvmulcli 30005 |
. . . . . . . . . . . 12
โข (i
ยทโ (๐โ๐ด)) โ โ |
74 | 1, 29, 8, 73 | hisubcomi 30095 |
. . . . . . . . . . 11
โข ((๐ต โโ (i
ยทโ ๐ด)) ยทih
((๐โ๐ต) โโ (i
ยทโ (๐โ๐ด)))) = (((i
ยทโ ๐ด) โโ ๐ต)
ยทih ((i ยทโ
(๐โ๐ด)) โโ (๐โ๐ต))) |
75 | 34 | oveq1i 7371 |
. . . . . . . . . . . . . . 15
โข ((i
ยท i) ยทโ ๐ต) = (-1 ยทโ
๐ต) |
76 | 32, 75 | eqtr3i 2763 |
. . . . . . . . . . . . . 14
โข (i
ยทโ (i ยทโ ๐ต)) = (-1
ยทโ ๐ต) |
77 | 76 | oveq2i 7372 |
. . . . . . . . . . . . 13
โข ((i
ยทโ ๐ด) +โ (i
ยทโ (i ยทโ ๐ต))) = ((i
ยทโ ๐ด) +โ (-1
ยทโ ๐ต)) |
78 | 22, 2, 23 | hvdistr1i 30042 |
. . . . . . . . . . . . 13
โข (i
ยทโ (๐ด +โ (i
ยทโ ๐ต))) = ((i ยทโ
๐ด) +โ (i
ยทโ (i ยทโ ๐ต))) |
79 | 29, 1 | hvsubvali 30011 |
. . . . . . . . . . . . 13
โข ((i
ยทโ ๐ด) โโ ๐ต) = ((i
ยทโ ๐ด) +โ (-1
ยทโ ๐ต)) |
80 | 77, 78, 79 | 3eqtr4i 2771 |
. . . . . . . . . . . 12
โข (i
ยทโ (๐ด +โ (i
ยทโ ๐ต))) = ((i ยทโ
๐ด)
โโ ๐ต) |
81 | 80 | fveq2i 6849 |
. . . . . . . . . . . . 13
โข (๐โ(i
ยทโ (๐ด +โ (i
ยทโ ๐ต)))) = (๐โ((i
ยทโ ๐ด) โโ ๐ต)) |
82 | 2, 23 | hvaddcli 30009 |
. . . . . . . . . . . . . 14
โข (๐ด +โ (i
ยทโ ๐ต)) โ โ |
83 | 3 | lnopmuli 30963 |
. . . . . . . . . . . . . 14
โข ((i
โ โ โง (๐ด
+โ (i ยทโ ๐ต)) โ โ) โ (๐โ(i ยทโ
(๐ด +โ (i
ยทโ ๐ต)))) = (i ยทโ
(๐โ(๐ด +โ (i
ยทโ ๐ต))))) |
84 | 22, 82, 83 | mp2an 691 |
. . . . . . . . . . . . 13
โข (๐โ(i
ยทโ (๐ด +โ (i
ยทโ ๐ต)))) = (i ยทโ
(๐โ(๐ด +โ (i
ยทโ ๐ต)))) |
85 | 3 | lnopmulsubi 30967 |
. . . . . . . . . . . . . 14
โข ((i
โ โ โง ๐ด
โ โ โง ๐ต
โ โ) โ (๐โ((i
ยทโ ๐ด) โโ ๐ต)) = ((i
ยทโ (๐โ๐ด)) โโ (๐โ๐ต))) |
86 | 22, 2, 1, 85 | mp3an 1462 |
. . . . . . . . . . . . 13
โข (๐โ((i
ยทโ ๐ด) โโ ๐ต)) = ((i
ยทโ (๐โ๐ด)) โโ (๐โ๐ต)) |
87 | 81, 84, 86 | 3eqtr3i 2769 |
. . . . . . . . . . . 12
โข (i
ยทโ (๐โ(๐ด +โ (i
ยทโ ๐ต)))) = ((i
ยทโ (๐โ๐ด)) โโ (๐โ๐ต)) |
88 | 80, 87 | oveq12i 7373 |
. . . . . . . . . . 11
โข ((i
ยทโ (๐ด +โ (i
ยทโ ๐ต))) ยทih (i
ยทโ (๐โ(๐ด +โ (i
ยทโ ๐ต))))) = (((i
ยทโ ๐ด) โโ ๐ต)
ยทih ((i ยทโ
(๐โ๐ด)) โโ (๐โ๐ต))) |
89 | 74, 88 | eqtr4i 2764 |
. . . . . . . . . 10
โข ((๐ต โโ (i
ยทโ ๐ด)) ยทih
((๐โ๐ต) โโ (i
ยทโ (๐โ๐ด)))) = ((i
ยทโ (๐ด +โ (i
ยทโ ๐ต))) ยทih (i
ยทโ (๐โ(๐ด +โ (i
ยทโ ๐ต))))) |
90 | 4 | ffvelcdmi 7038 |
. . . . . . . . . . . 12
โข ((๐ด +โ (i
ยทโ ๐ต)) โ โ โ (๐โ(๐ด +โ (i
ยทโ ๐ต))) โ โ) |
91 | 82, 90 | ax-mp 5 |
. . . . . . . . . . 11
โข (๐โ(๐ด +โ (i
ยทโ ๐ต))) โ โ |
92 | 22, 22, 82, 91 | his35i 30080 |
. . . . . . . . . 10
โข ((i
ยทโ (๐ด +โ (i
ยทโ ๐ต))) ยทih (i
ยทโ (๐โ(๐ด +โ (i
ยทโ ๐ต))))) = ((i ยท (โโi))
ยท ((๐ด
+โ (i ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต))))) |
93 | 65 | oveq1i 7371 |
. . . . . . . . . . 11
โข ((i
ยท (โโi)) ยท ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต))))) = (1 ยท ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต))))) |
94 | 82, 2, 3, 67 | lnophmlem1 31007 |
. . . . . . . . . . . . 13
โข ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต)))) โ โ |
95 | 94 | recni 11177 |
. . . . . . . . . . . 12
โข ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต)))) โ โ |
96 | 95 | mulid2i 11168 |
. . . . . . . . . . 11
โข (1
ยท ((๐ด
+โ (i ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต))))) = ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต)))) |
97 | 93, 96 | eqtri 2761 |
. . . . . . . . . 10
โข ((i
ยท (โโi)) ยท ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต))))) = ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต)))) |
98 | 89, 92, 97 | 3eqtri 2765 |
. . . . . . . . 9
โข ((๐ต โโ (i
ยทโ ๐ด)) ยทih
((๐โ๐ต) โโ (i
ยทโ (๐โ๐ด)))) = ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต)))) |
99 | 72, 98 | oveq12i 7373 |
. . . . . . . 8
โข (((๐ต +โ (i
ยทโ ๐ด)) ยทih
((๐โ๐ต) +โ (i
ยทโ (๐โ๐ด)))) โ ((๐ต โโ (i
ยทโ ๐ด)) ยทih
((๐โ๐ต) โโ (i
ยทโ (๐โ๐ด))))) = (((๐ด โโ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด โโ (i
ยทโ ๐ต)))) โ ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต))))) |
100 | 99 | oveq2i 7372 |
. . . . . . 7
โข (i
ยท (((๐ต
+โ (i ยทโ ๐ด)) ยทih
((๐โ๐ต) +โ (i
ยทโ (๐โ๐ด)))) โ ((๐ต โโ (i
ยทโ ๐ด)) ยทih
((๐โ๐ต) โโ (i
ยทโ (๐โ๐ด)))))) = (i ยท (((๐ด โโ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด โโ (i
ยทโ ๐ต)))) โ ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต)))))) |
101 | 21, 100 | oveq12i 7373 |
. . . . . 6
โข ((((๐ต +โ ๐ด)
ยทih ((๐โ๐ต) +โ (๐โ๐ด))) โ ((๐ต โโ ๐ด)
ยทih ((๐โ๐ต) โโ (๐โ๐ด)))) + (i ยท (((๐ต +โ (i
ยทโ ๐ด)) ยทih
((๐โ๐ต) +โ (i
ยทโ (๐โ๐ด)))) โ ((๐ต โโ (i
ยทโ ๐ด)) ยทih
((๐โ๐ต) โโ (i
ยทโ (๐โ๐ด))))))) = ((((๐ด +โ ๐ต) ยทih (๐โ(๐ด +โ ๐ต))) โ ((๐ด โโ ๐ต)
ยทih (๐โ(๐ด โโ ๐ต)))) + (i ยท (((๐ด โโ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด โโ (i
ยทโ ๐ต)))) โ ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต))))))) |
102 | 101 | oveq1i 7371 |
. . . . 5
โข
(((((๐ต
+โ ๐ด)
ยทih ((๐โ๐ต) +โ (๐โ๐ด))) โ ((๐ต โโ ๐ด)
ยทih ((๐โ๐ต) โโ (๐โ๐ด)))) + (i ยท (((๐ต +โ (i
ยทโ ๐ด)) ยทih
((๐โ๐ต) +โ (i
ยทโ (๐โ๐ด)))) โ ((๐ต โโ (i
ยทโ ๐ด)) ยทih
((๐โ๐ต) โโ (i
ยทโ (๐โ๐ด))))))) / 4) = (((((๐ด +โ ๐ต) ยทih (๐โ(๐ด +โ ๐ต))) โ ((๐ด โโ ๐ต)
ยทih (๐โ(๐ด โโ ๐ต)))) + (i ยท (((๐ด โโ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด โโ (i
ยทโ ๐ต)))) โ ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต))))))) / 4) |
103 | 9, 102 | eqtri 2761 |
. . . 4
โข (๐ต
ยทih (๐โ๐ด)) = (((((๐ด +โ ๐ต) ยทih (๐โ(๐ด +โ ๐ต))) โ ((๐ด โโ ๐ต)
ยทih (๐โ(๐ด โโ ๐ต)))) + (i ยท (((๐ด โโ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด โโ (i
ยทโ ๐ต)))) โ ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต))))))) / 4) |
104 | 103 | fveq2i 6849 |
. . 3
โข
(โโ(๐ต
ยทih (๐โ๐ด))) = (โโ(((((๐ด +โ ๐ต) ยทih (๐โ(๐ด +โ ๐ต))) โ ((๐ด โโ ๐ต)
ยทih (๐โ(๐ด โโ ๐ต)))) + (i ยท (((๐ด โโ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด โโ (i
ยทโ ๐ต)))) โ ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต))))))) / 4)) |
105 | | 4ne0 12269 |
. . . 4
โข 4 โ
0 |
106 | 2, 1 | hvaddcli 30009 |
. . . . . . . . 9
โข (๐ด +โ ๐ต) โ
โ |
107 | 106, 2, 3, 67 | lnophmlem1 31007 |
. . . . . . . 8
โข ((๐ด +โ ๐ต)
ยทih (๐โ(๐ด +โ ๐ต))) โ โ |
108 | 2, 1 | hvsubcli 30012 |
. . . . . . . . 9
โข (๐ด โโ
๐ต) โ
โ |
109 | 108, 2, 3, 67 | lnophmlem1 31007 |
. . . . . . . 8
โข ((๐ด โโ
๐ต)
ยทih (๐โ(๐ด โโ ๐ต))) โ
โ |
110 | 107, 109 | resubcli 11471 |
. . . . . . 7
โข (((๐ด +โ ๐ต)
ยทih (๐โ(๐ด +โ ๐ต))) โ ((๐ด โโ ๐ต)
ยทih (๐โ(๐ด โโ ๐ต)))) โ
โ |
111 | 110 | recni 11177 |
. . . . . 6
โข (((๐ด +โ ๐ต)
ยทih (๐โ(๐ด +โ ๐ต))) โ ((๐ด โโ ๐ต)
ยทih (๐โ(๐ด โโ ๐ต)))) โ
โ |
112 | 68, 94 | resubcli 11471 |
. . . . . . . 8
โข (((๐ด โโ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด โโ (i
ยทโ ๐ต)))) โ ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต))))) โ โ |
113 | 112 | recni 11177 |
. . . . . . 7
โข (((๐ด โโ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด โโ (i
ยทโ ๐ต)))) โ ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต))))) โ โ |
114 | 22, 113 | mulcli 11170 |
. . . . . 6
โข (i
ยท (((๐ด
โโ (i ยทโ ๐ต))
ยทih (๐โ(๐ด โโ (i
ยทโ ๐ต)))) โ ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต)))))) โ โ |
115 | 111, 114 | addcli 11169 |
. . . . 5
โข ((((๐ด +โ ๐ต)
ยทih (๐โ(๐ด +โ ๐ต))) โ ((๐ด โโ ๐ต)
ยทih (๐โ(๐ด โโ ๐ต)))) + (i ยท (((๐ด โโ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด โโ (i
ยทโ ๐ต)))) โ ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต))))))) โ โ |
116 | | 4re 12245 |
. . . . . 6
โข 4 โ
โ |
117 | 116 | recni 11177 |
. . . . 5
โข 4 โ
โ |
118 | 115, 117 | cjdivi 15085 |
. . . 4
โข (4 โ 0
โ (โโ(((((๐ด +โ ๐ต) ยทih (๐โ(๐ด +โ ๐ต))) โ ((๐ด โโ ๐ต)
ยทih (๐โ(๐ด โโ ๐ต)))) + (i ยท (((๐ด โโ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด โโ (i
ยทโ ๐ต)))) โ ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต))))))) / 4)) = ((โโ((((๐ด +โ ๐ต)
ยทih (๐โ(๐ด +โ ๐ต))) โ ((๐ด โโ ๐ต)
ยทih (๐โ(๐ด โโ ๐ต)))) + (i ยท (((๐ด โโ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด โโ (i
ยทโ ๐ต)))) โ ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต)))))))) /
(โโ4))) |
119 | 105, 118 | ax-mp 5 |
. . 3
โข
(โโ(((((๐ด +โ ๐ต) ยทih (๐โ(๐ด +โ ๐ต))) โ ((๐ด โโ ๐ต)
ยทih (๐โ(๐ด โโ ๐ต)))) + (i ยท (((๐ด โโ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด โโ (i
ยทโ ๐ต)))) โ ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต))))))) / 4)) = ((โโ((((๐ด +โ ๐ต)
ยทih (๐โ(๐ด +โ ๐ต))) โ ((๐ด โโ ๐ต)
ยทih (๐โ(๐ด โโ ๐ต)))) + (i ยท (((๐ด โโ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด โโ (i
ยทโ ๐ต)))) โ ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต)))))))) /
(โโ4)) |
120 | | cjreim 15054 |
. . . . . . 7
โข
(((((๐ด
+โ ๐ต)
ยทih (๐โ(๐ด +โ ๐ต))) โ ((๐ด โโ ๐ต)
ยทih (๐โ(๐ด โโ ๐ต)))) โ โ โง
(((๐ด
โโ (i ยทโ ๐ต))
ยทih (๐โ(๐ด โโ (i
ยทโ ๐ต)))) โ ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต))))) โ โ) โ
(โโ((((๐ด
+โ ๐ต)
ยทih (๐โ(๐ด +โ ๐ต))) โ ((๐ด โโ ๐ต)
ยทih (๐โ(๐ด โโ ๐ต)))) + (i ยท (((๐ด โโ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด โโ (i
ยทโ ๐ต)))) โ ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต)))))))) = ((((๐ด +โ ๐ต) ยทih (๐โ(๐ด +โ ๐ต))) โ ((๐ด โโ ๐ต)
ยทih (๐โ(๐ด โโ ๐ต)))) โ (i ยท
(((๐ด
โโ (i ยทโ ๐ต))
ยทih (๐โ(๐ด โโ (i
ยทโ ๐ต)))) โ ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต)))))))) |
121 | 110, 112,
120 | mp2an 691 |
. . . . . 6
โข
(โโ((((๐ด +โ ๐ต) ยทih (๐โ(๐ด +โ ๐ต))) โ ((๐ด โโ ๐ต)
ยทih (๐โ(๐ด โโ ๐ต)))) + (i ยท (((๐ด โโ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด โโ (i
ยทโ ๐ต)))) โ ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต)))))))) = ((((๐ด +โ ๐ต) ยทih (๐โ(๐ด +โ ๐ต))) โ ((๐ด โโ ๐ต)
ยทih (๐โ(๐ด โโ ๐ต)))) โ (i ยท
(((๐ด
โโ (i ยทโ ๐ต))
ยทih (๐โ(๐ด โโ (i
ยทโ ๐ต)))) โ ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต))))))) |
122 | 82, 1, 3, 67 | lnophmlem1 31007 |
. . . . . . . . . 10
โข ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต)))) โ โ |
123 | 68, 122 | resubcli 11471 |
. . . . . . . . 9
โข (((๐ด โโ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด โโ (i
ยทโ ๐ต)))) โ ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต))))) โ โ |
124 | 123 | recni 11177 |
. . . . . . . 8
โข (((๐ด โโ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด โโ (i
ยทโ ๐ต)))) โ ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต))))) โ โ |
125 | 22, 124 | mulcli 11170 |
. . . . . . 7
โข (i
ยท (((๐ด
โโ (i ยทโ ๐ต))
ยทih (๐โ(๐ด โโ (i
ยทโ ๐ต)))) โ ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต)))))) โ โ |
126 | 111, 125 | negsubi 11487 |
. . . . . 6
โข ((((๐ด +โ ๐ต)
ยทih (๐โ(๐ด +โ ๐ต))) โ ((๐ด โโ ๐ต)
ยทih (๐โ(๐ด โโ ๐ต)))) + -(i ยท (((๐ด โโ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด โโ (i
ยทโ ๐ต)))) โ ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต))))))) = ((((๐ด +โ ๐ต) ยทih (๐โ(๐ด +โ ๐ต))) โ ((๐ด โโ ๐ต)
ยทih (๐โ(๐ด โโ ๐ต)))) โ (i ยท
(((๐ด
โโ (i ยทโ ๐ต))
ยทih (๐โ(๐ด โโ (i
ยทโ ๐ต)))) โ ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต))))))) |
127 | 121, 126 | eqtr4i 2764 |
. . . . 5
โข
(โโ((((๐ด +โ ๐ต) ยทih (๐โ(๐ด +โ ๐ต))) โ ((๐ด โโ ๐ต)
ยทih (๐โ(๐ด โโ ๐ต)))) + (i ยท (((๐ด โโ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด โโ (i
ยทโ ๐ต)))) โ ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต)))))))) = ((((๐ด +โ ๐ต) ยทih (๐โ(๐ด +โ ๐ต))) โ ((๐ด โโ ๐ต)
ยทih (๐โ(๐ด โโ ๐ต)))) + -(i ยท (((๐ด โโ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด โโ (i
ยทโ ๐ต)))) โ ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต))))))) |
128 | 22, 113 | mulneg2i 11610 |
. . . . . . 7
โข (i
ยท -(((๐ด
โโ (i ยทโ ๐ต))
ยทih (๐โ(๐ด โโ (i
ยทโ ๐ต)))) โ ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต)))))) = -(i ยท (((๐ด โโ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด โโ (i
ยทโ ๐ต)))) โ ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต)))))) |
129 | 69, 95 | negsubdi2i 11495 |
. . . . . . . 8
โข -(((๐ด โโ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด โโ (i
ยทโ ๐ต)))) โ ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต))))) = (((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต)))) โ ((๐ด โโ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด โโ (i
ยทโ ๐ต))))) |
130 | 129 | oveq2i 7372 |
. . . . . . 7
โข (i
ยท -(((๐ด
โโ (i ยทโ ๐ต))
ยทih (๐โ(๐ด โโ (i
ยทโ ๐ต)))) โ ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต)))))) = (i ยท (((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต)))) โ ((๐ด โโ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด โโ (i
ยทโ ๐ต)))))) |
131 | 128, 130 | eqtr3i 2763 |
. . . . . 6
โข -(i
ยท (((๐ด
โโ (i ยทโ ๐ต))
ยทih (๐โ(๐ด โโ (i
ยทโ ๐ต)))) โ ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต)))))) = (i ยท (((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต)))) โ ((๐ด โโ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด โโ (i
ยทโ ๐ต)))))) |
132 | 131 | oveq2i 7372 |
. . . . 5
โข ((((๐ด +โ ๐ต)
ยทih (๐โ(๐ด +โ ๐ต))) โ ((๐ด โโ ๐ต)
ยทih (๐โ(๐ด โโ ๐ต)))) + -(i ยท (((๐ด โโ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด โโ (i
ยทโ ๐ต)))) โ ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต))))))) = ((((๐ด +โ ๐ต) ยทih (๐โ(๐ด +โ ๐ต))) โ ((๐ด โโ ๐ต)
ยทih (๐โ(๐ด โโ ๐ต)))) + (i ยท (((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต)))) โ ((๐ด โโ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด โโ (i
ยทโ ๐ต))))))) |
133 | 13 | oveq2i 7372 |
. . . . . . 7
โข ((๐ด +โ ๐ต)
ยทih (๐โ(๐ด +โ ๐ต))) = ((๐ด +โ ๐ต) ยทih
((๐โ๐ด) +โ (๐โ๐ต))) |
134 | 133, 19 | oveq12i 7373 |
. . . . . 6
โข (((๐ด +โ ๐ต)
ยทih (๐โ(๐ด +โ ๐ต))) โ ((๐ด โโ ๐ต)
ยทih (๐โ(๐ด โโ ๐ต)))) = (((๐ด +โ ๐ต) ยทih
((๐โ๐ด) +โ (๐โ๐ต))) โ ((๐ด โโ ๐ต)
ยทih ((๐โ๐ด) โโ (๐โ๐ต)))) |
135 | 3 | lnopaddmuli 30964 |
. . . . . . . . . 10
โข ((i
โ โ โง ๐ด
โ โ โง ๐ต
โ โ) โ (๐โ(๐ด +โ (i
ยทโ ๐ต))) = ((๐โ๐ด) +โ (i
ยทโ (๐โ๐ต)))) |
136 | 22, 2, 1, 135 | mp3an 1462 |
. . . . . . . . 9
โข (๐โ(๐ด +โ (i
ยทโ ๐ต))) = ((๐โ๐ด) +โ (i
ยทโ (๐โ๐ต))) |
137 | 136 | oveq2i 7372 |
. . . . . . . 8
โข ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต)))) = ((๐ด +โ (i
ยทโ ๐ต)) ยทih
((๐โ๐ด) +โ (i
ยทโ (๐โ๐ต)))) |
138 | 3 | lnopsubmuli 30966 |
. . . . . . . . . 10
โข ((i
โ โ โง ๐ด
โ โ โง ๐ต
โ โ) โ (๐โ(๐ด โโ (i
ยทโ ๐ต))) = ((๐โ๐ด) โโ (i
ยทโ (๐โ๐ต)))) |
139 | 22, 2, 1, 138 | mp3an 1462 |
. . . . . . . . 9
โข (๐โ(๐ด โโ (i
ยทโ ๐ต))) = ((๐โ๐ด) โโ (i
ยทโ (๐โ๐ต))) |
140 | 139 | oveq2i 7372 |
. . . . . . . 8
โข ((๐ด โโ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด โโ (i
ยทโ ๐ต)))) = ((๐ด โโ (i
ยทโ ๐ต)) ยทih
((๐โ๐ด) โโ (i
ยทโ (๐โ๐ต)))) |
141 | 137, 140 | oveq12i 7373 |
. . . . . . 7
โข (((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต)))) โ ((๐ด โโ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด โโ (i
ยทโ ๐ต))))) = (((๐ด +โ (i
ยทโ ๐ต)) ยทih
((๐โ๐ด) +โ (i
ยทโ (๐โ๐ต)))) โ ((๐ด โโ (i
ยทโ ๐ต)) ยทih
((๐โ๐ด) โโ (i
ยทโ (๐โ๐ต))))) |
142 | 141 | oveq2i 7372 |
. . . . . 6
โข (i
ยท (((๐ด
+โ (i ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต)))) โ ((๐ด โโ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด โโ (i
ยทโ ๐ต)))))) = (i ยท (((๐ด +โ (i
ยทโ ๐ต)) ยทih
((๐โ๐ด) +โ (i
ยทโ (๐โ๐ต)))) โ ((๐ด โโ (i
ยทโ ๐ต)) ยทih
((๐โ๐ด) โโ (i
ยทโ (๐โ๐ต)))))) |
143 | 134, 142 | oveq12i 7373 |
. . . . 5
โข ((((๐ด +โ ๐ต)
ยทih (๐โ(๐ด +โ ๐ต))) โ ((๐ด โโ ๐ต)
ยทih (๐โ(๐ด โโ ๐ต)))) + (i ยท (((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต)))) โ ((๐ด โโ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด โโ (i
ยทโ ๐ต))))))) = ((((๐ด +โ ๐ต) ยทih
((๐โ๐ด) +โ (๐โ๐ต))) โ ((๐ด โโ ๐ต)
ยทih ((๐โ๐ด) โโ (๐โ๐ต)))) + (i ยท (((๐ด +โ (i
ยทโ ๐ต)) ยทih
((๐โ๐ด) +โ (i
ยทโ (๐โ๐ต)))) โ ((๐ด โโ (i
ยทโ ๐ต)) ยทih
((๐โ๐ด) โโ (i
ยทโ (๐โ๐ต))))))) |
144 | 127, 132,
143 | 3eqtri 2765 |
. . . 4
โข
(โโ((((๐ด +โ ๐ต) ยทih (๐โ(๐ด +โ ๐ต))) โ ((๐ด โโ ๐ต)
ยทih (๐โ(๐ด โโ ๐ต)))) + (i ยท (((๐ด โโ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด โโ (i
ยทโ ๐ต)))) โ ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต)))))))) = ((((๐ด +โ ๐ต) ยทih
((๐โ๐ด) +โ (๐โ๐ต))) โ ((๐ด โโ ๐ต)
ยทih ((๐โ๐ด) โโ (๐โ๐ต)))) + (i ยท (((๐ด +โ (i
ยทโ ๐ต)) ยทih
((๐โ๐ด) +โ (i
ยทโ (๐โ๐ต)))) โ ((๐ด โโ (i
ยทโ ๐ต)) ยทih
((๐โ๐ด) โโ (i
ยทโ (๐โ๐ต))))))) |
145 | | cjre 15033 |
. . . . 5
โข (4 โ
โ โ (โโ4) = 4) |
146 | 116, 145 | ax-mp 5 |
. . . 4
โข
(โโ4) = 4 |
147 | 144, 146 | oveq12i 7373 |
. . 3
โข
((โโ((((๐ด +โ ๐ต) ยทih (๐โ(๐ด +โ ๐ต))) โ ((๐ด โโ ๐ต)
ยทih (๐โ(๐ด โโ ๐ต)))) + (i ยท (((๐ด โโ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด โโ (i
ยทโ ๐ต)))) โ ((๐ด +โ (i
ยทโ ๐ต)) ยทih
(๐โ(๐ด +โ (i
ยทโ ๐ต)))))))) / (โโ4)) = (((((๐ด +โ ๐ต)
ยทih ((๐โ๐ด) +โ (๐โ๐ต))) โ ((๐ด โโ ๐ต)
ยทih ((๐โ๐ด) โโ (๐โ๐ต)))) + (i ยท (((๐ด +โ (i
ยทโ ๐ต)) ยทih
((๐โ๐ด) +โ (i
ยทโ (๐โ๐ต)))) โ ((๐ด โโ (i
ยทโ ๐ต)) ยทih
((๐โ๐ด) โโ (i
ยทโ (๐โ๐ต))))))) / 4) |
148 | 104, 119,
147 | 3eqtrri 2766 |
. 2
โข
(((((๐ด
+โ ๐ต)
ยทih ((๐โ๐ด) +โ (๐โ๐ต))) โ ((๐ด โโ ๐ต)
ยทih ((๐โ๐ด) โโ (๐โ๐ต)))) + (i ยท (((๐ด +โ (i
ยทโ ๐ต)) ยทih
((๐โ๐ด) +โ (i
ยทโ (๐โ๐ต)))) โ ((๐ด โโ (i
ยทโ ๐ต)) ยทih
((๐โ๐ด) โโ (i
ยทโ (๐โ๐ต))))))) / 4) = (โโ(๐ต
ยทih (๐โ๐ด))) |
149 | 2, 8, 1, 6 | polid2i 30148 |
. 2
โข (๐ด
ยทih (๐โ๐ต)) = (((((๐ด +โ ๐ต) ยทih
((๐โ๐ด) +โ (๐โ๐ต))) โ ((๐ด โโ ๐ต)
ยทih ((๐โ๐ด) โโ (๐โ๐ต)))) + (i ยท (((๐ด +โ (i
ยทโ ๐ต)) ยทih
((๐โ๐ด) +โ (i
ยทโ (๐โ๐ต)))) โ ((๐ด โโ (i
ยทโ ๐ต)) ยทih
((๐โ๐ด) โโ (i
ยทโ (๐โ๐ต))))))) / 4) |
150 | 6, 1 | his1i 30091 |
. 2
โข ((๐โ๐ด) ยทih ๐ต) = (โโ(๐ต
ยทih (๐โ๐ด))) |
151 | 148, 149,
150 | 3eqtr4i 2771 |
1
โข (๐ด
ยทih (๐โ๐ต)) = ((๐โ๐ด) ยทih ๐ต) |