Step | Hyp | Ref
| Expression |
1 | | elcnfn 31135 |
. . . 4
β’ (π β ContFn β (π: ββΆβ β§
βπ§ β β
βπ€ β
β+ βπ₯ β β+ βπ¦ β β
((normββ(π¦ ββ π§)) < π₯ β (absβ((πβπ¦) β (πβπ§))) < π€))) |
2 | 1 | simprbi 498 |
. . 3
β’ (π β ContFn β
βπ§ β β
βπ€ β
β+ βπ₯ β β+ βπ¦ β β
((normββ(π¦ ββ π§)) < π₯ β (absβ((πβπ¦) β (πβπ§))) < π€)) |
3 | | oveq2 7417 |
. . . . . . . 8
β’ (π§ = π΄ β (π¦ ββ π§) = (π¦ ββ π΄)) |
4 | 3 | fveq2d 6896 |
. . . . . . 7
β’ (π§ = π΄ β
(normββ(π¦ ββ π§)) =
(normββ(π¦ ββ π΄))) |
5 | 4 | breq1d 5159 |
. . . . . 6
β’ (π§ = π΄ β
((normββ(π¦ ββ π§)) < π₯ β (normββ(π¦ ββ
π΄)) < π₯)) |
6 | | fveq2 6892 |
. . . . . . . . 9
β’ (π§ = π΄ β (πβπ§) = (πβπ΄)) |
7 | 6 | oveq2d 7425 |
. . . . . . . 8
β’ (π§ = π΄ β ((πβπ¦) β (πβπ§)) = ((πβπ¦) β (πβπ΄))) |
8 | 7 | fveq2d 6896 |
. . . . . . 7
β’ (π§ = π΄ β (absβ((πβπ¦) β (πβπ§))) = (absβ((πβπ¦) β (πβπ΄)))) |
9 | 8 | breq1d 5159 |
. . . . . 6
β’ (π§ = π΄ β ((absβ((πβπ¦) β (πβπ§))) < π€ β (absβ((πβπ¦) β (πβπ΄))) < π€)) |
10 | 5, 9 | imbi12d 345 |
. . . . 5
β’ (π§ = π΄ β
(((normββ(π¦ ββ π§)) < π₯ β (absβ((πβπ¦) β (πβπ§))) < π€) β
((normββ(π¦ ββ π΄)) < π₯ β (absβ((πβπ¦) β (πβπ΄))) < π€))) |
11 | 10 | rexralbidv 3221 |
. . . 4
β’ (π§ = π΄ β (βπ₯ β β+ βπ¦ β β
((normββ(π¦ ββ π§)) < π₯ β (absβ((πβπ¦) β (πβπ§))) < π€) β βπ₯ β β+ βπ¦ β β
((normββ(π¦ ββ π΄)) < π₯ β (absβ((πβπ¦) β (πβπ΄))) < π€))) |
12 | | breq2 5153 |
. . . . . 6
β’ (π€ = π΅ β ((absβ((πβπ¦) β (πβπ΄))) < π€ β (absβ((πβπ¦) β (πβπ΄))) < π΅)) |
13 | 12 | imbi2d 341 |
. . . . 5
β’ (π€ = π΅ β
(((normββ(π¦ ββ π΄)) < π₯ β (absβ((πβπ¦) β (πβπ΄))) < π€) β
((normββ(π¦ ββ π΄)) < π₯ β (absβ((πβπ¦) β (πβπ΄))) < π΅))) |
14 | 13 | rexralbidv 3221 |
. . . 4
β’ (π€ = π΅ β (βπ₯ β β+ βπ¦ β β
((normββ(π¦ ββ π΄)) < π₯ β (absβ((πβπ¦) β (πβπ΄))) < π€) β βπ₯ β β+ βπ¦ β β
((normββ(π¦ ββ π΄)) < π₯ β (absβ((πβπ¦) β (πβπ΄))) < π΅))) |
15 | 11, 14 | rspc2v 3623 |
. . 3
β’ ((π΄ β β β§ π΅ β β+)
β (βπ§ β
β βπ€ β
β+ βπ₯ β β+ βπ¦ β β
((normββ(π¦ ββ π§)) < π₯ β (absβ((πβπ¦) β (πβπ§))) < π€) β βπ₯ β β+ βπ¦ β β
((normββ(π¦ ββ π΄)) < π₯ β (absβ((πβπ¦) β (πβπ΄))) < π΅))) |
16 | 2, 15 | syl5com 31 |
. 2
β’ (π β ContFn β ((π΄ β β β§ π΅ β β+)
β βπ₯ β
β+ βπ¦ β β
((normββ(π¦ ββ π΄)) < π₯ β (absβ((πβπ¦) β (πβπ΄))) < π΅))) |
17 | 16 | 3impib 1117 |
1
β’ ((π β ContFn β§ π΄ β β β§ π΅ β β+)
β βπ₯ β
β+ βπ¦ β β
((normββ(π¦ ββ π΄)) < π₯ β (absβ((πβπ¦) β (πβπ΄))) < π΅)) |