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 ⊢ 𝑂 = { 𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧 }
Assertion oddprm2 ( ℙ ∖ { 2 } ) = ( 𝑂 ∩ ℙ )

Proof

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