This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )