Step | Hyp | Ref
| Expression |
1 | | 0cn 11155 |
. . 3
β’ 0 β
β |
2 | 1 | fconst6 6736 |
. 2
β’ ( β
Γ {0}): ββΆβ |
3 | | 1rp 12927 |
. . . 4
β’ 1 β
β+ |
4 | | c0ex 11157 |
. . . . . . . . . . . . 13
β’ 0 β
V |
5 | 4 | fvconst2 7157 |
. . . . . . . . . . . 12
β’ (π€ β β β ((
β Γ {0})βπ€) = 0) |
6 | 4 | fvconst2 7157 |
. . . . . . . . . . . 12
β’ (π₯ β β β ((
β Γ {0})βπ₯) = 0) |
7 | 5, 6 | oveqan12rd 7381 |
. . . . . . . . . . 11
β’ ((π₯ β β β§ π€ β β) β (((
β Γ {0})βπ€) β (( β Γ {0})βπ₯)) = (0 β
0)) |
8 | 7 | adantlr 714 |
. . . . . . . . . 10
β’ (((π₯ β β β§ π¦ β β+)
β§ π€ β β)
β ((( β Γ {0})βπ€) β (( β Γ {0})βπ₯)) = (0 β
0)) |
9 | | 0m0e0 12281 |
. . . . . . . . . 10
β’ (0
β 0) = 0 |
10 | 8, 9 | eqtrdi 2789 |
. . . . . . . . 9
β’ (((π₯ β β β§ π¦ β β+)
β§ π€ β β)
β ((( β Γ {0})βπ€) β (( β Γ {0})βπ₯)) = 0) |
11 | 10 | fveq2d 6850 |
. . . . . . . 8
β’ (((π₯ β β β§ π¦ β β+)
β§ π€ β β)
β (absβ((( β Γ {0})βπ€) β (( β Γ {0})βπ₯))) =
(absβ0)) |
12 | | abs0 15179 |
. . . . . . . 8
β’
(absβ0) = 0 |
13 | 11, 12 | eqtrdi 2789 |
. . . . . . 7
β’ (((π₯ β β β§ π¦ β β+)
β§ π€ β β)
β (absβ((( β Γ {0})βπ€) β (( β Γ {0})βπ₯))) = 0) |
14 | | rpgt0 12935 |
. . . . . . . 8
β’ (π¦ β β+
β 0 < π¦) |
15 | 14 | ad2antlr 726 |
. . . . . . 7
β’ (((π₯ β β β§ π¦ β β+)
β§ π€ β β)
β 0 < π¦) |
16 | 13, 15 | eqbrtrd 5131 |
. . . . . 6
β’ (((π₯ β β β§ π¦ β β+)
β§ π€ β β)
β (absβ((( β Γ {0})βπ€) β (( β Γ {0})βπ₯))) < π¦) |
17 | 16 | a1d 25 |
. . . . 5
β’ (((π₯ β β β§ π¦ β β+)
β§ π€ β β)
β ((normββ(π€ ββ π₯)) < 1 β (absβ(((
β Γ {0})βπ€) β (( β Γ {0})βπ₯))) < π¦)) |
18 | 17 | ralrimiva 3140 |
. . . 4
β’ ((π₯ β β β§ π¦ β β+)
β βπ€ β
β ((normββ(π€ ββ π₯)) < 1 β (absβ(((
β Γ {0})βπ€) β (( β Γ {0})βπ₯))) < π¦)) |
19 | | breq2 5113 |
. . . . 5
β’ (π§ = 1 β
((normββ(π€ ββ π₯)) < π§ β (normββ(π€ ββ
π₯)) <
1)) |
20 | 19 | rspceaimv 3587 |
. . . 4
β’ ((1
β β+ β§ βπ€ β β
((normββ(π€ ββ π₯)) < 1 β (absβ(((
β Γ {0})βπ€) β (( β Γ {0})βπ₯))) < π¦)) β βπ§ β β+ βπ€ β β
((normββ(π€ ββ π₯)) < π§ β (absβ((( β Γ
{0})βπ€) β ((
β Γ {0})βπ₯))) < π¦)) |
21 | 3, 18, 20 | sylancr 588 |
. . 3
β’ ((π₯ β β β§ π¦ β β+)
β βπ§ β
β+ βπ€ β β
((normββ(π€ ββ π₯)) < π§ β (absβ((( β Γ
{0})βπ€) β ((
β Γ {0})βπ₯))) < π¦)) |
22 | 21 | rgen2 3191 |
. 2
β’
βπ₯ β
β βπ¦ β
β+ βπ§ β β+ βπ€ β β
((normββ(π€ ββ π₯)) < π§ β (absβ((( β Γ
{0})βπ€) β ((
β Γ {0})βπ₯))) < π¦) |
23 | | elcnfn 30873 |
. 2
β’ ((
β Γ {0}) β ContFn β (( β Γ {0}):
ββΆβ β§ βπ₯ β β βπ¦ β β+ βπ§ β β+
βπ€ β β
((normββ(π€ ββ π₯)) < π§ β (absβ((( β Γ
{0})βπ€) β ((
β Γ {0})βπ₯))) < π¦))) |
24 | 2, 22, 23 | mpbir2an 710 |
1
β’ ( β
Γ {0}) β ContFn |