Metamath Proof Explorer

Theorem isodd7

Description: The predicate "is an odd number". An odd number and 2 have 1 as greatest common divisor. (Contributed by AV, 1-Jul-2020)

Ref Expression
Assertion isodd7 ⊢ Z ∈ Odd ↔ Z ∈ ℤ ∧ 2 gcd Z = 1

Proof

Step Hyp Ref Expression
1 isodd3 ⊢ Z ∈ Odd ↔ Z ∈ ℤ ∧ ¬ 2 ∥ Z
2 2prm ⊢ 2 ∈ ℙ
3 coprm ⊢ 2 ∈ ℙ ∧ Z ∈ ℤ → ¬ 2 ∥ Z ↔ 2 gcd Z = 1
4 2 3 mpan ⊢ Z ∈ ℤ → ¬ 2 ∥ Z ↔ 2 gcd Z = 1
5 4 pm5.32i ⊢ Z ∈ ℤ ∧ ¬ 2 ∥ Z ↔ Z ∈ ℤ ∧ 2 gcd Z = 1
6 1 5 bitri ⊢ Z ∈ Odd ↔ Z ∈ ℤ ∧ 2 gcd Z = 1