Step | Hyp | Ref
| Expression |
1 | | nmcex.2 |
. . 3
โข (๐โ๐) = sup({๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))}, โ*, <
) |
2 | | nmcex.3 |
. . . . . . . . 9
โข (๐ฅ โ โ โ (๐โ(๐โ๐ฅ)) โ โ) |
3 | | eleq1 2821 |
. . . . . . . . 9
โข (๐ = (๐โ(๐โ๐ฅ)) โ (๐ โ โ โ (๐โ(๐โ๐ฅ)) โ โ)) |
4 | 2, 3 | syl5ibrcom 246 |
. . . . . . . 8
โข (๐ฅ โ โ โ (๐ = (๐โ(๐โ๐ฅ)) โ ๐ โ โ)) |
5 | 4 | imp 407 |
. . . . . . 7
โข ((๐ฅ โ โ โง ๐ = (๐โ(๐โ๐ฅ))) โ ๐ โ โ) |
6 | 5 | adantrl 714 |
. . . . . 6
โข ((๐ฅ โ โ โง
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))) โ ๐ โ โ) |
7 | 6 | rexlimiva 3147 |
. . . . 5
โข
(โ๐ฅ โ
โ ((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ))) โ ๐ โ โ) |
8 | 7 | abssi 4067 |
. . . 4
โข {๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))} โ โ |
9 | | ax-hv0cl 30251 |
. . . . . . 7
โข
0โ โ โ |
10 | | norm0 30376 |
. . . . . . . . 9
โข
(normโโ0โ) =
0 |
11 | | 0le1 11736 |
. . . . . . . . 9
โข 0 โค
1 |
12 | 10, 11 | eqbrtri 5169 |
. . . . . . . 8
โข
(normโโ0โ) โค
1 |
13 | | nmcex.4 |
. . . . . . . . 9
โข (๐โ(๐โ0โ)) =
0 |
14 | 13 | eqcomi 2741 |
. . . . . . . 8
โข 0 =
(๐โ(๐โ0โ)) |
15 | 12, 14 | pm3.2i 471 |
. . . . . . 7
โข
((normโโ0โ) โค 1 โง 0 =
(๐โ(๐โ0โ))) |
16 | | fveq2 6891 |
. . . . . . . . . 10
โข (๐ฅ = 0โ โ
(normโโ๐ฅ) =
(normโโ0โ)) |
17 | 16 | breq1d 5158 |
. . . . . . . . 9
โข (๐ฅ = 0โ โ
((normโโ๐ฅ) โค 1 โ
(normโโ0โ) โค 1)) |
18 | | 2fveq3 6896 |
. . . . . . . . . 10
โข (๐ฅ = 0โ โ
(๐โ(๐โ๐ฅ)) = (๐โ(๐โ0โ))) |
19 | 18 | eqeq2d 2743 |
. . . . . . . . 9
โข (๐ฅ = 0โ โ
(0 = (๐โ(๐โ๐ฅ)) โ 0 = (๐โ(๐โ0โ)))) |
20 | 17, 19 | anbi12d 631 |
. . . . . . . 8
โข (๐ฅ = 0โ โ
(((normโโ๐ฅ) โค 1 โง 0 = (๐โ(๐โ๐ฅ))) โ
((normโโ0โ) โค 1 โง 0 = (๐โ(๐โ0โ))))) |
21 | 20 | rspcev 3612 |
. . . . . . 7
โข
((0โ โ โ โง
((normโโ0โ) โค 1 โง 0 = (๐โ(๐โ0โ)))) โ
โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง 0 = (๐โ(๐โ๐ฅ)))) |
22 | 9, 15, 21 | mp2an 690 |
. . . . . 6
โข
โ๐ฅ โ
โ ((normโโ๐ฅ) โค 1 โง 0 = (๐โ(๐โ๐ฅ))) |
23 | | c0ex 11207 |
. . . . . . 7
โข 0 โ
V |
24 | | eqeq1 2736 |
. . . . . . . . 9
โข (๐ = 0 โ (๐ = (๐โ(๐โ๐ฅ)) โ 0 = (๐โ(๐โ๐ฅ)))) |
25 | 24 | anbi2d 629 |
. . . . . . . 8
โข (๐ = 0 โ
(((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ))) โ
((normโโ๐ฅ) โค 1 โง 0 = (๐โ(๐โ๐ฅ))))) |
26 | 25 | rexbidv 3178 |
. . . . . . 7
โข (๐ = 0 โ (โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ))) โ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง 0 = (๐โ(๐โ๐ฅ))))) |
27 | 23, 26 | elab 3668 |
. . . . . 6
โข (0 โ
{๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))} โ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง 0 = (๐โ(๐โ๐ฅ)))) |
28 | 22, 27 | mpbir 230 |
. . . . 5
โข 0 โ
{๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))} |
29 | 28 | ne0ii 4337 |
. . . 4
โข {๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))} โ โ
|
30 | | nmcex.1 |
. . . . 5
โข
โ๐ฆ โ
โ+ โ๐ง โ โ
((normโโ๐ง) < ๐ฆ โ (๐โ(๐โ๐ง)) < 1) |
31 | | 2rp 12978 |
. . . . . . . . . 10
โข 2 โ
โ+ |
32 | | rpdivcl 12998 |
. . . . . . . . . 10
โข ((2
โ โ+ โง ๐ฆ โ โ+) โ (2 /
๐ฆ) โ
โ+) |
33 | 31, 32 | mpan 688 |
. . . . . . . . 9
โข (๐ฆ โ โ+
โ (2 / ๐ฆ) โ
โ+) |
34 | 33 | rpred 13015 |
. . . . . . . 8
โข (๐ฆ โ โ+
โ (2 / ๐ฆ) โ
โ) |
35 | 34 | adantr 481 |
. . . . . . 7
โข ((๐ฆ โ โ+
โง โ๐ง โ
โ ((normโโ๐ง) < ๐ฆ โ (๐โ(๐โ๐ง)) < 1)) โ (2 / ๐ฆ) โ โ) |
36 | | rpre 12981 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฆ โ โ+
โ ๐ฆ โ
โ) |
37 | 36 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ ๐ฆ โ โ) |
38 | 37 | rehalfcld 12458 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ (๐ฆ / 2) โ โ) |
39 | 38 | recnd 11241 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ (๐ฆ / 2) โ โ) |
40 | | simprl 769 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ ๐ฅ โ โ) |
41 | | hvmulcl 30261 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ฆ / 2) โ โ โง ๐ฅ โ โ) โ ((๐ฆ / 2)
ยทโ ๐ฅ) โ โ) |
42 | 39, 40, 41 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ ((๐ฆ / 2) ยทโ
๐ฅ) โ
โ) |
43 | | normcl 30373 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ฆ / 2)
ยทโ ๐ฅ) โ โ โ
(normโโ((๐ฆ / 2) ยทโ
๐ฅ)) โ
โ) |
44 | 42, 43 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ
(normโโ((๐ฆ / 2) ยทโ
๐ฅ)) โ
โ) |
45 | | simprr 771 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ
(normโโ๐ฅ) โค 1) |
46 | | normcl 30373 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ฅ โ โ โ
(normโโ๐ฅ) โ โ) |
47 | 46 | ad2antrl 726 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ
(normโโ๐ฅ) โ โ) |
48 | | 1red 11214 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ 1 โ
โ) |
49 | | rphalfcl 13000 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ฆ โ โ+
โ (๐ฆ / 2) โ
โ+) |
50 | 49 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ (๐ฆ / 2) โ
โ+) |
51 | 47, 48, 50 | lemul2d 13059 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ
((normโโ๐ฅ) โค 1 โ ((๐ฆ / 2) ยท
(normโโ๐ฅ)) โค ((๐ฆ / 2) ยท 1))) |
52 | 45, 51 | mpbid 231 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ ((๐ฆ / 2) ยท
(normโโ๐ฅ)) โค ((๐ฆ / 2) ยท 1)) |
53 | | rpcn 12983 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ฆ / 2) โ โ+
โ (๐ฆ / 2) โ
โ) |
54 | | norm-iii 30388 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ฆ / 2) โ โ โง ๐ฅ โ โ) โ
(normโโ((๐ฆ / 2) ยทโ
๐ฅ)) = ((absโ(๐ฆ / 2)) ยท
(normโโ๐ฅ))) |
55 | 53, 54 | sylan 580 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ฆ / 2) โ โ+
โง ๐ฅ โ โ)
โ (normโโ((๐ฆ / 2) ยทโ
๐ฅ)) = ((absโ(๐ฆ / 2)) ยท
(normโโ๐ฅ))) |
56 | | rpre 12981 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ฆ / 2) โ โ+
โ (๐ฆ / 2) โ
โ) |
57 | | rpge0 12986 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ฆ / 2) โ โ+
โ 0 โค (๐ฆ /
2)) |
58 | 56, 57 | absidd 15368 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ฆ / 2) โ โ+
โ (absโ(๐ฆ / 2))
= (๐ฆ / 2)) |
59 | 58 | oveq1d 7423 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ฆ / 2) โ โ+
โ ((absโ(๐ฆ / 2))
ยท (normโโ๐ฅ)) = ((๐ฆ / 2) ยท
(normโโ๐ฅ))) |
60 | 59 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ฆ / 2) โ โ+
โง ๐ฅ โ โ)
โ ((absโ(๐ฆ / 2))
ยท (normโโ๐ฅ)) = ((๐ฆ / 2) ยท
(normโโ๐ฅ))) |
61 | 55, 60 | eqtr2d 2773 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ฆ / 2) โ โ+
โง ๐ฅ โ โ)
โ ((๐ฆ / 2) ยท
(normโโ๐ฅ)) = (normโโ((๐ฆ / 2)
ยทโ ๐ฅ))) |
62 | 50, 40, 61 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ ((๐ฆ / 2) ยท
(normโโ๐ฅ)) = (normโโ((๐ฆ / 2)
ยทโ ๐ฅ))) |
63 | 39 | mulridd 11230 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ ((๐ฆ / 2) ยท 1) = (๐ฆ / 2)) |
64 | 52, 62, 63 | 3brtr3d 5179 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ
(normโโ((๐ฆ / 2) ยทโ
๐ฅ)) โค (๐ฆ / 2)) |
65 | | rphalflt 13002 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฆ โ โ+
โ (๐ฆ / 2) < ๐ฆ) |
66 | 65 | adantr 481 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ (๐ฆ / 2) < ๐ฆ) |
67 | 44, 38, 37, 64, 66 | lelttrd 11371 |
. . . . . . . . . . . . . . . 16
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ
(normโโ((๐ฆ / 2) ยทโ
๐ฅ)) < ๐ฆ) |
68 | | fveq2 6891 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ง = ((๐ฆ / 2) ยทโ
๐ฅ) โ
(normโโ๐ง) = (normโโ((๐ฆ / 2)
ยทโ ๐ฅ))) |
69 | 68 | breq1d 5158 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ง = ((๐ฆ / 2) ยทโ
๐ฅ) โ
((normโโ๐ง) < ๐ฆ โ
(normโโ((๐ฆ / 2) ยทโ
๐ฅ)) < ๐ฆ)) |
70 | | 2fveq3 6896 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ง = ((๐ฆ / 2) ยทโ
๐ฅ) โ (๐โ(๐โ๐ง)) = (๐โ(๐โ((๐ฆ / 2) ยทโ
๐ฅ)))) |
71 | 70 | breq1d 5158 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ง = ((๐ฆ / 2) ยทโ
๐ฅ) โ ((๐โ(๐โ๐ง)) < 1 โ (๐โ(๐โ((๐ฆ / 2) ยทโ
๐ฅ))) <
1)) |
72 | 69, 71 | imbi12d 344 |
. . . . . . . . . . . . . . . . . 18
โข (๐ง = ((๐ฆ / 2) ยทโ
๐ฅ) โ
(((normโโ๐ง) < ๐ฆ โ (๐โ(๐โ๐ง)) < 1) โ
((normโโ((๐ฆ / 2) ยทโ
๐ฅ)) < ๐ฆ โ (๐โ(๐โ((๐ฆ / 2) ยทโ
๐ฅ))) <
1))) |
73 | 72 | rspcv 3608 |
. . . . . . . . . . . . . . . . 17
โข (((๐ฆ / 2)
ยทโ ๐ฅ) โ โ โ (โ๐ง โ โ
((normโโ๐ง) < ๐ฆ โ (๐โ(๐โ๐ง)) < 1) โ
((normโโ((๐ฆ / 2) ยทโ
๐ฅ)) < ๐ฆ โ (๐โ(๐โ((๐ฆ / 2) ยทโ
๐ฅ))) <
1))) |
74 | 42, 73 | syl 17 |
. . . . . . . . . . . . . . . 16
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ (โ๐ง โ โ
((normโโ๐ง) < ๐ฆ โ (๐โ(๐โ๐ง)) < 1) โ
((normโโ((๐ฆ / 2) ยทโ
๐ฅ)) < ๐ฆ โ (๐โ(๐โ((๐ฆ / 2) ยทโ
๐ฅ))) <
1))) |
75 | 67, 74 | mpid 44 |
. . . . . . . . . . . . . . 15
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ (โ๐ง โ โ
((normโโ๐ง) < ๐ฆ โ (๐โ(๐โ๐ง)) < 1) โ (๐โ(๐โ((๐ฆ / 2) ยทโ
๐ฅ))) <
1)) |
76 | 2 | ad2antrl 726 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ (๐โ(๐โ๐ฅ)) โ โ) |
77 | 76, 48, 50 | ltmuldiv2d 13063 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ (((๐ฆ / 2) ยท (๐โ(๐โ๐ฅ))) < 1 โ (๐โ(๐โ๐ฅ)) < (1 / (๐ฆ / 2)))) |
78 | 50 | rprecred 13026 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ (1 / (๐ฆ / 2)) โ โ) |
79 | | ltle 11301 |
. . . . . . . . . . . . . . . . . 18
โข (((๐โ(๐โ๐ฅ)) โ โ โง (1 / (๐ฆ / 2)) โ โ) โ
((๐โ(๐โ๐ฅ)) < (1 / (๐ฆ / 2)) โ (๐โ(๐โ๐ฅ)) โค (1 / (๐ฆ / 2)))) |
80 | 76, 78, 79 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ ((๐โ(๐โ๐ฅ)) < (1 / (๐ฆ / 2)) โ (๐โ(๐โ๐ฅ)) โค (1 / (๐ฆ / 2)))) |
81 | 77, 80 | sylbid 239 |
. . . . . . . . . . . . . . . 16
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ (((๐ฆ / 2) ยท (๐โ(๐โ๐ฅ))) < 1 โ (๐โ(๐โ๐ฅ)) โค (1 / (๐ฆ / 2)))) |
82 | | nmcex.5 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ฆ / 2) โ โ+
โง ๐ฅ โ โ)
โ ((๐ฆ / 2) ยท
(๐โ(๐โ๐ฅ))) = (๐โ(๐โ((๐ฆ / 2) ยทโ
๐ฅ)))) |
83 | 50, 40, 82 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ ((๐ฆ / 2) ยท (๐โ(๐โ๐ฅ))) = (๐โ(๐โ((๐ฆ / 2) ยทโ
๐ฅ)))) |
84 | 83 | breq1d 5158 |
. . . . . . . . . . . . . . . 16
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ (((๐ฆ / 2) ยท (๐โ(๐โ๐ฅ))) < 1 โ (๐โ(๐โ((๐ฆ / 2) ยทโ
๐ฅ))) <
1)) |
85 | | rpcn 12983 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฆ โ โ+
โ ๐ฆ โ
โ) |
86 | | rpne0 12989 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฆ โ โ+
โ ๐ฆ โ
0) |
87 | | 2cn 12286 |
. . . . . . . . . . . . . . . . . . . 20
โข 2 โ
โ |
88 | | 2ne0 12315 |
. . . . . . . . . . . . . . . . . . . 20
โข 2 โ
0 |
89 | | recdiv 11919 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ฆ โ โ โง ๐ฆ โ 0) โง (2 โ โ
โง 2 โ 0)) โ (1 / (๐ฆ / 2)) = (2 / ๐ฆ)) |
90 | 87, 88, 89 | mpanr12 703 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ฆ โ โ โง ๐ฆ โ 0) โ (1 / (๐ฆ / 2)) = (2 / ๐ฆ)) |
91 | 85, 86, 90 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฆ โ โ+
โ (1 / (๐ฆ / 2)) = (2 /
๐ฆ)) |
92 | 91 | adantr 481 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ (1 / (๐ฆ / 2)) = (2 / ๐ฆ)) |
93 | 92 | breq2d 5160 |
. . . . . . . . . . . . . . . 16
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ ((๐โ(๐โ๐ฅ)) โค (1 / (๐ฆ / 2)) โ (๐โ(๐โ๐ฅ)) โค (2 / ๐ฆ))) |
94 | 81, 84, 93 | 3imtr3d 292 |
. . . . . . . . . . . . . . 15
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ ((๐โ(๐โ((๐ฆ / 2) ยทโ
๐ฅ))) < 1 โ (๐โ(๐โ๐ฅ)) โค (2 / ๐ฆ))) |
95 | 75, 94 | syld 47 |
. . . . . . . . . . . . . 14
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ (โ๐ง โ โ
((normโโ๐ง) < ๐ฆ โ (๐โ(๐โ๐ง)) < 1) โ (๐โ(๐โ๐ฅ)) โค (2 / ๐ฆ))) |
96 | 95 | imp 407 |
. . . . . . . . . . . . 13
โข (((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โง โ๐ง โ โ
((normโโ๐ง) < ๐ฆ โ (๐โ(๐โ๐ง)) < 1)) โ (๐โ(๐โ๐ฅ)) โค (2 / ๐ฆ)) |
97 | 96 | an32s 650 |
. . . . . . . . . . . 12
โข (((๐ฆ โ โ+
โง โ๐ง โ
โ ((normโโ๐ง) < ๐ฆ โ (๐โ(๐โ๐ง)) < 1)) โง (๐ฅ โ โ โง
(normโโ๐ฅ) โค 1)) โ (๐โ(๐โ๐ฅ)) โค (2 / ๐ฆ)) |
98 | 97 | anassrs 468 |
. . . . . . . . . . 11
โข ((((๐ฆ โ โ+
โง โ๐ง โ
โ ((normโโ๐ง) < ๐ฆ โ (๐โ(๐โ๐ง)) < 1)) โง ๐ฅ โ โ) โง
(normโโ๐ฅ) โค 1) โ (๐โ(๐โ๐ฅ)) โค (2 / ๐ฆ)) |
99 | | breq1 5151 |
. . . . . . . . . . 11
โข (๐ = (๐โ(๐โ๐ฅ)) โ (๐ โค (2 / ๐ฆ) โ (๐โ(๐โ๐ฅ)) โค (2 / ๐ฆ))) |
100 | 98, 99 | syl5ibrcom 246 |
. . . . . . . . . 10
โข ((((๐ฆ โ โ+
โง โ๐ง โ
โ ((normโโ๐ง) < ๐ฆ โ (๐โ(๐โ๐ง)) < 1)) โง ๐ฅ โ โ) โง
(normโโ๐ฅ) โค 1) โ (๐ = (๐โ(๐โ๐ฅ)) โ ๐ โค (2 / ๐ฆ))) |
101 | 100 | expimpd 454 |
. . . . . . . . 9
โข (((๐ฆ โ โ+
โง โ๐ง โ
โ ((normโโ๐ง) < ๐ฆ โ (๐โ(๐โ๐ง)) < 1)) โง ๐ฅ โ โ) โ
(((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ))) โ ๐ โค (2 / ๐ฆ))) |
102 | 101 | rexlimdva 3155 |
. . . . . . . 8
โข ((๐ฆ โ โ+
โง โ๐ง โ
โ ((normโโ๐ง) < ๐ฆ โ (๐โ(๐โ๐ง)) < 1)) โ (โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ))) โ ๐ โค (2 / ๐ฆ))) |
103 | 102 | alrimiv 1930 |
. . . . . . 7
โข ((๐ฆ โ โ+
โง โ๐ง โ
โ ((normโโ๐ง) < ๐ฆ โ (๐โ(๐โ๐ง)) < 1)) โ โ๐(โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ))) โ ๐ โค (2 / ๐ฆ))) |
104 | | eqeq1 2736 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (๐ = (๐โ(๐โ๐ฅ)) โ ๐ = (๐โ(๐โ๐ฅ)))) |
105 | 104 | anbi2d 629 |
. . . . . . . . . . 11
โข (๐ = ๐ โ
(((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ))) โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ))))) |
106 | 105 | rexbidv 3178 |
. . . . . . . . . 10
โข (๐ = ๐ โ (โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ))) โ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ))))) |
107 | 106 | ralab 3687 |
. . . . . . . . 9
โข
(โ๐ โ
{๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))}๐ โค ๐ง โ โ๐(โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ))) โ ๐ โค ๐ง)) |
108 | | breq2 5152 |
. . . . . . . . . . 11
โข (๐ง = (2 / ๐ฆ) โ (๐ โค ๐ง โ ๐ โค (2 / ๐ฆ))) |
109 | 108 | imbi2d 340 |
. . . . . . . . . 10
โข (๐ง = (2 / ๐ฆ) โ ((โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ))) โ ๐ โค ๐ง) โ (โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ))) โ ๐ โค (2 / ๐ฆ)))) |
110 | 109 | albidv 1923 |
. . . . . . . . 9
โข (๐ง = (2 / ๐ฆ) โ (โ๐(โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ))) โ ๐ โค ๐ง) โ โ๐(โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ))) โ ๐ โค (2 / ๐ฆ)))) |
111 | 107, 110 | bitrid 282 |
. . . . . . . 8
โข (๐ง = (2 / ๐ฆ) โ (โ๐ โ {๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))}๐ โค ๐ง โ โ๐(โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ))) โ ๐ โค (2 / ๐ฆ)))) |
112 | 111 | rspcev 3612 |
. . . . . . 7
โข (((2 /
๐ฆ) โ โ โง
โ๐(โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ))) โ ๐ โค (2 / ๐ฆ))) โ โ๐ง โ โ โ๐ โ {๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))}๐ โค ๐ง) |
113 | 35, 103, 112 | syl2anc 584 |
. . . . . 6
โข ((๐ฆ โ โ+
โง โ๐ง โ
โ ((normโโ๐ง) < ๐ฆ โ (๐โ(๐โ๐ง)) < 1)) โ โ๐ง โ โ โ๐ โ {๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))}๐ โค ๐ง) |
114 | 113 | rexlimiva 3147 |
. . . . 5
โข
(โ๐ฆ โ
โ+ โ๐ง โ โ
((normโโ๐ง) < ๐ฆ โ (๐โ(๐โ๐ง)) < 1) โ โ๐ง โ โ โ๐ โ {๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))}๐ โค ๐ง) |
115 | 30, 114 | ax-mp 5 |
. . . 4
โข
โ๐ง โ
โ โ๐ โ
{๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))}๐ โค ๐ง |
116 | | supxrre 13305 |
. . . 4
โข (({๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))} โ โ โง {๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))} โ โ
โง โ๐ง โ โ โ๐ โ {๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))}๐ โค ๐ง) โ sup({๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))}, โ*, < ) =
sup({๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))}, โ, < )) |
117 | 8, 29, 115, 116 | mp3an 1461 |
. . 3
โข
sup({๐ โฃ
โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))}, โ*, < ) =
sup({๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))}, โ, < ) |
118 | 1, 117 | eqtri 2760 |
. 2
โข (๐โ๐) = sup({๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))}, โ, < ) |
119 | | suprcl 12173 |
. . 3
โข (({๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))} โ โ โง {๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))} โ โ
โง โ๐ง โ โ โ๐ โ {๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))}๐ โค ๐ง) โ sup({๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))}, โ, < ) โ
โ) |
120 | 8, 29, 115, 119 | mp3an 1461 |
. 2
โข
sup({๐ โฃ
โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))}, โ, < ) โ
โ |
121 | 118, 120 | eqeltri 2829 |
1
โข (๐โ๐) โ โ |