Step | Hyp | Ref
| Expression |
1 | | nmcex.2 |
. . 3
โข (๐โ๐) = sup({๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))}, โ*, <
) |
2 | | nmcex.3 |
. . . . . . . . 9
โข (๐ฅ โ โ โ (๐โ(๐โ๐ฅ)) โ โ) |
3 | | eleq1 2822 |
. . . . . . . . 9
โข (๐ = (๐โ(๐โ๐ฅ)) โ (๐ โ โ โ (๐โ(๐โ๐ฅ)) โ โ)) |
4 | 2, 3 | syl5ibrcom 247 |
. . . . . . . 8
โข (๐ฅ โ โ โ (๐ = (๐โ(๐โ๐ฅ)) โ ๐ โ โ)) |
5 | 4 | imp 408 |
. . . . . . 7
โข ((๐ฅ โ โ โง ๐ = (๐โ(๐โ๐ฅ))) โ ๐ โ โ) |
6 | 5 | adantrl 715 |
. . . . . 6
โข ((๐ฅ โ โ โง
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))) โ ๐ โ โ) |
7 | 6 | rexlimiva 3141 |
. . . . 5
โข
(โ๐ฅ โ
โ ((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ))) โ ๐ โ โ) |
8 | 7 | abssi 4031 |
. . . 4
โข {๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))} โ โ |
9 | | ax-hv0cl 29994 |
. . . . . . 7
โข
0โ โ โ |
10 | | norm0 30119 |
. . . . . . . . 9
โข
(normโโ0โ) =
0 |
11 | | 0le1 11686 |
. . . . . . . . 9
โข 0 โค
1 |
12 | 10, 11 | eqbrtri 5130 |
. . . . . . . 8
โข
(normโโ0โ) โค
1 |
13 | | nmcex.4 |
. . . . . . . . 9
โข (๐โ(๐โ0โ)) =
0 |
14 | 13 | eqcomi 2742 |
. . . . . . . 8
โข 0 =
(๐โ(๐โ0โ)) |
15 | 12, 14 | pm3.2i 472 |
. . . . . . 7
โข
((normโโ0โ) โค 1 โง 0 =
(๐โ(๐โ0โ))) |
16 | | fveq2 6846 |
. . . . . . . . . 10
โข (๐ฅ = 0โ โ
(normโโ๐ฅ) =
(normโโ0โ)) |
17 | 16 | breq1d 5119 |
. . . . . . . . 9
โข (๐ฅ = 0โ โ
((normโโ๐ฅ) โค 1 โ
(normโโ0โ) โค 1)) |
18 | | 2fveq3 6851 |
. . . . . . . . . 10
โข (๐ฅ = 0โ โ
(๐โ(๐โ๐ฅ)) = (๐โ(๐โ0โ))) |
19 | 18 | eqeq2d 2744 |
. . . . . . . . 9
โข (๐ฅ = 0โ โ
(0 = (๐โ(๐โ๐ฅ)) โ 0 = (๐โ(๐โ0โ)))) |
20 | 17, 19 | anbi12d 632 |
. . . . . . . 8
โข (๐ฅ = 0โ โ
(((normโโ๐ฅ) โค 1 โง 0 = (๐โ(๐โ๐ฅ))) โ
((normโโ0โ) โค 1 โง 0 = (๐โ(๐โ0โ))))) |
21 | 20 | rspcev 3583 |
. . . . . . 7
โข
((0โ โ โ โง
((normโโ0โ) โค 1 โง 0 = (๐โ(๐โ0โ)))) โ
โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง 0 = (๐โ(๐โ๐ฅ)))) |
22 | 9, 15, 21 | mp2an 691 |
. . . . . 6
โข
โ๐ฅ โ
โ ((normโโ๐ฅ) โค 1 โง 0 = (๐โ(๐โ๐ฅ))) |
23 | | c0ex 11157 |
. . . . . . 7
โข 0 โ
V |
24 | | eqeq1 2737 |
. . . . . . . . 9
โข (๐ = 0 โ (๐ = (๐โ(๐โ๐ฅ)) โ 0 = (๐โ(๐โ๐ฅ)))) |
25 | 24 | anbi2d 630 |
. . . . . . . 8
โข (๐ = 0 โ
(((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ))) โ
((normโโ๐ฅ) โค 1 โง 0 = (๐โ(๐โ๐ฅ))))) |
26 | 25 | rexbidv 3172 |
. . . . . . 7
โข (๐ = 0 โ (โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ))) โ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง 0 = (๐โ(๐โ๐ฅ))))) |
27 | 23, 26 | elab 3634 |
. . . . . 6
โข (0 โ
{๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))} โ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง 0 = (๐โ(๐โ๐ฅ)))) |
28 | 22, 27 | mpbir 230 |
. . . . 5
โข 0 โ
{๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))} |
29 | 28 | ne0ii 4301 |
. . . 4
โข {๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))} โ โ
|
30 | | nmcex.1 |
. . . . 5
โข
โ๐ฆ โ
โ+ โ๐ง โ โ
((normโโ๐ง) < ๐ฆ โ (๐โ(๐โ๐ง)) < 1) |
31 | | 2rp 12928 |
. . . . . . . . . 10
โข 2 โ
โ+ |
32 | | rpdivcl 12948 |
. . . . . . . . . 10
โข ((2
โ โ+ โง ๐ฆ โ โ+) โ (2 /
๐ฆ) โ
โ+) |
33 | 31, 32 | mpan 689 |
. . . . . . . . 9
โข (๐ฆ โ โ+
โ (2 / ๐ฆ) โ
โ+) |
34 | 33 | rpred 12965 |
. . . . . . . 8
โข (๐ฆ โ โ+
โ (2 / ๐ฆ) โ
โ) |
35 | 34 | adantr 482 |
. . . . . . 7
โข ((๐ฆ โ โ+
โง โ๐ง โ
โ ((normโโ๐ง) < ๐ฆ โ (๐โ(๐โ๐ง)) < 1)) โ (2 / ๐ฆ) โ โ) |
36 | | rpre 12931 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฆ โ โ+
โ ๐ฆ โ
โ) |
37 | 36 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ ๐ฆ โ โ) |
38 | 37 | rehalfcld 12408 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ (๐ฆ / 2) โ โ) |
39 | 38 | recnd 11191 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ (๐ฆ / 2) โ โ) |
40 | | simprl 770 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ ๐ฅ โ โ) |
41 | | hvmulcl 30004 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ฆ / 2) โ โ โง ๐ฅ โ โ) โ ((๐ฆ / 2)
ยทโ ๐ฅ) โ โ) |
42 | 39, 40, 41 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ ((๐ฆ / 2) ยทโ
๐ฅ) โ
โ) |
43 | | normcl 30116 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ฆ / 2)
ยทโ ๐ฅ) โ โ โ
(normโโ((๐ฆ / 2) ยทโ
๐ฅ)) โ
โ) |
44 | 42, 43 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ
(normโโ((๐ฆ / 2) ยทโ
๐ฅ)) โ
โ) |
45 | | simprr 772 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ
(normโโ๐ฅ) โค 1) |
46 | | normcl 30116 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ฅ โ โ โ
(normโโ๐ฅ) โ โ) |
47 | 46 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ
(normโโ๐ฅ) โ โ) |
48 | | 1red 11164 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ 1 โ
โ) |
49 | | rphalfcl 12950 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ฆ โ โ+
โ (๐ฆ / 2) โ
โ+) |
50 | 49 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ (๐ฆ / 2) โ
โ+) |
51 | 47, 48, 50 | lemul2d 13009 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ
((normโโ๐ฅ) โค 1 โ ((๐ฆ / 2) ยท
(normโโ๐ฅ)) โค ((๐ฆ / 2) ยท 1))) |
52 | 45, 51 | mpbid 231 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ ((๐ฆ / 2) ยท
(normโโ๐ฅ)) โค ((๐ฆ / 2) ยท 1)) |
53 | | rpcn 12933 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ฆ / 2) โ โ+
โ (๐ฆ / 2) โ
โ) |
54 | | norm-iii 30131 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ฆ / 2) โ โ โง ๐ฅ โ โ) โ
(normโโ((๐ฆ / 2) ยทโ
๐ฅ)) = ((absโ(๐ฆ / 2)) ยท
(normโโ๐ฅ))) |
55 | 53, 54 | sylan 581 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ฆ / 2) โ โ+
โง ๐ฅ โ โ)
โ (normโโ((๐ฆ / 2) ยทโ
๐ฅ)) = ((absโ(๐ฆ / 2)) ยท
(normโโ๐ฅ))) |
56 | | rpre 12931 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ฆ / 2) โ โ+
โ (๐ฆ / 2) โ
โ) |
57 | | rpge0 12936 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ฆ / 2) โ โ+
โ 0 โค (๐ฆ /
2)) |
58 | 56, 57 | absidd 15316 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ฆ / 2) โ โ+
โ (absโ(๐ฆ / 2))
= (๐ฆ / 2)) |
59 | 58 | oveq1d 7376 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ฆ / 2) โ โ+
โ ((absโ(๐ฆ / 2))
ยท (normโโ๐ฅ)) = ((๐ฆ / 2) ยท
(normโโ๐ฅ))) |
60 | 59 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ฆ / 2) โ โ+
โง ๐ฅ โ โ)
โ ((absโ(๐ฆ / 2))
ยท (normโโ๐ฅ)) = ((๐ฆ / 2) ยท
(normโโ๐ฅ))) |
61 | 55, 60 | eqtr2d 2774 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ฆ / 2) โ โ+
โง ๐ฅ โ โ)
โ ((๐ฆ / 2) ยท
(normโโ๐ฅ)) = (normโโ((๐ฆ / 2)
ยทโ ๐ฅ))) |
62 | 50, 40, 61 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ ((๐ฆ / 2) ยท
(normโโ๐ฅ)) = (normโโ((๐ฆ / 2)
ยทโ ๐ฅ))) |
63 | 39 | mulridd 11180 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ ((๐ฆ / 2) ยท 1) = (๐ฆ / 2)) |
64 | 52, 62, 63 | 3brtr3d 5140 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ
(normโโ((๐ฆ / 2) ยทโ
๐ฅ)) โค (๐ฆ / 2)) |
65 | | rphalflt 12952 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฆ โ โ+
โ (๐ฆ / 2) < ๐ฆ) |
66 | 65 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ (๐ฆ / 2) < ๐ฆ) |
67 | 44, 38, 37, 64, 66 | lelttrd 11321 |
. . . . . . . . . . . . . . . 16
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ
(normโโ((๐ฆ / 2) ยทโ
๐ฅ)) < ๐ฆ) |
68 | | fveq2 6846 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ง = ((๐ฆ / 2) ยทโ
๐ฅ) โ
(normโโ๐ง) = (normโโ((๐ฆ / 2)
ยทโ ๐ฅ))) |
69 | 68 | breq1d 5119 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ง = ((๐ฆ / 2) ยทโ
๐ฅ) โ
((normโโ๐ง) < ๐ฆ โ
(normโโ((๐ฆ / 2) ยทโ
๐ฅ)) < ๐ฆ)) |
70 | | 2fveq3 6851 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ง = ((๐ฆ / 2) ยทโ
๐ฅ) โ (๐โ(๐โ๐ง)) = (๐โ(๐โ((๐ฆ / 2) ยทโ
๐ฅ)))) |
71 | 70 | breq1d 5119 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ง = ((๐ฆ / 2) ยทโ
๐ฅ) โ ((๐โ(๐โ๐ง)) < 1 โ (๐โ(๐โ((๐ฆ / 2) ยทโ
๐ฅ))) <
1)) |
72 | 69, 71 | imbi12d 345 |
. . . . . . . . . . . . . . . . . 18
โข (๐ง = ((๐ฆ / 2) ยทโ
๐ฅ) โ
(((normโโ๐ง) < ๐ฆ โ (๐โ(๐โ๐ง)) < 1) โ
((normโโ((๐ฆ / 2) ยทโ
๐ฅ)) < ๐ฆ โ (๐โ(๐โ((๐ฆ / 2) ยทโ
๐ฅ))) <
1))) |
73 | 72 | rspcv 3579 |
. . . . . . . . . . . . . . . . 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 727 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ (๐โ(๐โ๐ฅ)) โ โ) |
77 | 76, 48, 50 | ltmuldiv2d 13013 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ (((๐ฆ / 2) ยท (๐โ(๐โ๐ฅ))) < 1 โ (๐โ(๐โ๐ฅ)) < (1 / (๐ฆ / 2)))) |
78 | 50 | rprecred 12976 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ (1 / (๐ฆ / 2)) โ โ) |
79 | | ltle 11251 |
. . . . . . . . . . . . . . . . . 18
โข (((๐โ(๐โ๐ฅ)) โ โ โง (1 / (๐ฆ / 2)) โ โ) โ
((๐โ(๐โ๐ฅ)) < (1 / (๐ฆ / 2)) โ (๐โ(๐โ๐ฅ)) โค (1 / (๐ฆ / 2)))) |
80 | 76, 78, 79 | syl2anc 585 |
. . . . . . . . . . . . . . . . 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 585 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ ((๐ฆ / 2) ยท (๐โ(๐โ๐ฅ))) = (๐โ(๐โ((๐ฆ / 2) ยทโ
๐ฅ)))) |
84 | 83 | breq1d 5119 |
. . . . . . . . . . . . . . . 16
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ (((๐ฆ / 2) ยท (๐โ(๐โ๐ฅ))) < 1 โ (๐โ(๐โ((๐ฆ / 2) ยทโ
๐ฅ))) <
1)) |
85 | | rpcn 12933 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฆ โ โ+
โ ๐ฆ โ
โ) |
86 | | rpne0 12939 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฆ โ โ+
โ ๐ฆ โ
0) |
87 | | 2cn 12236 |
. . . . . . . . . . . . . . . . . . . 20
โข 2 โ
โ |
88 | | 2ne0 12265 |
. . . . . . . . . . . . . . . . . . . 20
โข 2 โ
0 |
89 | | recdiv 11869 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ฆ โ โ โง ๐ฆ โ 0) โง (2 โ โ
โง 2 โ 0)) โ (1 / (๐ฆ / 2)) = (2 / ๐ฆ)) |
90 | 87, 88, 89 | mpanr12 704 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ฆ โ โ โง ๐ฆ โ 0) โ (1 / (๐ฆ / 2)) = (2 / ๐ฆ)) |
91 | 85, 86, 90 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฆ โ โ+
โ (1 / (๐ฆ / 2)) = (2 /
๐ฆ)) |
92 | 91 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ (1 / (๐ฆ / 2)) = (2 / ๐ฆ)) |
93 | 92 | breq2d 5121 |
. . . . . . . . . . . . . . . 16
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ ((๐โ(๐โ๐ฅ)) โค (1 / (๐ฆ / 2)) โ (๐โ(๐โ๐ฅ)) โค (2 / ๐ฆ))) |
94 | 81, 84, 93 | 3imtr3d 293 |
. . . . . . . . . . . . . . 15
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ ((๐โ(๐โ((๐ฆ / 2) ยทโ
๐ฅ))) < 1 โ (๐โ(๐โ๐ฅ)) โค (2 / ๐ฆ))) |
95 | 75, 94 | syld 47 |
. . . . . . . . . . . . . 14
โข ((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โ (โ๐ง โ โ
((normโโ๐ง) < ๐ฆ โ (๐โ(๐โ๐ง)) < 1) โ (๐โ(๐โ๐ฅ)) โค (2 / ๐ฆ))) |
96 | 95 | imp 408 |
. . . . . . . . . . . . 13
โข (((๐ฆ โ โ+
โง (๐ฅ โ โ
โง (normโโ๐ฅ) โค 1)) โง โ๐ง โ โ
((normโโ๐ง) < ๐ฆ โ (๐โ(๐โ๐ง)) < 1)) โ (๐โ(๐โ๐ฅ)) โค (2 / ๐ฆ)) |
97 | 96 | an32s 651 |
. . . . . . . . . . . 12
โข (((๐ฆ โ โ+
โง โ๐ง โ
โ ((normโโ๐ง) < ๐ฆ โ (๐โ(๐โ๐ง)) < 1)) โง (๐ฅ โ โ โง
(normโโ๐ฅ) โค 1)) โ (๐โ(๐โ๐ฅ)) โค (2 / ๐ฆ)) |
98 | 97 | anassrs 469 |
. . . . . . . . . . 11
โข ((((๐ฆ โ โ+
โง โ๐ง โ
โ ((normโโ๐ง) < ๐ฆ โ (๐โ(๐โ๐ง)) < 1)) โง ๐ฅ โ โ) โง
(normโโ๐ฅ) โค 1) โ (๐โ(๐โ๐ฅ)) โค (2 / ๐ฆ)) |
99 | | breq1 5112 |
. . . . . . . . . . 11
โข (๐ = (๐โ(๐โ๐ฅ)) โ (๐ โค (2 / ๐ฆ) โ (๐โ(๐โ๐ฅ)) โค (2 / ๐ฆ))) |
100 | 98, 99 | syl5ibrcom 247 |
. . . . . . . . . 10
โข ((((๐ฆ โ โ+
โง โ๐ง โ
โ ((normโโ๐ง) < ๐ฆ โ (๐โ(๐โ๐ง)) < 1)) โง ๐ฅ โ โ) โง
(normโโ๐ฅ) โค 1) โ (๐ = (๐โ(๐โ๐ฅ)) โ ๐ โค (2 / ๐ฆ))) |
101 | 100 | expimpd 455 |
. . . . . . . . 9
โข (((๐ฆ โ โ+
โง โ๐ง โ
โ ((normโโ๐ง) < ๐ฆ โ (๐โ(๐โ๐ง)) < 1)) โง ๐ฅ โ โ) โ
(((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ))) โ ๐ โค (2 / ๐ฆ))) |
102 | 101 | rexlimdva 3149 |
. . . . . . . 8
โข ((๐ฆ โ โ+
โง โ๐ง โ
โ ((normโโ๐ง) < ๐ฆ โ (๐โ(๐โ๐ง)) < 1)) โ (โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ))) โ ๐ โค (2 / ๐ฆ))) |
103 | 102 | alrimiv 1931 |
. . . . . . 7
โข ((๐ฆ โ โ+
โง โ๐ง โ
โ ((normโโ๐ง) < ๐ฆ โ (๐โ(๐โ๐ง)) < 1)) โ โ๐(โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ))) โ ๐ โค (2 / ๐ฆ))) |
104 | | eqeq1 2737 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (๐ = (๐โ(๐โ๐ฅ)) โ ๐ = (๐โ(๐โ๐ฅ)))) |
105 | 104 | anbi2d 630 |
. . . . . . . . . . 11
โข (๐ = ๐ โ
(((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ))) โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ))))) |
106 | 105 | rexbidv 3172 |
. . . . . . . . . 10
โข (๐ = ๐ โ (โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ))) โ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ))))) |
107 | 106 | ralab 3653 |
. . . . . . . . 9
โข
(โ๐ โ
{๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))}๐ โค ๐ง โ โ๐(โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ))) โ ๐ โค ๐ง)) |
108 | | breq2 5113 |
. . . . . . . . . . 11
โข (๐ง = (2 / ๐ฆ) โ (๐ โค ๐ง โ ๐ โค (2 / ๐ฆ))) |
109 | 108 | imbi2d 341 |
. . . . . . . . . 10
โข (๐ง = (2 / ๐ฆ) โ ((โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ))) โ ๐ โค ๐ง) โ (โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ))) โ ๐ โค (2 / ๐ฆ)))) |
110 | 109 | albidv 1924 |
. . . . . . . . 9
โข (๐ง = (2 / ๐ฆ) โ (โ๐(โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ))) โ ๐ โค ๐ง) โ โ๐(โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ))) โ ๐ โค (2 / ๐ฆ)))) |
111 | 107, 110 | bitrid 283 |
. . . . . . . 8
โข (๐ง = (2 / ๐ฆ) โ (โ๐ โ {๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))}๐ โค ๐ง โ โ๐(โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ))) โ ๐ โค (2 / ๐ฆ)))) |
112 | 111 | rspcev 3583 |
. . . . . . 7
โข (((2 /
๐ฆ) โ โ โง
โ๐(โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ))) โ ๐ โค (2 / ๐ฆ))) โ โ๐ง โ โ โ๐ โ {๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))}๐ โค ๐ง) |
113 | 35, 103, 112 | syl2anc 585 |
. . . . . 6
โข ((๐ฆ โ โ+
โง โ๐ง โ
โ ((normโโ๐ง) < ๐ฆ โ (๐โ(๐โ๐ง)) < 1)) โ โ๐ง โ โ โ๐ โ {๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))}๐ โค ๐ง) |
114 | 113 | rexlimiva 3141 |
. . . . 5
โข
(โ๐ฆ โ
โ+ โ๐ง โ โ
((normโโ๐ง) < ๐ฆ โ (๐โ(๐โ๐ง)) < 1) โ โ๐ง โ โ โ๐ โ {๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))}๐ โค ๐ง) |
115 | 30, 114 | ax-mp 5 |
. . . 4
โข
โ๐ง โ
โ โ๐ โ
{๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))}๐ โค ๐ง |
116 | | supxrre 13255 |
. . . 4
โข (({๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))} โ โ โง {๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))} โ โ
โง โ๐ง โ โ โ๐ โ {๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))}๐ โค ๐ง) โ sup({๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))}, โ*, < ) =
sup({๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))}, โ, < )) |
117 | 8, 29, 115, 116 | mp3an 1462 |
. . 3
โข
sup({๐ โฃ
โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))}, โ*, < ) =
sup({๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))}, โ, < ) |
118 | 1, 117 | eqtri 2761 |
. 2
โข (๐โ๐) = sup({๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))}, โ, < ) |
119 | | suprcl 12123 |
. . 3
โข (({๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))} โ โ โง {๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))} โ โ
โง โ๐ง โ โ โ๐ โ {๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))}๐ โค ๐ง) โ sup({๐ โฃ โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))}, โ, < ) โ
โ) |
120 | 8, 29, 115, 119 | mp3an 1462 |
. 2
โข
sup({๐ โฃ
โ๐ฅ โ โ
((normโโ๐ฅ) โค 1 โง ๐ = (๐โ(๐โ๐ฅ)))}, โ, < ) โ
โ |
121 | 118, 120 | eqeltri 2830 |
1
โข (๐โ๐) โ โ |