Users' Mathboxes 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 39881
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 df-even 39879 . . 3 Even = {𝑧 ∈ ℤ ∣ (𝑧 / 2) ∈ ℤ}
21eleq2i 2676 . 2 (𝑍 ∈ Even ↔ 𝑍 ∈ {𝑧 ∈ ℤ ∣ (𝑧 / 2) ∈ ℤ})
3 oveq1 6531 . . . 4 (𝑧 = 𝑍 → (𝑧 / 2) = (𝑍 / 2))
43eleq1d 2668 . . 3 (𝑧 = 𝑍 → ((𝑧 / 2) ∈ ℤ ↔ (𝑍 / 2) ∈ ℤ))
54elrab 3327 . 2 (𝑍 ∈ {𝑧 ∈ ℤ ∣ (𝑧 / 2) ∈ ℤ} ↔ (𝑍 ∈ ℤ ∧ (𝑍 / 2) ∈ ℤ))
62, 5bitri 262 1 (𝑍 ∈ Even ↔ (𝑍 ∈ ℤ ∧ (𝑍 / 2) ∈ ℤ))
Colors of variables: wff setvar class
Syntax hints:  wb 194  wa 382   = wceq 1474  wcel 1976  {crab 2896  (class class class)co 6524   / cdiv 10530  2c2 10914  cz 11207   Even ceven 39877
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-rex 2898  df-rab 2901  df-v 3171  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-nul 3871  df-if 4033  df-sn 4122  df-pr 4124  df-op 4128  df-uni 4364  df-br 4575  df-iota 5751  df-fv 5795  df-ov 6527  df-even 39879
This theorem is referenced by:  evenz  39883  evendiv2z  39885  evenm1odd  39892  evenp1odd  39893  oddp1eveni  39894  oddm1eveni  39895  evennodd  39896  oddneven  39897  enege  39898  zeoALTV  39921  oddm1evenALTV  39926  oddp1evenALTV  39927  0evenALTV  39939  2evenALTV  39943  6even  39960  8even  39962
  Copyright terms: Public domain W3C validator