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 o. cos ) ` 0 ) = _e

Proof

Step	Hyp	Ref	Expression
1		cos0	|- ( cos ` 0 ) = 1
2	1	fveq2i	|- ( exp ` ( cos ` 0 ) ) = ( exp ` 1 )
3		cosf	|- cos : CC --> CC
4		0cn	|- 0 e. CC
5		fvco3	|- ( ( cos : CC --> CC /\ 0 e. CC ) -> ( ( exp o. cos ) ` 0 ) = ( exp ` ( cos ` 0 ) ) )
6	3 4 5	mp2an	|- ( ( exp o. cos ) ` 0 ) = ( exp ` ( cos ` 0 ) )
7		df-e	|- _e = ( exp ` 1 )
8	2 6 7	3eqtr4i	|- ( ( exp o. cos ) ` 0 ) = _e