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

Metamath Proof Explorer

Theorem ex-co

Description: Example for df-co . Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015)

		Ref	Expression
	Assertion	ex-co	$⊢ (\exp \circ \cos) (0) = e$

Step	Hyp	Ref	Expression
1		cos0	$⊢ \cos 0 = 1$
2	1	fveq2i	$⊢ e^{\cos 0} = e^{1}$
3		cosf	$⊢ \cos : ℂ ⟶ ℂ$
4		0cn	$⊢ 0 \in ℂ$
5		fvco3	$⊢ (\cos : ℂ ⟶ ℂ \land 0 \in ℂ) \to (\exp \circ \cos) (0) = e^{\cos 0}$
6	3 4 5	mp2an	$⊢ (\exp \circ \cos) (0) = e^{\cos 0}$
7		df-e	$⊢ e = e^{1}$
8	2 6 7	3eqtr4i	$⊢ (\exp \circ \cos) (0) = e$