Description: A differentiable function is continuous. (Contributed by Mario Carneiro, 7-Sep-2014) (Revised by Mario Carneiro, 7-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | dvcn | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl2 | |
|
2 | eqid | |
|
3 | eqid | |
|
4 | 2 3 | dvcnp2 | |
5 | 4 | ralrimiva | |
6 | raleq | |
|
7 | 6 | biimpd | |
8 | 5 7 | mpan9 | |
9 | 3 | cnfldtopon | |
10 | simpl3 | |
|
11 | simpl1 | |
|
12 | 10 11 | sstrd | |
13 | resttopon | |
|
14 | 9 12 13 | sylancr | |
15 | cncnp | |
|
16 | 14 9 15 | sylancl | |
17 | 1 8 16 | mpbir2and | |
18 | ssid | |
|
19 | 9 | toponrestid | |
20 | 3 2 19 | cncfcn | |
21 | 12 18 20 | sylancl | |
22 | 17 21 | eleqtrrd | |