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 ∘ cos ) ‘ 0 ) = e

Proof

Step	Hyp	Ref	Expression
1		cos0	⊢ ( cos ‘ 0 ) = 1
2	1	fveq2i	⊢ ( exp ‘ ( cos ‘ 0 ) ) = ( exp ‘ 1 )
3		cosf	⊢ cos : ℂ ⟶ ℂ
4		0cn	⊢ 0 ∈ ℂ
5		fvco3	⊢ ( ( cos : ℂ ⟶ ℂ ∧ 0 ∈ ℂ ) → ( ( exp ∘ cos ) ‘ 0 ) = ( exp ‘ ( cos ‘ 0 ) ) )
6	3 4 5	mp2an	⊢ ( ( exp ∘ cos ) ‘ 0 ) = ( exp ‘ ( cos ‘ 0 ) )
7		df-e	⊢ e = ( exp ‘ 1 )
8	2 6 7	3eqtr4i	⊢ ( ( exp ∘ cos ) ‘ 0 ) = e