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		sinf	|- sin : CC --> CC
3		ffn	|- ( sin : CC --> CC -> sin Fn CC )
4		fniniseg	|- ( sin Fn CC -> ( A e. ( `' sin " { 0 } ) <-> ( A e. CC /\ ( sin ` A ) = 0 ) ) )
5	2 3 4	mp2b	|- ( A e. ( `' sin " { 0 } ) <-> ( A e. CC /\ ( sin ` A ) = 0 ) )
6		rpcn	|- ( A e. RR+ -> A e. CC )
7	6	biantrurd	|- ( A e. RR+ -> ( ( sin ` A ) = 0 <-> ( A e. CC /\ ( sin ` A ) = 0 ) ) )
8	5 7	bitr4id	|- ( 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 ) )