Metamath Proof Explorer


Theorem resincncf

Description: sin restricted to reals is continuous from reals to reals. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion resincncf sin : cn

Proof

Step Hyp Ref Expression
1 sinf sin :
2 ffn sin : sin Fn
3 1 2 ax-mp sin Fn
4 ax-resscn
5 fnssres sin Fn sin Fn
6 3 4 5 mp2an sin Fn
7 fvres x sin x = sin x
8 resincl x sin x
9 7 8 eqeltrd x sin x
10 9 rgen x sin x
11 ffnfv sin : sin Fn x sin x
12 6 10 11 mpbir2an sin :
13 sincn sin : cn
14 rescncf sin : cn sin : cn
15 4 13 14 mp2 sin : cn
16 cncffvrn sin : cn sin : cn sin :
17 4 15 16 mp2an sin : cn sin :
18 12 17 mpbir sin : cn