Step | Hyp | Ref
| Expression |
1 | | absval2 11065 |
. . . . . . 7
โข (๐ด โ โ โ
(absโ๐ด) =
(โโ(((โโ๐ด)โ2) + ((โโ๐ด)โ2)))) |
2 | | absval2 11065 |
. . . . . . 7
โข (๐ต โ โ โ
(absโ๐ต) =
(โโ(((โโ๐ต)โ2) + ((โโ๐ต)โ2)))) |
3 | 1, 2 | breqan12d 4019 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ
((absโ๐ด) #
(absโ๐ต) โ
(โโ(((โโ๐ด)โ2) + ((โโ๐ด)โ2))) #
(โโ(((โโ๐ต)โ2) + ((โโ๐ต)โ2))))) |
4 | | simpl 109 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ด โ
โ) |
5 | 4 | recld 10946 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ๐ด) โ
โ) |
6 | 5 | resqcld 10679 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ๐ด)โ2)
โ โ) |
7 | 4 | imcld 10947 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ๐ด) โ
โ) |
8 | 7 | resqcld 10679 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ๐ด)โ2)
โ โ) |
9 | 6, 8 | readdcld 7986 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ
(((โโ๐ด)โ2)
+ ((โโ๐ด)โ2)) โ โ) |
10 | 5 | sqge0d 10680 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ 0 โค
((โโ๐ด)โ2)) |
11 | 7 | sqge0d 10680 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ 0 โค
((โโ๐ด)โ2)) |
12 | 6, 8, 10, 11 | addge0d 8478 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ 0 โค
(((โโ๐ด)โ2)
+ ((โโ๐ด)โ2))) |
13 | | simpr 110 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ต โ
โ) |
14 | 13 | recld 10946 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ๐ต) โ
โ) |
15 | 14 | resqcld 10679 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ๐ต)โ2)
โ โ) |
16 | 13 | imcld 10947 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ๐ต) โ
โ) |
17 | 16 | resqcld 10679 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ๐ต)โ2)
โ โ) |
18 | 15, 17 | readdcld 7986 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ
(((โโ๐ต)โ2)
+ ((โโ๐ต)โ2)) โ โ) |
19 | 14 | sqge0d 10680 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ 0 โค
((โโ๐ต)โ2)) |
20 | 16 | sqge0d 10680 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ 0 โค
((โโ๐ต)โ2)) |
21 | 15, 17, 19, 20 | addge0d 8478 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ 0 โค
(((โโ๐ต)โ2)
+ ((โโ๐ต)โ2))) |
22 | | sqrt11ap 11046 |
. . . . . . 7
โข
((((((โโ๐ด)โ2) + ((โโ๐ด)โ2)) โ โ โง
0 โค (((โโ๐ด)โ2) + ((โโ๐ด)โ2))) โง
((((โโ๐ต)โ2)
+ ((โโ๐ต)โ2)) โ โ โง 0 โค
(((โโ๐ต)โ2)
+ ((โโ๐ต)โ2)))) โ
((โโ(((โโ๐ด)โ2) + ((โโ๐ด)โ2))) #
(โโ(((โโ๐ต)โ2) + ((โโ๐ต)โ2))) โ
(((โโ๐ด)โ2)
+ ((โโ๐ด)โ2)) # (((โโ๐ต)โ2) +
((โโ๐ต)โ2)))) |
23 | 9, 12, 18, 21, 22 | syl22anc 1239 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ(((โโ๐ด)โ2) + ((โโ๐ด)โ2))) #
(โโ(((โโ๐ต)โ2) + ((โโ๐ต)โ2))) โ
(((โโ๐ด)โ2)
+ ((โโ๐ด)โ2)) # (((โโ๐ต)โ2) +
((โโ๐ต)โ2)))) |
24 | 3, 23 | bitrd 188 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ
((absโ๐ด) #
(absโ๐ต) โ
(((โโ๐ด)โ2)
+ ((โโ๐ด)โ2)) # (((โโ๐ต)โ2) +
((โโ๐ต)โ2)))) |
25 | 6 | recnd 7985 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ๐ด)โ2)
โ โ) |
26 | 8 | recnd 7985 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ๐ด)โ2)
โ โ) |
27 | 15 | recnd 7985 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ๐ต)โ2)
โ โ) |
28 | 17 | recnd 7985 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ๐ต)โ2)
โ โ) |
29 | | addext 8566 |
. . . . . 6
โข
(((((โโ๐ด)โ2) โ โ โง
((โโ๐ด)โ2)
โ โ) โง (((โโ๐ต)โ2) โ โ โง
((โโ๐ต)โ2)
โ โ)) โ ((((โโ๐ด)โ2) + ((โโ๐ด)โ2)) #
(((โโ๐ต)โ2)
+ ((โโ๐ต)โ2)) โ (((โโ๐ด)โ2) # ((โโ๐ต)โ2) โจ
((โโ๐ด)โ2)
# ((โโ๐ต)โ2)))) |
30 | 25, 26, 27, 28, 29 | syl22anc 1239 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ
((((โโ๐ด)โ2)
+ ((โโ๐ด)โ2)) # (((โโ๐ต)โ2) +
((โโ๐ต)โ2))
โ (((โโ๐ด)โ2) # ((โโ๐ต)โ2) โจ ((โโ๐ด)โ2) #
((โโ๐ต)โ2)))) |
31 | 24, 30 | sylbid 150 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ
((absโ๐ด) #
(absโ๐ต) โ
(((โโ๐ด)โ2)
# ((โโ๐ต)โ2)
โจ ((โโ๐ด)โ2) # ((โโ๐ต)โ2)))) |
32 | 5 | recnd 7985 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ๐ด) โ
โ) |
33 | 32 | sqvald 10650 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ๐ด)โ2) =
((โโ๐ด) ยท
(โโ๐ด))) |
34 | 14 | recnd 7985 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ๐ต) โ
โ) |
35 | 34 | sqvald 10650 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ๐ต)โ2) =
((โโ๐ต) ยท
(โโ๐ต))) |
36 | 33, 35 | breq12d 4016 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ
(((โโ๐ด)โ2)
# ((โโ๐ต)โ2)
โ ((โโ๐ด)
ยท (โโ๐ด))
# ((โโ๐ต)
ยท (โโ๐ต)))) |
37 | | mulext 8570 |
. . . . . . . 8
โข
((((โโ๐ด)
โ โ โง (โโ๐ด) โ โ) โง ((โโ๐ต) โ โ โง
(โโ๐ต) โ
โ)) โ (((โโ๐ด) ยท (โโ๐ด)) # ((โโ๐ต) ยท (โโ๐ต)) โ ((โโ๐ด) # (โโ๐ต) โจ (โโ๐ด) # (โโ๐ต)))) |
38 | 32, 32, 34, 34, 37 | syl22anc 1239 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ
(((โโ๐ด) ยท
(โโ๐ด)) #
((โโ๐ต) ยท
(โโ๐ต)) โ
((โโ๐ด) #
(โโ๐ต) โจ
(โโ๐ด) #
(โโ๐ต)))) |
39 | 36, 38 | sylbid 150 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ
(((โโ๐ด)โ2)
# ((โโ๐ต)โ2)
โ ((โโ๐ด) #
(โโ๐ต) โจ
(โโ๐ด) #
(โโ๐ต)))) |
40 | | oridm 757 |
. . . . . 6
โข
(((โโ๐ด) #
(โโ๐ต) โจ
(โโ๐ด) #
(โโ๐ต)) โ
(โโ๐ด) #
(โโ๐ต)) |
41 | 39, 40 | imbitrdi 161 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ
(((โโ๐ด)โ2)
# ((โโ๐ต)โ2)
โ (โโ๐ด) #
(โโ๐ต))) |
42 | 7 | recnd 7985 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ๐ด) โ
โ) |
43 | 42 | sqvald 10650 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ๐ด)โ2)
= ((โโ๐ด)
ยท (โโ๐ด))) |
44 | 16 | recnd 7985 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โโ๐ต) โ
โ) |
45 | 44 | sqvald 10650 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ
((โโ๐ต)โ2)
= ((โโ๐ต)
ยท (โโ๐ต))) |
46 | 43, 45 | breq12d 4016 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ
(((โโ๐ด)โ2)
# ((โโ๐ต)โ2) โ ((โโ๐ด) ยท (โโ๐ด)) # ((โโ๐ต) ยท (โโ๐ต)))) |
47 | | mulext 8570 |
. . . . . . . 8
โข
((((โโ๐ด)
โ โ โง (โโ๐ด) โ โ) โง
((โโ๐ต) โ
โ โง (โโ๐ต) โ โ)) โ
(((โโ๐ด)
ยท (โโ๐ด))
# ((โโ๐ต)
ยท (โโ๐ต))
โ ((โโ๐ด) #
(โโ๐ต) โจ
(โโ๐ด) #
(โโ๐ต)))) |
48 | 42, 42, 44, 44, 47 | syl22anc 1239 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ
(((โโ๐ด)
ยท (โโ๐ด))
# ((โโ๐ต)
ยท (โโ๐ต))
โ ((โโ๐ด) #
(โโ๐ต) โจ
(โโ๐ด) #
(โโ๐ต)))) |
49 | 46, 48 | sylbid 150 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ
(((โโ๐ด)โ2)
# ((โโ๐ต)โ2) โ ((โโ๐ด) # (โโ๐ต) โจ (โโ๐ด) # (โโ๐ต)))) |
50 | | oridm 757 |
. . . . . 6
โข
(((โโ๐ด)
# (โโ๐ต) โจ
(โโ๐ด) #
(โโ๐ต)) โ
(โโ๐ด) #
(โโ๐ต)) |
51 | 49, 50 | imbitrdi 161 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ
(((โโ๐ด)โ2)
# ((โโ๐ต)โ2) โ (โโ๐ด) # (โโ๐ต))) |
52 | 41, 51 | orim12d 786 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ
((((โโ๐ด)โ2)
# ((โโ๐ต)โ2)
โจ ((โโ๐ด)โ2) # ((โโ๐ต)โ2)) โ
((โโ๐ด) #
(โโ๐ต) โจ
(โโ๐ด) #
(โโ๐ต)))) |
53 | 31, 52 | syld 45 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ
((absโ๐ด) #
(absโ๐ต) โ
((โโ๐ด) #
(โโ๐ต) โจ
(โโ๐ด) #
(โโ๐ต)))) |
54 | | apreim 8559 |
. . . 4
โข
((((โโ๐ด)
โ โ โง (โโ๐ด) โ โ) โง ((โโ๐ต) โ โ โง
(โโ๐ต) โ
โ)) โ (((โโ๐ด) + (i ยท (โโ๐ด))) # ((โโ๐ต) + (i ยท
(โโ๐ต))) โ
((โโ๐ด) #
(โโ๐ต) โจ
(โโ๐ด) #
(โโ๐ต)))) |
55 | 5, 7, 14, 16, 54 | syl22anc 1239 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ
(((โโ๐ด) + (i
ยท (โโ๐ด))) # ((โโ๐ต) + (i ยท (โโ๐ต))) โ ((โโ๐ด) # (โโ๐ต) โจ (โโ๐ด) # (โโ๐ต)))) |
56 | 53, 55 | sylibrd 169 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ
((absโ๐ด) #
(absโ๐ต) โ
((โโ๐ด) + (i
ยท (โโ๐ด))) # ((โโ๐ต) + (i ยท (โโ๐ต))))) |
57 | 4 | replimd 10949 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ด = ((โโ๐ด) + (i ยท
(โโ๐ด)))) |
58 | 13 | replimd 10949 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ต = ((โโ๐ต) + (i ยท
(โโ๐ต)))) |
59 | 57, 58 | breq12d 4016 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด # ๐ต โ ((โโ๐ด) + (i ยท (โโ๐ด))) # ((โโ๐ต) + (i ยท
(โโ๐ต))))) |
60 | 56, 59 | sylibrd 169 |
1
โข ((๐ด โ โ โง ๐ต โ โ) โ
((absโ๐ด) #
(absโ๐ต) โ ๐ด # ๐ต)) |