Step | Hyp | Ref
| Expression |
1 | | nmcfnex.2 |
. . . 4
β’ π β ContFn |
2 | | ax-hv0cl 29994 |
. . . 4
β’
0β β β |
3 | | 1rp 12927 |
. . . 4
β’ 1 β
β+ |
4 | | cnfnc 30921 |
. . . 4
β’ ((π β ContFn β§
0β β β β§ 1 β β+) β
βπ¦ β
β+ βπ§ β β
((normββ(π§ ββ
0β)) < π¦ β (absβ((πβπ§) β (πβ0β))) <
1)) |
5 | 1, 2, 3, 4 | mp3an 1462 |
. . 3
β’
βπ¦ β
β+ βπ§ β β
((normββ(π§ ββ
0β)) < π¦ β (absβ((πβπ§) β (πβ0β))) <
1) |
6 | | hvsub0 30067 |
. . . . . . . 8
β’ (π§ β β β (π§ ββ
0β) = π§) |
7 | 6 | fveq2d 6850 |
. . . . . . 7
β’ (π§ β β β
(normββ(π§ ββ
0β)) = (normββπ§)) |
8 | 7 | breq1d 5119 |
. . . . . 6
β’ (π§ β β β
((normββ(π§ ββ
0β)) < π¦ β (normββπ§) < π¦)) |
9 | | nmcfnex.1 |
. . . . . . . . . . 11
β’ π β LinFn |
10 | 9 | lnfn0i 31033 |
. . . . . . . . . 10
β’ (πβ0β) =
0 |
11 | 10 | oveq2i 7372 |
. . . . . . . . 9
β’ ((πβπ§) β (πβ0β)) = ((πβπ§) β 0) |
12 | 9 | lnfnfi 31032 |
. . . . . . . . . . 11
β’ π:
ββΆβ |
13 | 12 | ffvelcdmi 7038 |
. . . . . . . . . 10
β’ (π§ β β β (πβπ§) β β) |
14 | 13 | subid1d 11509 |
. . . . . . . . 9
β’ (π§ β β β ((πβπ§) β 0) = (πβπ§)) |
15 | 11, 14 | eqtrid 2785 |
. . . . . . . 8
β’ (π§ β β β ((πβπ§) β (πβ0β)) = (πβπ§)) |
16 | 15 | fveq2d 6850 |
. . . . . . 7
β’ (π§ β β β
(absβ((πβπ§) β (πβ0β))) =
(absβ(πβπ§))) |
17 | 16 | breq1d 5119 |
. . . . . 6
β’ (π§ β β β
((absβ((πβπ§) β (πβ0β))) < 1 β
(absβ(πβπ§)) < 1)) |
18 | 8, 17 | imbi12d 345 |
. . . . 5
β’ (π§ β β β
(((normββ(π§ ββ
0β)) < π¦ β (absβ((πβπ§) β (πβ0β))) < 1)
β ((normββπ§) < π¦ β (absβ(πβπ§)) < 1))) |
19 | 18 | ralbiia 3091 |
. . . 4
β’
(βπ§ β
β ((normββ(π§ ββ
0β)) < π¦ β (absβ((πβπ§) β (πβ0β))) < 1)
β βπ§ β
β ((normββπ§) < π¦ β (absβ(πβπ§)) < 1)) |
20 | 19 | rexbii 3094 |
. . 3
β’
(βπ¦ β
β+ βπ§ β β
((normββ(π§ ββ
0β)) < π¦ β (absβ((πβπ§) β (πβ0β))) < 1)
β βπ¦ β
β+ βπ§ β β
((normββπ§) < π¦ β (absβ(πβπ§)) < 1)) |
21 | 5, 20 | mpbi 229 |
. 2
β’
βπ¦ β
β+ βπ§ β β
((normββπ§) < π¦ β (absβ(πβπ§)) < 1) |
22 | | nmfnval 30867 |
. . 3
β’ (π: ββΆβ β
(normfnβπ)
= sup({π β£
βπ₯ β β
((normββπ₯) β€ 1 β§ π = (absβ(πβπ₯)))}, β*, <
)) |
23 | 12, 22 | ax-mp 5 |
. 2
β’
(normfnβπ) = sup({π β£ βπ₯ β β
((normββπ₯) β€ 1 β§ π = (absβ(πβπ₯)))}, β*, <
) |
24 | 12 | ffvelcdmi 7038 |
. . 3
β’ (π₯ β β β (πβπ₯) β β) |
25 | 24 | abscld 15330 |
. 2
β’ (π₯ β β β
(absβ(πβπ₯)) β
β) |
26 | 10 | fveq2i 6849 |
. . 3
β’
(absβ(πβ0β)) =
(absβ0) |
27 | | abs0 15179 |
. . 3
β’
(absβ0) = 0 |
28 | 26, 27 | eqtri 2761 |
. 2
β’
(absβ(πβ0β)) =
0 |
29 | | rpcn 12933 |
. . . . 5
β’ ((π¦ / 2) β β+
β (π¦ / 2) β
β) |
30 | 9 | lnfnmuli 31035 |
. . . . 5
β’ (((π¦ / 2) β β β§ π₯ β β) β (πβ((π¦ / 2) Β·β
π₯)) = ((π¦ / 2) Β· (πβπ₯))) |
31 | 29, 30 | sylan 581 |
. . . 4
β’ (((π¦ / 2) β β+
β§ π₯ β β)
β (πβ((π¦ / 2)
Β·β π₯)) = ((π¦ / 2) Β· (πβπ₯))) |
32 | 31 | fveq2d 6850 |
. . 3
β’ (((π¦ / 2) β β+
β§ π₯ β β)
β (absβ(πβ((π¦ / 2) Β·β
π₯))) = (absβ((π¦ / 2) Β· (πβπ₯)))) |
33 | | absmul 15188 |
. . . 4
β’ (((π¦ / 2) β β β§
(πβπ₯) β β) β (absβ((π¦ / 2) Β· (πβπ₯))) = ((absβ(π¦ / 2)) Β· (absβ(πβπ₯)))) |
34 | 29, 24, 33 | syl2an 597 |
. . 3
β’ (((π¦ / 2) β β+
β§ π₯ β β)
β (absβ((π¦ / 2)
Β· (πβπ₯))) = ((absβ(π¦ / 2)) Β·
(absβ(πβπ₯)))) |
35 | | rpre 12931 |
. . . . . 6
β’ ((π¦ / 2) β β+
β (π¦ / 2) β
β) |
36 | | rpge0 12936 |
. . . . . 6
β’ ((π¦ / 2) β β+
β 0 β€ (π¦ /
2)) |
37 | 35, 36 | absidd 15316 |
. . . . 5
β’ ((π¦ / 2) β β+
β (absβ(π¦ / 2))
= (π¦ / 2)) |
38 | 37 | adantr 482 |
. . . 4
β’ (((π¦ / 2) β β+
β§ π₯ β β)
β (absβ(π¦ / 2))
= (π¦ / 2)) |
39 | 38 | oveq1d 7376 |
. . 3
β’ (((π¦ / 2) β β+
β§ π₯ β β)
β ((absβ(π¦ / 2))
Β· (absβ(πβπ₯))) = ((π¦ / 2) Β· (absβ(πβπ₯)))) |
40 | 32, 34, 39 | 3eqtrrd 2778 |
. 2
β’ (((π¦ / 2) β β+
β§ π₯ β β)
β ((π¦ / 2) Β·
(absβ(πβπ₯))) = (absβ(πβ((π¦ / 2) Β·β
π₯)))) |
41 | 21, 23, 25, 28, 40 | nmcexi 31017 |
1
β’
(normfnβπ) β β |