Description: Value of the limit predicate. C is the limit of the function F at B if the function G , formed by adding B to the domain of F and setting it to C , is continuous at B . (Contributed by Mario Carneiro, 25-Dec-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | limcval.j | |
|
limcval.k | |
||
ellimc.g | |
||
ellimc.f | |
||
ellimc.a | |
||
ellimc.b | |
||
Assertion | ellimc | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | limcval.j | |
|
2 | limcval.k | |
|
3 | ellimc.g | |
|
4 | ellimc.f | |
|
5 | ellimc.a | |
|
6 | ellimc.b | |
|
7 | 1 2 | limcfval | |
8 | 4 5 6 7 | syl3anc | |
9 | 8 | simpld | |
10 | 9 | eleq2d | |
11 | 1 2 3 | limcvallem | |
12 | 4 5 6 11 | syl3anc | |
13 | ifeq1 | |
|
14 | 13 | mpteq2dv | |
15 | 14 3 | eqtr4di | |
16 | 15 | eleq1d | |
17 | 16 | elab3g | |
18 | 12 17 | syl | |
19 | 10 18 | bitrd | |