Step | Hyp | Ref
| Expression |
1 | | gt0ne0 11554 |
. . . . . . 7
โข ((๐ค โ โ โง 0 <
๐ค) โ ๐ค โ 0) |
2 | | rereccl 11807 |
. . . . . . 7
โข ((๐ค โ โ โง ๐ค โ 0) โ (1 / ๐ค) โ
โ) |
3 | 1, 2 | syldan 592 |
. . . . . 6
โข ((๐ค โ โ โง 0 <
๐ค) โ (1 / ๐ค) โ
โ) |
4 | 3 | adantrr 716 |
. . . . 5
โข ((๐ค โ โ โง (0 <
๐ค โง โ๐ฆ โ ๐ด โ๐ฃ โ ๐ต ((normโโ๐ฆ) +
(normโโ๐ฃ)) โค (๐ค ยท
(normโโ(๐ฆ +โ ๐ฃ))))) โ (1 / ๐ค) โ โ) |
5 | | recgt0 11935 |
. . . . . 6
โข ((๐ค โ โ โง 0 <
๐ค) โ 0 < (1 / ๐ค)) |
6 | 5 | adantrr 716 |
. . . . 5
โข ((๐ค โ โ โง (0 <
๐ค โง โ๐ฆ โ ๐ด โ๐ฃ โ ๐ต ((normโโ๐ฆ) +
(normโโ๐ฃ)) โค (๐ค ยท
(normโโ(๐ฆ +โ ๐ฃ))))) โ 0 < (1 / ๐ค)) |
7 | | 1red 11090 |
. . . . . . . . . . . . . . . 16
โข ((((๐ค โ โ โง ๐ฆ โ ๐ด) โง ๐ง โ ๐ต) โง (โ๐ฃ โ ๐ต ((normโโ๐ฆ) +
(normโโ๐ฃ)) โค (๐ค ยท
(normโโ(๐ฆ +โ ๐ฃ))) โง
(normโโ๐ฆ) = 1)) โ 1 โ
โ) |
8 | | 1re 11089 |
. . . . . . . . . . . . . . . . . 18
โข 1 โ
โ |
9 | | neg1cn 12201 |
. . . . . . . . . . . . . . . . . . . . 21
โข -1 โ
โ |
10 | | cdj1.2 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ๐ต โ
Sโ |
11 | 10 | sheli 29955 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ง โ ๐ต โ ๐ง โ โ) |
12 | | hvmulcl 29754 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((-1
โ โ โง ๐ง
โ โ) โ (-1 ยทโ ๐ง) โ
โ) |
13 | 9, 11, 12 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ง โ ๐ต โ (-1
ยทโ ๐ง) โ โ) |
14 | | normcl 29866 |
. . . . . . . . . . . . . . . . . . . 20
โข ((-1
ยทโ ๐ง) โ โ โ
(normโโ(-1 ยทโ ๐ง)) โ
โ) |
15 | 13, 14 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ง โ ๐ต โ (normโโ(-1
ยทโ ๐ง)) โ โ) |
16 | 15 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ค โ โ โง ๐ฆ โ ๐ด) โง ๐ง โ ๐ต) โ (normโโ(-1
ยทโ ๐ง)) โ โ) |
17 | | readdcl 11068 |
. . . . . . . . . . . . . . . . . 18
โข ((1
โ โ โง (normโโ(-1
ยทโ ๐ง)) โ โ) โ (1 +
(normโโ(-1 ยทโ ๐ง))) โ
โ) |
18 | 8, 16, 17 | sylancr 588 |
. . . . . . . . . . . . . . . . 17
โข (((๐ค โ โ โง ๐ฆ โ ๐ด) โง ๐ง โ ๐ต) โ (1 +
(normโโ(-1 ยทโ ๐ง))) โ
โ) |
19 | 18 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข ((((๐ค โ โ โง ๐ฆ โ ๐ด) โง ๐ง โ ๐ต) โง (โ๐ฃ โ ๐ต ((normโโ๐ฆ) +
(normโโ๐ฃ)) โค (๐ค ยท
(normโโ(๐ฆ +โ ๐ฃ))) โง
(normโโ๐ฆ) = 1)) โ (1 +
(normโโ(-1 ยทโ ๐ง))) โ
โ) |
20 | | cdj1.1 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ๐ด โ
Sโ |
21 | 20 | sheli 29955 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ฆ โ ๐ด โ ๐ฆ โ โ) |
22 | | hvsubcl 29758 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ฆ โ โ โง ๐ง โ โ) โ (๐ฆ โโ
๐ง) โ
โ) |
23 | 21, 11, 22 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ฆ โ ๐ด โง ๐ง โ ๐ต) โ (๐ฆ โโ ๐ง) โ
โ) |
24 | | normcl 29866 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ฆ โโ
๐ง) โ โ โ
(normโโ(๐ฆ โโ ๐ง)) โ
โ) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ฆ โ ๐ด โง ๐ง โ ๐ต) โ
(normโโ(๐ฆ โโ ๐ง)) โ
โ) |
26 | | remulcl 11070 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ค โ โ โง
(normโโ(๐ฆ โโ ๐ง)) โ โ) โ (๐ค ยท
(normโโ(๐ฆ โโ ๐ง))) โ
โ) |
27 | 25, 26 | sylan2 594 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ค โ โ โง (๐ฆ โ ๐ด โง ๐ง โ ๐ต)) โ (๐ค ยท
(normโโ(๐ฆ โโ ๐ง))) โ
โ) |
28 | 27 | anassrs 469 |
. . . . . . . . . . . . . . . . 17
โข (((๐ค โ โ โง ๐ฆ โ ๐ด) โง ๐ง โ ๐ต) โ (๐ค ยท
(normโโ(๐ฆ โโ ๐ง))) โ
โ) |
29 | 28 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข ((((๐ค โ โ โง ๐ฆ โ ๐ด) โง ๐ง โ ๐ต) โง (โ๐ฃ โ ๐ต ((normโโ๐ฆ) +
(normโโ๐ฃ)) โค (๐ค ยท
(normโโ(๐ฆ +โ ๐ฃ))) โง
(normโโ๐ฆ) = 1)) โ (๐ค ยท
(normโโ(๐ฆ โโ ๐ง))) โ
โ) |
30 | | normge0 29867 |
. . . . . . . . . . . . . . . . . . 19
โข ((-1
ยทโ ๐ง) โ โ โ 0 โค
(normโโ(-1 ยทโ ๐ง))) |
31 | 13, 30 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข (๐ง โ ๐ต โ 0 โค
(normโโ(-1 ยทโ ๐ง))) |
32 | | addge01 11599 |
. . . . . . . . . . . . . . . . . . . 20
โข ((1
โ โ โง (normโโ(-1
ยทโ ๐ง)) โ โ) โ (0 โค
(normโโ(-1 ยทโ ๐ง)) โ 1 โค (1 +
(normโโ(-1 ยทโ ๐ง))))) |
33 | 8, 32 | mpan 689 |
. . . . . . . . . . . . . . . . . . 19
โข
((normโโ(-1 ยทโ
๐ง)) โ โ โ
(0 โค (normโโ(-1 ยทโ
๐ง)) โ 1 โค (1 +
(normโโ(-1 ยทโ ๐ง))))) |
34 | 33 | biimpa 478 |
. . . . . . . . . . . . . . . . . 18
โข
(((normโโ(-1 ยทโ
๐ง)) โ โ โง 0
โค (normโโ(-1 ยทโ
๐ง))) โ 1 โค (1 +
(normโโ(-1 ยทโ ๐ง)))) |
35 | 15, 31, 34 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
โข (๐ง โ ๐ต โ 1 โค (1 +
(normโโ(-1 ยทโ ๐ง)))) |
36 | 35 | ad2antlr 726 |
. . . . . . . . . . . . . . . 16
โข ((((๐ค โ โ โง ๐ฆ โ ๐ด) โง ๐ง โ ๐ต) โง (โ๐ฃ โ ๐ต ((normโโ๐ฆ) +
(normโโ๐ฃ)) โค (๐ค ยท
(normโโ(๐ฆ +โ ๐ฃ))) โง
(normโโ๐ฆ) = 1)) โ 1 โค (1 +
(normโโ(-1 ยทโ ๐ง)))) |
37 | | shmulcl 29959 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ต โ
Sโ โง -1 โ โ โง ๐ง โ ๐ต) โ (-1
ยทโ ๐ง) โ ๐ต) |
38 | 10, 9, 37 | mp3an12 1452 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ง โ ๐ต โ (-1
ยทโ ๐ง) โ ๐ต) |
39 | | fveq2 6838 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ฃ = (-1
ยทโ ๐ง) โ (normโโ๐ฃ) =
(normโโ(-1 ยทโ ๐ง))) |
40 | 39 | oveq2d 7366 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฃ = (-1
ยทโ ๐ง) โ
((normโโ๐ฆ) + (normโโ๐ฃ)) =
((normโโ๐ฆ) + (normโโ(-1
ยทโ ๐ง)))) |
41 | | oveq2 7358 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ฃ = (-1
ยทโ ๐ง) โ (๐ฆ +โ ๐ฃ) = (๐ฆ +โ (-1
ยทโ ๐ง))) |
42 | 41 | fveq2d 6842 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ฃ = (-1
ยทโ ๐ง) โ
(normโโ(๐ฆ +โ ๐ฃ)) = (normโโ(๐ฆ +โ (-1
ยทโ ๐ง)))) |
43 | 42 | oveq2d 7366 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฃ = (-1
ยทโ ๐ง) โ (๐ค ยท
(normโโ(๐ฆ +โ ๐ฃ))) = (๐ค ยท
(normโโ(๐ฆ +โ (-1
ยทโ ๐ง))))) |
44 | 40, 43 | breq12d 5117 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ฃ = (-1
ยทโ ๐ง) โ
(((normโโ๐ฆ) + (normโโ๐ฃ)) โค (๐ค ยท
(normโโ(๐ฆ +โ ๐ฃ))) โ
((normโโ๐ฆ) + (normโโ(-1
ยทโ ๐ง))) โค (๐ค ยท
(normโโ(๐ฆ +โ (-1
ยทโ ๐ง)))))) |
45 | 44 | rspcv 3576 |
. . . . . . . . . . . . . . . . . . . 20
โข ((-1
ยทโ ๐ง) โ ๐ต โ (โ๐ฃ โ ๐ต ((normโโ๐ฆ) +
(normโโ๐ฃ)) โค (๐ค ยท
(normโโ(๐ฆ +โ ๐ฃ))) โ
((normโโ๐ฆ) + (normโโ(-1
ยทโ ๐ง))) โค (๐ค ยท
(normโโ(๐ฆ +โ (-1
ยทโ ๐ง)))))) |
46 | 38, 45 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ง โ ๐ต โ (โ๐ฃ โ ๐ต ((normโโ๐ฆ) +
(normโโ๐ฃ)) โค (๐ค ยท
(normโโ(๐ฆ +โ ๐ฃ))) โ
((normโโ๐ฆ) + (normโโ(-1
ยทโ ๐ง))) โค (๐ค ยท
(normโโ(๐ฆ +โ (-1
ยทโ ๐ง)))))) |
47 | 46 | imp 408 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ง โ ๐ต โง โ๐ฃ โ ๐ต ((normโโ๐ฆ) +
(normโโ๐ฃ)) โค (๐ค ยท
(normโโ(๐ฆ +โ ๐ฃ)))) โ
((normโโ๐ฆ) + (normโโ(-1
ยทโ ๐ง))) โค (๐ค ยท
(normโโ(๐ฆ +โ (-1
ยทโ ๐ง))))) |
48 | 47 | ad2ant2lr 747 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ค โ โ โง ๐ฆ โ ๐ด) โง ๐ง โ ๐ต) โง (โ๐ฃ โ ๐ต ((normโโ๐ฆ) +
(normโโ๐ฃ)) โค (๐ค ยท
(normโโ(๐ฆ +โ ๐ฃ))) โง
(normโโ๐ฆ) = 1)) โ
((normโโ๐ฆ) + (normโโ(-1
ยทโ ๐ง))) โค (๐ค ยท
(normโโ(๐ฆ +โ (-1
ยทโ ๐ง))))) |
49 | | oveq1 7357 |
. . . . . . . . . . . . . . . . . . 19
โข (1 =
(normโโ๐ฆ) โ (1 +
(normโโ(-1 ยทโ ๐ง))) =
((normโโ๐ฆ) + (normโโ(-1
ยทโ ๐ง)))) |
50 | 49 | eqcoms 2746 |
. . . . . . . . . . . . . . . . . 18
โข
((normโโ๐ฆ) = 1 โ (1 +
(normโโ(-1 ยทโ ๐ง))) =
((normโโ๐ฆ) + (normโโ(-1
ยทโ ๐ง)))) |
51 | 50 | ad2antll 728 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ค โ โ โง ๐ฆ โ ๐ด) โง ๐ง โ ๐ต) โง (โ๐ฃ โ ๐ต ((normโโ๐ฆ) +
(normโโ๐ฃ)) โค (๐ค ยท
(normโโ(๐ฆ +โ ๐ฃ))) โง
(normโโ๐ฆ) = 1)) โ (1 +
(normโโ(-1 ยทโ ๐ง))) =
((normโโ๐ฆ) + (normโโ(-1
ยทโ ๐ง)))) |
52 | | hvsubval 29757 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ฆ โ โ โง ๐ง โ โ) โ (๐ฆ โโ
๐ง) = (๐ฆ +โ (-1
ยทโ ๐ง))) |
53 | 21, 11, 52 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ฆ โ ๐ด โง ๐ง โ ๐ต) โ (๐ฆ โโ ๐ง) = (๐ฆ +โ (-1
ยทโ ๐ง))) |
54 | 53 | fveq2d 6842 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ฆ โ ๐ด โง ๐ง โ ๐ต) โ
(normโโ(๐ฆ โโ ๐ง)) =
(normโโ(๐ฆ +โ (-1
ยทโ ๐ง)))) |
55 | 54 | oveq2d 7366 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ฆ โ ๐ด โง ๐ง โ ๐ต) โ (๐ค ยท
(normโโ(๐ฆ โโ ๐ง))) = (๐ค ยท
(normโโ(๐ฆ +โ (-1
ยทโ ๐ง))))) |
56 | 55 | adantll 713 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ค โ โ โง ๐ฆ โ ๐ด) โง ๐ง โ ๐ต) โ (๐ค ยท
(normโโ(๐ฆ โโ ๐ง))) = (๐ค ยท
(normโโ(๐ฆ +โ (-1
ยทโ ๐ง))))) |
57 | 56 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ค โ โ โง ๐ฆ โ ๐ด) โง ๐ง โ ๐ต) โง (โ๐ฃ โ ๐ต ((normโโ๐ฆ) +
(normโโ๐ฃ)) โค (๐ค ยท
(normโโ(๐ฆ +โ ๐ฃ))) โง
(normโโ๐ฆ) = 1)) โ (๐ค ยท
(normโโ(๐ฆ โโ ๐ง))) = (๐ค ยท
(normโโ(๐ฆ +โ (-1
ยทโ ๐ง))))) |
58 | 48, 51, 57 | 3brtr4d 5136 |
. . . . . . . . . . . . . . . 16
โข ((((๐ค โ โ โง ๐ฆ โ ๐ด) โง ๐ง โ ๐ต) โง (โ๐ฃ โ ๐ต ((normโโ๐ฆ) +
(normโโ๐ฃ)) โค (๐ค ยท
(normโโ(๐ฆ +โ ๐ฃ))) โง
(normโโ๐ฆ) = 1)) โ (1 +
(normโโ(-1 ยทโ ๐ง))) โค (๐ค ยท
(normโโ(๐ฆ โโ ๐ง)))) |
59 | 7, 19, 29, 36, 58 | letrd 11246 |
. . . . . . . . . . . . . . 15
โข ((((๐ค โ โ โง ๐ฆ โ ๐ด) โง ๐ง โ ๐ต) โง (โ๐ฃ โ ๐ต ((normโโ๐ฆ) +
(normโโ๐ฃ)) โค (๐ค ยท
(normโโ(๐ฆ +โ ๐ฃ))) โง
(normโโ๐ฆ) = 1)) โ 1 โค (๐ค ยท
(normโโ(๐ฆ โโ ๐ง)))) |
60 | 59 | ex 414 |
. . . . . . . . . . . . . 14
โข (((๐ค โ โ โง ๐ฆ โ ๐ด) โง ๐ง โ ๐ต) โ ((โ๐ฃ โ ๐ต ((normโโ๐ฆ) +
(normโโ๐ฃ)) โค (๐ค ยท
(normโโ(๐ฆ +โ ๐ฃ))) โง
(normโโ๐ฆ) = 1) โ 1 โค (๐ค ยท
(normโโ(๐ฆ โโ ๐ง))))) |
61 | 60 | adantllr 718 |
. . . . . . . . . . . . 13
โข ((((๐ค โ โ โง 0 <
๐ค) โง ๐ฆ โ ๐ด) โง ๐ง โ ๐ต) โ ((โ๐ฃ โ ๐ต ((normโโ๐ฆ) +
(normโโ๐ฃ)) โค (๐ค ยท
(normโโ(๐ฆ +โ ๐ฃ))) โง
(normโโ๐ฆ) = 1) โ 1 โค (๐ค ยท
(normโโ(๐ฆ โโ ๐ง))))) |
62 | | simplll 774 |
. . . . . . . . . . . . . . 15
โข ((((๐ค โ โ โง 0 <
๐ค) โง ๐ฆ โ ๐ด) โง ๐ง โ ๐ต) โ ๐ค โ โ) |
63 | 23 | adantll 713 |
. . . . . . . . . . . . . . . 16
โข ((((๐ค โ โ โง 0 <
๐ค) โง ๐ฆ โ ๐ด) โง ๐ง โ ๐ต) โ (๐ฆ โโ ๐ง) โ
โ) |
64 | 63, 24 | syl 17 |
. . . . . . . . . . . . . . 15
โข ((((๐ค โ โ โง 0 <
๐ค) โง ๐ฆ โ ๐ด) โง ๐ง โ ๐ต) โ
(normโโ(๐ฆ โโ ๐ง)) โ
โ) |
65 | 62, 64, 26 | syl2anc 585 |
. . . . . . . . . . . . . 14
โข ((((๐ค โ โ โง 0 <
๐ค) โง ๐ฆ โ ๐ด) โง ๐ง โ ๐ต) โ (๐ค ยท
(normโโ(๐ฆ โโ ๐ง))) โ
โ) |
66 | | simpllr 775 |
. . . . . . . . . . . . . 14
โข ((((๐ค โ โ โง 0 <
๐ค) โง ๐ฆ โ ๐ด) โง ๐ง โ ๐ต) โ 0 < ๐ค) |
67 | | lediv1 11954 |
. . . . . . . . . . . . . . 15
โข ((1
โ โ โง (๐ค
ยท (normโโ(๐ฆ โโ ๐ง))) โ โ โง (๐ค โ โ โง 0 <
๐ค)) โ (1 โค (๐ค ยท
(normโโ(๐ฆ โโ ๐ง))) โ (1 / ๐ค) โค ((๐ค ยท
(normโโ(๐ฆ โโ ๐ง))) / ๐ค))) |
68 | 8, 67 | mp3an1 1449 |
. . . . . . . . . . . . . 14
โข (((๐ค ยท
(normโโ(๐ฆ โโ ๐ง))) โ โ โง (๐ค โ โ โง 0 <
๐ค)) โ (1 โค (๐ค ยท
(normโโ(๐ฆ โโ ๐ง))) โ (1 / ๐ค) โค ((๐ค ยท
(normโโ(๐ฆ โโ ๐ง))) / ๐ค))) |
69 | 65, 62, 66, 68 | syl12anc 836 |
. . . . . . . . . . . . 13
โข ((((๐ค โ โ โง 0 <
๐ค) โง ๐ฆ โ ๐ด) โง ๐ง โ ๐ต) โ (1 โค (๐ค ยท
(normโโ(๐ฆ โโ ๐ง))) โ (1 / ๐ค) โค ((๐ค ยท
(normโโ(๐ฆ โโ ๐ง))) / ๐ค))) |
70 | 61, 69 | sylibd 238 |
. . . . . . . . . . . 12
โข ((((๐ค โ โ โง 0 <
๐ค) โง ๐ฆ โ ๐ด) โง ๐ง โ ๐ต) โ ((โ๐ฃ โ ๐ต ((normโโ๐ฆ) +
(normโโ๐ฃ)) โค (๐ค ยท
(normโโ(๐ฆ +โ ๐ฃ))) โง
(normโโ๐ฆ) = 1) โ (1 / ๐ค) โค ((๐ค ยท
(normโโ(๐ฆ โโ ๐ง))) / ๐ค))) |
71 | 70 | imp 408 |
. . . . . . . . . . 11
โข
(((((๐ค โ
โ โง 0 < ๐ค)
โง ๐ฆ โ ๐ด) โง ๐ง โ ๐ต) โง (โ๐ฃ โ ๐ต ((normโโ๐ฆ) +
(normโโ๐ฃ)) โค (๐ค ยท
(normโโ(๐ฆ +โ ๐ฃ))) โง
(normโโ๐ฆ) = 1)) โ (1 / ๐ค) โค ((๐ค ยท
(normโโ(๐ฆ โโ ๐ง))) / ๐ค)) |
72 | 25 | recnd 11117 |
. . . . . . . . . . . . . 14
โข ((๐ฆ โ ๐ด โง ๐ง โ ๐ต) โ
(normโโ(๐ฆ โโ ๐ง)) โ
โ) |
73 | 72 | adantll 713 |
. . . . . . . . . . . . 13
โข ((((๐ค โ โ โง 0 <
๐ค) โง ๐ฆ โ ๐ด) โง ๐ง โ ๐ต) โ
(normโโ(๐ฆ โโ ๐ง)) โ
โ) |
74 | | recn 11075 |
. . . . . . . . . . . . . 14
โข (๐ค โ โ โ ๐ค โ
โ) |
75 | 74 | ad3antrrr 729 |
. . . . . . . . . . . . 13
โข ((((๐ค โ โ โง 0 <
๐ค) โง ๐ฆ โ ๐ด) โง ๐ง โ ๐ต) โ ๐ค โ โ) |
76 | 1 | ad2antrr 725 |
. . . . . . . . . . . . 13
โข ((((๐ค โ โ โง 0 <
๐ค) โง ๐ฆ โ ๐ด) โง ๐ง โ ๐ต) โ ๐ค โ 0) |
77 | 73, 75, 76 | divcan3d 11870 |
. . . . . . . . . . . 12
โข ((((๐ค โ โ โง 0 <
๐ค) โง ๐ฆ โ ๐ด) โง ๐ง โ ๐ต) โ ((๐ค ยท
(normโโ(๐ฆ โโ ๐ง))) / ๐ค) = (normโโ(๐ฆ โโ
๐ง))) |
78 | 77 | adantr 482 |
. . . . . . . . . . 11
โข
(((((๐ค โ
โ โง 0 < ๐ค)
โง ๐ฆ โ ๐ด) โง ๐ง โ ๐ต) โง (โ๐ฃ โ ๐ต ((normโโ๐ฆ) +
(normโโ๐ฃ)) โค (๐ค ยท
(normโโ(๐ฆ +โ ๐ฃ))) โง
(normโโ๐ฆ) = 1)) โ ((๐ค ยท
(normโโ(๐ฆ โโ ๐ง))) / ๐ค) = (normโโ(๐ฆ โโ
๐ง))) |
79 | 71, 78 | breqtrd 5130 |
. . . . . . . . . 10
โข
(((((๐ค โ
โ โง 0 < ๐ค)
โง ๐ฆ โ ๐ด) โง ๐ง โ ๐ต) โง (โ๐ฃ โ ๐ต ((normโโ๐ฆ) +
(normโโ๐ฃ)) โค (๐ค ยท
(normโโ(๐ฆ +โ ๐ฃ))) โง
(normโโ๐ฆ) = 1)) โ (1 / ๐ค) โค (normโโ(๐ฆ โโ
๐ง))) |
80 | 79 | exp43 438 |
. . . . . . . . 9
โข (((๐ค โ โ โง 0 <
๐ค) โง ๐ฆ โ ๐ด) โ (๐ง โ ๐ต โ (โ๐ฃ โ ๐ต ((normโโ๐ฆ) +
(normโโ๐ฃ)) โค (๐ค ยท
(normโโ(๐ฆ +โ ๐ฃ))) โ
((normโโ๐ฆ) = 1 โ (1 / ๐ค) โค (normโโ(๐ฆ โโ
๐ง)))))) |
81 | 80 | com23 86 |
. . . . . . . 8
โข (((๐ค โ โ โง 0 <
๐ค) โง ๐ฆ โ ๐ด) โ (โ๐ฃ โ ๐ต ((normโโ๐ฆ) +
(normโโ๐ฃ)) โค (๐ค ยท
(normโโ(๐ฆ +โ ๐ฃ))) โ (๐ง โ ๐ต โ
((normโโ๐ฆ) = 1 โ (1 / ๐ค) โค (normโโ(๐ฆ โโ
๐ง)))))) |
82 | 81 | ralrimdv 3148 |
. . . . . . 7
โข (((๐ค โ โ โง 0 <
๐ค) โง ๐ฆ โ ๐ด) โ (โ๐ฃ โ ๐ต ((normโโ๐ฆ) +
(normโโ๐ฃ)) โค (๐ค ยท
(normโโ(๐ฆ +โ ๐ฃ))) โ โ๐ง โ ๐ต ((normโโ๐ฆ) = 1 โ (1 / ๐ค) โค
(normโโ(๐ฆ โโ ๐ง))))) |
83 | 82 | ralimdva 3163 |
. . . . . 6
โข ((๐ค โ โ โง 0 <
๐ค) โ (โ๐ฆ โ ๐ด โ๐ฃ โ ๐ต ((normโโ๐ฆ) +
(normโโ๐ฃ)) โค (๐ค ยท
(normโโ(๐ฆ +โ ๐ฃ))) โ โ๐ฆ โ ๐ด โ๐ง โ ๐ต ((normโโ๐ฆ) = 1 โ (1 / ๐ค) โค
(normโโ(๐ฆ โโ ๐ง))))) |
84 | 83 | impr 456 |
. . . . 5
โข ((๐ค โ โ โง (0 <
๐ค โง โ๐ฆ โ ๐ด โ๐ฃ โ ๐ต ((normโโ๐ฆ) +
(normโโ๐ฃ)) โค (๐ค ยท
(normโโ(๐ฆ +โ ๐ฃ))))) โ โ๐ฆ โ ๐ด โ๐ง โ ๐ต ((normโโ๐ฆ) = 1 โ (1 / ๐ค) โค
(normโโ(๐ฆ โโ ๐ง)))) |
85 | 4, 6, 84 | jca32 517 |
. . . 4
โข ((๐ค โ โ โง (0 <
๐ค โง โ๐ฆ โ ๐ด โ๐ฃ โ ๐ต ((normโโ๐ฆ) +
(normโโ๐ฃ)) โค (๐ค ยท
(normโโ(๐ฆ +โ ๐ฃ))))) โ ((1 / ๐ค) โ โ โง (0 < (1 / ๐ค) โง โ๐ฆ โ ๐ด โ๐ง โ ๐ต ((normโโ๐ฆ) = 1 โ (1 / ๐ค) โค
(normโโ(๐ฆ โโ ๐ง)))))) |
86 | 85 | ex 414 |
. . 3
โข (๐ค โ โ โ ((0 <
๐ค โง โ๐ฆ โ ๐ด โ๐ฃ โ ๐ต ((normโโ๐ฆ) +
(normโโ๐ฃ)) โค (๐ค ยท
(normโโ(๐ฆ +โ ๐ฃ)))) โ ((1 / ๐ค) โ โ โง (0 < (1 / ๐ค) โง โ๐ฆ โ ๐ด โ๐ง โ ๐ต ((normโโ๐ฆ) = 1 โ (1 / ๐ค) โค
(normโโ(๐ฆ โโ ๐ง))))))) |
87 | | breq2 5108 |
. . . . 5
โข (๐ฅ = (1 / ๐ค) โ (0 < ๐ฅ โ 0 < (1 / ๐ค))) |
88 | | breq1 5107 |
. . . . . . 7
โข (๐ฅ = (1 / ๐ค) โ (๐ฅ โค (normโโ(๐ฆ โโ
๐ง)) โ (1 / ๐ค) โค
(normโโ(๐ฆ โโ ๐ง)))) |
89 | 88 | imbi2d 341 |
. . . . . 6
โข (๐ฅ = (1 / ๐ค) โ
(((normโโ๐ฆ) = 1 โ ๐ฅ โค (normโโ(๐ฆ โโ
๐ง))) โ
((normโโ๐ฆ) = 1 โ (1 / ๐ค) โค (normโโ(๐ฆ โโ
๐ง))))) |
90 | 89 | 2ralbidv 3211 |
. . . . 5
โข (๐ฅ = (1 / ๐ค) โ (โ๐ฆ โ ๐ด โ๐ง โ ๐ต ((normโโ๐ฆ) = 1 โ ๐ฅ โค (normโโ(๐ฆ โโ
๐ง))) โ โ๐ฆ โ ๐ด โ๐ง โ ๐ต ((normโโ๐ฆ) = 1 โ (1 / ๐ค) โค
(normโโ(๐ฆ โโ ๐ง))))) |
91 | 87, 90 | anbi12d 632 |
. . . 4
โข (๐ฅ = (1 / ๐ค) โ ((0 < ๐ฅ โง โ๐ฆ โ ๐ด โ๐ง โ ๐ต ((normโโ๐ฆ) = 1 โ ๐ฅ โค (normโโ(๐ฆ โโ
๐ง)))) โ (0 < (1 /
๐ค) โง โ๐ฆ โ ๐ด โ๐ง โ ๐ต ((normโโ๐ฆ) = 1 โ (1 / ๐ค) โค
(normโโ(๐ฆ โโ ๐ง)))))) |
92 | 91 | rspcev 3580 |
. . 3
โข (((1 /
๐ค) โ โ โง (0
< (1 / ๐ค) โง
โ๐ฆ โ ๐ด โ๐ง โ ๐ต ((normโโ๐ฆ) = 1 โ (1 / ๐ค) โค
(normโโ(๐ฆ โโ ๐ง))))) โ โ๐ฅ โ โ (0 < ๐ฅ โง โ๐ฆ โ ๐ด โ๐ง โ ๐ต ((normโโ๐ฆ) = 1 โ ๐ฅ โค (normโโ(๐ฆ โโ
๐ง))))) |
93 | 86, 92 | syl6 35 |
. 2
โข (๐ค โ โ โ ((0 <
๐ค โง โ๐ฆ โ ๐ด โ๐ฃ โ ๐ต ((normโโ๐ฆ) +
(normโโ๐ฃ)) โค (๐ค ยท
(normโโ(๐ฆ +โ ๐ฃ)))) โ โ๐ฅ โ โ (0 < ๐ฅ โง โ๐ฆ โ ๐ด โ๐ง โ ๐ต ((normโโ๐ฆ) = 1 โ ๐ฅ โค (normโโ(๐ฆ โโ
๐ง)))))) |
94 | 93 | rexlimiv 3144 |
1
โข
(โ๐ค โ
โ (0 < ๐ค โง
โ๐ฆ โ ๐ด โ๐ฃ โ ๐ต ((normโโ๐ฆ) +
(normโโ๐ฃ)) โค (๐ค ยท
(normโโ(๐ฆ +โ ๐ฃ)))) โ โ๐ฅ โ โ (0 < ๐ฅ โง โ๐ฆ โ ๐ด โ๐ง โ ๐ต ((normโโ๐ฆ) = 1 โ ๐ฅ โค (normโโ(๐ฆ โโ
๐ง))))) |