Theorem isodd 42373

Description: The predicate "is an odd number". An odd number is an integer which is not divisible by 2, i.e. the result of dividing the odd integer increased by 1 and then divided by 2 is still an integer. (Contributed by AV, 14-Jun-2020.)

Assertion

Ref	Expression
isodd	⊢ (𝑍 ∈ Odd ↔ (𝑍 ∈ ℤ ∧ ((𝑍 + 1) / 2) ∈ ℤ))

Proof of Theorem isodd

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq1 6913	. . . 4 ⊢ (𝑧 = 𝑍 → (𝑧 + 1) = (𝑍 + 1))
2	1	oveq1d 6921	. . 3 ⊢ (𝑧 = 𝑍 → ((𝑧 + 1) / 2) = ((𝑍 + 1) / 2))
3	2	eleq1d 2892	. 2 ⊢ (𝑧 = 𝑍 → (((𝑧 + 1) / 2) ∈ ℤ ↔ ((𝑍 + 1) / 2) ∈ ℤ))
4		df-odd 42371	. 2 ⊢ Odd = {𝑧 ∈ ℤ ∣ ((𝑧 + 1) / 2) ∈ ℤ}
5	3, 4	elrab2 3590	1 ⊢ (𝑍 ∈ Odd ↔ (𝑍 ∈ ℤ ∧ ((𝑍 + 1) / 2) ∈ ℤ))

Syntax hints:   ↔ wb 198   ∧ wa 386   = wceq 1658   ∈ wcel 2166  (class class class)co 6906  1c1 10254   + caddc 10256   / cdiv 11010  2c2 11407  ℤcz 11705   Odd codd 42369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2804

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-rex 3124  df-rab 3127  df-v 3417  df-dif 3802  df-un 3804  df-in 3806  df-ss 3813  df-nul 4146  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4660  df-br 4875  df-iota 6087  df-fv 6132  df-ov 6909  df-odd 42371

This theorem is referenced by:  oddz  42375  oddp1div2z  42377  isodd2  42379  evenm1odd  42383  evennodd  42387  oddneven  42388  onego  42390  zeoALTV  42412  oddp1evenALTV  42418  1oddALTV  42432