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		rpcn	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℂ )
3	2	biantrurd	⊢ ( 𝐴 ∈ ℝ+ → ( ( sin ‘ 𝐴 ) = 0 ↔ ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) ) )
4		sinf	⊢ sin : ℂ ⟶ ℂ
5		ffn	⊢ ( sin : ℂ ⟶ ℂ → sin Fn ℂ )
6		fniniseg	⊢ ( sin Fn ℂ → ( 𝐴 ∈ ( ◡ sin “ { 0 } ) ↔ ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) ) )
7	4 5 6	mp2b	⊢ ( 𝐴 ∈ ( ◡ sin “ { 0 } ) ↔ ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) )
8	3 7	syl6rbbr	⊢ ( 𝐴 ∈ ℝ+ → ( 𝐴 ∈ ( ◡ sin “ { 0 } ) ↔ ( sin ‘ 𝐴 ) = 0 ) )
9	8	pm5.32i	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐴 ∈ ( ◡ sin “ { 0 } ) ) ↔ ( 𝐴 ∈ ℝ+ ∧ ( sin ‘ 𝐴 ) = 0 ) )
10	1 9	bitri	⊢ ( 𝐴 ∈ ( ℝ+ ∩ ( ◡ sin “ { 0 } ) ) ↔ ( 𝐴 ∈ ℝ+ ∧ ( sin ‘ 𝐴 ) = 0 ) )