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

Metamath Proof Explorer

Theorem isodd3

Description: The predicate "is an odd number". An odd number is an integer which is not divisible by 2. (Contributed by AV, 18-Jun-2020)

Ref Expression
Assertion isodd3 ⊢ Z ∈ Odd ↔ Z ∈ ℤ ∧ ¬ 2 ∥ Z

Proof

Step Hyp Ref Expression
1 breq2 ⊢ z = Z → 2 ∥ z ↔ 2 ∥ Z
2 1 notbid ⊢ z = Z → ¬ 2 ∥ z ↔ ¬ 2 ∥ Z
3 dfodd3 ⊢ Odd = z ∈ ℤ | ¬ 2 ∥ z
4 2 3 elrab2 ⊢ Z ∈ Odd ↔ Z ∈ ℤ ∧ ¬ 2 ∥ Z