Step | Hyp | Ref
| Expression |
1 | | absval2 11065 |
. . . . . . . . . 10
โข (๐ด โ โ โ
(absโ๐ด) =
(โโ(((โโ๐ด)โ2) + ((โโ๐ด)โ2)))) |
2 | 1 | breq1d 4013 |
. . . . . . . . 9
โข (๐ด โ โ โ
((absโ๐ด) # 0 โ
(โโ(((โโ๐ด)โ2) + ((โโ๐ด)โ2))) #
0)) |
3 | | sqrt0 11012 |
. . . . . . . . . 10
โข
(โโ0) = 0 |
4 | 3 | breq2i 4011 |
. . . . . . . . 9
โข
((โโ(((โโ๐ด)โ2) + ((โโ๐ด)โ2))) # (โโ0)
โ (โโ(((โโ๐ด)โ2) + ((โโ๐ด)โ2))) #
0) |
5 | 2, 4 | bitr4di 198 |
. . . . . . . 8
โข (๐ด โ โ โ
((absโ๐ด) # 0 โ
(โโ(((โโ๐ด)โ2) + ((โโ๐ด)โ2))) #
(โโ0))) |
6 | | recl 10861 |
. . . . . . . . . . 11
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
7 | 6 | resqcld 10679 |
. . . . . . . . . 10
โข (๐ด โ โ โ
((โโ๐ด)โ2)
โ โ) |
8 | | imcl 10862 |
. . . . . . . . . . 11
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
9 | 8 | resqcld 10679 |
. . . . . . . . . 10
โข (๐ด โ โ โ
((โโ๐ด)โ2)
โ โ) |
10 | 7, 9 | readdcld 7986 |
. . . . . . . . 9
โข (๐ด โ โ โ
(((โโ๐ด)โ2)
+ ((โโ๐ด)โ2)) โ โ) |
11 | 6 | sqge0d 10680 |
. . . . . . . . . 10
โข (๐ด โ โ โ 0 โค
((โโ๐ด)โ2)) |
12 | 8 | sqge0d 10680 |
. . . . . . . . . 10
โข (๐ด โ โ โ 0 โค
((โโ๐ด)โ2)) |
13 | 7, 9, 11, 12 | addge0d 8478 |
. . . . . . . . 9
โข (๐ด โ โ โ 0 โค
(((โโ๐ด)โ2)
+ ((โโ๐ด)โ2))) |
14 | | 0red 7957 |
. . . . . . . . 9
โข (๐ด โ โ โ 0 โ
โ) |
15 | 14 | leidd 8470 |
. . . . . . . . 9
โข (๐ด โ โ โ 0 โค
0) |
16 | | sqrt11ap 11046 |
. . . . . . . . 9
โข
((((((โโ๐ด)โ2) + ((โโ๐ด)โ2)) โ โ โง
0 โค (((โโ๐ด)โ2) + ((โโ๐ด)โ2))) โง (0 โ
โ โง 0 โค 0)) โ ((โโ(((โโ๐ด)โ2) +
((โโ๐ด)โ2))) # (โโ0) โ
(((โโ๐ด)โ2)
+ ((โโ๐ด)โ2)) # 0)) |
17 | 10, 13, 14, 15, 16 | syl22anc 1239 |
. . . . . . . 8
โข (๐ด โ โ โ
((โโ(((โโ๐ด)โ2) + ((โโ๐ด)โ2))) # (โโ0)
โ (((โโ๐ด)โ2) + ((โโ๐ด)โ2)) #
0)) |
18 | 5, 17 | bitrd 188 |
. . . . . . 7
โข (๐ด โ โ โ
((absโ๐ด) # 0 โ
(((โโ๐ด)โ2)
+ ((โโ๐ด)โ2)) # 0)) |
19 | | 00id 8097 |
. . . . . . . 8
โข (0 + 0) =
0 |
20 | 19 | breq2i 4011 |
. . . . . . 7
โข
((((โโ๐ด)โ2) + ((โโ๐ด)โ2)) # (0 + 0) โ
(((โโ๐ด)โ2)
+ ((โโ๐ด)โ2)) # 0) |
21 | 18, 20 | bitr4di 198 |
. . . . . 6
โข (๐ด โ โ โ
((absโ๐ด) # 0 โ
(((โโ๐ด)โ2)
+ ((โโ๐ด)โ2)) # (0 + 0))) |
22 | 7 | recnd 7985 |
. . . . . . 7
โข (๐ด โ โ โ
((โโ๐ด)โ2)
โ โ) |
23 | 9 | recnd 7985 |
. . . . . . 7
โข (๐ด โ โ โ
((โโ๐ด)โ2)
โ โ) |
24 | | 0cnd 7949 |
. . . . . . 7
โข (๐ด โ โ โ 0 โ
โ) |
25 | | addext 8566 |
. . . . . . 7
โข
(((((โโ๐ด)โ2) โ โ โง
((โโ๐ด)โ2)
โ โ) โง (0 โ โ โง 0 โ โ)) โ
((((โโ๐ด)โ2)
+ ((โโ๐ด)โ2)) # (0 + 0) โ
(((โโ๐ด)โ2)
# 0 โจ ((โโ๐ด)โ2) # 0))) |
26 | 22, 23, 24, 24, 25 | syl22anc 1239 |
. . . . . 6
โข (๐ด โ โ โ
((((โโ๐ด)โ2)
+ ((โโ๐ด)โ2)) # (0 + 0) โ
(((โโ๐ด)โ2)
# 0 โจ ((โโ๐ด)โ2) # 0))) |
27 | 21, 26 | sylbid 150 |
. . . . 5
โข (๐ด โ โ โ
((absโ๐ด) # 0 โ
(((โโ๐ด)โ2)
# 0 โจ ((โโ๐ด)โ2) # 0))) |
28 | 6 | recnd 7985 |
. . . . . . 7
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
29 | | 2nn 9079 |
. . . . . . 7
โข 2 โ
โ |
30 | | expap0 10549 |
. . . . . . 7
โข
(((โโ๐ด)
โ โ โง 2 โ โ) โ (((โโ๐ด)โ2) # 0 โ (โโ๐ด) # 0)) |
31 | 28, 29, 30 | sylancl 413 |
. . . . . 6
โข (๐ด โ โ โ
(((โโ๐ด)โ2)
# 0 โ (โโ๐ด)
# 0)) |
32 | 8 | recnd 7985 |
. . . . . . 7
โข (๐ด โ โ โ
(โโ๐ด) โ
โ) |
33 | | expap0 10549 |
. . . . . . 7
โข
(((โโ๐ด)
โ โ โง 2 โ โ) โ (((โโ๐ด)โ2) # 0 โ
(โโ๐ด) #
0)) |
34 | 32, 29, 33 | sylancl 413 |
. . . . . 6
โข (๐ด โ โ โ
(((โโ๐ด)โ2)
# 0 โ (โโ๐ด) # 0)) |
35 | 31, 34 | orbi12d 793 |
. . . . 5
โข (๐ด โ โ โ
((((โโ๐ด)โ2)
# 0 โจ ((โโ๐ด)โ2) # 0) โ ((โโ๐ด) # 0 โจ (โโ๐ด) # 0))) |
36 | 27, 35 | sylibd 149 |
. . . 4
โข (๐ด โ โ โ
((absโ๐ด) # 0 โ
((โโ๐ด) # 0 โจ
(โโ๐ด) #
0))) |
37 | | crap0 8914 |
. . . . 5
โข
(((โโ๐ด)
โ โ โง (โโ๐ด) โ โ) โ
(((โโ๐ด) # 0 โจ
(โโ๐ด) # 0)
โ ((โโ๐ด) +
(i ยท (โโ๐ด))) # 0)) |
38 | 6, 8, 37 | syl2anc 411 |
. . . 4
โข (๐ด โ โ โ
(((โโ๐ด) # 0 โจ
(โโ๐ด) # 0)
โ ((โโ๐ด) +
(i ยท (โโ๐ด))) # 0)) |
39 | 36, 38 | sylibd 149 |
. . 3
โข (๐ด โ โ โ
((absโ๐ด) # 0 โ
((โโ๐ด) + (i
ยท (โโ๐ด))) # 0)) |
40 | | replim 10867 |
. . . 4
โข (๐ด โ โ โ ๐ด = ((โโ๐ด) + (i ยท
(โโ๐ด)))) |
41 | 40 | breq1d 4013 |
. . 3
โข (๐ด โ โ โ (๐ด # 0 โ ((โโ๐ด) + (i ยท
(โโ๐ด))) #
0)) |
42 | 39, 41 | sylibrd 169 |
. 2
โข (๐ด โ โ โ
((absโ๐ด) # 0 โ
๐ด # 0)) |
43 | | absrpclap 11069 |
. . . 4
โข ((๐ด โ โ โง ๐ด # 0) โ (absโ๐ด) โ
โ+) |
44 | 43 | rpap0d 9701 |
. . 3
โข ((๐ด โ โ โง ๐ด # 0) โ (absโ๐ด) # 0) |
45 | 44 | ex 115 |
. 2
โข (๐ด โ โ โ (๐ด # 0 โ (absโ๐ด) # 0)) |
46 | 42, 45 | impbid 129 |
1
โข (๐ด โ โ โ
((absโ๐ด) # 0 โ
๐ด # 0)) |