Step | Hyp | Ref
| Expression |
1 | | cdj3.1 |
. . . 4
โข ๐ด โ
Sโ |
2 | | cdj3.2 |
. . . 4
โข ๐ต โ
Sโ |
3 | 1, 2 | cdj3lem1 31418 |
. . 3
โข
(โ๐ฃ โ
โ (0 < ๐ฃ โง
โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ((normโโ๐ฅ) +
(normโโ๐ฆ)) โค (๐ฃ ยท
(normโโ(๐ฅ +โ ๐ฆ)))) โ (๐ด โฉ ๐ต) = 0โ) |
4 | | cdj3.3 |
. . . . 5
โข ๐ = (๐ฅ โ (๐ด +โ ๐ต) โฆ (โฉ๐ง โ ๐ด โ๐ค โ ๐ต ๐ฅ = (๐ง +โ ๐ค))) |
5 | 1, 2, 4 | cdj3lem2b 31421 |
. . . 4
โข
(โ๐ฃ โ
โ (0 < ๐ฃ โง
โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ((normโโ๐ฅ) +
(normโโ๐ฆ)) โค (๐ฃ ยท
(normโโ(๐ฅ +โ ๐ฆ)))) โ โ๐ฃ โ โ (0 < ๐ฃ โง โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ฃ ยท
(normโโ๐ข)))) |
6 | | cdj3.5 |
. . . 4
โข (๐ โ โ๐ฃ โ โ (0 < ๐ฃ โง โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ฃ ยท
(normโโ๐ข)))) |
7 | 5, 6 | sylibr 233 |
. . 3
โข
(โ๐ฃ โ
โ (0 < ๐ฃ โง
โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ((normโโ๐ฅ) +
(normโโ๐ฆ)) โค (๐ฃ ยท
(normโโ(๐ฅ +โ ๐ฆ)))) โ ๐) |
8 | | cdj3.4 |
. . . . 5
โข ๐ = (๐ฅ โ (๐ด +โ ๐ต) โฆ (โฉ๐ค โ ๐ต โ๐ง โ ๐ด ๐ฅ = (๐ง +โ ๐ค))) |
9 | 1, 2, 8 | cdj3lem3b 31424 |
. . . 4
โข
(โ๐ฃ โ
โ (0 < ๐ฃ โง
โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ((normโโ๐ฅ) +
(normโโ๐ฆ)) โค (๐ฃ ยท
(normโโ(๐ฅ +โ ๐ฆ)))) โ โ๐ฃ โ โ (0 < ๐ฃ โง โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ฃ ยท
(normโโ๐ข)))) |
10 | | cdj3.6 |
. . . 4
โข (๐ โ โ๐ฃ โ โ (0 < ๐ฃ โง โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ฃ ยท
(normโโ๐ข)))) |
11 | 9, 10 | sylibr 233 |
. . 3
โข
(โ๐ฃ โ
โ (0 < ๐ฃ โง
โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ((normโโ๐ฅ) +
(normโโ๐ฆ)) โค (๐ฃ ยท
(normโโ(๐ฅ +โ ๐ฆ)))) โ ๐) |
12 | 3, 7, 11 | 3jca 1129 |
. 2
โข
(โ๐ฃ โ
โ (0 < ๐ฃ โง
โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ((normโโ๐ฅ) +
(normโโ๐ฆ)) โค (๐ฃ ยท
(normโโ(๐ฅ +โ ๐ฆ)))) โ ((๐ด โฉ ๐ต) = 0โ โง ๐ โง ๐)) |
13 | | breq2 5114 |
. . . . . . . . 9
โข (๐ฃ = ๐ โ (0 < ๐ฃ โ 0 < ๐)) |
14 | | oveq1 7369 |
. . . . . . . . . . 11
โข (๐ฃ = ๐ โ (๐ฃ ยท
(normโโ๐ข)) = (๐ ยท
(normโโ๐ข))) |
15 | 14 | breq2d 5122 |
. . . . . . . . . 10
โข (๐ฃ = ๐ โ
((normโโ(๐โ๐ข)) โค (๐ฃ ยท
(normโโ๐ข)) โ
(normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข)))) |
16 | 15 | ralbidv 3175 |
. . . . . . . . 9
โข (๐ฃ = ๐ โ (โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ฃ ยท
(normโโ๐ข)) โ โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข)))) |
17 | 13, 16 | anbi12d 632 |
. . . . . . . 8
โข (๐ฃ = ๐ โ ((0 < ๐ฃ โง โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ฃ ยท
(normโโ๐ข))) โ (0 < ๐ โง โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข))))) |
18 | 17 | cbvrexvw 3229 |
. . . . . . 7
โข
(โ๐ฃ โ
โ (0 < ๐ฃ โง
โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ฃ ยท
(normโโ๐ข))) โ โ๐ โ โ (0 < ๐ โง โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข)))) |
19 | 6, 18 | bitri 275 |
. . . . . 6
โข (๐ โ โ๐ โ โ (0 < ๐ โง โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข)))) |
20 | | breq2 5114 |
. . . . . . . . 9
โข (๐ฃ = ๐ โ (0 < ๐ฃ โ 0 < ๐)) |
21 | | oveq1 7369 |
. . . . . . . . . . 11
โข (๐ฃ = ๐ โ (๐ฃ ยท
(normโโ๐ข)) = (๐ ยท
(normโโ๐ข))) |
22 | 21 | breq2d 5122 |
. . . . . . . . . 10
โข (๐ฃ = ๐ โ
((normโโ(๐โ๐ข)) โค (๐ฃ ยท
(normโโ๐ข)) โ
(normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข)))) |
23 | 22 | ralbidv 3175 |
. . . . . . . . 9
โข (๐ฃ = ๐ โ (โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ฃ ยท
(normโโ๐ข)) โ โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข)))) |
24 | 20, 23 | anbi12d 632 |
. . . . . . . 8
โข (๐ฃ = ๐ โ ((0 < ๐ฃ โง โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ฃ ยท
(normโโ๐ข))) โ (0 < ๐ โง โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข))))) |
25 | 24 | cbvrexvw 3229 |
. . . . . . 7
โข
(โ๐ฃ โ
โ (0 < ๐ฃ โง
โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ฃ ยท
(normโโ๐ข))) โ โ๐ โ โ (0 < ๐ โง โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข)))) |
26 | 10, 25 | bitri 275 |
. . . . . 6
โข (๐ โ โ๐ โ โ (0 < ๐ โง โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข)))) |
27 | 19, 26 | anbi12i 628 |
. . . . 5
โข ((๐ โง ๐) โ (โ๐ โ โ (0 < ๐ โง โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข))) โง โ๐ โ โ (0 < ๐ โง โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข))))) |
28 | | reeanv 3220 |
. . . . 5
โข
(โ๐ โ
โ โ๐ โ
โ ((0 < ๐ โง
โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข))) โง (0 < ๐ โง โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข)))) โ (โ๐ โ โ (0 < ๐ โง โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข))) โง โ๐ โ โ (0 < ๐ โง โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข))))) |
29 | 27, 28 | bitr4i 278 |
. . . 4
โข ((๐ โง ๐) โ โ๐ โ โ โ๐ โ โ ((0 < ๐ โง โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข))) โง (0 < ๐ โง โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข))))) |
30 | | an4 655 |
. . . . . 6
โข (((0 <
๐ โง โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข))) โง (0 < ๐ โง โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข)))) โ ((0 < ๐ โง 0 < ๐) โง (โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข)) โง โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข))))) |
31 | | addgt0 11648 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ โ) โง (0 <
๐ โง 0 < ๐)) โ 0 < (๐ + ๐)) |
32 | 31 | ex 414 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ) โ ((0 <
๐ โง 0 < ๐) โ 0 < (๐ + ๐))) |
33 | 32 | adantl 483 |
. . . . . . 7
โข (((๐ด โฉ ๐ต) = 0โ โง (๐ โ โ โง ๐ โ โ)) โ ((0
< ๐ โง 0 < ๐) โ 0 < (๐ + ๐))) |
34 | 1, 2 | shsvai 30348 |
. . . . . . . . . . 11
โข ((๐ก โ ๐ด โง โ โ ๐ต) โ (๐ก +โ โ) โ (๐ด +โ ๐ต)) |
35 | | 2fveq3 6852 |
. . . . . . . . . . . . . 14
โข (๐ข = (๐ก +โ โ) โ (normโโ(๐โ๐ข)) = (normโโ(๐โ(๐ก +โ โ)))) |
36 | | fveq2 6847 |
. . . . . . . . . . . . . . 15
โข (๐ข = (๐ก +โ โ) โ (normโโ๐ข) =
(normโโ(๐ก +โ โ))) |
37 | 36 | oveq2d 7378 |
. . . . . . . . . . . . . 14
โข (๐ข = (๐ก +โ โ) โ (๐ ยท
(normโโ๐ข)) = (๐ ยท
(normโโ(๐ก +โ โ)))) |
38 | 35, 37 | breq12d 5123 |
. . . . . . . . . . . . 13
โข (๐ข = (๐ก +โ โ) โ
((normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข)) โ
(normโโ(๐โ(๐ก +โ โ))) โค (๐ ยท
(normโโ(๐ก +โ โ))))) |
39 | 38 | rspcv 3580 |
. . . . . . . . . . . 12
โข ((๐ก +โ โ) โ (๐ด +โ ๐ต) โ (โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข)) โ
(normโโ(๐โ(๐ก +โ โ))) โค (๐ ยท
(normโโ(๐ก +โ โ))))) |
40 | | 2fveq3 6852 |
. . . . . . . . . . . . . 14
โข (๐ข = (๐ก +โ โ) โ (normโโ(๐โ๐ข)) = (normโโ(๐โ(๐ก +โ โ)))) |
41 | 36 | oveq2d 7378 |
. . . . . . . . . . . . . 14
โข (๐ข = (๐ก +โ โ) โ (๐ ยท
(normโโ๐ข)) = (๐ ยท
(normโโ(๐ก +โ โ)))) |
42 | 40, 41 | breq12d 5123 |
. . . . . . . . . . . . 13
โข (๐ข = (๐ก +โ โ) โ
((normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข)) โ
(normโโ(๐โ(๐ก +โ โ))) โค (๐ ยท
(normโโ(๐ก +โ โ))))) |
43 | 42 | rspcv 3580 |
. . . . . . . . . . . 12
โข ((๐ก +โ โ) โ (๐ด +โ ๐ต) โ (โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข)) โ
(normโโ(๐โ(๐ก +โ โ))) โค (๐ ยท
(normโโ(๐ก +โ โ))))) |
44 | 39, 43 | anim12d 610 |
. . . . . . . . . . 11
โข ((๐ก +โ โ) โ (๐ด +โ ๐ต) โ ((โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข)) โง โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข))) โ
((normโโ(๐โ(๐ก +โ โ))) โค (๐ ยท
(normโโ(๐ก +โ โ))) โง
(normโโ(๐โ(๐ก +โ โ))) โค (๐ ยท
(normโโ(๐ก +โ โ)))))) |
45 | 34, 44 | syl 17 |
. . . . . . . . . 10
โข ((๐ก โ ๐ด โง โ โ ๐ต) โ ((โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข)) โง โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข))) โ
((normโโ(๐โ(๐ก +โ โ))) โค (๐ ยท
(normโโ(๐ก +โ โ))) โง
(normโโ(๐โ(๐ก +โ โ))) โค (๐ ยท
(normโโ(๐ก +โ โ)))))) |
46 | 45 | adantl 483 |
. . . . . . . . 9
โข ((((๐ด โฉ ๐ต) = 0โ โง (๐ โ โ โง ๐ โ โ)) โง (๐ก โ ๐ด โง โ โ ๐ต)) โ ((โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข)) โง โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข))) โ
((normโโ(๐โ(๐ก +โ โ))) โค (๐ ยท
(normโโ(๐ก +โ โ))) โง
(normโโ(๐โ(๐ก +โ โ))) โค (๐ ยท
(normโโ(๐ก +โ โ)))))) |
47 | 1 | sheli 30198 |
. . . . . . . . . . . . . . 15
โข (๐ก โ ๐ด โ ๐ก โ โ) |
48 | | normcl 30109 |
. . . . . . . . . . . . . . 15
โข (๐ก โ โ โ
(normโโ๐ก) โ โ) |
49 | 47, 48 | syl 17 |
. . . . . . . . . . . . . 14
โข (๐ก โ ๐ด โ (normโโ๐ก) โ
โ) |
50 | 2 | sheli 30198 |
. . . . . . . . . . . . . . 15
โข (โ โ ๐ต โ โ โ โ) |
51 | | normcl 30109 |
. . . . . . . . . . . . . . 15
โข (โ โ โ โ
(normโโโ) โ โ) |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . . . 14
โข (โ โ ๐ต โ (normโโโ) โ
โ) |
53 | 49, 52 | anim12i 614 |
. . . . . . . . . . . . 13
โข ((๐ก โ ๐ด โง โ โ ๐ต) โ
((normโโ๐ก) โ โ โง
(normโโโ) โ โ)) |
54 | 53 | adantl 483 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ โ โ) โง (๐ก โ ๐ด โง โ โ ๐ต)) โ
((normโโ๐ก) โ โ โง
(normโโโ) โ โ)) |
55 | | hvaddcl 29996 |
. . . . . . . . . . . . . . . 16
โข ((๐ก โ โ โง โ โ โ) โ (๐ก +โ โ) โ
โ) |
56 | 47, 50, 55 | syl2an 597 |
. . . . . . . . . . . . . . 15
โข ((๐ก โ ๐ด โง โ โ ๐ต) โ (๐ก +โ โ) โ โ) |
57 | | normcl 30109 |
. . . . . . . . . . . . . . 15
โข ((๐ก +โ โ) โ โ โ
(normโโ(๐ก +โ โ)) โ โ) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . . 14
โข ((๐ก โ ๐ด โง โ โ ๐ต) โ
(normโโ(๐ก +โ โ)) โ โ) |
59 | | remulcl 11143 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง
(normโโ(๐ก +โ โ)) โ โ) โ (๐ ยท
(normโโ(๐ก +โ โ))) โ โ) |
60 | 58, 59 | sylan2 594 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง (๐ก โ ๐ด โง โ โ ๐ต)) โ (๐ ยท
(normโโ(๐ก +โ โ))) โ โ) |
61 | 60 | adantlr 714 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ โ โ) โง (๐ก โ ๐ด โง โ โ ๐ต)) โ (๐ ยท
(normโโ(๐ก +โ โ))) โ โ) |
62 | | remulcl 11143 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง
(normโโ(๐ก +โ โ)) โ โ) โ (๐ ยท
(normโโ(๐ก +โ โ))) โ โ) |
63 | 58, 62 | sylan2 594 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง (๐ก โ ๐ด โง โ โ ๐ต)) โ (๐ ยท
(normโโ(๐ก +โ โ))) โ โ) |
64 | 63 | adantll 713 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ โ โ) โง (๐ก โ ๐ด โง โ โ ๐ต)) โ (๐ ยท
(normโโ(๐ก +โ โ))) โ โ) |
65 | | le2add 11644 |
. . . . . . . . . . . 12
โข
((((normโโ๐ก) โ โ โง
(normโโโ) โ โ) โง ((๐ ยท
(normโโ(๐ก +โ โ))) โ โ โง (๐ ยท
(normโโ(๐ก +โ โ))) โ โ)) โ
(((normโโ๐ก) โค (๐ ยท
(normโโ(๐ก +โ โ))) โง (normโโโ) โค (๐ ยท
(normโโ(๐ก +โ โ)))) โ
((normโโ๐ก) + (normโโโ)) โค ((๐ ยท
(normโโ(๐ก +โ โ))) + (๐ ยท
(normโโ(๐ก +โ โ)))))) |
66 | 54, 61, 64, 65 | syl12anc 836 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ) โง (๐ก โ ๐ด โง โ โ ๐ต)) โ
(((normโโ๐ก) โค (๐ ยท
(normโโ(๐ก +โ โ))) โง (normโโโ) โค (๐ ยท
(normโโ(๐ก +โ โ)))) โ
((normโโ๐ก) + (normโโโ)) โค ((๐ ยท
(normโโ(๐ก +โ โ))) + (๐ ยท
(normโโ(๐ก +โ โ)))))) |
67 | 66 | adantll 713 |
. . . . . . . . . 10
โข ((((๐ด โฉ ๐ต) = 0โ โง (๐ โ โ โง ๐ โ โ)) โง (๐ก โ ๐ด โง โ โ ๐ต)) โ
(((normโโ๐ก) โค (๐ ยท
(normโโ(๐ก +โ โ))) โง (normโโโ) โค (๐ ยท
(normโโ(๐ก +โ โ)))) โ
((normโโ๐ก) + (normโโโ)) โค ((๐ ยท
(normโโ(๐ก +โ โ))) + (๐ ยท
(normโโ(๐ก +โ โ)))))) |
68 | 1, 2, 4 | cdj3lem2 31419 |
. . . . . . . . . . . . . . . 16
โข ((๐ก โ ๐ด โง โ โ ๐ต โง (๐ด โฉ ๐ต) = 0โ) โ (๐โ(๐ก +โ โ)) = ๐ก) |
69 | 68 | fveq2d 6851 |
. . . . . . . . . . . . . . 15
โข ((๐ก โ ๐ด โง โ โ ๐ต โง (๐ด โฉ ๐ต) = 0โ) โ
(normโโ(๐โ(๐ก +โ โ))) = (normโโ๐ก)) |
70 | 69 | breq1d 5120 |
. . . . . . . . . . . . . 14
โข ((๐ก โ ๐ด โง โ โ ๐ต โง (๐ด โฉ ๐ต) = 0โ) โ
((normโโ(๐โ(๐ก +โ โ))) โค (๐ ยท
(normโโ(๐ก +โ โ))) โ
(normโโ๐ก) โค (๐ ยท
(normโโ(๐ก +โ โ))))) |
71 | 1, 2, 8 | cdj3lem3 31422 |
. . . . . . . . . . . . . . . 16
โข ((๐ก โ ๐ด โง โ โ ๐ต โง (๐ด โฉ ๐ต) = 0โ) โ (๐โ(๐ก +โ โ)) = โ) |
72 | 71 | fveq2d 6851 |
. . . . . . . . . . . . . . 15
โข ((๐ก โ ๐ด โง โ โ ๐ต โง (๐ด โฉ ๐ต) = 0โ) โ
(normโโ(๐โ(๐ก +โ โ))) = (normโโโ)) |
73 | 72 | breq1d 5120 |
. . . . . . . . . . . . . 14
โข ((๐ก โ ๐ด โง โ โ ๐ต โง (๐ด โฉ ๐ต) = 0โ) โ
((normโโ(๐โ(๐ก +โ โ))) โค (๐ ยท
(normโโ(๐ก +โ โ))) โ
(normโโโ) โค (๐ ยท
(normโโ(๐ก +โ โ))))) |
74 | 70, 73 | anbi12d 632 |
. . . . . . . . . . . . 13
โข ((๐ก โ ๐ด โง โ โ ๐ต โง (๐ด โฉ ๐ต) = 0โ) โ
(((normโโ(๐โ(๐ก +โ โ))) โค (๐ ยท
(normโโ(๐ก +โ โ))) โง
(normโโ(๐โ(๐ก +โ โ))) โค (๐ ยท
(normโโ(๐ก +โ โ)))) โ
((normโโ๐ก) โค (๐ ยท
(normโโ(๐ก +โ โ))) โง (normโโโ) โค (๐ ยท
(normโโ(๐ก +โ โ)))))) |
75 | 74 | 3expa 1119 |
. . . . . . . . . . . 12
โข (((๐ก โ ๐ด โง โ โ ๐ต) โง (๐ด โฉ ๐ต) = 0โ) โ
(((normโโ(๐โ(๐ก +โ โ))) โค (๐ ยท
(normโโ(๐ก +โ โ))) โง
(normโโ(๐โ(๐ก +โ โ))) โค (๐ ยท
(normโโ(๐ก +โ โ)))) โ
((normโโ๐ก) โค (๐ ยท
(normโโ(๐ก +โ โ))) โง (normโโโ) โค (๐ ยท
(normโโ(๐ก +โ โ)))))) |
76 | 75 | ancoms 460 |
. . . . . . . . . . 11
โข (((๐ด โฉ ๐ต) = 0โ โง (๐ก โ ๐ด โง โ โ ๐ต)) โ
(((normโโ(๐โ(๐ก +โ โ))) โค (๐ ยท
(normโโ(๐ก +โ โ))) โง
(normโโ(๐โ(๐ก +โ โ))) โค (๐ ยท
(normโโ(๐ก +โ โ)))) โ
((normโโ๐ก) โค (๐ ยท
(normโโ(๐ก +โ โ))) โง (normโโโ) โค (๐ ยท
(normโโ(๐ก +โ โ)))))) |
77 | 76 | adantlr 714 |
. . . . . . . . . 10
โข ((((๐ด โฉ ๐ต) = 0โ โง (๐ โ โ โง ๐ โ โ)) โง (๐ก โ ๐ด โง โ โ ๐ต)) โ
(((normโโ(๐โ(๐ก +โ โ))) โค (๐ ยท
(normโโ(๐ก +โ โ))) โง
(normโโ(๐โ(๐ก +โ โ))) โค (๐ ยท
(normโโ(๐ก +โ โ)))) โ
((normโโ๐ก) โค (๐ ยท
(normโโ(๐ก +โ โ))) โง (normโโโ) โค (๐ ยท
(normโโ(๐ก +โ โ)))))) |
78 | | recn 11148 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ๐ โ
โ) |
79 | | recn 11148 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ๐ โ
โ) |
80 | 58 | recnd 11190 |
. . . . . . . . . . . . . 14
โข ((๐ก โ ๐ด โง โ โ ๐ต) โ
(normโโ(๐ก +โ โ)) โ โ) |
81 | | adddir 11153 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐ โ โ โง
(normโโ(๐ก +โ โ)) โ โ) โ ((๐ + ๐) ยท
(normโโ(๐ก +โ โ))) = ((๐ ยท
(normโโ(๐ก +โ โ))) + (๐ ยท
(normโโ(๐ก +โ โ))))) |
82 | 78, 79, 80, 81 | syl3an 1161 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ โ โ โง (๐ก โ ๐ด โง โ โ ๐ต)) โ ((๐ + ๐) ยท
(normโโ(๐ก +โ โ))) = ((๐ ยท
(normโโ(๐ก +โ โ))) + (๐ ยท
(normโโ(๐ก +โ โ))))) |
83 | 82 | 3expa 1119 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐ โ โ) โง (๐ก โ ๐ด โง โ โ ๐ต)) โ ((๐ + ๐) ยท
(normโโ(๐ก +โ โ))) = ((๐ ยท
(normโโ(๐ก +โ โ))) + (๐ ยท
(normโโ(๐ก +โ โ))))) |
84 | 83 | breq2d 5122 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐ โ โ) โง (๐ก โ ๐ด โง โ โ ๐ต)) โ
(((normโโ๐ก) + (normโโโ)) โค ((๐ + ๐) ยท
(normโโ(๐ก +โ โ))) โ
((normโโ๐ก) + (normโโโ)) โค ((๐ ยท
(normโโ(๐ก +โ โ))) + (๐ ยท
(normโโ(๐ก +โ โ)))))) |
85 | 84 | adantll 713 |
. . . . . . . . . 10
โข ((((๐ด โฉ ๐ต) = 0โ โง (๐ โ โ โง ๐ โ โ)) โง (๐ก โ ๐ด โง โ โ ๐ต)) โ
(((normโโ๐ก) + (normโโโ)) โค ((๐ + ๐) ยท
(normโโ(๐ก +โ โ))) โ
((normโโ๐ก) + (normโโโ)) โค ((๐ ยท
(normโโ(๐ก +โ โ))) + (๐ ยท
(normโโ(๐ก +โ โ)))))) |
86 | 67, 77, 85 | 3imtr4d 294 |
. . . . . . . . 9
โข ((((๐ด โฉ ๐ต) = 0โ โง (๐ โ โ โง ๐ โ โ)) โง (๐ก โ ๐ด โง โ โ ๐ต)) โ
(((normโโ(๐โ(๐ก +โ โ))) โค (๐ ยท
(normโโ(๐ก +โ โ))) โง
(normโโ(๐โ(๐ก +โ โ))) โค (๐ ยท
(normโโ(๐ก +โ โ)))) โ
((normโโ๐ก) + (normโโโ)) โค ((๐ + ๐) ยท
(normโโ(๐ก +โ โ))))) |
87 | 46, 86 | syld 47 |
. . . . . . . 8
โข ((((๐ด โฉ ๐ต) = 0โ โง (๐ โ โ โง ๐ โ โ)) โง (๐ก โ ๐ด โง โ โ ๐ต)) โ ((โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข)) โง โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข))) โ
((normโโ๐ก) + (normโโโ)) โค ((๐ + ๐) ยท
(normโโ(๐ก +โ โ))))) |
88 | 87 | ralrimdvva 3204 |
. . . . . . 7
โข (((๐ด โฉ ๐ต) = 0โ โง (๐ โ โ โง ๐ โ โ)) โ
((โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข)) โง โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข))) โ โ๐ก โ ๐ด โโ โ ๐ต ((normโโ๐ก) +
(normโโโ)) โค ((๐ + ๐) ยท
(normโโ(๐ก +โ โ))))) |
89 | | readdcl 11141 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ โ) โ (๐ + ๐) โ โ) |
90 | | breq2 5114 |
. . . . . . . . . . . 12
โข (๐ฃ = (๐ + ๐) โ (0 < ๐ฃ โ 0 < (๐ + ๐))) |
91 | | fveq2 6847 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ = ๐ก โ (normโโ๐ฅ) =
(normโโ๐ก)) |
92 | 91 | oveq1d 7377 |
. . . . . . . . . . . . . . 15
โข (๐ฅ = ๐ก โ ((normโโ๐ฅ) +
(normโโ๐ฆ)) = ((normโโ๐ก) +
(normโโ๐ฆ))) |
93 | | fvoveq1 7385 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ = ๐ก โ (normโโ(๐ฅ +โ ๐ฆ)) =
(normโโ(๐ก +โ ๐ฆ))) |
94 | 93 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
โข (๐ฅ = ๐ก โ (๐ฃ ยท
(normโโ(๐ฅ +โ ๐ฆ))) = (๐ฃ ยท
(normโโ(๐ก +โ ๐ฆ)))) |
95 | 92, 94 | breq12d 5123 |
. . . . . . . . . . . . . 14
โข (๐ฅ = ๐ก โ
(((normโโ๐ฅ) + (normโโ๐ฆ)) โค (๐ฃ ยท
(normโโ(๐ฅ +โ ๐ฆ))) โ
((normโโ๐ก) + (normโโ๐ฆ)) โค (๐ฃ ยท
(normโโ(๐ก +โ ๐ฆ))))) |
96 | | fveq2 6847 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ = โ โ (normโโ๐ฆ) =
(normโโโ)) |
97 | 96 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
โข (๐ฆ = โ โ ((normโโ๐ก) +
(normโโ๐ฆ)) = ((normโโ๐ก) +
(normโโโ))) |
98 | | oveq2 7370 |
. . . . . . . . . . . . . . . . 17
โข (๐ฆ = โ โ (๐ก +โ ๐ฆ) = (๐ก +โ โ)) |
99 | 98 | fveq2d 6851 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ = โ โ (normโโ(๐ก +โ ๐ฆ)) =
(normโโ(๐ก +โ โ))) |
100 | 99 | oveq2d 7378 |
. . . . . . . . . . . . . . 15
โข (๐ฆ = โ โ (๐ฃ ยท
(normโโ(๐ก +โ ๐ฆ))) = (๐ฃ ยท
(normโโ(๐ก +โ โ)))) |
101 | 97, 100 | breq12d 5123 |
. . . . . . . . . . . . . 14
โข (๐ฆ = โ โ (((normโโ๐ก) +
(normโโ๐ฆ)) โค (๐ฃ ยท
(normโโ(๐ก +โ ๐ฆ))) โ
((normโโ๐ก) + (normโโโ)) โค (๐ฃ ยท
(normโโ(๐ก +โ โ))))) |
102 | 95, 101 | cbvral2vw 3230 |
. . . . . . . . . . . . 13
โข
(โ๐ฅ โ
๐ด โ๐ฆ โ ๐ต ((normโโ๐ฅ) +
(normโโ๐ฆ)) โค (๐ฃ ยท
(normโโ(๐ฅ +โ ๐ฆ))) โ โ๐ก โ ๐ด โโ โ ๐ต ((normโโ๐ก) +
(normโโโ)) โค (๐ฃ ยท
(normโโ(๐ก +โ โ)))) |
103 | | oveq1 7369 |
. . . . . . . . . . . . . . 15
โข (๐ฃ = (๐ + ๐) โ (๐ฃ ยท
(normโโ(๐ก +โ โ))) = ((๐ + ๐) ยท
(normโโ(๐ก +โ โ)))) |
104 | 103 | breq2d 5122 |
. . . . . . . . . . . . . 14
โข (๐ฃ = (๐ + ๐) โ
(((normโโ๐ก) + (normโโโ)) โค (๐ฃ ยท
(normโโ(๐ก +โ โ))) โ
((normโโ๐ก) + (normโโโ)) โค ((๐ + ๐) ยท
(normโโ(๐ก +โ โ))))) |
105 | 104 | 2ralbidv 3213 |
. . . . . . . . . . . . 13
โข (๐ฃ = (๐ + ๐) โ (โ๐ก โ ๐ด โโ โ ๐ต ((normโโ๐ก) +
(normโโโ)) โค (๐ฃ ยท
(normโโ(๐ก +โ โ))) โ โ๐ก โ ๐ด โโ โ ๐ต ((normโโ๐ก) +
(normโโโ)) โค ((๐ + ๐) ยท
(normโโ(๐ก +โ โ))))) |
106 | 102, 105 | bitrid 283 |
. . . . . . . . . . . 12
โข (๐ฃ = (๐ + ๐) โ (โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ((normโโ๐ฅ) +
(normโโ๐ฆ)) โค (๐ฃ ยท
(normโโ(๐ฅ +โ ๐ฆ))) โ โ๐ก โ ๐ด โโ โ ๐ต ((normโโ๐ก) +
(normโโโ)) โค ((๐ + ๐) ยท
(normโโ(๐ก +โ โ))))) |
107 | 90, 106 | anbi12d 632 |
. . . . . . . . . . 11
โข (๐ฃ = (๐ + ๐) โ ((0 < ๐ฃ โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ((normโโ๐ฅ) +
(normโโ๐ฆ)) โค (๐ฃ ยท
(normโโ(๐ฅ +โ ๐ฆ)))) โ (0 < (๐ + ๐) โง โ๐ก โ ๐ด โโ โ ๐ต ((normโโ๐ก) +
(normโโโ)) โค ((๐ + ๐) ยท
(normโโ(๐ก +โ โ)))))) |
108 | 107 | rspcev 3584 |
. . . . . . . . . 10
โข (((๐ + ๐) โ โ โง (0 < (๐ + ๐) โง โ๐ก โ ๐ด โโ โ ๐ต ((normโโ๐ก) +
(normโโโ)) โค ((๐ + ๐) ยท
(normโโ(๐ก +โ โ))))) โ โ๐ฃ โ โ (0 < ๐ฃ โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ((normโโ๐ฅ) +
(normโโ๐ฆ)) โค (๐ฃ ยท
(normโโ(๐ฅ +โ ๐ฆ))))) |
109 | 108 | ex 414 |
. . . . . . . . 9
โข ((๐ + ๐) โ โ โ ((0 < (๐ + ๐) โง โ๐ก โ ๐ด โโ โ ๐ต ((normโโ๐ก) +
(normโโโ)) โค ((๐ + ๐) ยท
(normโโ(๐ก +โ โ)))) โ โ๐ฃ โ โ (0 < ๐ฃ โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ((normโโ๐ฅ) +
(normโโ๐ฆ)) โค (๐ฃ ยท
(normโโ(๐ฅ +โ ๐ฆ)))))) |
110 | 89, 109 | syl 17 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โ) โ ((0 <
(๐ + ๐) โง โ๐ก โ ๐ด โโ โ ๐ต ((normโโ๐ก) +
(normโโโ)) โค ((๐ + ๐) ยท
(normโโ(๐ก +โ โ)))) โ โ๐ฃ โ โ (0 < ๐ฃ โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ((normโโ๐ฅ) +
(normโโ๐ฆ)) โค (๐ฃ ยท
(normโโ(๐ฅ +โ ๐ฆ)))))) |
111 | 110 | adantl 483 |
. . . . . . 7
โข (((๐ด โฉ ๐ต) = 0โ โง (๐ โ โ โง ๐ โ โ)) โ ((0
< (๐ + ๐) โง โ๐ก โ ๐ด โโ โ ๐ต ((normโโ๐ก) +
(normโโโ)) โค ((๐ + ๐) ยท
(normโโ(๐ก +โ โ)))) โ โ๐ฃ โ โ (0 < ๐ฃ โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ((normโโ๐ฅ) +
(normโโ๐ฆ)) โค (๐ฃ ยท
(normโโ(๐ฅ +โ ๐ฆ)))))) |
112 | 33, 88, 111 | syl2and 609 |
. . . . . 6
โข (((๐ด โฉ ๐ต) = 0โ โง (๐ โ โ โง ๐ โ โ)) โ (((0
< ๐ โง 0 < ๐) โง (โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข)) โง โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข)))) โ โ๐ฃ โ โ (0 < ๐ฃ โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ((normโโ๐ฅ) +
(normโโ๐ฆ)) โค (๐ฃ ยท
(normโโ(๐ฅ +โ ๐ฆ)))))) |
113 | 30, 112 | biimtrid 241 |
. . . . 5
โข (((๐ด โฉ ๐ต) = 0โ โง (๐ โ โ โง ๐ โ โ)) โ (((0
< ๐ โง โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข))) โง (0 < ๐ โง โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข)))) โ โ๐ฃ โ โ (0 < ๐ฃ โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ((normโโ๐ฅ) +
(normโโ๐ฆ)) โค (๐ฃ ยท
(normโโ(๐ฅ +โ ๐ฆ)))))) |
114 | 113 | rexlimdvva 3206 |
. . . 4
โข ((๐ด โฉ ๐ต) = 0โ โ (โ๐ โ โ โ๐ โ โ ((0 < ๐ โง โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข))) โง (0 < ๐ โง โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ ยท
(normโโ๐ข)))) โ โ๐ฃ โ โ (0 < ๐ฃ โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ((normโโ๐ฅ) +
(normโโ๐ฆ)) โค (๐ฃ ยท
(normโโ(๐ฅ +โ ๐ฆ)))))) |
115 | 29, 114 | biimtrid 241 |
. . 3
โข ((๐ด โฉ ๐ต) = 0โ โ ((๐ โง ๐) โ โ๐ฃ โ โ (0 < ๐ฃ โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ((normโโ๐ฅ) +
(normโโ๐ฆ)) โค (๐ฃ ยท
(normโโ(๐ฅ +โ ๐ฆ)))))) |
116 | 115 | 3impib 1117 |
. 2
โข (((๐ด โฉ ๐ต) = 0โ โง ๐ โง ๐) โ โ๐ฃ โ โ (0 < ๐ฃ โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ((normโโ๐ฅ) +
(normโโ๐ฆ)) โค (๐ฃ ยท
(normโโ(๐ฅ +โ ๐ฆ))))) |
117 | 12, 116 | impbii 208 |
1
โข
(โ๐ฃ โ
โ (0 < ๐ฃ โง
โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ((normโโ๐ฅ) +
(normโโ๐ฆ)) โค (๐ฃ ยท
(normโโ(๐ฅ +โ ๐ฆ)))) โ ((๐ด โฉ ๐ต) = 0โ โง ๐ โง ๐)) |