Step | Hyp | Ref
| Expression |
1 | | fveq2 6846 |
. . . . . 6
β’ (π΄ = 0β β
(πβπ΄) = (πβ0β)) |
2 | | nmcfnex.1 |
. . . . . . 7
β’ π β LinFn |
3 | 2 | lnfn0i 31033 |
. . . . . 6
β’ (πβ0β) =
0 |
4 | 1, 3 | eqtrdi 2789 |
. . . . 5
β’ (π΄ = 0β β
(πβπ΄) = 0) |
5 | 4 | abs00bd 15185 |
. . . 4
β’ (π΄ = 0β β
(absβ(πβπ΄)) = 0) |
6 | | 0le0 12262 |
. . . . 5
β’ 0 β€
0 |
7 | | fveq2 6846 |
. . . . . . . 8
β’ (π΄ = 0β β
(normββπ΄) =
(normββ0β)) |
8 | | norm0 30119 |
. . . . . . . 8
β’
(normββ0β) =
0 |
9 | 7, 8 | eqtrdi 2789 |
. . . . . . 7
β’ (π΄ = 0β β
(normββπ΄) = 0) |
10 | 9 | oveq2d 7377 |
. . . . . 6
β’ (π΄ = 0β β
((normfnβπ) Β·
(normββπ΄)) = ((normfnβπ) Β· 0)) |
11 | | nmcfnex.2 |
. . . . . . . . 9
β’ π β ContFn |
12 | 2, 11 | nmcfnexi 31042 |
. . . . . . . 8
β’
(normfnβπ) β β |
13 | 12 | recni 11177 |
. . . . . . 7
β’
(normfnβπ) β β |
14 | 13 | mul01i 11353 |
. . . . . 6
β’
((normfnβπ) Β· 0) = 0 |
15 | 10, 14 | eqtr2di 2790 |
. . . . 5
β’ (π΄ = 0β β 0
= ((normfnβπ) Β·
(normββπ΄))) |
16 | 6, 15 | breqtrid 5146 |
. . . 4
β’ (π΄ = 0β β 0
β€ ((normfnβπ) Β·
(normββπ΄))) |
17 | 5, 16 | eqbrtrd 5131 |
. . 3
β’ (π΄ = 0β β
(absβ(πβπ΄)) β€
((normfnβπ) Β·
(normββπ΄))) |
18 | 17 | adantl 483 |
. 2
β’ ((π΄ β β β§ π΄ = 0β) β
(absβ(πβπ΄)) β€
((normfnβπ) Β·
(normββπ΄))) |
19 | 2 | lnfnfi 31032 |
. . . . . . . . . 10
β’ π:
ββΆβ |
20 | 19 | ffvelcdmi 7038 |
. . . . . . . . 9
β’ (π΄ β β β (πβπ΄) β β) |
21 | 20 | abscld 15330 |
. . . . . . . 8
β’ (π΄ β β β
(absβ(πβπ΄)) β
β) |
22 | 21 | adantr 482 |
. . . . . . 7
β’ ((π΄ β β β§ Β¬
π΄ = 0β)
β (absβ(πβπ΄)) β β) |
23 | 22 | recnd 11191 |
. . . . . 6
β’ ((π΄ β β β§ Β¬
π΄ = 0β)
β (absβ(πβπ΄)) β β) |
24 | | normcl 30116 |
. . . . . . . 8
β’ (π΄ β β β
(normββπ΄) β β) |
25 | 24 | adantr 482 |
. . . . . . 7
β’ ((π΄ β β β§ Β¬
π΄ = 0β)
β (normββπ΄) β β) |
26 | 25 | recnd 11191 |
. . . . . 6
β’ ((π΄ β β β§ Β¬
π΄ = 0β)
β (normββπ΄) β β) |
27 | | norm-i 30120 |
. . . . . . . . 9
β’ (π΄ β β β
((normββπ΄) = 0 β π΄ = 0β)) |
28 | 27 | notbid 318 |
. . . . . . . 8
β’ (π΄ β β β (Β¬
(normββπ΄) = 0 β Β¬ π΄ = 0β)) |
29 | 28 | biimpar 479 |
. . . . . . 7
β’ ((π΄ β β β§ Β¬
π΄ = 0β)
β Β¬ (normββπ΄) = 0) |
30 | 29 | neqned 2947 |
. . . . . 6
β’ ((π΄ β β β§ Β¬
π΄ = 0β)
β (normββπ΄) β 0) |
31 | 23, 26, 30 | divrec2d 11943 |
. . . . 5
β’ ((π΄ β β β§ Β¬
π΄ = 0β)
β ((absβ(πβπ΄)) / (normββπ΄)) = ((1 /
(normββπ΄)) Β· (absβ(πβπ΄)))) |
32 | 25, 30 | rereccld 11990 |
. . . . . . . . 9
β’ ((π΄ β β β§ Β¬
π΄ = 0β)
β (1 / (normββπ΄)) β β) |
33 | 32 | recnd 11191 |
. . . . . . . 8
β’ ((π΄ β β β§ Β¬
π΄ = 0β)
β (1 / (normββπ΄)) β β) |
34 | | simpl 484 |
. . . . . . . 8
β’ ((π΄ β β β§ Β¬
π΄ = 0β)
β π΄ β
β) |
35 | 2 | lnfnmuli 31035 |
. . . . . . . 8
β’ (((1 /
(normββπ΄)) β β β§ π΄ β β) β (πβ((1 /
(normββπ΄)) Β·β π΄)) = ((1 /
(normββπ΄)) Β· (πβπ΄))) |
36 | 33, 34, 35 | syl2anc 585 |
. . . . . . 7
β’ ((π΄ β β β§ Β¬
π΄ = 0β)
β (πβ((1 /
(normββπ΄)) Β·β π΄)) = ((1 /
(normββπ΄)) Β· (πβπ΄))) |
37 | 36 | fveq2d 6850 |
. . . . . 6
β’ ((π΄ β β β§ Β¬
π΄ = 0β)
β (absβ(πβ((1 /
(normββπ΄)) Β·β π΄))) = (absβ((1 /
(normββπ΄)) Β· (πβπ΄)))) |
38 | 20 | adantr 482 |
. . . . . . 7
β’ ((π΄ β β β§ Β¬
π΄ = 0β)
β (πβπ΄) β
β) |
39 | 33, 38 | absmuld 15348 |
. . . . . 6
β’ ((π΄ β β β§ Β¬
π΄ = 0β)
β (absβ((1 / (normββπ΄)) Β· (πβπ΄))) = ((absβ(1 /
(normββπ΄))) Β· (absβ(πβπ΄)))) |
40 | | df-ne 2941 |
. . . . . . . . . . . 12
β’ (π΄ β 0β
β Β¬ π΄ =
0β) |
41 | | normgt0 30118 |
. . . . . . . . . . . 12
β’ (π΄ β β β (π΄ β 0β
β 0 < (normββπ΄))) |
42 | 40, 41 | bitr3id 285 |
. . . . . . . . . . 11
β’ (π΄ β β β (Β¬
π΄ = 0β
β 0 < (normββπ΄))) |
43 | 42 | biimpa 478 |
. . . . . . . . . 10
β’ ((π΄ β β β§ Β¬
π΄ = 0β)
β 0 < (normββπ΄)) |
44 | 25, 43 | recgt0d 12097 |
. . . . . . . . 9
β’ ((π΄ β β β§ Β¬
π΄ = 0β)
β 0 < (1 / (normββπ΄))) |
45 | | 0re 11165 |
. . . . . . . . . 10
β’ 0 β
β |
46 | | ltle 11251 |
. . . . . . . . . 10
β’ ((0
β β β§ (1 / (normββπ΄)) β β) β (0 < (1 /
(normββπ΄)) β 0 β€ (1 /
(normββπ΄)))) |
47 | 45, 46 | mpan 689 |
. . . . . . . . 9
β’ ((1 /
(normββπ΄)) β β β (0 < (1 /
(normββπ΄)) β 0 β€ (1 /
(normββπ΄)))) |
48 | 32, 44, 47 | sylc 65 |
. . . . . . . 8
β’ ((π΄ β β β§ Β¬
π΄ = 0β)
β 0 β€ (1 / (normββπ΄))) |
49 | 32, 48 | absidd 15316 |
. . . . . . 7
β’ ((π΄ β β β§ Β¬
π΄ = 0β)
β (absβ(1 / (normββπ΄))) = (1 /
(normββπ΄))) |
50 | 49 | oveq1d 7376 |
. . . . . 6
β’ ((π΄ β β β§ Β¬
π΄ = 0β)
β ((absβ(1 / (normββπ΄))) Β· (absβ(πβπ΄))) = ((1 /
(normββπ΄)) Β· (absβ(πβπ΄)))) |
51 | 37, 39, 50 | 3eqtrrd 2778 |
. . . . 5
β’ ((π΄ β β β§ Β¬
π΄ = 0β)
β ((1 / (normββπ΄)) Β· (absβ(πβπ΄))) = (absβ(πβ((1 /
(normββπ΄)) Β·β π΄)))) |
52 | 31, 51 | eqtrd 2773 |
. . . 4
β’ ((π΄ β β β§ Β¬
π΄ = 0β)
β ((absβ(πβπ΄)) / (normββπ΄)) = (absβ(πβ((1 /
(normββπ΄)) Β·β π΄)))) |
53 | | hvmulcl 30004 |
. . . . . 6
β’ (((1 /
(normββπ΄)) β β β§ π΄ β β) β ((1 /
(normββπ΄)) Β·β π΄) β
β) |
54 | 33, 34, 53 | syl2anc 585 |
. . . . 5
β’ ((π΄ β β β§ Β¬
π΄ = 0β)
β ((1 / (normββπ΄)) Β·β π΄) β
β) |
55 | | normcl 30116 |
. . . . . . 7
β’ (((1 /
(normββπ΄)) Β·β π΄) β β β
(normββ((1 / (normββπ΄))
Β·β π΄)) β β) |
56 | 54, 55 | syl 17 |
. . . . . 6
β’ ((π΄ β β β§ Β¬
π΄ = 0β)
β (normββ((1 /
(normββπ΄)) Β·β π΄)) β
β) |
57 | | norm1 30240 |
. . . . . . 7
β’ ((π΄ β β β§ π΄ β 0β)
β (normββ((1 /
(normββπ΄)) Β·β π΄)) = 1) |
58 | 40, 57 | sylan2br 596 |
. . . . . 6
β’ ((π΄ β β β§ Β¬
π΄ = 0β)
β (normββ((1 /
(normββπ΄)) Β·β π΄)) = 1) |
59 | | eqle 11265 |
. . . . . 6
β’
(((normββ((1 /
(normββπ΄)) Β·β π΄)) β β β§
(normββ((1 / (normββπ΄))
Β·β π΄)) = 1) β
(normββ((1 / (normββπ΄))
Β·β π΄)) β€ 1) |
60 | 56, 58, 59 | syl2anc 585 |
. . . . 5
β’ ((π΄ β β β§ Β¬
π΄ = 0β)
β (normββ((1 /
(normββπ΄)) Β·β π΄)) β€ 1) |
61 | | nmfnlb 30915 |
. . . . . 6
β’ ((π: ββΆβ β§
((1 / (normββπ΄)) Β·β π΄) β β β§
(normββ((1 / (normββπ΄))
Β·β π΄)) β€ 1) β (absβ(πβ((1 /
(normββπ΄)) Β·β π΄))) β€
(normfnβπ)) |
62 | 19, 61 | mp3an1 1449 |
. . . . 5
β’ ((((1 /
(normββπ΄)) Β·β π΄) β β β§
(normββ((1 / (normββπ΄))
Β·β π΄)) β€ 1) β (absβ(πβ((1 /
(normββπ΄)) Β·β π΄))) β€
(normfnβπ)) |
63 | 54, 60, 62 | syl2anc 585 |
. . . 4
β’ ((π΄ β β β§ Β¬
π΄ = 0β)
β (absβ(πβ((1 /
(normββπ΄)) Β·β π΄))) β€
(normfnβπ)) |
64 | 52, 63 | eqbrtrd 5131 |
. . 3
β’ ((π΄ β β β§ Β¬
π΄ = 0β)
β ((absβ(πβπ΄)) / (normββπ΄)) β€
(normfnβπ)) |
65 | 12 | a1i 11 |
. . . 4
β’ ((π΄ β β β§ Β¬
π΄ = 0β)
β (normfnβπ) β β) |
66 | | ledivmul2 12042 |
. . . 4
β’
(((absβ(πβπ΄)) β β β§
(normfnβπ)
β β β§ ((normββπ΄) β β β§ 0 <
(normββπ΄))) β (((absβ(πβπ΄)) / (normββπ΄)) β€
(normfnβπ)
β (absβ(πβπ΄)) β€ ((normfnβπ) Β·
(normββπ΄)))) |
67 | 22, 65, 25, 43, 66 | syl112anc 1375 |
. . 3
β’ ((π΄ β β β§ Β¬
π΄ = 0β)
β (((absβ(πβπ΄)) / (normββπ΄)) β€
(normfnβπ)
β (absβ(πβπ΄)) β€ ((normfnβπ) Β·
(normββπ΄)))) |
68 | 64, 67 | mpbid 231 |
. 2
β’ ((π΄ β β β§ Β¬
π΄ = 0β)
β (absβ(πβπ΄)) β€ ((normfnβπ) Β·
(normββπ΄))) |
69 | 18, 68 | pm2.61dan 812 |
1
β’ (π΄ β β β
(absβ(πβπ΄)) β€
((normfnβπ) Β·
(normββπ΄))) |