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 ( 𝐴 ∈ ( ℝ+ ∩ ( ◡ 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 ) )