This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isoddgcd1

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

Ref Expression
Assertion isoddgcd1 ⊢ Z ∈ ℤ → ¬ 2 ∥ Z ↔ 2 gcd Z = 1

Proof

Step Hyp Ref Expression
1 2prm ⊢ 2 ∈ ℙ
2 coprm ⊢ 2 ∈ ℙ ∧ Z ∈ ℤ → ¬ 2 ∥ Z ↔ 2 gcd Z = 1
3 1 2 mpan ⊢ Z ∈ ℤ → ¬ 2 ∥ Z ↔ 2 gcd Z = 1