Step | Hyp | Ref
| Expression |
1 | | lawcoslem1.1 |
. . 3
โข (๐ โ ๐ โ โ) |
2 | | lawcoslem1.2 |
. . 3
โข (๐ โ ๐ โ โ) |
3 | | sqabssub 15227 |
. . 3
โข ((๐ โ โ โง ๐ โ โ) โ
((absโ(๐ โ
๐))โ2) =
((((absโ๐)โ2) +
((absโ๐)โ2))
โ (2 ยท (โโ(๐ ยท (โโ๐)))))) |
4 | 1, 2, 3 | syl2anc 583 |
. 2
โข (๐ โ ((absโ(๐ โ ๐))โ2) = ((((absโ๐)โ2) + ((absโ๐)โ2)) โ (2 ยท
(โโ(๐ ยท
(โโ๐)))))) |
5 | | lawcoslem1.4 |
. . . . . . . . 9
โข (๐ โ ๐ โ 0) |
6 | 1, 2, 5 | absdivd 15399 |
. . . . . . . 8
โข (๐ โ (absโ(๐ / ๐)) = ((absโ๐) / (absโ๐))) |
7 | 6 | oveq2d 7417 |
. . . . . . 7
โข (๐ โ ((โโ(๐ / ๐)) / (absโ(๐ / ๐))) = ((โโ(๐ / ๐)) / ((absโ๐) / (absโ๐)))) |
8 | 7 | oveq2d 7417 |
. . . . . 6
โข (๐ โ (((absโ๐) ยท (absโ๐)) ยท
((โโ(๐ / ๐)) / (absโ(๐ / ๐)))) = (((absโ๐) ยท (absโ๐)) ยท ((โโ(๐ / ๐)) / ((absโ๐) / (absโ๐))))) |
9 | 1 | abscld 15380 |
. . . . . . . . 9
โข (๐ โ (absโ๐) โ
โ) |
10 | 2 | abscld 15380 |
. . . . . . . . 9
โข (๐ โ (absโ๐) โ
โ) |
11 | 9, 10 | remulcld 11241 |
. . . . . . . 8
โข (๐ โ ((absโ๐) ยท (absโ๐)) โ
โ) |
12 | 11 | recnd 11239 |
. . . . . . 7
โข (๐ โ ((absโ๐) ยท (absโ๐)) โ
โ) |
13 | 1, 2, 5 | divcld 11987 |
. . . . . . . . 9
โข (๐ โ (๐ / ๐) โ โ) |
14 | 13 | recld 15138 |
. . . . . . . 8
โข (๐ โ (โโ(๐ / ๐)) โ โ) |
15 | 14 | recnd 11239 |
. . . . . . 7
โข (๐ โ (โโ(๐ / ๐)) โ โ) |
16 | 9 | recnd 11239 |
. . . . . . . 8
โข (๐ โ (absโ๐) โ
โ) |
17 | 10 | recnd 11239 |
. . . . . . . 8
โข (๐ โ (absโ๐) โ
โ) |
18 | 2, 5 | absne0d 15391 |
. . . . . . . 8
โข (๐ โ (absโ๐) โ 0) |
19 | 16, 17, 18 | divcld 11987 |
. . . . . . 7
โข (๐ โ ((absโ๐) / (absโ๐)) โ โ) |
20 | | lawcoslem1.3 |
. . . . . . . . 9
โข (๐ โ ๐ โ 0) |
21 | 1, 20 | absne0d 15391 |
. . . . . . . 8
โข (๐ โ (absโ๐) โ 0) |
22 | 16, 17, 21, 18 | divne0d 12003 |
. . . . . . 7
โข (๐ โ ((absโ๐) / (absโ๐)) โ 0) |
23 | 12, 15, 19, 22 | div12d 12023 |
. . . . . 6
โข (๐ โ (((absโ๐) ยท (absโ๐)) ยท
((โโ(๐ / ๐)) / ((absโ๐) / (absโ๐)))) = ((โโ(๐ / ๐)) ยท (((absโ๐) ยท (absโ๐)) / ((absโ๐) / (absโ๐))))) |
24 | 8, 23 | eqtrd 2764 |
. . . . 5
โข (๐ โ (((absโ๐) ยท (absโ๐)) ยท
((โโ(๐ / ๐)) / (absโ(๐ / ๐)))) = ((โโ(๐ / ๐)) ยท (((absโ๐) ยท (absโ๐)) / ((absโ๐) / (absโ๐))))) |
25 | 12, 16, 17, 21, 18 | divdiv2d 12019 |
. . . . . . 7
โข (๐ โ (((absโ๐) ยท (absโ๐)) / ((absโ๐) / (absโ๐))) = ((((absโ๐) ยท (absโ๐)) ยท (absโ๐)) / (absโ๐))) |
26 | 17 | sqvald 14105 |
. . . . . . . . . 10
โข (๐ โ ((absโ๐)โ2) = ((absโ๐) ยท (absโ๐))) |
27 | 26 | oveq1d 7416 |
. . . . . . . . 9
โข (๐ โ (((absโ๐)โ2) ยท
(absโ๐)) =
(((absโ๐) ยท
(absโ๐)) ยท
(absโ๐))) |
28 | 16, 17, 17 | mul31d 11422 |
. . . . . . . . 9
โข (๐ โ (((absโ๐) ยท (absโ๐)) ยท (absโ๐)) = (((absโ๐) ยท (absโ๐)) ยท (absโ๐))) |
29 | 27, 28 | eqtr4d 2767 |
. . . . . . . 8
โข (๐ โ (((absโ๐)โ2) ยท
(absโ๐)) =
(((absโ๐) ยท
(absโ๐)) ยท
(absโ๐))) |
30 | 29 | oveq1d 7416 |
. . . . . . 7
โข (๐ โ ((((absโ๐)โ2) ยท
(absโ๐)) /
(absโ๐)) =
((((absโ๐) ยท
(absโ๐)) ยท
(absโ๐)) /
(absโ๐))) |
31 | 17 | sqcld 14106 |
. . . . . . . 8
โข (๐ โ ((absโ๐)โ2) โ
โ) |
32 | 31, 16, 21 | divcan4d 11993 |
. . . . . . 7
โข (๐ โ ((((absโ๐)โ2) ยท
(absโ๐)) /
(absโ๐)) =
((absโ๐)โ2)) |
33 | 25, 30, 32 | 3eqtr2rd 2771 |
. . . . . 6
โข (๐ โ ((absโ๐)โ2) = (((absโ๐) ยท (absโ๐)) / ((absโ๐) / (absโ๐)))) |
34 | 33 | oveq2d 7417 |
. . . . 5
โข (๐ โ ((โโ(๐ / ๐)) ยท ((absโ๐)โ2)) = ((โโ(๐ / ๐)) ยท (((absโ๐) ยท (absโ๐)) / ((absโ๐) / (absโ๐))))) |
35 | 15, 31 | mulcomd 11232 |
. . . . . . 7
โข (๐ โ ((โโ(๐ / ๐)) ยท ((absโ๐)โ2)) = (((absโ๐)โ2) ยท (โโ(๐ / ๐)))) |
36 | 10 | resqcld 14087 |
. . . . . . . 8
โข (๐ โ ((absโ๐)โ2) โ
โ) |
37 | 36, 13 | remul2d 15171 |
. . . . . . 7
โข (๐ โ
(โโ(((absโ๐)โ2) ยท (๐ / ๐))) = (((absโ๐)โ2) ยท (โโ(๐ / ๐)))) |
38 | 35, 37 | eqtr4d 2767 |
. . . . . 6
โข (๐ โ ((โโ(๐ / ๐)) ยท ((absโ๐)โ2)) =
(โโ(((absโ๐)โ2) ยท (๐ / ๐)))) |
39 | 1, 31, 2, 5 | div12d 12023 |
. . . . . . . 8
โข (๐ โ (๐ ยท (((absโ๐)โ2) / ๐)) = (((absโ๐)โ2) ยท (๐ / ๐))) |
40 | 31, 2, 5 | divrecd 11990 |
. . . . . . . . . 10
โข (๐ โ (((absโ๐)โ2) / ๐) = (((absโ๐)โ2) ยท (1 / ๐))) |
41 | | recval 15266 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ 0) โ (1 / ๐) = ((โโ๐) / ((absโ๐)โ2))) |
42 | 2, 5, 41 | syl2anc 583 |
. . . . . . . . . . . 12
โข (๐ โ (1 / ๐) = ((โโ๐) / ((absโ๐)โ2))) |
43 | 42 | oveq2d 7417 |
. . . . . . . . . . 11
โข (๐ โ (((absโ๐)โ2) ยท (1 / ๐)) = (((absโ๐)โ2) ยท
((โโ๐) /
((absโ๐)โ2)))) |
44 | 2 | cjcld 15140 |
. . . . . . . . . . . 12
โข (๐ โ (โโ๐) โ
โ) |
45 | | sqne0 14085 |
. . . . . . . . . . . . . 14
โข
((absโ๐)
โ โ โ (((absโ๐)โ2) โ 0 โ (absโ๐) โ 0)) |
46 | 17, 45 | syl 17 |
. . . . . . . . . . . . 13
โข (๐ โ (((absโ๐)โ2) โ 0 โ
(absโ๐) โ
0)) |
47 | 18, 46 | mpbird 257 |
. . . . . . . . . . . 12
โข (๐ โ ((absโ๐)โ2) โ
0) |
48 | 44, 31, 47 | divcan2d 11989 |
. . . . . . . . . . 11
โข (๐ โ (((absโ๐)โ2) ยท
((โโ๐) /
((absโ๐)โ2))) =
(โโ๐)) |
49 | 43, 48 | eqtrd 2764 |
. . . . . . . . . 10
โข (๐ โ (((absโ๐)โ2) ยท (1 / ๐)) = (โโ๐)) |
50 | 40, 49 | eqtrd 2764 |
. . . . . . . . 9
โข (๐ โ (((absโ๐)โ2) / ๐) = (โโ๐)) |
51 | 50 | oveq2d 7417 |
. . . . . . . 8
โข (๐ โ (๐ ยท (((absโ๐)โ2) / ๐)) = (๐ ยท (โโ๐))) |
52 | 39, 51 | eqtr3d 2766 |
. . . . . . 7
โข (๐ โ (((absโ๐)โ2) ยท (๐ / ๐)) = (๐ ยท (โโ๐))) |
53 | 52 | fveq2d 6885 |
. . . . . 6
โข (๐ โ
(โโ(((absโ๐)โ2) ยท (๐ / ๐))) = (โโ(๐ ยท (โโ๐)))) |
54 | 38, 53 | eqtrd 2764 |
. . . . 5
โข (๐ โ ((โโ(๐ / ๐)) ยท ((absโ๐)โ2)) = (โโ(๐ ยท (โโ๐)))) |
55 | 24, 34, 54 | 3eqtr2rd 2771 |
. . . 4
โข (๐ โ (โโ(๐ ยท (โโ๐))) = (((absโ๐) ยท (absโ๐)) ยท
((โโ(๐ / ๐)) / (absโ(๐ / ๐))))) |
56 | 55 | oveq2d 7417 |
. . 3
โข (๐ โ (2 ยท
(โโ(๐ ยท
(โโ๐)))) = (2
ยท (((absโ๐)
ยท (absโ๐))
ยท ((โโ(๐
/ ๐)) / (absโ(๐ / ๐)))))) |
57 | 56 | oveq2d 7417 |
. 2
โข (๐ โ ((((absโ๐)โ2) + ((absโ๐)โ2)) โ (2 ยท
(โโ(๐ ยท
(โโ๐))))) =
((((absโ๐)โ2) +
((absโ๐)โ2))
โ (2 ยท (((absโ๐) ยท (absโ๐)) ยท ((โโ(๐ / ๐)) / (absโ(๐ / ๐))))))) |
58 | 4, 57 | eqtrd 2764 |
1
โข (๐ โ ((absโ(๐ โ ๐))โ2) = ((((absโ๐)โ2) + ((absโ๐)โ2)) โ (2 ยท
(((absโ๐) ยท
(absโ๐)) ยท
((โโ(๐ / ๐)) / (absโ(๐ / ๐))))))) |