Theorem itgsin0pi

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

	Ref	Expression
Assertion	itgsin0pi	⊢ ∫ ( 0 (,) π ) ( sin ‘ 𝑥 ) d 𝑥 = 2

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝑡 ∈ ( 0 [,] π ) ↦ - ( cos ‘ 𝑡 ) ) = ( 𝑡 ∈ ( 0 [,] π ) ↦ - ( cos ‘ 𝑡 ) )
2	1	itgsin0pilem1	⊢ ∫ ( 0 (,) π ) ( sin ‘ 𝑥 ) d 𝑥 = 2