Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  iseven Structured version   Visualization version   GIF version

Theorem iseven 42059
 Description: The predicate "is an even number". An even number is an integer which is divisible by 2, i.e. the result of dividing the even integer by 2 is still an integer. (Contributed by AV, 14-Jun-2020.)
Assertion
Ref Expression
iseven (𝑍 ∈ Even ↔ (𝑍 ∈ ℤ ∧ (𝑍 / 2) ∈ ℤ))

Proof of Theorem iseven
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 oveq1 6799 . . 3 (𝑧 = 𝑍 → (𝑧 / 2) = (𝑍 / 2))
21eleq1d 2834 . 2 (𝑧 = 𝑍 → ((𝑧 / 2) ∈ ℤ ↔ (𝑍 / 2) ∈ ℤ))
3 df-even 42057 . 2 Even = {𝑧 ∈ ℤ ∣ (𝑧 / 2) ∈ ℤ}
42, 3elrab2 3516 1 (𝑍 ∈ Even ↔ (𝑍 ∈ ℤ ∧ (𝑍 / 2) ∈ ℤ))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196   ∧ wa 382   = wceq 1630   ∈ wcel 2144  (class class class)co 6792   / cdiv 10885  2c2 11271  ℤcz 11578   Even ceven 42055 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-rex 3066  df-rab 3069  df-v 3351  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-nul 4062  df-if 4224  df-sn 4315  df-pr 4317  df-op 4321  df-uni 4573  df-br 4785  df-iota 5994  df-fv 6039  df-ov 6795  df-even 42057 This theorem is referenced by:  evenz  42061  evendiv2z  42063  evenm1odd  42070  evenp1odd  42071  oddp1eveni  42072  oddm1eveni  42073  evennodd  42074  oddneven  42075  enege  42076  zeoALTV  42099  oddm1evenALTV  42104  oddp1evenALTV  42105  0evenALTV  42117  2evenALTV  42121  6even  42138  8even  42140
 Copyright terms: Public domain W3C validator