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 ⊢ A ∈ ℝ + ∩ sin -1 0 ↔ A ∈ ℝ + ∧ sin ⁡ A = 0

Proof

Step Hyp Ref Expression
1 elin ⊢ A ∈ ℝ + ∩ sin -1 0 ↔ A ∈ ℝ + ∧ A ∈ sin -1 0
2 sinf ⊢ sin : ℂ ⟶ ℂ
3 ffn ⊢ sin : ℂ ⟶ ℂ → sin Fn ℂ
4 fniniseg ⊢ sin Fn ℂ → A ∈ sin -1 0 ↔ A ∈ ℂ ∧ sin ⁡ A = 0
5 2 3 4 mp2b ⊢ A ∈ sin -1 0 ↔ A ∈ ℂ ∧ sin ⁡ A = 0
6 rpcn ⊢ A ∈ ℝ + → A ∈ ℂ
7 6 biantrurd ⊢ A ∈ ℝ + → sin ⁡ A = 0 ↔ A ∈ ℂ ∧ sin ⁡ A = 0
8 5 7 bitr4id ⊢ A ∈ ℝ + → A ∈ sin -1 0 ↔ sin ⁡ A = 0
9 8 pm5.32i ⊢ A ∈ ℝ + ∧ A ∈ sin -1 0 ↔ A ∈ ℝ + ∧ sin ⁡ A = 0
10 1 9 bitri ⊢ A ∈ ℝ + ∩ sin -1 0 ↔ A ∈ ℝ + ∧ sin ⁡ A = 0