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 e. ZZ | -. 2 || z }
Assertion oddprm2 
|- ( Prime \ { 2 } ) = ( O i^i Prime )

Proof

Step Hyp Ref Expression
1 hgt750leme.o 
 |-  O = { z e. ZZ | -. 2 || z }
2 ancom 
 |-  ( ( z e. O /\ z e. Prime ) <-> ( z e. Prime /\ z e. O ) )
3 prmz 
 |-  ( z e. Prime -> z e. ZZ )
4 1 reqabi 
 |-  ( z e. O <-> ( z e. ZZ /\ -. 2 || z ) )
5 4 baib 
 |-  ( z e. ZZ -> ( z e. O <-> -. 2 || z ) )
6 3 5 syl 
 |-  ( z e. Prime -> ( z e. O <-> -. 2 || z ) )
7 6 pm5.32i 
 |-  ( ( z e. Prime /\ z e. O ) <-> ( z e. Prime /\ -. 2 || z ) )
8 2 7 bitr2i 
 |-  ( ( z e. Prime /\ -. 2 || z ) <-> ( z e. O /\ z e. Prime ) )
9 nnoddn2prmb 
 |-  ( z e. ( Prime \ { 2 } ) <-> ( z e. Prime /\ -. 2 || z ) )
10 elin 
 |-  ( z e. ( O i^i Prime ) <-> ( z e. O /\ z e. Prime ) )
11 8 9 10 3bitr4i 
 |-  ( z e. ( Prime \ { 2 } ) <-> z e. ( O i^i Prime ) )
12 11 eqriv 
 |-  ( Prime \ { 2 } ) = ( O i^i Prime )