Step | Hyp | Ref
| Expression |
1 | | lncon.1 |
. . 3
โข (๐ โ ๐ถ โ ๐ โ โ) |
2 | | lncon.2 |
. . . 4
โข ((๐ โ ๐ถ โง ๐ฆ โ โ) โ (๐โ(๐โ๐ฆ)) โค (๐ ยท
(normโโ๐ฆ))) |
3 | 2 | ralrimiva 3140 |
. . 3
โข (๐ โ ๐ถ โ โ๐ฆ โ โ (๐โ(๐โ๐ฆ)) โค (๐ ยท
(normโโ๐ฆ))) |
4 | | oveq1 7368 |
. . . . . 6
โข (๐ฅ = ๐ โ (๐ฅ ยท
(normโโ๐ฆ)) = (๐ ยท
(normโโ๐ฆ))) |
5 | 4 | breq2d 5121 |
. . . . 5
โข (๐ฅ = ๐ โ ((๐โ(๐โ๐ฆ)) โค (๐ฅ ยท
(normโโ๐ฆ)) โ (๐โ(๐โ๐ฆ)) โค (๐ ยท
(normโโ๐ฆ)))) |
6 | 5 | ralbidv 3171 |
. . . 4
โข (๐ฅ = ๐ โ (โ๐ฆ โ โ (๐โ(๐โ๐ฆ)) โค (๐ฅ ยท
(normโโ๐ฆ)) โ โ๐ฆ โ โ (๐โ(๐โ๐ฆ)) โค (๐ ยท
(normโโ๐ฆ)))) |
7 | 6 | rspcev 3583 |
. . 3
โข ((๐ โ โ โง
โ๐ฆ โ โ
(๐โ(๐โ๐ฆ)) โค (๐ ยท
(normโโ๐ฆ))) โ โ๐ฅ โ โ โ๐ฆ โ โ (๐โ(๐โ๐ฆ)) โค (๐ฅ ยท
(normโโ๐ฆ))) |
8 | 1, 3, 7 | syl2anc 585 |
. 2
โข (๐ โ ๐ถ โ โ๐ฅ โ โ โ๐ฆ โ โ (๐โ(๐โ๐ฆ)) โค (๐ฅ ยท
(normโโ๐ฆ))) |
9 | | arch 12418 |
. . . . . 6
โข (๐ฅ โ โ โ
โ๐ โ โ
๐ฅ < ๐) |
10 | 9 | adantr 482 |
. . . . 5
โข ((๐ฅ โ โ โง
โ๐ฆ โ โ
(๐โ(๐โ๐ฆ)) โค (๐ฅ ยท
(normโโ๐ฆ))) โ โ๐ โ โ ๐ฅ < ๐) |
11 | | nnre 12168 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โ) |
12 | | simplll 774 |
. . . . . . . . . . . 12
โข ((((๐ฅ โ โ โง ๐ โ โ) โง ๐ฅ < ๐) โง ๐ฆ โ โ) โ ๐ฅ โ โ) |
13 | | simpllr 775 |
. . . . . . . . . . . 12
โข ((((๐ฅ โ โ โง ๐ โ โ) โง ๐ฅ < ๐) โง ๐ฆ โ โ) โ ๐ โ โ) |
14 | | normcl 30116 |
. . . . . . . . . . . . 13
โข (๐ฆ โ โ โ
(normโโ๐ฆ) โ โ) |
15 | 14 | adantl 483 |
. . . . . . . . . . . 12
โข ((((๐ฅ โ โ โง ๐ โ โ) โง ๐ฅ < ๐) โง ๐ฆ โ โ) โ
(normโโ๐ฆ) โ โ) |
16 | | normge0 30117 |
. . . . . . . . . . . . 13
โข (๐ฆ โ โ โ 0 โค
(normโโ๐ฆ)) |
17 | 16 | adantl 483 |
. . . . . . . . . . . 12
โข ((((๐ฅ โ โ โง ๐ โ โ) โง ๐ฅ < ๐) โง ๐ฆ โ โ) โ 0 โค
(normโโ๐ฆ)) |
18 | | ltle 11251 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ โ โง ๐ โ โ) โ (๐ฅ < ๐ โ ๐ฅ โค ๐)) |
19 | 18 | imp 408 |
. . . . . . . . . . . . 13
โข (((๐ฅ โ โ โง ๐ โ โ) โง ๐ฅ < ๐) โ ๐ฅ โค ๐) |
20 | 19 | adantr 482 |
. . . . . . . . . . . 12
โข ((((๐ฅ โ โ โง ๐ โ โ) โง ๐ฅ < ๐) โง ๐ฆ โ โ) โ ๐ฅ โค ๐) |
21 | 12, 13, 15, 17, 20 | lemul1ad 12102 |
. . . . . . . . . . 11
โข ((((๐ฅ โ โ โง ๐ โ โ) โง ๐ฅ < ๐) โง ๐ฆ โ โ) โ (๐ฅ ยท
(normโโ๐ฆ)) โค (๐ ยท
(normโโ๐ฆ))) |
22 | | lncon.4 |
. . . . . . . . . . . . 13
โข (๐ฆ โ โ โ (๐โ(๐โ๐ฆ)) โ โ) |
23 | 22 | adantl 483 |
. . . . . . . . . . . 12
โข ((((๐ฅ โ โ โง ๐ โ โ) โง ๐ฅ < ๐) โง ๐ฆ โ โ) โ (๐โ(๐โ๐ฆ)) โ โ) |
24 | | simpll 766 |
. . . . . . . . . . . . 13
โข (((๐ฅ โ โ โง ๐ โ โ) โง ๐ฅ < ๐) โ ๐ฅ โ โ) |
25 | | remulcl 11144 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โ โง
(normโโ๐ฆ) โ โ) โ (๐ฅ ยท
(normโโ๐ฆ)) โ โ) |
26 | 24, 14, 25 | syl2an 597 |
. . . . . . . . . . . 12
โข ((((๐ฅ โ โ โง ๐ โ โ) โง ๐ฅ < ๐) โง ๐ฆ โ โ) โ (๐ฅ ยท
(normโโ๐ฆ)) โ โ) |
27 | | simplr 768 |
. . . . . . . . . . . . 13
โข (((๐ฅ โ โ โง ๐ โ โ) โง ๐ฅ < ๐) โ ๐ โ โ) |
28 | | remulcl 11144 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง
(normโโ๐ฆ) โ โ) โ (๐ ยท
(normโโ๐ฆ)) โ โ) |
29 | 27, 14, 28 | syl2an 597 |
. . . . . . . . . . . 12
โข ((((๐ฅ โ โ โง ๐ โ โ) โง ๐ฅ < ๐) โง ๐ฆ โ โ) โ (๐ ยท
(normโโ๐ฆ)) โ โ) |
30 | | letr 11257 |
. . . . . . . . . . . 12
โข (((๐โ(๐โ๐ฆ)) โ โ โง (๐ฅ ยท
(normโโ๐ฆ)) โ โ โง (๐ ยท
(normโโ๐ฆ)) โ โ) โ (((๐โ(๐โ๐ฆ)) โค (๐ฅ ยท
(normโโ๐ฆ)) โง (๐ฅ ยท
(normโโ๐ฆ)) โค (๐ ยท
(normโโ๐ฆ))) โ (๐โ(๐โ๐ฆ)) โค (๐ ยท
(normโโ๐ฆ)))) |
31 | 23, 26, 29, 30 | syl3anc 1372 |
. . . . . . . . . . 11
โข ((((๐ฅ โ โ โง ๐ โ โ) โง ๐ฅ < ๐) โง ๐ฆ โ โ) โ (((๐โ(๐โ๐ฆ)) โค (๐ฅ ยท
(normโโ๐ฆ)) โง (๐ฅ ยท
(normโโ๐ฆ)) โค (๐ ยท
(normโโ๐ฆ))) โ (๐โ(๐โ๐ฆ)) โค (๐ ยท
(normโโ๐ฆ)))) |
32 | 21, 31 | mpan2d 693 |
. . . . . . . . . 10
โข ((((๐ฅ โ โ โง ๐ โ โ) โง ๐ฅ < ๐) โง ๐ฆ โ โ) โ ((๐โ(๐โ๐ฆ)) โค (๐ฅ ยท
(normโโ๐ฆ)) โ (๐โ(๐โ๐ฆ)) โค (๐ ยท
(normโโ๐ฆ)))) |
33 | 32 | ralimdva 3161 |
. . . . . . . . 9
โข (((๐ฅ โ โ โง ๐ โ โ) โง ๐ฅ < ๐) โ (โ๐ฆ โ โ (๐โ(๐โ๐ฆ)) โค (๐ฅ ยท
(normโโ๐ฆ)) โ โ๐ฆ โ โ (๐โ(๐โ๐ฆ)) โค (๐ ยท
(normโโ๐ฆ)))) |
34 | 33 | impancom 453 |
. . . . . . . 8
โข (((๐ฅ โ โ โง ๐ โ โ) โง
โ๐ฆ โ โ
(๐โ(๐โ๐ฆ)) โค (๐ฅ ยท
(normโโ๐ฆ))) โ (๐ฅ < ๐ โ โ๐ฆ โ โ (๐โ(๐โ๐ฆ)) โค (๐ ยท
(normโโ๐ฆ)))) |
35 | 34 | an32s 651 |
. . . . . . 7
โข (((๐ฅ โ โ โง
โ๐ฆ โ โ
(๐โ(๐โ๐ฆ)) โค (๐ฅ ยท
(normโโ๐ฆ))) โง ๐ โ โ) โ (๐ฅ < ๐ โ โ๐ฆ โ โ (๐โ(๐โ๐ฆ)) โค (๐ ยท
(normโโ๐ฆ)))) |
36 | 11, 35 | sylan2 594 |
. . . . . 6
โข (((๐ฅ โ โ โง
โ๐ฆ โ โ
(๐โ(๐โ๐ฆ)) โค (๐ฅ ยท
(normโโ๐ฆ))) โง ๐ โ โ) โ (๐ฅ < ๐ โ โ๐ฆ โ โ (๐โ(๐โ๐ฆ)) โค (๐ ยท
(normโโ๐ฆ)))) |
37 | 36 | reximdva 3162 |
. . . . 5
โข ((๐ฅ โ โ โง
โ๐ฆ โ โ
(๐โ(๐โ๐ฆ)) โค (๐ฅ ยท
(normโโ๐ฆ))) โ (โ๐ โ โ ๐ฅ < ๐ โ โ๐ โ โ โ๐ฆ โ โ (๐โ(๐โ๐ฆ)) โค (๐ ยท
(normโโ๐ฆ)))) |
38 | 10, 37 | mpd 15 |
. . . 4
โข ((๐ฅ โ โ โง
โ๐ฆ โ โ
(๐โ(๐โ๐ฆ)) โค (๐ฅ ยท
(normโโ๐ฆ))) โ โ๐ โ โ โ๐ฆ โ โ (๐โ(๐โ๐ฆ)) โค (๐ ยท
(normโโ๐ฆ))) |
39 | 38 | rexlimiva 3141 |
. . 3
โข
(โ๐ฅ โ
โ โ๐ฆ โ
โ (๐โ(๐โ๐ฆ)) โค (๐ฅ ยท
(normโโ๐ฆ)) โ โ๐ โ โ โ๐ฆ โ โ (๐โ(๐โ๐ฆ)) โค (๐ ยท
(normโโ๐ฆ))) |
40 | | simprr 772 |
. . . . . . . 8
โข (((๐ โ โ โง
โ๐ฆ โ โ
(๐โ(๐โ๐ฆ)) โค (๐ ยท
(normโโ๐ฆ))) โง (๐ฅ โ โ โง ๐ง โ โ+)) โ ๐ง โ
โ+) |
41 | | simpll 766 |
. . . . . . . . 9
โข (((๐ โ โ โง
โ๐ฆ โ โ
(๐โ(๐โ๐ฆ)) โค (๐ ยท
(normโโ๐ฆ))) โง (๐ฅ โ โ โง ๐ง โ โ+)) โ ๐ โ
โ) |
42 | 41 | nnrpd 12963 |
. . . . . . . 8
โข (((๐ โ โ โง
โ๐ฆ โ โ
(๐โ(๐โ๐ฆ)) โค (๐ ยท
(normโโ๐ฆ))) โง (๐ฅ โ โ โง ๐ง โ โ+)) โ ๐ โ
โ+) |
43 | 40, 42 | rpdivcld 12982 |
. . . . . . 7
โข (((๐ โ โ โง
โ๐ฆ โ โ
(๐โ(๐โ๐ฆ)) โค (๐ ยท
(normโโ๐ฆ))) โง (๐ฅ โ โ โง ๐ง โ โ+)) โ (๐ง / ๐) โ
โ+) |
44 | | simprr 772 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ((๐ฅ โ โ โง ๐ง โ โ+)
โง ๐ค โ โ))
โ ๐ค โ
โ) |
45 | | simprll 778 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ((๐ฅ โ โ โง ๐ง โ โ+)
โง ๐ค โ โ))
โ ๐ฅ โ
โ) |
46 | | hvsubcl 30008 |
. . . . . . . . . . . . . 14
โข ((๐ค โ โ โง ๐ฅ โ โ) โ (๐ค โโ
๐ฅ) โ
โ) |
47 | 44, 45, 46 | syl2anc 585 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ((๐ฅ โ โ โง ๐ง โ โ+)
โง ๐ค โ โ))
โ (๐ค
โโ ๐ฅ) โ โ) |
48 | | 2fveq3 6851 |
. . . . . . . . . . . . . . 15
โข (๐ฆ = (๐ค โโ ๐ฅ) โ (๐โ(๐โ๐ฆ)) = (๐โ(๐โ(๐ค โโ ๐ฅ)))) |
49 | | fveq2 6846 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ = (๐ค โโ ๐ฅ) โ
(normโโ๐ฆ) = (normโโ(๐ค โโ
๐ฅ))) |
50 | 49 | oveq2d 7377 |
. . . . . . . . . . . . . . 15
โข (๐ฆ = (๐ค โโ ๐ฅ) โ (๐ ยท
(normโโ๐ฆ)) = (๐ ยท
(normโโ(๐ค โโ ๐ฅ)))) |
51 | 48, 50 | breq12d 5122 |
. . . . . . . . . . . . . 14
โข (๐ฆ = (๐ค โโ ๐ฅ) โ ((๐โ(๐โ๐ฆ)) โค (๐ ยท
(normโโ๐ฆ)) โ (๐โ(๐โ(๐ค โโ ๐ฅ))) โค (๐ ยท
(normโโ(๐ค โโ ๐ฅ))))) |
52 | 51 | rspcva 3581 |
. . . . . . . . . . . . 13
โข (((๐ค โโ
๐ฅ) โ โ โง
โ๐ฆ โ โ
(๐โ(๐โ๐ฆ)) โค (๐ ยท
(normโโ๐ฆ))) โ (๐โ(๐โ(๐ค โโ ๐ฅ))) โค (๐ ยท
(normโโ(๐ค โโ ๐ฅ)))) |
53 | 47, 52 | sylan 581 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ((๐ฅ โ โ โง ๐ง โ โ+)
โง ๐ค โ โ))
โง โ๐ฆ โ
โ (๐โ(๐โ๐ฆ)) โค (๐ ยท
(normโโ๐ฆ))) โ (๐โ(๐โ(๐ค โโ ๐ฅ))) โค (๐ ยท
(normโโ(๐ค โโ ๐ฅ)))) |
54 | 53 | an32s 651 |
. . . . . . . . . . 11
โข (((๐ โ โ โง
โ๐ฆ โ โ
(๐โ(๐โ๐ฆ)) โค (๐ ยท
(normโโ๐ฆ))) โง ((๐ฅ โ โ โง ๐ง โ โ+) โง ๐ค โ โ)) โ (๐โ(๐โ(๐ค โโ ๐ฅ))) โค (๐ ยท
(normโโ(๐ค โโ ๐ฅ)))) |
55 | 48 | eleq1d 2819 |
. . . . . . . . . . . . . . 15
โข (๐ฆ = (๐ค โโ ๐ฅ) โ ((๐โ(๐โ๐ฆ)) โ โ โ (๐โ(๐โ(๐ค โโ ๐ฅ))) โ
โ)) |
56 | 55, 22 | vtoclga 3536 |
. . . . . . . . . . . . . 14
โข ((๐ค โโ
๐ฅ) โ โ โ
(๐โ(๐โ(๐ค โโ ๐ฅ))) โ
โ) |
57 | 47, 56 | syl 17 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ((๐ฅ โ โ โง ๐ง โ โ+)
โง ๐ค โ โ))
โ (๐โ(๐โ(๐ค โโ ๐ฅ))) โ
โ) |
58 | 11 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ((๐ฅ โ โ โง ๐ง โ โ+)
โง ๐ค โ โ))
โ ๐ โ
โ) |
59 | | normcl 30116 |
. . . . . . . . . . . . . . 15
โข ((๐ค โโ
๐ฅ) โ โ โ
(normโโ(๐ค โโ ๐ฅ)) โ
โ) |
60 | 47, 59 | syl 17 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ((๐ฅ โ โ โง ๐ง โ โ+)
โง ๐ค โ โ))
โ (normโโ(๐ค โโ ๐ฅ)) โ
โ) |
61 | | remulcl 11144 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง
(normโโ(๐ค โโ ๐ฅ)) โ โ) โ (๐ ยท
(normโโ(๐ค โโ ๐ฅ))) โ
โ) |
62 | 58, 60, 61 | syl2anc 585 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ((๐ฅ โ โ โง ๐ง โ โ+)
โง ๐ค โ โ))
โ (๐ ยท
(normโโ(๐ค โโ ๐ฅ))) โ
โ) |
63 | | simprlr 779 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ((๐ฅ โ โ โง ๐ง โ โ+)
โง ๐ค โ โ))
โ ๐ง โ
โ+) |
64 | 63 | rpred 12965 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ((๐ฅ โ โ โง ๐ง โ โ+)
โง ๐ค โ โ))
โ ๐ง โ
โ) |
65 | | lelttr 11253 |
. . . . . . . . . . . . 13
โข (((๐โ(๐โ(๐ค โโ ๐ฅ))) โ โ โง (๐ ยท
(normโโ(๐ค โโ ๐ฅ))) โ โ โง ๐ง โ โ) โ (((๐โ(๐โ(๐ค โโ ๐ฅ))) โค (๐ ยท
(normโโ(๐ค โโ ๐ฅ))) โง (๐ ยท
(normโโ(๐ค โโ ๐ฅ))) < ๐ง) โ (๐โ(๐โ(๐ค โโ ๐ฅ))) < ๐ง)) |
66 | 57, 62, 64, 65 | syl3anc 1372 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ((๐ฅ โ โ โง ๐ง โ โ+)
โง ๐ค โ โ))
โ (((๐โ(๐โ(๐ค โโ ๐ฅ))) โค (๐ ยท
(normโโ(๐ค โโ ๐ฅ))) โง (๐ ยท
(normโโ(๐ค โโ ๐ฅ))) < ๐ง) โ (๐โ(๐โ(๐ค โโ ๐ฅ))) < ๐ง)) |
67 | 66 | adantlr 714 |
. . . . . . . . . . 11
โข (((๐ โ โ โง
โ๐ฆ โ โ
(๐โ(๐โ๐ฆ)) โค (๐ ยท
(normโโ๐ฆ))) โง ((๐ฅ โ โ โง ๐ง โ โ+) โง ๐ค โ โ)) โ
(((๐โ(๐โ(๐ค โโ ๐ฅ))) โค (๐ ยท
(normโโ(๐ค โโ ๐ฅ))) โง (๐ ยท
(normโโ(๐ค โโ ๐ฅ))) < ๐ง) โ (๐โ(๐โ(๐ค โโ ๐ฅ))) < ๐ง)) |
68 | 54, 67 | mpand 694 |
. . . . . . . . . 10
โข (((๐ โ โ โง
โ๐ฆ โ โ
(๐โ(๐โ๐ฆ)) โค (๐ ยท
(normโโ๐ฆ))) โง ((๐ฅ โ โ โง ๐ง โ โ+) โง ๐ค โ โ)) โ ((๐ ยท
(normโโ(๐ค โโ ๐ฅ))) < ๐ง โ (๐โ(๐โ(๐ค โโ ๐ฅ))) < ๐ง)) |
69 | | nnrp 12934 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ๐ โ
โ+) |
70 | 69 | rpregt0d 12971 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (๐ โ โ โง 0 <
๐)) |
71 | 70 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ((๐ฅ โ โ โง ๐ง โ โ+)
โง ๐ค โ โ))
โ (๐ โ โ
โง 0 < ๐)) |
72 | | ltmuldiv2 12037 |
. . . . . . . . . . . 12
โข
(((normโโ(๐ค โโ ๐ฅ)) โ โ โง ๐ง โ โ โง (๐ โ โ โง 0 <
๐)) โ ((๐ ยท
(normโโ(๐ค โโ ๐ฅ))) < ๐ง โ (normโโ(๐ค โโ
๐ฅ)) < (๐ง / ๐))) |
73 | 60, 64, 71, 72 | syl3anc 1372 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ((๐ฅ โ โ โง ๐ง โ โ+)
โง ๐ค โ โ))
โ ((๐ ยท
(normโโ(๐ค โโ ๐ฅ))) < ๐ง โ (normโโ(๐ค โโ
๐ฅ)) < (๐ง / ๐))) |
74 | 73 | adantlr 714 |
. . . . . . . . . 10
โข (((๐ โ โ โง
โ๐ฆ โ โ
(๐โ(๐โ๐ฆ)) โค (๐ ยท
(normโโ๐ฆ))) โง ((๐ฅ โ โ โง ๐ง โ โ+) โง ๐ค โ โ)) โ ((๐ ยท
(normโโ(๐ค โโ ๐ฅ))) < ๐ง โ (normโโ(๐ค โโ
๐ฅ)) < (๐ง / ๐))) |
75 | | lncon.5 |
. . . . . . . . . . . . . 14
โข ((๐ค โ โ โง ๐ฅ โ โ) โ (๐โ(๐ค โโ ๐ฅ)) = ((๐โ๐ค)๐(๐โ๐ฅ))) |
76 | 44, 45, 75 | syl2anc 585 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ((๐ฅ โ โ โง ๐ง โ โ+)
โง ๐ค โ โ))
โ (๐โ(๐ค โโ
๐ฅ)) = ((๐โ๐ค)๐(๐โ๐ฅ))) |
77 | 76 | adantlr 714 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง
โ๐ฆ โ โ
(๐โ(๐โ๐ฆ)) โค (๐ ยท
(normโโ๐ฆ))) โง ((๐ฅ โ โ โง ๐ง โ โ+) โง ๐ค โ โ)) โ (๐โ(๐ค โโ ๐ฅ)) = ((๐โ๐ค)๐(๐โ๐ฅ))) |
78 | 77 | fveq2d 6850 |
. . . . . . . . . . 11
โข (((๐ โ โ โง
โ๐ฆ โ โ
(๐โ(๐โ๐ฆ)) โค (๐ ยท
(normโโ๐ฆ))) โง ((๐ฅ โ โ โง ๐ง โ โ+) โง ๐ค โ โ)) โ (๐โ(๐โ(๐ค โโ ๐ฅ))) = (๐โ((๐โ๐ค)๐(๐โ๐ฅ)))) |
79 | 78 | breq1d 5119 |
. . . . . . . . . 10
โข (((๐ โ โ โง
โ๐ฆ โ โ
(๐โ(๐โ๐ฆ)) โค (๐ ยท
(normโโ๐ฆ))) โง ((๐ฅ โ โ โง ๐ง โ โ+) โง ๐ค โ โ)) โ ((๐โ(๐โ(๐ค โโ ๐ฅ))) < ๐ง โ (๐โ((๐โ๐ค)๐(๐โ๐ฅ))) < ๐ง)) |
80 | 68, 74, 79 | 3imtr3d 293 |
. . . . . . . . 9
โข (((๐ โ โ โง
โ๐ฆ โ โ
(๐โ(๐โ๐ฆ)) โค (๐ ยท
(normโโ๐ฆ))) โง ((๐ฅ โ โ โง ๐ง โ โ+) โง ๐ค โ โ)) โ
((normโโ(๐ค โโ ๐ฅ)) < (๐ง / ๐) โ (๐โ((๐โ๐ค)๐(๐โ๐ฅ))) < ๐ง)) |
81 | 80 | anassrs 469 |
. . . . . . . 8
โข ((((๐ โ โ โง
โ๐ฆ โ โ
(๐โ(๐โ๐ฆ)) โค (๐ ยท
(normโโ๐ฆ))) โง (๐ฅ โ โ โง ๐ง โ โ+)) โง ๐ค โ โ) โ
((normโโ(๐ค โโ ๐ฅ)) < (๐ง / ๐) โ (๐โ((๐โ๐ค)๐(๐โ๐ฅ))) < ๐ง)) |
82 | 81 | ralrimiva 3140 |
. . . . . . 7
โข (((๐ โ โ โง
โ๐ฆ โ โ
(๐โ(๐โ๐ฆ)) โค (๐ ยท
(normโโ๐ฆ))) โง (๐ฅ โ โ โง ๐ง โ โ+)) โ
โ๐ค โ โ
((normโโ(๐ค โโ ๐ฅ)) < (๐ง / ๐) โ (๐โ((๐โ๐ค)๐(๐โ๐ฅ))) < ๐ง)) |
83 | | breq2 5113 |
. . . . . . . 8
โข (๐ฆ = (๐ง / ๐) โ
((normโโ(๐ค โโ ๐ฅ)) < ๐ฆ โ (normโโ(๐ค โโ
๐ฅ)) < (๐ง / ๐))) |
84 | 83 | rspceaimv 3587 |
. . . . . . 7
โข (((๐ง / ๐) โ โ+ โง
โ๐ค โ โ
((normโโ(๐ค โโ ๐ฅ)) < (๐ง / ๐) โ (๐โ((๐โ๐ค)๐(๐โ๐ฅ))) < ๐ง)) โ โ๐ฆ โ โ+ โ๐ค โ โ
((normโโ(๐ค โโ ๐ฅ)) < ๐ฆ โ (๐โ((๐โ๐ค)๐(๐โ๐ฅ))) < ๐ง)) |
85 | 43, 82, 84 | syl2anc 585 |
. . . . . 6
โข (((๐ โ โ โง
โ๐ฆ โ โ
(๐โ(๐โ๐ฆ)) โค (๐ ยท
(normโโ๐ฆ))) โง (๐ฅ โ โ โง ๐ง โ โ+)) โ
โ๐ฆ โ
โ+ โ๐ค โ โ
((normโโ(๐ค โโ ๐ฅ)) < ๐ฆ โ (๐โ((๐โ๐ค)๐(๐โ๐ฅ))) < ๐ง)) |
86 | 85 | ralrimivva 3194 |
. . . . 5
โข ((๐ โ โ โง
โ๐ฆ โ โ
(๐โ(๐โ๐ฆ)) โค (๐ ยท
(normโโ๐ฆ))) โ โ๐ฅ โ โ โ๐ง โ โ+ โ๐ฆ โ โ+
โ๐ค โ โ
((normโโ(๐ค โโ ๐ฅ)) < ๐ฆ โ (๐โ((๐โ๐ค)๐(๐โ๐ฅ))) < ๐ง)) |
87 | 86 | rexlimiva 3141 |
. . . 4
โข
(โ๐ โ
โ โ๐ฆ โ
โ (๐โ(๐โ๐ฆ)) โค (๐ ยท
(normโโ๐ฆ)) โ โ๐ฅ โ โ โ๐ง โ โ+ โ๐ฆ โ โ+
โ๐ค โ โ
((normโโ(๐ค โโ ๐ฅ)) < ๐ฆ โ (๐โ((๐โ๐ค)๐(๐โ๐ฅ))) < ๐ง)) |
88 | | lncon.3 |
. . . 4
โข (๐ โ ๐ถ โ โ๐ฅ โ โ โ๐ง โ โ+ โ๐ฆ โ โ+
โ๐ค โ โ
((normโโ(๐ค โโ ๐ฅ)) < ๐ฆ โ (๐โ((๐โ๐ค)๐(๐โ๐ฅ))) < ๐ง)) |
89 | 87, 88 | sylibr 233 |
. . 3
โข
(โ๐ โ
โ โ๐ฆ โ
โ (๐โ(๐โ๐ฆ)) โค (๐ ยท
(normโโ๐ฆ)) โ ๐ โ ๐ถ) |
90 | 39, 89 | syl 17 |
. 2
โข
(โ๐ฅ โ
โ โ๐ฆ โ
โ (๐โ(๐โ๐ฆ)) โค (๐ฅ ยท
(normโโ๐ฆ)) โ ๐ โ ๐ถ) |
91 | 8, 90 | impbii 208 |
1
โข (๐ โ ๐ถ โ โ๐ฅ โ โ โ๐ฆ โ โ (๐โ(๐โ๐ฆ)) โค (๐ฅ ยท
(normโโ๐ฆ))) |