Metamath Proof Explorer

Theorem itgsin0pi

Description: Calculation of the integral for sine on the (0,π) interval. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Assertion itgsin0pi 
|- S. ( 0 (,) _pi ) ( sin ` x ) _d x = 2

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( t e. ( 0 [,] _pi ) |-> -u ( cos ` t ) ) = ( t e. ( 0 [,] _pi ) |-> -u ( cos ` t ) )
2 1 itgsin0pilem1 
 |-  S. ( 0 (,) _pi ) ( sin ` x ) _d x = 2