Metamath Proof Explorer


Theorem dfodd7

Description: Alternate definition for odd numbers. (Contributed by AV, 1-Jul-2020)

Ref Expression
Assertion dfodd7 Odd = z | 2 gcd z = 1

Proof

Step Hyp Ref Expression
1 isodd7 x Odd x 2 gcd x = 1
2 oveq2 z = x 2 gcd z = 2 gcd x
3 2 eqeq1d z = x 2 gcd z = 1 2 gcd x = 1
4 3 elrab x z | 2 gcd z = 1 x 2 gcd x = 1
5 1 4 bitr4i x Odd x z | 2 gcd z = 1
6 5 eqriv Odd = z | 2 gcd z = 1