This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	$⊢ \int_{(0, π)} \sin x d x = 2$

Step	Hyp	Ref	Expression
1		eqid	$⊢ (t \in [0, π] ⟼ - \cos t) = (t \in [0, π] ⟼ - \cos t)$
2	1	itgsin0pilem1	$⊢ \int_{(0, π)} \sin x d x = 2$