This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oddprm2

Description: Two ways to write the set of odd primes. (Contributed by Thierry Arnoux, 27-Dec-2021)

Ref Expression
Hypothesis hgt750leme.o ⊢ O = z ∈ ℤ | ¬ 2 ∥ z
Assertion oddprm2 ⊢ ℙ ∖ 2 = O ∩ ℙ

Proof

Step Hyp Ref Expression
1 hgt750leme.o ⊢ O = z ∈ ℤ | ¬ 2 ∥ z
2 ancom ⊢ z ∈ O ∧ z ∈ ℙ ↔ z ∈ ℙ ∧ z ∈ O
3 prmz ⊢ z ∈ ℙ → z ∈ ℤ
4 1 reqabi ⊢ z ∈ O ↔ z ∈ ℤ ∧ ¬ 2 ∥ z
5 4 baib ⊢ z ∈ ℤ → z ∈ O ↔ ¬ 2 ∥ z
6 3 5 syl ⊢ z ∈ ℙ → z ∈ O ↔ ¬ 2 ∥ z
7 6 pm5.32i ⊢ z ∈ ℙ ∧ z ∈ O ↔ z ∈ ℙ ∧ ¬ 2 ∥ z
8 2 7 bitr2i ⊢ z ∈ ℙ ∧ ¬ 2 ∥ z ↔ z ∈ O ∧ z ∈ ℙ
9 nnoddn2prmb ⊢ z ∈ ℙ ∖ 2 ↔ z ∈ ℙ ∧ ¬ 2 ∥ z
10 elin ⊢ z ∈ O ∩ ℙ ↔ z ∈ O ∧ z ∈ ℙ
11 8 9 10 3bitr4i ⊢ z ∈ ℙ ∖ 2 ↔ z ∈ O ∩ ℙ
12 11 eqriv ⊢ ℙ ∖ 2 = O ∩ ℙ