Theorem pilem1

Description: Lemma for pire , pigt2lt4 and sinpi . (Contributed by Mario Carneiro, 9-May-2014)

	Ref	Expression
Assertion	pilem1	|- ( A e. ( RR+ i^i ( `' sin " { 0 } ) ) <-> ( A e. RR+ /\ ( sin ` A ) = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		elin	|- ( A e. ( RR+ i^i ( `' sin " { 0 } ) ) <-> ( A e. RR+ /\ A e. ( `' sin " { 0 } ) ) )
2		rpcn	|- ( A e. RR+ -> A e. CC )
3	2	biantrurd	|- ( A e. RR+ -> ( ( sin ` A ) = 0 <-> ( A e. CC /\ ( sin ` A ) = 0 ) ) )
4		sinf	|- sin : CC --> CC
5		ffn	|- ( sin : CC --> CC -> sin Fn CC )
6		fniniseg	|- ( sin Fn CC -> ( A e. ( `' sin " { 0 } ) <-> ( A e. CC /\ ( sin ` A ) = 0 ) ) )
7	4 5 6	mp2b	|- ( A e. ( `' sin " { 0 } ) <-> ( A e. CC /\ ( sin ` A ) = 0 ) )
8	3 7	syl6rbbr	|- ( A e. RR+ -> ( A e. ( `' sin " { 0 } ) <-> ( sin ` A ) = 0 ) )
9	8	pm5.32i	|- ( ( A e. RR+ /\ A e. ( `' sin " { 0 } ) ) <-> ( A e. RR+ /\ ( sin ` A ) = 0 ) )
10	1 9	bitri	|- ( A e. ( RR+ i^i ( `' sin " { 0 } ) ) <-> ( A e. RR+ /\ ( sin ` A ) = 0 ) )