Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-odd Structured version   Visualization version   GIF version

Definition df-odd 40078
Description: Define the set of odd numbers. (Contributed by AV, 14-Jun-2020.)
Assertion
Ref Expression
df-odd Odd = {𝑧 ∈ ℤ ∣ ((𝑧 + 1) / 2) ∈ ℤ}

Detailed syntax breakdown of Definition df-odd
StepHypRef Expression
1 codd 40076 . 2 class Odd
2 vz . . . . . . 7 setvar 𝑧
32cv 1474 . . . . . 6 class 𝑧
4 c1 9816 . . . . . 6 class 1
5 caddc 9818 . . . . . 6 class +
63, 4, 5co 6549 . . . . 5 class (𝑧 + 1)
7 c2 10947 . . . . 5 class 2
8 cdiv 10563 . . . . 5 class /
96, 7, 8co 6549 . . . 4 class ((𝑧 + 1) / 2)
10 cz 11254 . . . 4 class
119, 10wcel 1977 . . 3 wff ((𝑧 + 1) / 2) ∈ ℤ
1211, 2, 10crab 2900 . 2 class {𝑧 ∈ ℤ ∣ ((𝑧 + 1) / 2) ∈ ℤ}
131, 12wceq 1475 1 wff Odd = {𝑧 ∈ ℤ ∣ ((𝑧 + 1) / 2) ∈ ℤ}
Colors of variables: wff setvar class
This definition is referenced by:  isodd  40080
  Copyright terms: Public domain W3C validator