Metamath Proof Explorer


Theorem recsccl

Description: The closure of the cosecant function with a real argument. (Contributed by David A. Wheeler, 15-Mar-2014)

Ref Expression
Assertion recsccl A sin A 0 csc A

Proof

Step Hyp Ref Expression
1 recn A A
2 cscval A sin A 0 csc A = 1 sin A
3 1 2 sylan A sin A 0 csc A = 1 sin A
4 resincl A sin A
5 1red A 1
6 redivcl 1 sin A sin A 0 1 sin A
7 5 6 syl3an1 A sin A sin A 0 1 sin A
8 4 7 syl3an2 A A sin A 0 1 sin A
9 8 3anidm12 A sin A 0 1 sin A
10 3 9 eqeltrd A sin A 0 csc A