Step | Hyp | Ref
| Expression |
1 | | 0le0 12262 |
. . . . 5
โข 0 โค
0 |
2 | 1 | a1i 11 |
. . . 4
โข (๐ด = 0โ โ 0
โค 0) |
3 | | fveq2 6846 |
. . . . . . 7
โข (๐ด = 0โ โ
(๐โ๐ด) = (๐โ0โ)) |
4 | | nmcopex.1 |
. . . . . . . 8
โข ๐ โ LinOp |
5 | 4 | lnop0i 30961 |
. . . . . . 7
โข (๐โ0โ) =
0โ |
6 | 3, 5 | eqtrdi 2789 |
. . . . . 6
โข (๐ด = 0โ โ
(๐โ๐ด) = 0โ) |
7 | 6 | fveq2d 6850 |
. . . . 5
โข (๐ด = 0โ โ
(normโโ(๐โ๐ด)) =
(normโโ0โ)) |
8 | | norm0 30119 |
. . . . 5
โข
(normโโ0โ) =
0 |
9 | 7, 8 | eqtrdi 2789 |
. . . 4
โข (๐ด = 0โ โ
(normโโ(๐โ๐ด)) = 0) |
10 | | fveq2 6846 |
. . . . . . 7
โข (๐ด = 0โ โ
(normโโ๐ด) =
(normโโ0โ)) |
11 | 10, 8 | eqtrdi 2789 |
. . . . . 6
โข (๐ด = 0โ โ
(normโโ๐ด) = 0) |
12 | 11 | oveq2d 7377 |
. . . . 5
โข (๐ด = 0โ โ
((normopโ๐) ยท
(normโโ๐ด)) = ((normopโ๐) ยท 0)) |
13 | | nmcopex.2 |
. . . . . . . 8
โข ๐ โ ContOp |
14 | 4, 13 | nmcopexi 31018 |
. . . . . . 7
โข
(normopโ๐) โ โ |
15 | 14 | recni 11177 |
. . . . . 6
โข
(normopโ๐) โ โ |
16 | 15 | mul01i 11353 |
. . . . 5
โข
((normopโ๐) ยท 0) = 0 |
17 | 12, 16 | eqtrdi 2789 |
. . . 4
โข (๐ด = 0โ โ
((normopโ๐) ยท
(normโโ๐ด)) = 0) |
18 | 2, 9, 17 | 3brtr4d 5141 |
. . 3
โข (๐ด = 0โ โ
(normโโ(๐โ๐ด)) โค ((normopโ๐) ยท
(normโโ๐ด))) |
19 | 18 | adantl 483 |
. 2
โข ((๐ด โ โ โง ๐ด = 0โ) โ
(normโโ(๐โ๐ด)) โค ((normopโ๐) ยท
(normโโ๐ด))) |
20 | | normcl 30116 |
. . . . . . . . 9
โข (๐ด โ โ โ
(normโโ๐ด) โ โ) |
21 | 20 | adantr 482 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ (normโโ๐ด) โ โ) |
22 | | normne0 30121 |
. . . . . . . . 9
โข (๐ด โ โ โ
((normโโ๐ด) โ 0 โ ๐ด โ
0โ)) |
23 | 22 | biimpar 479 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ (normโโ๐ด) โ 0) |
24 | 21, 23 | rereccld 11990 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ (1 / (normโโ๐ด)) โ โ) |
25 | | normgt0 30118 |
. . . . . . . . . 10
โข (๐ด โ โ โ (๐ด โ 0โ
โ 0 < (normโโ๐ด))) |
26 | 25 | biimpa 478 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ 0 < (normโโ๐ด)) |
27 | 21, 26 | recgt0d 12097 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ 0 < (1 / (normโโ๐ด))) |
28 | | 0re 11165 |
. . . . . . . . 9
โข 0 โ
โ |
29 | | ltle 11251 |
. . . . . . . . 9
โข ((0
โ โ โง (1 / (normโโ๐ด)) โ โ) โ (0 < (1 /
(normโโ๐ด)) โ 0 โค (1 /
(normโโ๐ด)))) |
30 | 28, 29 | mpan 689 |
. . . . . . . 8
โข ((1 /
(normโโ๐ด)) โ โ โ (0 < (1 /
(normโโ๐ด)) โ 0 โค (1 /
(normโโ๐ด)))) |
31 | 24, 27, 30 | sylc 65 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ 0 โค (1 / (normโโ๐ด))) |
32 | 24, 31 | absidd 15316 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ (absโ(1 / (normโโ๐ด))) = (1 /
(normโโ๐ด))) |
33 | 32 | oveq1d 7376 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ ((absโ(1 / (normโโ๐ด))) ยท
(normโโ(๐โ๐ด))) = ((1 /
(normโโ๐ด)) ยท
(normโโ(๐โ๐ด)))) |
34 | 24 | recnd 11191 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ (1 / (normโโ๐ด)) โ โ) |
35 | | simpl 484 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ ๐ด โ
โ) |
36 | 4 | lnopmuli 30963 |
. . . . . . . 8
โข (((1 /
(normโโ๐ด)) โ โ โง ๐ด โ โ) โ (๐โ((1 /
(normโโ๐ด)) ยทโ ๐ด)) = ((1 /
(normโโ๐ด)) ยทโ (๐โ๐ด))) |
37 | 34, 35, 36 | syl2anc 585 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ (๐โ((1 /
(normโโ๐ด)) ยทโ ๐ด)) = ((1 /
(normโโ๐ด)) ยทโ (๐โ๐ด))) |
38 | 37 | fveq2d 6850 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ (normโโ(๐โ((1 /
(normโโ๐ด)) ยทโ ๐ด))) =
(normโโ((1 / (normโโ๐ด))
ยทโ (๐โ๐ด)))) |
39 | 4 | lnopfi 30960 |
. . . . . . . . 9
โข ๐: โโถ
โ |
40 | 39 | ffvelcdmi 7038 |
. . . . . . . 8
โข (๐ด โ โ โ (๐โ๐ด) โ โ) |
41 | 40 | adantr 482 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ (๐โ๐ด) โ
โ) |
42 | | norm-iii 30131 |
. . . . . . 7
โข (((1 /
(normโโ๐ด)) โ โ โง (๐โ๐ด) โ โ) โ
(normโโ((1 / (normโโ๐ด))
ยทโ (๐โ๐ด))) = ((absโ(1 /
(normโโ๐ด))) ยท
(normโโ(๐โ๐ด)))) |
43 | 34, 41, 42 | syl2anc 585 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ (normโโ((1 /
(normโโ๐ด)) ยทโ (๐โ๐ด))) = ((absโ(1 /
(normโโ๐ด))) ยท
(normโโ(๐โ๐ด)))) |
44 | 38, 43 | eqtrd 2773 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ (normโโ(๐โ((1 /
(normโโ๐ด)) ยทโ ๐ด))) = ((absโ(1 /
(normโโ๐ด))) ยท
(normโโ(๐โ๐ด)))) |
45 | | normcl 30116 |
. . . . . . . . 9
โข ((๐โ๐ด) โ โ โ
(normโโ(๐โ๐ด)) โ โ) |
46 | 40, 45 | syl 17 |
. . . . . . . 8
โข (๐ด โ โ โ
(normโโ(๐โ๐ด)) โ โ) |
47 | 46 | adantr 482 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ (normโโ(๐โ๐ด)) โ โ) |
48 | 47 | recnd 11191 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ (normโโ(๐โ๐ด)) โ โ) |
49 | 21 | recnd 11191 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ (normโโ๐ด) โ โ) |
50 | 48, 49, 23 | divrec2d 11943 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ ((normโโ(๐โ๐ด)) / (normโโ๐ด)) = ((1 /
(normโโ๐ด)) ยท
(normโโ(๐โ๐ด)))) |
51 | 33, 44, 50 | 3eqtr4rd 2784 |
. . . 4
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ ((normโโ(๐โ๐ด)) / (normโโ๐ด)) =
(normโโ(๐โ((1 /
(normโโ๐ด)) ยทโ ๐ด)))) |
52 | | hvmulcl 30004 |
. . . . . 6
โข (((1 /
(normโโ๐ด)) โ โ โง ๐ด โ โ) โ ((1 /
(normโโ๐ด)) ยทโ ๐ด) โ
โ) |
53 | 34, 35, 52 | syl2anc 585 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ ((1 / (normโโ๐ด)) ยทโ ๐ด) โ
โ) |
54 | | normcl 30116 |
. . . . . . 7
โข (((1 /
(normโโ๐ด)) ยทโ ๐ด) โ โ โ
(normโโ((1 / (normโโ๐ด))
ยทโ ๐ด)) โ โ) |
55 | 53, 54 | syl 17 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ (normโโ((1 /
(normโโ๐ด)) ยทโ ๐ด)) โ
โ) |
56 | | norm1 30240 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ (normโโ((1 /
(normโโ๐ด)) ยทโ ๐ด)) = 1) |
57 | | eqle 11265 |
. . . . . 6
โข
(((normโโ((1 /
(normโโ๐ด)) ยทโ ๐ด)) โ โ โง
(normโโ((1 / (normโโ๐ด))
ยทโ ๐ด)) = 1) โ
(normโโ((1 / (normโโ๐ด))
ยทโ ๐ด)) โค 1) |
58 | 55, 56, 57 | syl2anc 585 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ (normโโ((1 /
(normโโ๐ด)) ยทโ ๐ด)) โค 1) |
59 | | nmoplb 30898 |
. . . . . 6
โข ((๐: โโถ โ โง
((1 / (normโโ๐ด)) ยทโ ๐ด) โ โ โง
(normโโ((1 / (normโโ๐ด))
ยทโ ๐ด)) โค 1) โ
(normโโ(๐โ((1 /
(normโโ๐ด)) ยทโ ๐ด))) โค
(normopโ๐)) |
60 | 39, 59 | mp3an1 1449 |
. . . . 5
โข ((((1 /
(normโโ๐ด)) ยทโ ๐ด) โ โ โง
(normโโ((1 / (normโโ๐ด))
ยทโ ๐ด)) โค 1) โ
(normโโ(๐โ((1 /
(normโโ๐ด)) ยทโ ๐ด))) โค
(normopโ๐)) |
61 | 53, 58, 60 | syl2anc 585 |
. . . 4
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ (normโโ(๐โ((1 /
(normโโ๐ด)) ยทโ ๐ด))) โค
(normopโ๐)) |
62 | 51, 61 | eqbrtrd 5131 |
. . 3
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ ((normโโ(๐โ๐ด)) / (normโโ๐ด)) โค
(normopโ๐)) |
63 | 14 | a1i 11 |
. . . 4
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ (normopโ๐) โ โ) |
64 | | ledivmul2 12042 |
. . . 4
โข
(((normโโ(๐โ๐ด)) โ โ โง
(normopโ๐)
โ โ โง ((normโโ๐ด) โ โ โง 0 <
(normโโ๐ด))) โ
(((normโโ(๐โ๐ด)) / (normโโ๐ด)) โค
(normopโ๐)
โ (normโโ(๐โ๐ด)) โค ((normopโ๐) ยท
(normโโ๐ด)))) |
65 | 47, 63, 21, 26, 64 | syl112anc 1375 |
. . 3
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ (((normโโ(๐โ๐ด)) / (normโโ๐ด)) โค
(normopโ๐)
โ (normโโ(๐โ๐ด)) โค ((normopโ๐) ยท
(normโโ๐ด)))) |
66 | 62, 65 | mpbid 231 |
. 2
โข ((๐ด โ โ โง ๐ด โ 0โ)
โ (normโโ(๐โ๐ด)) โค ((normopโ๐) ยท
(normโโ๐ด))) |
67 | 19, 66 | pm2.61dane 3029 |
1
โข (๐ด โ โ โ
(normโโ(๐โ๐ด)) โค ((normopโ๐) ยท
(normโโ๐ด))) |