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	$$⊢\left(\exp \circ \cos \right)\left(0\right)=\mathrm{e}$$

Proof

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