Metamath Proof Explorer


Theorem pilem1

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

Ref Expression
Assertion pilem1 ( 𝐴 ∈ ( ℝ+ ∩ ( sin “ { 0 } ) ) ↔ ( 𝐴 ∈ ℝ+ ∧ ( sin ‘ 𝐴 ) = 0 ) )

Proof

Step Hyp Ref Expression
1 elin ( 𝐴 ∈ ( ℝ+ ∩ ( sin “ { 0 } ) ) ↔ ( 𝐴 ∈ ℝ+𝐴 ∈ ( sin “ { 0 } ) ) )
2 sinf sin : ℂ ⟶ ℂ
3 ffn ( sin : ℂ ⟶ ℂ → sin Fn ℂ )
4 fniniseg ( sin Fn ℂ → ( 𝐴 ∈ ( sin “ { 0 } ) ↔ ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) ) )
5 2 3 4 mp2b ( 𝐴 ∈ ( sin “ { 0 } ) ↔ ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) )
6 rpcn ( 𝐴 ∈ ℝ+𝐴 ∈ ℂ )
7 6 biantrurd ( 𝐴 ∈ ℝ+ → ( ( sin ‘ 𝐴 ) = 0 ↔ ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) ) )
8 5 7 bitr4id ( 𝐴 ∈ ℝ+ → ( 𝐴 ∈ ( sin “ { 0 } ) ↔ ( sin ‘ 𝐴 ) = 0 ) )
9 8 pm5.32i ( ( 𝐴 ∈ ℝ+𝐴 ∈ ( sin “ { 0 } ) ) ↔ ( 𝐴 ∈ ℝ+ ∧ ( sin ‘ 𝐴 ) = 0 ) )
10 1 9 bitri ( 𝐴 ∈ ( ℝ+ ∩ ( sin “ { 0 } ) ) ↔ ( 𝐴 ∈ ℝ+ ∧ ( sin ‘ 𝐴 ) = 0 ) )