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