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