Step | Hyp | Ref
| Expression |
1 | | normlem1.1 |
. . . . . 6
โข ๐ โ โ |
2 | | normlem1.2 |
. . . . . 6
โข ๐น โ โ |
3 | | normlem1.3 |
. . . . . 6
โข ๐บ โ โ |
4 | | eqid 2733 |
. . . . . 6
โข
-(((โโ๐) ยท (๐น ยทih ๐บ)) + (๐ ยท (๐บ ยทih ๐น))) = -(((โโ๐) ยท (๐น ยทih ๐บ)) + (๐ ยท (๐บ ยทih ๐น))) |
5 | 1, 2, 3, 4 | normlem2 30102 |
. . . . 5
โข
-(((โโ๐) ยท (๐น ยทih ๐บ)) + (๐ ยท (๐บ ยทih ๐น))) โ
โ |
6 | 1 | cjcli 15063 |
. . . . . . . 8
โข
(โโ๐)
โ โ |
7 | 2, 3 | hicli 30072 |
. . . . . . . 8
โข (๐น
ยทih ๐บ) โ โ |
8 | 6, 7 | mulcli 11170 |
. . . . . . 7
โข
((โโ๐)
ยท (๐น
ยทih ๐บ)) โ โ |
9 | 3, 2 | hicli 30072 |
. . . . . . . 8
โข (๐บ
ยทih ๐น) โ โ |
10 | 1, 9 | mulcli 11170 |
. . . . . . 7
โข (๐ ยท (๐บ ยทih ๐น)) โ
โ |
11 | 8, 10 | addcli 11169 |
. . . . . 6
โข
(((โโ๐)
ยท (๐น
ยทih ๐บ)) + (๐ ยท (๐บ ยทih ๐น))) โ
โ |
12 | 11 | negrebi 11483 |
. . . . 5
โข
(-(((โโ๐) ยท (๐น ยทih ๐บ)) + (๐ ยท (๐บ ยทih ๐น))) โ โ โ
(((โโ๐)
ยท (๐น
ยทih ๐บ)) + (๐ ยท (๐บ ยทih ๐น))) โ
โ) |
13 | 5, 12 | mpbi 229 |
. . . 4
โข
(((โโ๐)
ยท (๐น
ยทih ๐บ)) + (๐ ยท (๐บ ยทih ๐น))) โ
โ |
14 | 13 | leabsi 15273 |
. . 3
โข
(((โโ๐)
ยท (๐น
ยทih ๐บ)) + (๐ ยท (๐บ ยทih ๐น))) โค
(absโ(((โโ๐) ยท (๐น ยทih ๐บ)) + (๐ ยท (๐บ ยทih ๐น)))) |
15 | 11 | absnegi 15294 |
. . 3
โข
(absโ-(((โโ๐) ยท (๐น ยทih ๐บ)) + (๐ ยท (๐บ ยทih ๐น)))) =
(absโ(((โโ๐) ยท (๐น ยทih ๐บ)) + (๐ ยท (๐บ ยทih ๐น)))) |
16 | 14, 15 | breqtrri 5136 |
. 2
โข
(((โโ๐)
ยท (๐น
ยทih ๐บ)) + (๐ ยท (๐บ ยทih ๐น))) โค
(absโ-(((โโ๐) ยท (๐น ยทih ๐บ)) + (๐ ยท (๐บ ยทih ๐น)))) |
17 | | eqid 2733 |
. . 3
โข (๐บ
ยทih ๐บ) = (๐บ ยทih ๐บ) |
18 | | eqid 2733 |
. . 3
โข (๐น
ยทih ๐น) = (๐น ยทih ๐น) |
19 | | normlem7.4 |
. . 3
โข
(absโ๐) =
1 |
20 | 1, 2, 3, 4, 17, 18, 19 | normlem6 30106 |
. 2
โข
(absโ-(((โโ๐) ยท (๐น ยทih ๐บ)) + (๐ ยท (๐บ ยทih ๐น)))) โค (2 ยท
((โโ(๐บ
ยทih ๐บ)) ยท (โโ(๐น
ยทih ๐น)))) |
21 | 11 | negcli 11477 |
. . . 4
โข
-(((โโ๐) ยท (๐น ยทih ๐บ)) + (๐ ยท (๐บ ยทih ๐น))) โ
โ |
22 | 21 | abscli 15289 |
. . 3
โข
(absโ-(((โโ๐) ยท (๐น ยทih ๐บ)) + (๐ ยท (๐บ ยทih ๐น)))) โ
โ |
23 | | 2re 12235 |
. . . 4
โข 2 โ
โ |
24 | | hiidge0 30089 |
. . . . . 6
โข (๐บ โ โ โ 0 โค
(๐บ
ยทih ๐บ)) |
25 | | hiidrcl 30086 |
. . . . . . . 8
โข (๐บ โ โ โ (๐บ
ยทih ๐บ) โ โ) |
26 | 3, 25 | ax-mp 5 |
. . . . . . 7
โข (๐บ
ยทih ๐บ) โ โ |
27 | 26 | sqrtcli 15265 |
. . . . . 6
โข (0 โค
(๐บ
ยทih ๐บ) โ (โโ(๐บ ยทih ๐บ)) โ
โ) |
28 | 3, 24, 27 | mp2b 10 |
. . . . 5
โข
(โโ(๐บ
ยทih ๐บ)) โ โ |
29 | | hiidge0 30089 |
. . . . . 6
โข (๐น โ โ โ 0 โค
(๐น
ยทih ๐น)) |
30 | | hiidrcl 30086 |
. . . . . . . 8
โข (๐น โ โ โ (๐น
ยทih ๐น) โ โ) |
31 | 2, 30 | ax-mp 5 |
. . . . . . 7
โข (๐น
ยทih ๐น) โ โ |
32 | 31 | sqrtcli 15265 |
. . . . . 6
โข (0 โค
(๐น
ยทih ๐น) โ (โโ(๐น ยทih ๐น)) โ
โ) |
33 | 2, 29, 32 | mp2b 10 |
. . . . 5
โข
(โโ(๐น
ยทih ๐น)) โ โ |
34 | 28, 33 | remulcli 11179 |
. . . 4
โข
((โโ(๐บ
ยทih ๐บ)) ยท (โโ(๐น
ยทih ๐น))) โ โ |
35 | 23, 34 | remulcli 11179 |
. . 3
โข (2
ยท ((โโ(๐บ
ยทih ๐บ)) ยท (โโ(๐น
ยทih ๐น)))) โ โ |
36 | 13, 22, 35 | letri 11292 |
. 2
โข
(((((โโ๐) ยท (๐น ยทih ๐บ)) + (๐ ยท (๐บ ยทih ๐น))) โค
(absโ-(((โโ๐) ยท (๐น ยทih ๐บ)) + (๐ ยท (๐บ ยทih ๐น)))) โง
(absโ-(((โโ๐) ยท (๐น ยทih ๐บ)) + (๐ ยท (๐บ ยทih ๐น)))) โค (2 ยท
((โโ(๐บ
ยทih ๐บ)) ยท (โโ(๐น
ยทih ๐น))))) โ (((โโ๐) ยท (๐น ยทih ๐บ)) + (๐ ยท (๐บ ยทih ๐น))) โค (2 ยท
((โโ(๐บ
ยทih ๐บ)) ยท (โโ(๐น
ยทih ๐น))))) |
37 | 16, 20, 36 | mp2an 691 |
1
โข
(((โโ๐)
ยท (๐น
ยทih ๐บ)) + (๐ ยท (๐บ ยทih ๐น))) โค (2 ยท
((โโ(๐บ
ยทih ๐บ)) ยท (โโ(๐น
ยทih ๐น)))) |