Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Even and odd numbers
Alternate definitions using the "gcd" operation
dfodd7
Next ⟩
gcd2odd1
Metamath Proof Explorer
Ascii
Unicode
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