Step | Hyp | Ref
| Expression |
1 | | cdj3lem2.1 |
. . 3
โข ๐ด โ
Sโ |
2 | | cdj3lem2.2 |
. . 3
โข ๐ต โ
Sโ |
3 | 1, 2 | cdj3lem1 31687 |
. 2
โข
(โ๐ฃ โ
โ (0 < ๐ฃ โง
โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ((normโโ๐ฅ) +
(normโโ๐ฆ)) โค (๐ฃ ยท
(normโโ(๐ฅ +โ ๐ฆ)))) โ (๐ด โฉ ๐ต) = 0โ) |
4 | 1, 2 | shseli 30569 |
. . . . . . . 8
โข (๐ข โ (๐ด +โ ๐ต) โ โ๐ก โ ๐ด โโ โ ๐ต ๐ข = (๐ก +โ โ)) |
5 | 4 | biimpi 215 |
. . . . . . 7
โข (๐ข โ (๐ด +โ ๐ต) โ โ๐ก โ ๐ด โโ โ ๐ต ๐ข = (๐ก +โ โ)) |
6 | | fveq2 6892 |
. . . . . . . . . . . . . 14
โข (๐ฅ = ๐ก โ (normโโ๐ฅ) =
(normโโ๐ก)) |
7 | 6 | oveq1d 7424 |
. . . . . . . . . . . . 13
โข (๐ฅ = ๐ก โ ((normโโ๐ฅ) +
(normโโ๐ฆ)) = ((normโโ๐ก) +
(normโโ๐ฆ))) |
8 | | fvoveq1 7432 |
. . . . . . . . . . . . . 14
โข (๐ฅ = ๐ก โ (normโโ(๐ฅ +โ ๐ฆ)) =
(normโโ(๐ก +โ ๐ฆ))) |
9 | 8 | oveq2d 7425 |
. . . . . . . . . . . . 13
โข (๐ฅ = ๐ก โ (๐ฃ ยท
(normโโ(๐ฅ +โ ๐ฆ))) = (๐ฃ ยท
(normโโ(๐ก +โ ๐ฆ)))) |
10 | 7, 9 | breq12d 5162 |
. . . . . . . . . . . 12
โข (๐ฅ = ๐ก โ
(((normโโ๐ฅ) + (normโโ๐ฆ)) โค (๐ฃ ยท
(normโโ(๐ฅ +โ ๐ฆ))) โ
((normโโ๐ก) + (normโโ๐ฆ)) โค (๐ฃ ยท
(normโโ(๐ก +โ ๐ฆ))))) |
11 | | fveq2 6892 |
. . . . . . . . . . . . . 14
โข (๐ฆ = โ โ (normโโ๐ฆ) =
(normโโโ)) |
12 | 11 | oveq2d 7425 |
. . . . . . . . . . . . 13
โข (๐ฆ = โ โ ((normโโ๐ก) +
(normโโ๐ฆ)) = ((normโโ๐ก) +
(normโโโ))) |
13 | | oveq2 7417 |
. . . . . . . . . . . . . . 15
โข (๐ฆ = โ โ (๐ก +โ ๐ฆ) = (๐ก +โ โ)) |
14 | 13 | fveq2d 6896 |
. . . . . . . . . . . . . 14
โข (๐ฆ = โ โ (normโโ(๐ก +โ ๐ฆ)) =
(normโโ(๐ก +โ โ))) |
15 | 14 | oveq2d 7425 |
. . . . . . . . . . . . 13
โข (๐ฆ = โ โ (๐ฃ ยท
(normโโ(๐ก +โ ๐ฆ))) = (๐ฃ ยท
(normโโ(๐ก +โ โ)))) |
16 | 12, 15 | breq12d 5162 |
. . . . . . . . . . . 12
โข (๐ฆ = โ โ (((normโโ๐ก) +
(normโโ๐ฆ)) โค (๐ฃ ยท
(normโโ(๐ก +โ ๐ฆ))) โ
((normโโ๐ก) + (normโโโ)) โค (๐ฃ ยท
(normโโ(๐ก +โ โ))))) |
17 | 10, 16 | rspc2v 3623 |
. . . . . . . . . . 11
โข ((๐ก โ ๐ด โง โ โ ๐ต) โ (โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ((normโโ๐ฅ) +
(normโโ๐ฆ)) โค (๐ฃ ยท
(normโโ(๐ฅ +โ ๐ฆ))) โ
((normโโ๐ก) + (normโโโ)) โค (๐ฃ ยท
(normโโ(๐ก +โ โ))))) |
18 | | cdj3lem2.3 |
. . . . . . . . . . . . . . . . . 18
โข ๐ = (๐ฅ โ (๐ด +โ ๐ต) โฆ (โฉ๐ง โ ๐ด โ๐ค โ ๐ต ๐ฅ = (๐ง +โ ๐ค))) |
19 | 1, 2, 18 | cdj3lem2 31688 |
. . . . . . . . . . . . . . . . 17
โข ((๐ก โ ๐ด โง โ โ ๐ต โง (๐ด โฉ ๐ต) = 0โ) โ (๐โ(๐ก +โ โ)) = ๐ก) |
20 | 19 | 3expa 1119 |
. . . . . . . . . . . . . . . 16
โข (((๐ก โ ๐ด โง โ โ ๐ต) โง (๐ด โฉ ๐ต) = 0โ) โ (๐โ(๐ก +โ โ)) = ๐ก) |
21 | 20 | fveq2d 6896 |
. . . . . . . . . . . . . . 15
โข (((๐ก โ ๐ด โง โ โ ๐ต) โง (๐ด โฉ ๐ต) = 0โ) โ
(normโโ(๐โ(๐ก +โ โ))) = (normโโ๐ก)) |
22 | 21 | ad2ant2r 746 |
. . . . . . . . . . . . . 14
โข ((((๐ก โ ๐ด โง โ โ ๐ต) โง
((normโโ๐ก) + (normโโโ)) โค (๐ฃ ยท
(normโโ(๐ก +โ โ)))) โง ((๐ด โฉ ๐ต) = 0โ โง ๐ฃ โ โ)) โ
(normโโ(๐โ(๐ก +โ โ))) = (normโโ๐ก)) |
23 | 2 | sheli 30467 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (โ โ ๐ต โ โ โ โ) |
24 | | normge0 30379 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (โ โ โ โ 0 โค
(normโโโ)) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
โข (โ โ ๐ต โ 0 โค
(normโโโ)) |
26 | 25 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ก โ ๐ด โง โ โ ๐ต) โ 0 โค
(normโโโ)) |
27 | 1 | sheli 30467 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ก โ ๐ด โ ๐ก โ โ) |
28 | | normcl 30378 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ก โ โ โ
(normโโ๐ก) โ โ) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ก โ ๐ด โ (normโโ๐ก) โ
โ) |
30 | | normcl 30378 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (โ โ โ โ
(normโโโ) โ โ) |
31 | 23, 30 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
โข (โ โ ๐ต โ (normโโโ) โ
โ) |
32 | | addge01 11724 |
. . . . . . . . . . . . . . . . . . . . 21
โข
(((normโโ๐ก) โ โ โง
(normโโโ) โ โ) โ (0 โค
(normโโโ) โ (normโโ๐ก) โค
((normโโ๐ก) + (normโโโ)))) |
33 | 29, 31, 32 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ก โ ๐ด โง โ โ ๐ต) โ (0 โค
(normโโโ) โ (normโโ๐ก) โค
((normโโ๐ก) + (normโโโ)))) |
34 | 26, 33 | mpbid 231 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ก โ ๐ด โง โ โ ๐ต) โ
(normโโ๐ก) โค ((normโโ๐ก) +
(normโโโ))) |
35 | 34 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ก โ ๐ด โง โ โ ๐ต) โง ๐ฃ โ โ) โ
(normโโ๐ก) โค ((normโโ๐ก) +
(normโโโ))) |
36 | 29 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ก โ ๐ด โง โ โ ๐ต) โง ๐ฃ โ โ) โ
(normโโ๐ก) โ โ) |
37 | | readdcl 11193 |
. . . . . . . . . . . . . . . . . . . . 21
โข
(((normโโ๐ก) โ โ โง
(normโโโ) โ โ) โ
((normโโ๐ก) + (normโโโ)) โ
โ) |
38 | 29, 31, 37 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ก โ ๐ด โง โ โ ๐ต) โ
((normโโ๐ก) + (normโโโ)) โ
โ) |
39 | 38 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ก โ ๐ด โง โ โ ๐ต) โง ๐ฃ โ โ) โ
((normโโ๐ก) + (normโโโ)) โ
โ) |
40 | | hvaddcl 30265 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ก โ โ โง โ โ โ) โ (๐ก +โ โ) โ
โ) |
41 | 27, 23, 40 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ก โ ๐ด โง โ โ ๐ต) โ (๐ก +โ โ) โ โ) |
42 | | normcl 30378 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ก +โ โ) โ โ โ
(normโโ(๐ก +โ โ)) โ โ) |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ก โ ๐ด โง โ โ ๐ต) โ
(normโโ(๐ก +โ โ)) โ โ) |
44 | | remulcl 11195 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ฃ โ โ โง
(normโโ(๐ก +โ โ)) โ โ) โ (๐ฃ ยท
(normโโ(๐ก +โ โ))) โ โ) |
45 | 43, 44 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ฃ โ โ โง (๐ก โ ๐ด โง โ โ ๐ต)) โ (๐ฃ ยท
(normโโ(๐ก +โ โ))) โ โ) |
46 | 45 | ancoms 460 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ก โ ๐ด โง โ โ ๐ต) โง ๐ฃ โ โ) โ (๐ฃ ยท
(normโโ(๐ก +โ โ))) โ โ) |
47 | | letr 11308 |
. . . . . . . . . . . . . . . . . . 19
โข
(((normโโ๐ก) โ โ โง
((normโโ๐ก) + (normโโโ)) โ โ โง (๐ฃ ยท
(normโโ(๐ก +โ โ))) โ โ) โ
(((normโโ๐ก) โค ((normโโ๐ก) +
(normโโโ)) โง ((normโโ๐ก) +
(normโโโ)) โค (๐ฃ ยท
(normโโ(๐ก +โ โ)))) โ
(normโโ๐ก) โค (๐ฃ ยท
(normโโ(๐ก +โ โ))))) |
48 | 36, 39, 46, 47 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ก โ ๐ด โง โ โ ๐ต) โง ๐ฃ โ โ) โ
(((normโโ๐ก) โค ((normโโ๐ก) +
(normโโโ)) โง ((normโโ๐ก) +
(normโโโ)) โค (๐ฃ ยท
(normโโ(๐ก +โ โ)))) โ
(normโโ๐ก) โค (๐ฃ ยท
(normโโ(๐ก +โ โ))))) |
49 | 35, 48 | mpand 694 |
. . . . . . . . . . . . . . . . 17
โข (((๐ก โ ๐ด โง โ โ ๐ต) โง ๐ฃ โ โ) โ
(((normโโ๐ก) + (normโโโ)) โค (๐ฃ ยท
(normโโ(๐ก +โ โ))) โ
(normโโ๐ก) โค (๐ฃ ยท
(normโโ(๐ก +โ โ))))) |
50 | 49 | imp 408 |
. . . . . . . . . . . . . . . 16
โข ((((๐ก โ ๐ด โง โ โ ๐ต) โง ๐ฃ โ โ) โง
((normโโ๐ก) + (normโโโ)) โค (๐ฃ ยท
(normโโ(๐ก +โ โ)))) โ
(normโโ๐ก) โค (๐ฃ ยท
(normโโ(๐ก +โ โ)))) |
51 | 50 | an32s 651 |
. . . . . . . . . . . . . . 15
โข ((((๐ก โ ๐ด โง โ โ ๐ต) โง
((normโโ๐ก) + (normโโโ)) โค (๐ฃ ยท
(normโโ(๐ก +โ โ)))) โง ๐ฃ โ โ) โ
(normโโ๐ก) โค (๐ฃ ยท
(normโโ(๐ก +โ โ)))) |
52 | 51 | adantrl 715 |
. . . . . . . . . . . . . 14
โข ((((๐ก โ ๐ด โง โ โ ๐ต) โง
((normโโ๐ก) + (normโโโ)) โค (๐ฃ ยท
(normโโ(๐ก +โ โ)))) โง ((๐ด โฉ ๐ต) = 0โ โง ๐ฃ โ โ)) โ
(normโโ๐ก) โค (๐ฃ ยท
(normโโ(๐ก +โ โ)))) |
53 | 22, 52 | eqbrtrd 5171 |
. . . . . . . . . . . . 13
โข ((((๐ก โ ๐ด โง โ โ ๐ต) โง
((normโโ๐ก) + (normโโโ)) โค (๐ฃ ยท
(normโโ(๐ก +โ โ)))) โง ((๐ด โฉ ๐ต) = 0โ โง ๐ฃ โ โ)) โ
(normโโ(๐โ(๐ก +โ โ))) โค (๐ฃ ยท
(normโโ(๐ก +โ โ)))) |
54 | | 2fveq3 6897 |
. . . . . . . . . . . . . 14
โข (๐ข = (๐ก +โ โ) โ (normโโ(๐โ๐ข)) = (normโโ(๐โ(๐ก +โ โ)))) |
55 | | fveq2 6892 |
. . . . . . . . . . . . . . 15
โข (๐ข = (๐ก +โ โ) โ (normโโ๐ข) =
(normโโ(๐ก +โ โ))) |
56 | 55 | oveq2d 7425 |
. . . . . . . . . . . . . 14
โข (๐ข = (๐ก +โ โ) โ (๐ฃ ยท
(normโโ๐ข)) = (๐ฃ ยท
(normโโ(๐ก +โ โ)))) |
57 | 54, 56 | breq12d 5162 |
. . . . . . . . . . . . 13
โข (๐ข = (๐ก +โ โ) โ
((normโโ(๐โ๐ข)) โค (๐ฃ ยท
(normโโ๐ข)) โ
(normโโ(๐โ(๐ก +โ โ))) โค (๐ฃ ยท
(normโโ(๐ก +โ โ))))) |
58 | 53, 57 | syl5ibrcom 246 |
. . . . . . . . . . . 12
โข ((((๐ก โ ๐ด โง โ โ ๐ต) โง
((normโโ๐ก) + (normโโโ)) โค (๐ฃ ยท
(normโโ(๐ก +โ โ)))) โง ((๐ด โฉ ๐ต) = 0โ โง ๐ฃ โ โ)) โ (๐ข = (๐ก +โ โ) โ (normโโ(๐โ๐ข)) โค (๐ฃ ยท
(normโโ๐ข)))) |
59 | 58 | exp31 421 |
. . . . . . . . . . 11
โข ((๐ก โ ๐ด โง โ โ ๐ต) โ
(((normโโ๐ก) + (normโโโ)) โค (๐ฃ ยท
(normโโ(๐ก +โ โ))) โ (((๐ด โฉ ๐ต) = 0โ โง ๐ฃ โ โ) โ (๐ข = (๐ก +โ โ) โ (normโโ(๐โ๐ข)) โค (๐ฃ ยท
(normโโ๐ข)))))) |
60 | 17, 59 | syld 47 |
. . . . . . . . . 10
โข ((๐ก โ ๐ด โง โ โ ๐ต) โ (โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ((normโโ๐ฅ) +
(normโโ๐ฆ)) โค (๐ฃ ยท
(normโโ(๐ฅ +โ ๐ฆ))) โ (((๐ด โฉ ๐ต) = 0โ โง ๐ฃ โ โ) โ (๐ข = (๐ก +โ โ) โ (normโโ(๐โ๐ข)) โค (๐ฃ ยท
(normโโ๐ข)))))) |
61 | 60 | com14 96 |
. . . . . . . . 9
โข (๐ข = (๐ก +โ โ) โ (โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ((normโโ๐ฅ) +
(normโโ๐ฆ)) โค (๐ฃ ยท
(normโโ(๐ฅ +โ ๐ฆ))) โ (((๐ด โฉ ๐ต) = 0โ โง ๐ฃ โ โ) โ ((๐ก โ ๐ด โง โ โ ๐ต) โ
(normโโ(๐โ๐ข)) โค (๐ฃ ยท
(normโโ๐ข)))))) |
62 | 61 | com4t 93 |
. . . . . . . 8
โข (((๐ด โฉ ๐ต) = 0โ โง ๐ฃ โ โ) โ ((๐ก โ ๐ด โง โ โ ๐ต) โ (๐ข = (๐ก +โ โ) โ (โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ((normโโ๐ฅ) +
(normโโ๐ฆ)) โค (๐ฃ ยท
(normโโ(๐ฅ +โ ๐ฆ))) โ
(normโโ(๐โ๐ข)) โค (๐ฃ ยท
(normโโ๐ข)))))) |
63 | 62 | rexlimdvv 3211 |
. . . . . . 7
โข (((๐ด โฉ ๐ต) = 0โ โง ๐ฃ โ โ) โ
(โ๐ก โ ๐ด โโ โ ๐ต ๐ข = (๐ก +โ โ) โ (โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ((normโโ๐ฅ) +
(normโโ๐ฆ)) โค (๐ฃ ยท
(normโโ(๐ฅ +โ ๐ฆ))) โ
(normโโ(๐โ๐ข)) โค (๐ฃ ยท
(normโโ๐ข))))) |
64 | 5, 63 | syl5com 31 |
. . . . . 6
โข (๐ข โ (๐ด +โ ๐ต) โ (((๐ด โฉ ๐ต) = 0โ โง ๐ฃ โ โ) โ
(โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ((normโโ๐ฅ) +
(normโโ๐ฆ)) โค (๐ฃ ยท
(normโโ(๐ฅ +โ ๐ฆ))) โ
(normโโ(๐โ๐ข)) โค (๐ฃ ยท
(normโโ๐ข))))) |
65 | 64 | com3l 89 |
. . . . 5
โข (((๐ด โฉ ๐ต) = 0โ โง ๐ฃ โ โ) โ
(โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ((normโโ๐ฅ) +
(normโโ๐ฆ)) โค (๐ฃ ยท
(normโโ(๐ฅ +โ ๐ฆ))) โ (๐ข โ (๐ด +โ ๐ต) โ
(normโโ(๐โ๐ข)) โค (๐ฃ ยท
(normโโ๐ข))))) |
66 | 65 | ralrimdv 3153 |
. . . 4
โข (((๐ด โฉ ๐ต) = 0โ โง ๐ฃ โ โ) โ
(โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ((normโโ๐ฅ) +
(normโโ๐ฆ)) โค (๐ฃ ยท
(normโโ(๐ฅ +โ ๐ฆ))) โ โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ฃ ยท
(normโโ๐ข)))) |
67 | 66 | anim2d 613 |
. . 3
โข (((๐ด โฉ ๐ต) = 0โ โง ๐ฃ โ โ) โ ((0 <
๐ฃ โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ((normโโ๐ฅ) +
(normโโ๐ฆ)) โค (๐ฃ ยท
(normโโ(๐ฅ +โ ๐ฆ)))) โ (0 < ๐ฃ โง โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ฃ ยท
(normโโ๐ข))))) |
68 | 67 | reximdva 3169 |
. 2
โข ((๐ด โฉ ๐ต) = 0โ โ (โ๐ฃ โ โ (0 < ๐ฃ โง โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ((normโโ๐ฅ) +
(normโโ๐ฆ)) โค (๐ฃ ยท
(normโโ(๐ฅ +โ ๐ฆ)))) โ โ๐ฃ โ โ (0 < ๐ฃ โง โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ฃ ยท
(normโโ๐ข))))) |
69 | 3, 68 | mpcom 38 |
1
โข
(โ๐ฃ โ
โ (0 < ๐ฃ โง
โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ((normโโ๐ฅ) +
(normโโ๐ฆ)) โค (๐ฃ ยท
(normโโ(๐ฅ +โ ๐ฆ)))) โ โ๐ฃ โ โ (0 < ๐ฃ โง โ๐ข โ (๐ด +โ ๐ต)(normโโ(๐โ๐ข)) โค (๐ฃ ยท
(normโโ๐ข)))) |