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 41306
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 6642 . . 3 (𝑧 = 𝑍 → (𝑧 / 2) = (𝑍 / 2))
21eleq1d 2684 . 2 (𝑧 = 𝑍 → ((𝑧 / 2) ∈ ℤ ↔ (𝑍 / 2) ∈ ℤ))
3 df-even 41304 . 2 Even = {𝑧 ∈ ℤ ∣ (𝑧 / 2) ∈ ℤ}
42, 3elrab2 3360 1 (𝑍 ∈ Even ↔ (𝑍 ∈ ℤ ∧ (𝑍 / 2) ∈ ℤ))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384   = wceq 1481  wcel 1988  (class class class)co 6635   / cdiv 10669  2c2 11055  cz 11362   Even ceven 41302
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-rex 2915  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-iota 5839  df-fv 5884  df-ov 6638  df-even 41304
This theorem is referenced by:  evenz  41308  evendiv2z  41310  evenm1odd  41317  evenp1odd  41318  oddp1eveni  41319  oddm1eveni  41320  evennodd  41321  oddneven  41322  enege  41323  zeoALTV  41346  oddm1evenALTV  41351  oddp1evenALTV  41352  0evenALTV  41364  2evenALTV  41368  6even  41385  8even  41387
  Copyright terms: Public domain W3C validator