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	rabeq2i	|- ( 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 )