Step | Hyp | Ref
| Expression |
1 | | crrecz.1 |
. . . . . . . 8
โข ๐ด โ โ |
2 | 1 | recni 11177 |
. . . . . . 7
โข ๐ด โ โ |
3 | 2 | sqcli 14094 |
. . . . . 6
โข (๐ดโ2) โ
โ |
4 | | ax-icn 11118 |
. . . . . . . 8
โข i โ
โ |
5 | | crrecz.2 |
. . . . . . . . 9
โข ๐ต โ โ |
6 | 5 | recni 11177 |
. . . . . . . 8
โข ๐ต โ โ |
7 | 4, 6 | mulcli 11170 |
. . . . . . 7
โข (i
ยท ๐ต) โ
โ |
8 | 7 | sqcli 14094 |
. . . . . 6
โข ((i
ยท ๐ต)โ2) โ
โ |
9 | 3, 8 | negsubi 11487 |
. . . . 5
โข ((๐ดโ2) + -((i ยท ๐ต)โ2)) = ((๐ดโ2) โ ((i ยท ๐ต)โ2)) |
10 | 4, 6 | sqmuli 14097 |
. . . . . . . . 9
โข ((i
ยท ๐ต)โ2) =
((iโ2) ยท (๐ตโ2)) |
11 | | i2 14115 |
. . . . . . . . . 10
โข
(iโ2) = -1 |
12 | 11 | oveq1i 7371 |
. . . . . . . . 9
โข
((iโ2) ยท (๐ตโ2)) = (-1 ยท (๐ตโ2)) |
13 | | ax-1cn 11117 |
. . . . . . . . . 10
โข 1 โ
โ |
14 | 6 | sqcli 14094 |
. . . . . . . . . 10
โข (๐ตโ2) โ
โ |
15 | 13, 14 | mulneg1i 11609 |
. . . . . . . . 9
โข (-1
ยท (๐ตโ2)) = -(1
ยท (๐ตโ2)) |
16 | 10, 12, 15 | 3eqtri 2765 |
. . . . . . . 8
โข ((i
ยท ๐ต)โ2) = -(1
ยท (๐ตโ2)) |
17 | 16 | negeqi 11402 |
. . . . . . 7
โข -((i
ยท ๐ต)โ2) = --(1
ยท (๐ตโ2)) |
18 | 13, 14 | mulcli 11170 |
. . . . . . . 8
โข (1
ยท (๐ตโ2)) โ
โ |
19 | 18 | negnegi 11479 |
. . . . . . 7
โข --(1
ยท (๐ตโ2)) = (1
ยท (๐ตโ2)) |
20 | 14 | mulid2i 11168 |
. . . . . . 7
โข (1
ยท (๐ตโ2)) =
(๐ตโ2) |
21 | 17, 19, 20 | 3eqtri 2765 |
. . . . . 6
โข -((i
ยท ๐ต)โ2) =
(๐ตโ2) |
22 | 21 | oveq2i 7372 |
. . . . 5
โข ((๐ดโ2) + -((i ยท ๐ต)โ2)) = ((๐ดโ2) + (๐ตโ2)) |
23 | 2, 7 | subsqi 14126 |
. . . . 5
โข ((๐ดโ2) โ ((i ยท
๐ต)โ2)) = ((๐ด + (i ยท ๐ต)) ยท (๐ด โ (i ยท ๐ต))) |
24 | 9, 22, 23 | 3eqtr3ri 2770 |
. . . 4
โข ((๐ด + (i ยท ๐ต)) ยท (๐ด โ (i ยท ๐ต))) = ((๐ดโ2) + (๐ตโ2)) |
25 | 24 | oveq1i 7371 |
. . 3
โข (((๐ด + (i ยท ๐ต)) ยท (๐ด โ (i ยท ๐ต))) / ((๐ดโ2) + (๐ตโ2))) = (((๐ดโ2) + (๐ตโ2)) / ((๐ดโ2) + (๐ตโ2))) |
26 | | neorian 3036 |
. . . . 5
โข ((๐ด โ 0 โจ ๐ต โ 0) โ ยฌ (๐ด = 0 โง ๐ต = 0)) |
27 | | sumsqeq0 14092 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด = 0 โง ๐ต = 0) โ ((๐ดโ2) + (๐ตโ2)) = 0)) |
28 | 1, 5, 27 | mp2an 691 |
. . . . . 6
โข ((๐ด = 0 โง ๐ต = 0) โ ((๐ดโ2) + (๐ตโ2)) = 0) |
29 | 28 | necon3bbii 2988 |
. . . . 5
โข (ยฌ
(๐ด = 0 โง ๐ต = 0) โ ((๐ดโ2) + (๐ตโ2)) โ 0) |
30 | 26, 29 | bitri 275 |
. . . 4
โข ((๐ด โ 0 โจ ๐ต โ 0) โ ((๐ดโ2) + (๐ตโ2)) โ 0) |
31 | 2, 7 | addcli 11169 |
. . . . 5
โข (๐ด + (i ยท ๐ต)) โ โ |
32 | 2, 7 | subcli 11485 |
. . . . 5
โข (๐ด โ (i ยท ๐ต)) โ
โ |
33 | 3, 14 | addcli 11169 |
. . . . 5
โข ((๐ดโ2) + (๐ตโ2)) โ โ |
34 | 31, 32, 33 | divasszi 11913 |
. . . 4
โข (((๐ดโ2) + (๐ตโ2)) โ 0 โ (((๐ด + (i ยท ๐ต)) ยท (๐ด โ (i ยท ๐ต))) / ((๐ดโ2) + (๐ตโ2))) = ((๐ด + (i ยท ๐ต)) ยท ((๐ด โ (i ยท ๐ต)) / ((๐ดโ2) + (๐ตโ2))))) |
35 | 30, 34 | sylbi 216 |
. . 3
โข ((๐ด โ 0 โจ ๐ต โ 0) โ (((๐ด + (i ยท ๐ต)) ยท (๐ด โ (i ยท ๐ต))) / ((๐ดโ2) + (๐ตโ2))) = ((๐ด + (i ยท ๐ต)) ยท ((๐ด โ (i ยท ๐ต)) / ((๐ดโ2) + (๐ตโ2))))) |
36 | | divid 11850 |
. . . . 5
โข ((((๐ดโ2) + (๐ตโ2)) โ โ โง ((๐ดโ2) + (๐ตโ2)) โ 0) โ (((๐ดโ2) + (๐ตโ2)) / ((๐ดโ2) + (๐ตโ2))) = 1) |
37 | 33, 36 | mpan 689 |
. . . 4
โข (((๐ดโ2) + (๐ตโ2)) โ 0 โ (((๐ดโ2) + (๐ตโ2)) / ((๐ดโ2) + (๐ตโ2))) = 1) |
38 | 30, 37 | sylbi 216 |
. . 3
โข ((๐ด โ 0 โจ ๐ต โ 0) โ (((๐ดโ2) + (๐ตโ2)) / ((๐ดโ2) + (๐ตโ2))) = 1) |
39 | 25, 35, 38 | 3eqtr3a 2797 |
. 2
โข ((๐ด โ 0 โจ ๐ต โ 0) โ ((๐ด + (i ยท ๐ต)) ยท ((๐ด โ (i ยท ๐ต)) / ((๐ดโ2) + (๐ตโ2)))) = 1) |
40 | 32, 33 | divclzi 11898 |
. . . 4
โข (((๐ดโ2) + (๐ตโ2)) โ 0 โ ((๐ด โ (i ยท ๐ต)) / ((๐ดโ2) + (๐ตโ2))) โ โ) |
41 | 30, 40 | sylbi 216 |
. . 3
โข ((๐ด โ 0 โจ ๐ต โ 0) โ ((๐ด โ (i ยท ๐ต)) / ((๐ดโ2) + (๐ตโ2))) โ โ) |
42 | 31 | a1i 11 |
. . 3
โข ((๐ด โ 0 โจ ๐ต โ 0) โ (๐ด + (i ยท ๐ต)) โ โ) |
43 | | crne0 12154 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด โ 0 โจ ๐ต โ 0) โ (๐ด + (i ยท ๐ต)) โ 0)) |
44 | 1, 5, 43 | mp2an 691 |
. . . 4
โข ((๐ด โ 0 โจ ๐ต โ 0) โ (๐ด + (i ยท ๐ต)) โ 0) |
45 | 44 | biimpi 215 |
. . 3
โข ((๐ด โ 0 โจ ๐ต โ 0) โ (๐ด + (i ยท ๐ต)) โ 0) |
46 | | divmul 11824 |
. . . 4
โข ((1
โ โ โง ((๐ด
โ (i ยท ๐ต)) /
((๐ดโ2) + (๐ตโ2))) โ โ โง
((๐ด + (i ยท ๐ต)) โ โ โง (๐ด + (i ยท ๐ต)) โ 0)) โ ((1 / (๐ด + (i ยท ๐ต))) = ((๐ด โ (i ยท ๐ต)) / ((๐ดโ2) + (๐ตโ2))) โ ((๐ด + (i ยท ๐ต)) ยท ((๐ด โ (i ยท ๐ต)) / ((๐ดโ2) + (๐ตโ2)))) = 1)) |
47 | 13, 46 | mp3an1 1449 |
. . 3
โข ((((๐ด โ (i ยท ๐ต)) / ((๐ดโ2) + (๐ตโ2))) โ โ โง ((๐ด + (i ยท ๐ต)) โ โ โง (๐ด + (i ยท ๐ต)) โ 0)) โ ((1 / (๐ด + (i ยท ๐ต))) = ((๐ด โ (i ยท ๐ต)) / ((๐ดโ2) + (๐ตโ2))) โ ((๐ด + (i ยท ๐ต)) ยท ((๐ด โ (i ยท ๐ต)) / ((๐ดโ2) + (๐ตโ2)))) = 1)) |
48 | 41, 42, 45, 47 | syl12anc 836 |
. 2
โข ((๐ด โ 0 โจ ๐ต โ 0) โ ((1 / (๐ด + (i ยท ๐ต))) = ((๐ด โ (i ยท ๐ต)) / ((๐ดโ2) + (๐ตโ2))) โ ((๐ด + (i ยท ๐ต)) ยท ((๐ด โ (i ยท ๐ต)) / ((๐ดโ2) + (๐ตโ2)))) = 1)) |
49 | 39, 48 | mpbird 257 |
1
โข ((๐ด โ 0 โจ ๐ต โ 0) โ (1 / (๐ด + (i ยท ๐ต))) = ((๐ด โ (i ยท ๐ต)) / ((๐ดโ2) + (๐ตโ2)))) |